9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # The Uniform Proof--theoretic Foundation of Linear Logic Programming (Extended Abstract)

TheLogic Programming (Extended Abstract) Linear Uniform Proof{theoretic Foundation of

James Harland

Department of Computer Science University of Melbourne Parkville, 3052 Australia jah@cs.mu.oz.au

David Pym

Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ Scotland, U.K. dpym@lfcs.ed.ac.uk

Abstract

We present a proof-theoretic analysis of a natural notion of logic programming for Girard's linear logic. This analysis enables us to identify a suitable notion of uniform proof. This in turn enables us to identify choices of classes of de nite and goal formulae for which uniform proofs are complete and so to obtain the appropriate formulation of resolution proof for such choices. Resolution proofs in linear logic are somewhat di cult to de ne. This di culty arises from the need to decompose de nite formulae into a form suitable for the use of the linear resolution rule, a rule which requires the selected clause to be deleted after use, and from the presence of the modality ! (of course). We consider a translation | resembling those of Girard | of the intuitionistic hereditary Harrop formulae and intuitionistic uniform proofs into our framework, and show that certain properties are preserved under this translation. We sketch the design of an interpreter for linear logic programs.

An interesting recent development in logic of some signi cance for theoretical computer science is linear logic 8]. A natural question which arises is to determine what signi cance this development may have for logic programming; in particular, the identi cation of a particular set of formulae as a linear logic programming language, and the characterization of the novel features of a linear logic programming language. In this paper we show how linear logic programming languages may be identi ed, purely by a proof-theoretic analysis. This is done by studying certain permutation properties of a sequent calculus presentation of linear logic. This in turn allows us to identify classes of formulae for which a smaller class of proofs, known as uniform proofs, can be shown to be complete. Uniform proofs have been studied in the past 13], 12], and it seems that such proofs characterize the proof theory of logic programming. As it is easy to show that uniform proofs are not complete for full linear logic, we thus identify linear logic programming languages by classes of formulae for which uniform proofs are complete. Furthermore, we show how a linear logic version of the resolution rule may be given. The major di erence in this case is that the clause used in the resolution step is deleted from the program. This allows the programmer to specify an upper bound for the number of times a given clause is to be used, and we may think of the resolution step in linear logic to mean \resolve and retract". From a programming point of view, this property allows the speci cation, in a logical manner, of features such as destructive assignment and computation bounded by time and/or space.

1 Introduction

We assume a standard two-sided presentation of linear sequent calculus 8], 3], without the constants of linear logic, as presented in Appendix A. One of the distinguishing features of logic programming is goal-directed search. More precisely, there is a search operation corresponding to each logical connective, and when searching for a proof of a given goal one applies the search operation that corresponds to the outermost connective of that goal, and then to the outermost connective of each subgoal so generated, etc.. For Horn clause goals, i.e. existentially quanti ed conjunctions of atoms, this corresponds to using uni cation to \delay" the choice of witnesses for the variables, and a strategy for selecting a particular atom as the next subgoal. For a larger language, such as rst-order hereditary Harrop formulae 13], we need a richer set of primitive search operations, or search primitives, so that each distinct connective corresponds to a distinct search primitive. Clearly it is not di cult to identify the appropriate search operation for a given right rule, and indeed it is clear that such a procedure will be sound. However, in addition, we need to know that this method of searching for proofs is complete: that we are guaranteed not to miss a consequence. Hence our problem is not so much to identify the required search primitives for the right rules of linear logic as to show that the goal-directed search strategy is complete. Such considerations imply that a methodology for determining classes of formulae for which this strategy is complete is in a turn a methodology for nding logic programming languages. Hence, in order to determine what classes of formulae may be considered as linear logic programming languages, we need to consider a particular class of proofs which rei es such a strategy. In 13] it is shown how uniform proofs are complete for a certain fragment of (intuitionistic) rst-order logic. A uniform proof in that context is one in which the outermost connective of the succedent is introduced in the previous step. Thus, in terms of goal-directed search, this means that right rules are applied as early as possible in the proof search process. The de nition of such uniform proofs in linear logic is somewhat more intricate, the main di culty being that, under certain circumstances, it may be necessary to apply a left rule in the middle of a sequence of right rules in order to maintain completeness. For example, consider the sequent ` . Clearly there is a proof in which the -R rule precedes the -L rule,

2 Uniform Linear Proofs

However we need not be restricted to this rule, as linear logic contains modal operators which allow intuitionistic logic to be embedded within it, and so the standard resolution rule may be used under certain circumstances. Hence our linear logic programming language allows these two versions of the resolution rule to be used in the one system. We take as our point of departure the notion of uniform proof, introduced by Miller et al. 13], 12]. We present a proof-theoretic analysis of this notion and the attendant notions of de nite and goal formulae for linear logic. In Section 2 we develop the appropriate notion of uniform proof for linear logic and proceed to show how classes of de nite and goal formulae may be de ned. Section 3 shows how resolution works in this context, and in Section 4 we discuss some issues pertaining to the implementation of an interpreter for our language. Finally in Section 5 we show how the system of Miller et al. may be embedded in ours, thus showing our system to be a conservative extension of the standard ones. A preliminary account of this work appears in 9].

i.e.

`

; `

`

-L

-R

but we cannot apply the rules in the reverse order, as neither ` nor ` is provable. Hence, we cannot always push the -L above the -R rule; but the cases in which this is not possible may be classi ed. A similar example occurs for the C!-L rule. Consider the sequent ! ` . Clearly there is a proof in which the -R rule precedes the C!-L rule, i.e.

`

Definition 2.1 (RL, LR and Locally LR Proofs) We de ne the following sha-

-R ! ;! ` C!-L ! ` but we cannot apply the rules in the reverse order, as ` is not provable. Thus, as in the previous case, we cannot always push the C!-L above the -R rule; but the cases in which this is not possible may be classi ed. As it happens, these are the only two such cases; in all the others the \outermost connective rst" strategy will su ce. We develop formally the notion of a uniform proof in this context. In what follows -R and ]-L range respectively over the right and left rules for the linear connectives as well as the rules W?-R, W!-L, C?-R and C!-L.

pes of linear proofs: 1. A proof is RL if there is an occurrence of a right rule preceding a left rule; 2. A proof is LR if all occurrences of right rules appear after all left rules; 3. A proof is locally LR if the only occurrences of a right rule preceding a left rule are either of the form:

` ! `

!-L

` ! `

!-L

?` ; ?0; ` 0 ?; ?0; ? ` ; 0

where 1 and 2 are locally LR, or of the form:

1

-R

2

]-L

? -L

?` ; ?0 ` ; 0 ?; ?0 ` ; ; 0 ?00; ` ; ; 0

1

2

-R -L

where 2 ?, 2 ?0, and 1 and 2 are locally LR, or of the form:

?` ; ?; ?0 ` ?00; ! `

1

?0 ` ; 0 ; ; 0 ; ; 0

2

-R C!-L

where ! 2 ?, ! 2 ?0, and 1 and 2 are locally LR. 2

However, locally LR proofs are not quite satisfactory for our purposes, as they might involve some inessentially complicated subproofs on the right hand side of the ? -L rule. Hence we introduce the notion of a simple proof, cf. 12]. The intuition behind simple proofs is that the right hand subproof used in the ? -L rule should be trivial, i.e. require no e ort to prove. For example the following proof is not simple:

`

`

; ? ; ? `

; ? `

` ? -L

? -L

However, it is clear that the sequent ; ? ; ? ` does have a simple proof. This property in fact holds for any sequent in which the antecedent is a program and the consequent a goal.

Definition 2.2 (Simple Proofs) A linear proof

occurrence in

of the ? -L rule is of the form:

0

is said to be simple if every

?` ; ` 0` ; ; 0 ?; ? ; ?

2

Henceforth, we shall call simple locally LR proofs uniform proofs. Our aim here is to show how, with the linear rules read as reduction operators from conclusion to premisses1 , it is possible to obtain goal-directed proof-search procedures for certain classes of linear formulae. To this end, we identify classes of de nite and goal formulae for which uniform proofs are complete for consequence. There are several choices which may be made at this point, and in De nition 2.3 below we present illustrative classes of formulae rather than large ones. For example, we limit negation to be applied only to atoms; extensions to the class of negated formulae are possible. Also, for simplicity, we limit implicationalde nite formulae to Vx exclude G ? (A1 & : : : & Am ), G ? ~ : A, etc., see 10]. Some other extensions are mentioned at the end of this section.

1

Kleene 11] explains this in the case of classical predicate calculus.

Definition 2.3 (Definite and Goal Formulae) Let A range over atomic formulae. We de ne classes of de nite formulae and goal formulae as follows:

Definite formulae D ::= A j D & D j D D j G ? A j x : D j !D Goal formulae G ::= A j A? j G V j G G j G z G j G & G G j D? G j x:G j Wx:G

V

Programs are linear antecedents that consist of just closed de nite formulae and goals are linear succedents that consist of just closed goal formulae. We assume that all quanti ed variables are standardized apart. 2 The resemblance of these de nitions to those of hereditary Harrop formulae of intuitionistic logic should be clear. The reader who is unfamiliar with linear logic should note that full linear logic has four constants, whose ontological status is akin to that of ? in intuitionistic logic, and with which are associated special axioms and rules. We do not analyse the constants and their rules here: such an analysis is possible. An important point to note is that, unlike intuitionistic logic, in a given sequent ? ` , the antecedent ? and succedent need to be considered as multisets of formulae rather than sets. This di erence is due to the lack of the (general) weakening and contraction rules in linear logic, which are present in intuitionistic (and classical) logic. These properties may be recovered in certain cases by the use of the operators ! and ? and the W!, W?, C! and C? rules, which hence provide the ability to embed intuitionistic logic in linear logic. Furthermore, it is important to note that linear antecedents are proof-theoretically characterized by the tensor product ( ) of their components and that linear succedents are characterized by the tensor sum ( z ) of their components. We note that by considering the antecedents and succedents of linear sequents to be multisets of formulae we are able to suppress all occurrences of the exchange rules N linear proofs. If F = f 1; : : :; m g is a multiset in of linear formulae then we write 2F to denote the formula 1 : : : m . It is somewhat tedious but not very di cult to show the following result: Theorem 2.4 Let ? be a multiset of de nite formulae, and let be a multiset of goal formulae. Then ? ` has a linear proof if and only if ? ` has a uniform (or simple locally LR) proof. 22 As mentioned earlier, there are larger classes of formulae for which our analysis will hold. In particular, the analysis above still applies when ?G is allowed as a goal. In addition, goals of the form !G may be used, in which case a slightly more intricate notion of locally LR proofs is needed. In 10], restrictions are placed on de nite formulae to permit goal formulae of this form. Both of these extensions require additional detail rather than fundamentally new features. A more signi cant extension, again for which the above analysis remains germane, is the use of de nite formulae of the form D1 z D2 . The reason that this is more involved is that it requires an extension to the way that programs are used during computation, i.e. to the resolution rule and the notion of a clause. For simplicity we do not pursue this or other extensions here; however it should be noted that our analysis thus far applies to these other cases. These and other issues will be dealt with in a forthcoming paper by the authors.

2 This result amounts to a Permutation Theorem for the given fragment of linear logic. The reader who is interested in Permutation Theorems in general is referred to 5] for classical logic, 15] for a variety of non-standard rst-order connectives, and 14] for a constructive dependent type theory.

We saw in the previous section how simple locally LR proofs are complete for sequents P ` G where P is a multiset of de nite formulae (or program) and G is a multiset of goal formulae (or goal). In this section we show how a more speci c class of proofs, which we call resolution proofs, may be used in a similar fashion. We present this analysis for the de nite formulae and goal formulae of De nition 2.3: it can be extended to the additional classes of such formulae discussed above. The important characteristics of such resolution proofs are that they are goal-directed and that they use a single left rule, namely resolution3. First we introduce the notions of clause and clausal decomposition of a program P.

Definition 3.1 (Clause) A linear clause is a formula of the form A or G ? A, where A ranges over atomic formulae and G ranges over goal formulae. A mixed clause is a formula of the form A, G ? A or ! (C1 : : : Cn), where each Ci , 1 i n, is a linear clause. 2

3 Resolution

Note that when G is a conjunction of atoms, a linear clause in the above sense is just a Horn clause. Below we show how to generate a multiset of clauses from a multiset of de nite formulae via the mapping -]. We will nd it convenient to divide an antecedent into two parts | those formulae which are of the form !F, and those which are not.

Definition 3.2 (Antecedent Division) Let denote multiset union, and let D be a multiset of formulae. We de ne two multisets DI and DL such that D = DI DL as follows: DI = F 2D f F j the outermost connective of F is ! g DL = F 2D f F j the outermost connective of F is not ! g 2

S S

We may think of this distinction as specifying which formulae are known to be able to be re-used (those commencing with !) and those which are not.

Definition 3.3 (Clausal Decomposition) Let

denote multiset union. We de ne a mapping ?] from multisets of de nite formulae to multisets of mixed clauses as follows:

P]

=def D2P D] A] =def f A g D1 & D2 ] =def D1 ] or D2 ] D1 D2 ] =def D1 ] D2 ]

S

G ? A] =def f G ? A g V x : D] =def D] O C g D]I ! D] =def f !

C 2 D ]L

3 In this presentation, the resolution rule is split into two cases: in the purely linear fragment there would be just one. Such a split is inessential and a single rule will su ce provided one de nes a suitable notion of resolvant for mixed clauses (De nition 3.1). Indeed, such an approach is desirable if one considers de nite formulae of the form D1 z D2 , etc., which would otherwise require further cases of the resolution rule.

where variables x that occur in P and outwith the scope of some ! are marked as global and where variables x that occur in P within the scope of some ! are marked as local. 2

Note that P ] is V multiset of mixed clauses.4 For example, let P be given by the a de nite formula x : (p(x) (p(x) ? q(x))) ; then we have that P ] is the multiset f p(x); p(x) ? q(x) g. Thus we may think of the transformation ?] as a mapping which given a program, i.e. a multiset of de nite formulae, yields a multiset of clauses which are the compiled form of the program, i.e. the form for which resolution proof can be de ned. For given P , P ] can be considered to be a normal form of P . Note that there are no quanti ers on the variables in the clauses in P ], although certain of the variables are marked as being \global" and certain of the variables are marked as being \local"; these are the variables that are quanti ed in P . One point to note is that the mixture of universal quanti ers and ! may lead to some (possibly) surprising be the single de nite formula V x : ! V y : p(x; y), andresults. For example, let P p(a; c). It should be clear that consider the goal p(a; b) V V V ! y : p(a; y) ` p(a; b) p(a; c) is provable, and so x : ! y : p(x; y) ` p(a; b) p(a; c) is provable.5 Hence we may think of universally quanti ed variables outside the scope of ! as \global", in that all occurrences of the variable must be updated consistently. Due to the possibility of splitting the program during computation, this may mean updating variables simultaneously across several branches of the proof.6 On the other hand, the universally quanti ed variables within the scope of ! may be thought of as \local", in that they need only be updated in one formula. This leads us to the de nitions that follow.

gram. If x is a free variable in P ], then it is a global variable if it occurs outside the scope of any ! in P . Otherwise, x is a local variable. Let D be a multiset of de nite formulae. We say D0 and D00 are distinct copies of D if D0 and D00 are obtained from D by renaming the free variables of D so that D0 and D00 have no free variable names in common. 2

Definition 3.4 (Global and Local Variables, Distinctness) Let P be a pro-

Note that the marked \global" and \local" variables of De nition 3.3 satisfy this de nition. For a given substitution ~=~ ], we write ~=~ ]g to denote that the applitx tx cation of the substitution is to only those free variables that are global, throughout the proof. Otherwise, ~=~ ] applies to all global variables, throughout the proof, tx and to local variables only in the sequent in which the substitution arises (and to those above it, of course). One of the major di erences between intuitionistic logic programming and linear logic programming is that in the latter case we may need to split the program (and indeed the goal), due to the form of -R rule. In the case of linear clauses, this is simply a matter of dividing up the given multiset. However for mixed clauses, we need a more sophisticated approach, as formulae beginning with a ! may be used any number of times in a proof. From the contraction rule we know that if P ; !D; !D ` G is provable, then so is P ; !D ` G , and so when searching for an appropriate splitting of the program, we need to add a formula of the form !D to each branch. We will also need to \balance" the use of subformulae of !D, as we can only add an

4 The decomposition -] is related to the theory of proof nets, and indeed to the notions of reduction ordering | a combination of subformula ordering and substitution ordering | and matrix methods, described in 2], 4], 15] and 14]. Such constructions are useful in the study of Permutation Theorems, q.v. Theorem 2.4. 5 Cf. the Barcan formula : 8 x 2A(x) 28 x A(x). 6 In terms of the resolution proofs de ned below, those branches that are above the same premiss of the last & ?rule (Rule 8 in the de nition of resolution proof, below) as the sequent to which the resolution rule is applied. The form of the &-rule in such proofs enforces the restriction of substitutions to their own &-branches.

arbitrary number of copies of D to the antecedent, and not arbitrary numbers of a given subformula of D. For example, consider the program !(p q) and the goal p (q q).7 By use of the contraction rule in conjunction with !-L and -L, the program will imply the goal if p; q; !(p q) ` p (q q) is provable. If we reduce this to p; !(p q) ` p and q; !(p q) ` q q, then the rst sequent is provable, but the second is not, as we need to add p; q to the antecedent before splitting again, and we nd that p; q; !(p q) ` q is not provable. However, if we were allowed to duplicate more copies of the subformula q of p q than of the subformula p we should be able to prove the goal p (q q) from the program !(p q). Hence we need to ensure that the splitting of the program is done in such as way as to respect the structure of the original formulae. The reader should note however that as yet we have not provided any mechanism for the calculation of an appropriate splitting of the program (and goal). We postpone the description of such a procedure until we have de ned the notion of resolution proof and are ready to describe an interpreter. An essential feature of the mapping ?] is that it builds into resolution proofs all necessary instances of the -L and C!-L rules. Therefore the exceptional cases in the de nition of uniform (simple locally LR) proofs do not arise in resolution proofs. For example, as noted above, the sequent p q ` p q is provable, and requires the use of the left rule \below" that of the right rule. However, p q] = fp; qg, and so by replacing p q with fp; qg we eliminate the need for the left rule, and hence the need for an exception to be made to the \outermost connective rst" strategy. A similar simpli cation may be made for the other exceptional case by allowing formulae commencing with a ! to be added to both branches of a proof containing an occurrence of the -R rule and appropriately modifying the notion of an initial sequent.

C0 = ;

Definition 3.5 (Multiset Expansion) Let C be a multiset and let denote multiset union. We de ne C n for integers n 0 inductively as follows:

C n+1 = C C n

2

Definition 3.6 (Expansion) Let D be a multiset of mixed clauses, and suppose we have that DI = f!(C11 : : : C1n1 ); : : :; !(Cm1 : : : Cmnm )g. An expansion of D is a pair of multisets D1 and D2 such that

D1 D 2 = D L

f C11; : : :; C1n1 gi1

:::

f Cm1; : : :; Cmnm gim

for integers i1 ; : : :; im 0. A linear expansion of D is a pair of multisets D1 and D2 such that D1 D2 = DL . 2

Note that a linear expansion of D corresponds to the case in which i1 = : : : = im = 0. We come now to the de nition of resolution proof, De nition 3.7. Such proofs, which are computationally highly deterministic | they are goal-directed, with essentially one left rule | are characterized by uniform linear proofs. Note however that De nition 3.7 provides no mechanism for the non-deterministic decomposition of antecedents and succedents (programs and goals) required by the -rule. A similar issue arises if one considers de nite formulae of the form D1 z D2 . We remark that this non-determinism can be handled at the level of the design of an interpreter.

7

Note that the sequent p; q; !(p q) ` p (q q) is not provable in linear sequent calculus.

Definition 3.7 (Resolution Proof) We de ne the notion of resolution proof

by de ning a relation `R . Let D range over multisets of de nite formulae and let denote multiset union. A resolution proof is a tree regulated by the following rules, which is constructed so that when read from root to leaves, the resolution rules are applied only when no other rule is applicable: 1. The axiom judgement is given by:

tx where either DL = fA0g and A = A0 ~=~ ] or DL = ; and there exists !A0 2 DI such that A = A0 ~=~ ]; tx 2. We shall refer to this rule as the resolution rule:

where G ? A = (G0 ? A0 ) ~=~ ]; tx 3. We shall refer to this rule as the !-resolution rule:

D `R A

D ~=~ ]g `R G ; G f A g `R A tx D fG0 ? A0 g `R A; G

4. 5. 6. 7. 8.

V 10. The -rule: W

respectively. Note that we maintain \global" and \local" markings; D D] `R G; G 9. The ? -rule:

~ tx ~tx D ~=~ ]g C ~=~ ]] f(!(G0 ? A0 ) C) ~=~ ]g g `R G ; G f A g `R A tx ~ D f!(G0 ? A0) C g `R A; G ~ where G ? A = (G0 ? A0 ) ~=~ ], and where C denotes C1 : : : Cm for m 0; tx The ?-rule: D f A g `R G D ` R A? ; G DI ; D1 `R G1 ; G DI ; D2 `R G2; G 0 The -rule: D `R G1 G 2 ; G ; G 0 where D1 D2 is an expansion of D; D `R G1 ; G D `R G2; G The -rule: D `R G1 G2; G D `R G1 G2; G The z -rule: D ` R G1 ; G 2 ; G D `R G1 z G2; G The &-rule: D0 `R G01; G 0 D00 `R G00; G 00 2 D `R G1 & G2; G where D0 and D00 are distinct copies of D, and where G01; G 0 and G00; G 00 are 2 obtained from G1 ; G and G2 ; G by the applying the renamings of D0 and D00

where y is not free in D or G ; 11. The -rule: D `R G t=x]; G

D `R D ? G; G D `R V y=x]; G G D `R x : G; G D `R W x : G; G

Note that Rules 2 and 3 a ect other sequents in the proof, so that a resolution proof is well-de ned only if all occurrences of Rules 2 and 3 (and the axioms) yield compatible substitutions. 2

Note that the latter rules can be considered to correspond to the right rules of uniform proofs and the former ones to the left rules, in the presence of the decomposition ?]. It should be clear that the !-resolution rule and the second part of the axiom judgement are directly analogous to the corresponding rules in intuitionistic logic. The !-resolution rule clearly has the property that P ] `R A if there is a clause !(G0 ? A0 ) in P ] such that G ? A = (G0 ? A0) ~=~ ] and P ] `R G, which is a more tx intricate form of the resolution rule given in 12]. Similar remarks apply to the second part of the axiom judgement. For example, consider the sequent

f q; !(q ? p) g `R p :

By applying the !-resolution rule, we obtain the subgoals f q; !(q ? p) g `R p and f p g `R p: We now proceed to show that resolution proofs behave in the expected manner. First we present a useful lemma. D be a linear clause, D be a multiset of linear clauses and let G be a multiset of goal formulae. Then: 1. If P `R G , then P f!Dg `R G ; 2. If P f!Dg f!Dg `R G , then P f!Dg `R G ; 3. OP fDgn `R G then P f!Dg `R G for any n 0; 4. If If P D `R G then P f! C g `R G . 2

C 2 D]

Lemma 3.8 (Weakening and Contraction) Let P be a multiset of mixed clauses,

One interpretation of this result is that we may replace an occurrence of the resolution rule using the clause D with an occurrence of the !-resolution rule using the clause !D. Note that this lemma implies that the set-theoretic properties of formulae commencing with ! in arbitrary linear proofs are preserved in resolution proofs. It is this property which allows us to perform \mixed" intuitionistic and linear deduction in this system. This justi es our remark above that clauses with ! as the principal connective behave in an antecedent in precisely the same way as the clauses of intuitionistic logic programs 12]. We have the following main theorem:

Theorem 3.9 Let

P be a multiset of de nite formulae and let G be a multiset of goal formulae. Then P ` G is provable i P ] `R G . 2

In this way we may think of resolution proofs as a relatively e cient way of proving theorems in the given fragment of linear logic. Furthermore, such proofs form a basis for logic programming in this fragment, as the choice of step in the proof-search process is determined by the structure of the goal, and so any (multiset of) goal formulae may be considered as a goal. In particular, this determinism is characterized by resolution proofs.

4 A Sketch of an Interpreter

In this section we sketch the design of an interpreter for linear logic programs. Essentially, the interpreter will execute resolution proofs, however as we noted in Section 4, the de nition of resolution proof does not provide a mechanism for calculating the appropriate splitting of the antecedent and succedent in the -rule. This

problem is particularly acute in the presence of clauses whose top-level connective is the modality ! , and so we shall begin with an example of this case. We illustrate our method by presenting a series of examples. We introduce the key notion of path in Example 1. Example 1 Suppose that we are faced with the endsequent !(p q) ` (p q) & (p (q q) ; which is not provable in linear sequent calculus. We must attempt a resolution proof of f !(p q) g `R (p q) & (p (q q)) ; and fail. According to the de nition of resolution proof, we must identify a suitable expansion of !(p q) and proceed to identify suitable splittings of that expansion: computationally, this is unacceptable. Our solution is to adopt a lazy approach, and to this end we permit the interpreter to construct the following proto-proof by modifying the rules of resolution proof:

f!(p q)g`R q f!(p q)g`R q f !(p q) g `R p f !(p q) g `R q f !(p q) g `R p q f !(p q) g `R p f !(p q) g `R q q

&

f !(p q) g `R p (q q)

f !(p q) g `R (p q) & (p (q q))

De ne the construction of a path in such a proto-proof as follows: The endsequent is in every path; Traverse the tree towards the leaves, starting at the endsequent: { Whenever a &-rule is reached, choose a branch and proceed; { Whenever a -rule is reached, proceed along both branches; Continue until all branches of the path have reached a leaf. The proto-proof determines a resolution proof just in case for each possible such path in it, there is an expansion of the antecedent that is compatible with the leaves in the path. For example, the proto-proof given above has a path marked by asterisks (*). For this path, there are 2 occurrences of q in the leaves, so that we need the expansion f p; p; q; q g of f !(p q) g. However, there is only 1 occurrence of p in the leaves of this path, so this expansion is not suitable. We conclude that this proto-proof does not determine a resolution proof of the given endsequent. Example 2 Now we introduce the resolution rule. Suppose that we are faced with the endsequent p; q; r; (q r) ? p ` p p ; which is provable in linear sequent calculus. Since we have that p; q; r; (q r) ? p] = f p; q; r; (q r) ? p g, we must construct a resolution proof of f p; q; r; (q r) ? p g `R p p : Adopting our lazy approach we obtain the following proto-proof:

fp; q;r; (q r) ? pg`R q fp;q;r; (q r) ? pg`R r fp;q; r; (q r) ? pg`R p fp;q;r; (q r) ? pg`R q r fp; q;r; (q r) ? pg `R p fp;q;r; (q r) ? pg `R p f p; q;r; (q r) ? p g `R p p

res

We construct paths as before (in this case there is just one, marked by *), but upon reaching the lazy resolution rule (labelled by res) we must adjust our calculations. The branch of the lazy version of the resolution rule that corresponds to the branch of the resolution rule of the form f A g `R A, in this case fp; q; r; (q r) ? pg `R p, is not included in the calculation of the usage of the elements of the antecedent; however the resolvant clause, in this case the clause (q r) ? p, is used at this point in the proof. We note that for this proto-proof, each of the remaining components, namely p; q; r, is used exactly once in the remaining leaves; and so we conclude that a resolution proof of the given endsequent is indeed determined. Example 3 Now we introduce the universal quanti er, V, into the antecedent. Suppose that we are faced with the endsequent

^ x : (p(x)

q(x)) ` p(t) q(u) ;

which is not provable in linear sequent calculus. Since we have that x : (p(x) q(x))] = f p(x); q(x) g, with x marked as being global, we must attempt to construct a resolution proof of f p(x); q(x) g `R p(t) q(u) ; and fail. Adopting our lazy approach, we obtain the following proto-proof: f p(x); q(x) g `R p(t) f p(x); q(x) g `R q(u) f p(x); q(x) g `R p(t) q(u) Each of the leaves (on the unique path marked by *) is of the required form for axioms, but on one branch the global variable x receives the instantiation t and on the other it receives the instantiation u; since these are incompatible, we conclude that the given proto-proof does not determine a resolution proof of the given endsequent. The examples given above illustrate most of the di culties encountered in the construction of an interpreter for our notion of linear logic programming. We note that all of the necessary path constructions can be performed dynamically as the search proceeds. However, two further issues are noteworthy. Firstly, an occurrence of & in a program may result in backtracking, as each formula of the conjunct may be used as the premiss of a proof. However, unlike , only one of the conjuncts is to be used in the proof, and so the conjunct not chosen must not be available for subsequent use. Secondly, a goal in our system is a multiset of formulae, and hence there is the question of which goal to reduce next. Thus we will need a computation rule not only for determining the order of each conjunct in a goal, but also for which goal to reduce next. Clearly a depth- rst rule is one possibility; there may be others which are preferable and yet similar in e ciency.

V

A similar analysis, though somewhat more involved, may be performed for other connectives, including z and the modality ! . Full details of an interpreter are provided in a forthcoming paper by the authors which describes a prototype implementation of linear logic programming. In this section we show how proofs in the hereditary Harrop fragment of intuitionistic rst-order logic may be encoded as proofs in this fragment of linear logic. In order so to do, we recall some de nitions for intuitionistic logic from 12] and 13]. Definition 5.1 (Hereditary Harrop Formulae) Let A range over atomic formulae. We de ne the classes of hereditary Harrop de nite formulae and hereditary Harrop goal formulae as follows: Definite formulae D ::= A j D ^ D j G A j 8x : D Goal formulae

An hereditary Harrop program is a set of closed hereditary Harrop de nite formulae. An hereditary Harrop goal is a closed hereditary Harrop goal formula. 2 8 In 12] a relation `o denoting operational provability is de ned and discussed.

5 Intuitionistic Logic

G ::= A j G _ G j G ^ G j D G j 8x : G j 9x : G

The reader is referred to 12] and 13] for discussion and proof of:

Proposition 5.2 Let

P be a hereditary Harrop formula program and let G be a hereditary Harrop goal. Let `I denote intuitionistic provability. Then P `o G i P `I G. 2

Below we present an encoding of intuitionistic formulae. Definition 5.3 (Encoding) Let D range over hereditary Harrop de nite formulae, let P range over multisets of (linear) de nite formulae, let G range over hered(D)? of D and the linear encoding (G)+ of G as follows: (A)+ (G1 ^ G2)+ (G1 _ G2)+ (9~ : G)+ x (8~ : G)+ x (D G)+ =def =def =def =def =def =def A (G1)+ & (G2 )+ (G (G W ~1):+(G)+ 2)+ x V ~ : (G)+ x (D)? ? (G)+

itary Harrop goals, and let denote multiset union. We de ne the linear encoding

P?

=def (A)? =def (D1 ^ D2 )? =def (8~ : D)? =def x (G A)? =def

SD2P (D)?

!A ! (D1 )? ! (D2 )? Vx ! ( ~ : (D)? ) !((G)+ ? A)

We may think of these encodings as operating at the level of proofs, rather than at the level of formulae. This is due to the way that intuitionistic conjunctions and implications are each translated di erently, depending on whether they occur in a positive or negative position. We note that this encoding behaves as expected.

2

8 In this case taking G A here is equivalent to taking G D. However in the case of linear de nite formulae taking G A (De nition 2.3) is not equivalent to taking G D. This is because ? does not distribute over . Consequently the restriction to G A, which is required for the de nition of resolution proof, represents a further restriction of the class formulae that we consider. Recall from Section 2 that some simple extensions of this class are possible; for example G ? (A1 & : : : & Am ) and G ? ~ : A, etc., see 10]. x

V

Theorem 5.5 Let P be a hereditary Harrop program and G be a hereditary Harrop goal. Then the sequent P ` G is provable in intuitionistic logic i the sequent (P )? ` (G)+ is provable in linear logic. 2

Thus we arrive at the following theorem:

Proposition 5.4 Let P be a hereditary Harrop program and let G be a hereditary Harrop goal formula. Then P `o G i (P )? ] `R (G)+ . 2

6 Conclusion and Related Work

We have seen how a fragment of linear logic may be used as a logic programming language, and how this fragment may be seen as a conservative extension of an intuitionistic logic programming language. Related work in linear logic programming is presented in 10], 1]. 10] is the more closely related. Their class of goal formulae is richer than ours in that it permits formulae of the form !G. However, this forces their de nite formulae to be more constrained. In particular, they cannot have de nite formulae of the form !(D1 D2 ) and so cannot force the use of two clauses an unspeci ed, but equal, number of times. In fact, they take a notion of linear clause as their starting point, whereas we derive our notion of clause via a proof-theoretic analysis. Indeed, their identi cation of antecedents with the tensor product of their components, so that the -L rule is not explicitly considered, means that some proof-theoretic subtlety in the analysis of the notion of uniform proof in linear logic is less clear.

The authors are grateful to Simon Ambler, Gianluigi Bellin, Jean-Yves Girard, Dale Miller, Gordon Plotkin and Lincoln Wallen for their interest in, and encouragement of, this work. Harland is supported a grant of the Australian Research Council through the Machine Intelligence Project. Pym is supported by U.K. Science and Engineering Research Council grant GR/G 58588, \Logical and Semantical Frameworks"; and by European Community ESPRIT Basic Research Action 3245, \Logical Frameworks: Design, Implementation and Experiment".

7 Acknowledgements

8 References

496-510, Jerusalem, June, 1990. 2] Andrews, P.B. Theorem-proving via general matings. J. Assoc. Comp. Mach. 28(2):193-214, 1981. 3] Asperti, A. Categorical Topics in Computer Science. Dottorato Di Ricerca in Informatica, Universita di Pisa { Genova { Udine, 1990. 4] Bibel, W. Computationally Improved Versions of Herbrand's Theorem. Logic Colloquium '81, pp. 11-28. North-Holland, 1982. 5] Curry, H.B. The permutability of rules in the classical inferential calculus. J. Symb. Log. 17, pp. 245-248, 1952. 6] Gehlot, V., Gunter, C. Normal Process Representatives. Proc. 5th Annual IEEE Symposium on Logic in Computer Science. Philadelphia, June 1990. IEEE Computer Society Press. 7] Gentzen, G. Untersuchungen uber das logische Schliessen. Math. Zeitschrift 39(1934), pp. 176-210, 405-431.

1] Andreoli, J-M., Pareschi, R. Linear Objects: Logical Processes with Built-in Inheritance. Proceedings of the International Conference on Logic Programming

8] Girard, J-Y. Linear Logic. Theor. Comp. Sci. 50, 1987, pp. 1-102. 9] Harland, J.A., Pym, D.J. The Uniform Proof-theoretic Foundation of Linear Logic Programming. Report ECS-LFCS-90-124. University of Edinburgh, 1990. 10] Hodas, J., Miller, D. Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract. Proc. 6th Annual IEEE Symposium on Logic in Computer Science. Amsterdam, July 1991. IEEE Computer Society Press. 11] Kleene, S.C. Mathematical Logic. Wiley and Sons, 1968. 12] Miller, D. A Logical Analysis of Modules in Logic Programming. J. Log. Prog. 6(1&2), 1989, pp. 79-108. 13] Miller, D., Nadathur, G., Pfenning, F., Scedrov, A. Uniform Proofs as a Foundation for Logic Programming. University of Pennsylvania report, MS-CIS-89-36. To appear in the Annals of Pure and Applied Logic. 14] Pym, D.J., Wallen L.A. Proof-search in the -calculus. In: Logical Frameworks, G. Huet and G. Plotkin (editors), Cambridge University Press, 1991. 15] Wallen, L.A. Automated Deduction in Non-classical Logics. MIT Press, 1989. 16] Yetter, D. Quantales and (Non-commutative) Linear Logic. J. Symb. Log. 55(1), 1990, pp. 41-64. Appendix A

We present the two-sided linear sequent calculus. We let and range over formulae and ? and , etc. range over multisets of formulae. ?` ; ?0 ; ` 0 cut axiom 0` ; 0 ` ?; ? 0` ?; ; ; ? ? ` ; ; ; 0 X-R X-L 0` ?; ; ; ? ?` ; ; ; 0 ?; ` ?` ; ?; ? ` ?-L ? ` ? ; ?-R ?` ; ?0 ` ; 0 -R ?; ; ` -L ?; ` ?; ?0 ` ; ; 0 ?; ` ?` ; ? ` ; &-R ?; ` ?; & ` ?; & ` &-L ?` & ; ?` ; ?` ; ?; ` ?; ` -L -R ?; ` ?` ; ?` ; ?` ; ; ?; ` ?0 ; ` 0 z -L z -R 0; z ` ; 0 ?; ? ?` z ; ?` ; ?0 ; ` ?; ?0 ; ? ` ; 0 ?; ` ?; ! ` !-L !?; `? !?; ? `? ?-L ?` ?; ! ` W !-L ?; ! ; ! ` C !-L ?; ! ` ?; t=x] ` -L ?; x: `

0

? -L

V

V

?; ` ; ? ` ? ; ? -R !? ` ; ? !? `! ; ? !-R ?` ; ? `? ; ?-R ?` ? `? ; W ?-R ? `? ; ? ; C ?-R ? `? ; ? ` y=x]; -R ? ` x: ;

V

V

?; y=x] ` -L ?; x: ` where x is not free in ?, .

W

W

? ` t=x]; ? ` x: ;

W

W-R

- Proof-theoretic foundation of compilation in logic programming languages
- The semantics and proof theory of linear logic
- ABSTRACT A COMPILER SYSTEM OF A LINEAR LOGIC PROGRAMMING LANGUAGE
- Model checking linear temporal logic using tabled logic programming
- MULTIMEDIA TECHNOLOGY FOR SELF-LEARNING LOGIC AND PROGRAMMING LANGUAGES ABSTRACT
- Abstract On duality in linear programming under fuzzy environment
- A proof of the optimality of the MIN paging algorithm using linear programming duality
- Words as modules a lexicalised grammar in the framework of linear logic proof nets
- Abstract A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and
- Guarded programs and Proofs in Linear Logic (extended abstract)
- 学霸百科
- 新词新语