Canonical Proofs for Linear Logic Programming Frameworks^{⋆}

Didier Galmiche CRIN-CNRS & INRIA Lorraine Campus Scientifique - B.P. 239 54506 Vandœuvre-lès-Nancy Cedex France e-mail: galmiche@loria.fr

Abstract. We discuss here the proof-theoretic foundations for theorem proving and logic programming in linear logic, mainly studying how to define canonical proofs (that are complete) for efficient proof search in fragments of linear logic. We analyze the conception of such proof forms, for frameworks based on proof-construction as computation, emphasizing the relationship between the logical fragment and its proof search strategies. This point is essential for the definition and implementation of logic programming languages within linear logic.

1 Introduction

Linear logic (denoted LL) is a powerful and expressive logic with connections with a variety of topics in computer science. It is a logic of actions introducing notions like controlled and strict resource management [7]. It appears as an appropriate framework to study models of concurrency [15], extensions of logic programming [12], concurrent logic programming [2, 13] or concurrent functional programming [1]. Here we focus on the logical foundations for efficient proof search dedicated to theorem proving and logic programming in LL fragments. Different works deal with the question of significance of linear logic for logic programming, mainly why and how to define a logic programming language based on an interesting LL fragment [2, 10, 12], with restrictions on definite formulae (i.e., resources), goal formulae and queries definitions. They mainly take as conceptual departure a specific proof form (focusing or uniform proof) (that is complete) assuming a goal-directed proof search strategy as characteristic feature of logic programming [8]. In [2] the main point is to treat Horn clauses with multiple atoms in the head, in [10] it is to use resolution in a large LL fragment and in [12], considering some computational problems, it is to make a suitable logic programming language in a fragment of intuitionistic linear logic. For general theorem proving (not necessarily goal-oriented) we also need to define complete and tractable subclasses of proofs [3, 5]. Let us mention that in [13], a new linear logic framework, named ACL, is proposed for concurrent computation described in terms of proof construction in linear logic. Thus, efficient and adapted proof construction methods are essential for

⋆ In proceedings of the ICLP’94 Workshop on Proof-theoretical Extensions of Logic Programming, A. Momigliano and M. Ornaghi editors, pp 10-19, Santa Margherita Ligure, June 1994.

such linear logic programming frameworks and an important question arises: how to define complete (and tractable) proof subclasses and proof search strategies in a linear logical framework ? Some answers have been partially given in works on proof search and strategies dedicated to theorem proving in LL fragments [3, 5, 14, 17]that can help us to consider LL fragments for (concurrent) logic programming. We propose here a global analysis of this question based on the following procedure. We analyze the logic programming language and then deduce the logical rules involved by the computation process. Thus, we systematically study their permutability properties and analyze the possible inference movements in a proof, i.e., we identify the inference rules that can be easily moved up or down in a proof. After an analysis of inference movements and some non-determinisms reductions, we can propose various definitions of canonical proofs (with a partial order for rules application), that we have to prove to be complete. With this approach, we can study the potentialities of logical frameworks for theorem proving and logic programming and justify existing or new proof form definitions as bases for proof search (as uniform proofs in [9, 12]). Moreover, our results about permutability allow to define possible proof transformations to improve computations. The study of relationship with the proof-nets construction [4] and normalization will lead to refinements of this work for good implementations of linear logic programming languages. implementation of efficient interpretors.

2 Canonical Proofs in Linear Logic

We discuss about the proof-theoretic foundations to design subclasses of canonical proofs as bases for proof construction in linear logic frameworks. There have been some works devoted to the definition of such classes, for logic programming, mainly based on uniform proofs and the class of hereditary Harrop formulae of intuitionistic logic [16]. Let us mention that they assume that the characteristic feature of logic programming is the goal-directed proof search [8]. The notion of uniform proof has been adapted to adequate fragments of linear logic [12] for which a suitable proof search method, for instance resolution proof [9, 10], can be defined. Here, we will analyze the general concept of canonical proof in linear logic, dedicated to frameworks based on proof-search as computation paradigm.

2.1 Proof search and computation

Some recent works have been devoted to proof search in fragments of Linear Logic following two approaches. From the programming logic point of view computation is described in terms of proof search of LL formulae in some fragments adequate to describe the concurrent programming paradigm [2, 10, 12, 13]. The proposals for certain normal proofs (focusing, uniform or simple), that are complete and tractable, correspond to proof-theoretical extensions of logic programming with aims of mechanization and expressiveness. From the functional programming point of view, computation is described in terms of proof normalization. But before computing we must be able to build a proof of a LL formula that specifies a task, using the Curry-Howard isomorphism [1]. The (automatic or not) synthesis of efficient functional linear programs is connected to the potentialities of proof normalization and transformation. These approaches need specific proof search methods for automatic or interactive theorem proving depending on the proof direction (bottom-up or top-down) and the logic fragment [17]. Let us notice that based-on uniform proof proof-search [12] sometimes leads to failure with a simple petri net specification (expressed in intuitionistic LL). This motivates the analysis of the relationship between an appropriate fragment for theorem proving (with induced program synthesis) or logic programming in linear logic and the complete (or not) proof subclasses leading to efficient proof construction ?

2.2 A general procedure

To study this point we propose a general procedure leading to canonical proof proposals and also specific strategies for efficient proof search. Our conceptual departure is the notion of inference permutability in linear logic. It is a basic notion that appears to be very important for an efficient proof search (and theorem proving) in non-classical logics [18]. For a given fragment of LL and a given direction (bottom-up or top-down), we propose a general methodology leading to proof search methods. The first step consists in systematically studying the permutability properties of the LL fragment. The second step consists in analyzing the possible up or down movements of an inference in a proof that are justified by permutation possibilities and in fixing the sets I_{↑} and I_{↓} of inferences to move up or down. Then, we can define possible proof transformations on a given proof and canonical proof forms that will be complete. To define such forms we use knowledge about up and down inference movements with a view to fixing an order of the rule applications. Finally, we have to prove the completeness theorem saying that if Γ ⊢ Δ is provable then there exists a canonical proof of it. In fact, we can define general subclasses of canonical proofs that can be refined and instantiated, depending on the actual logic fragment we consider. Let us consider the full LL (with one-sided linear sequent calculus) as an example. After studying permutability properties and non-determinism reduction, we have I_{↑} = {cut, ⊗, ⊕,?, w?, ∃, ⊥} and I_{↓} = {℘, &, c?, ∀, ⊥}. Let us note that the ! inference has the specific property, not due to permutability, to be moved down. With such results [5] we can transform a proof by moving inferences up or down and also use such a transformation to define specific proof forms (normal forms) adequate to efficient proof construction or specific proof strategies [6].

2.3 Canonical proofs design

For a given proof direction, we can define a reduction order of the goal to prove or to satisfy and theorem proving will consist in constructing what we call a canonical proof. Thus, the main point is to define proof sub-classes [5] that will be both complete (any derivable formula in LL has a normal form) and tractable (many irrelevant choices in the proof search are eliminated) and to understand the reasons and the consequences of these definitions. The application of the previous analysis leads to such results. For our example, in a bottom-up approach, a canonical proof is a proof withouts cuts or conflicts between weakening and contraction rules where any intermediate conclusion is reduced, taking into account the results about movements. It means that, for each intermediate conclusion, we apply the c? rule then the ! rule, then a rule of I_{↓} and finally a rule of I_{↑}, with respect of the proof-theoretic results. We can thus prove the central result, that for any provable formula (or sequent) of LL there exists a canonical normal proof of it. We would like to have a sub-class of proofs that are complete and tractable that we can consider as the basis of an automatic theorem prover. It is clear that for efficiency reasons, it appears necessary to restrict the study to some particular fragments of LL being sufficiently large to develop logic programming or theorem proving for program synthesis. A similar study is possible for other proof directions.

The design of a prover for a LL fragment might be based on the canonical proofs definition. For such a design, we observe three fundamental selection choice points: the choice of a goal to satisfy, the choice of a principal formula in a goal and finally, from a given goal and a principal formula, the choice of an inference with this goal as conclusion and this formula as the principal one. For the goal choice, we have a don’t care non-determinism (result independent of it) but it has consequences on time and space resources. The choice of a principal formula is crucial for proof construction and it reduces effectively the don’t know non-determinism concerning it. It is based on the canonical proof definition. Thus, in the case of our example, we do not represent contractions as rules and if the goal ⊢ Δ′ we have chosen is of the form ⊢!A,?Δ the only possible principal formula is !A. Else if it contains formulae with connectives of I_{↓} we can choose any of them as principal formula (don’t care non-determinism). Else if it contains formulae with connectives of I_{↑} we can choose such a formula as principal formula. But if we have to choose among several possible formulae this choice is not without consequences (don’t know non-determinism) and can lead to backtracking on it. To summarize, the search of a canonical proof imposes constraints for the choice of the principal formula, that reduce significantly the don’t know non-determinism of it. Moreover, it could help us to elaborate specific tactics and strategies for the choice of the goal to prove. Let us mention that the relationship between proof-nets and canonical proofs has to be studied to refine proof search. Moreover, from an analysis of the sequent to prove, we can also refine the canonical proof definition (corresponding to the logical fragment) to make proof search more efficient.

Remark. Let us remark that in [14] one introduces an optimized form of dynamic skolemization that significantly reduces the amount of non-determinisms. This optimization is effectively combined with other optimizations based on permutability results. Relationships have to be studied, but our proposal, that is also general, consists in proposing canonical proof forms, for a LL fragment and a proof strategy.

3 Linear logic programming

Different works examine the question of significance of linear logic for logic programming, mainly how to define a logic programming language based on LL [2, 10, 11, 12, 13]. They include restrictions to specific LL fragments for concurrent computation through a goal-oriented proof search as characteristic feature of logic programming. In general they define classes D of definite formulae (resources) and G of goal formulae with queries of the form Γ ⊢ Δ where Γ is a multiset of resources and Δ is a multiset of goals. Thus, having in mind a proposal for linear logic programming, motivated by expressiveness, how can we analyze its design? An answer consists in applying the previous general procedure: defining at first the syntax of our logical language, secondly determinating what are the logical rules involved in the proof search process, thirdly analyzing their permutability and movement properties, deducing the possible proof transformations in this language and finally defining adequate subclasses of proofs that are complete. Let us illustrate these points through an example. We consider here the Harland-Pym’s proposal based on uniform proofs and resolution for fragments of LL [9, 10], and analyze the proof-theoretical results to build an interpretor.

1) The logic programming language

The logical framework includes the classes of definite formulae (or resources) (denoted D) and goal formulae (denoted G) that are defined by:

D := A|D&D|D ⊗ D|G —∘A|∀xD|!D.
G := A|A^{⊥}|G&G|G ⊗ G|G ⊕ G|G℘G|D —∘G|∃xG|∀xG.

with queries having the form Γ ⊢ Δ where Γ is a multiset of resources and Δ is a multiset of goals. This language is motivated by expressiveness potentialities [10] and we have to study the proof search methods connected with it.

2) The logical analysis

The set of rules that are used for the proof development in the given logic programming language is

R_{0} = { —∘_{L}, ⊗_{R}, ⊗_{L},—∘_{R}, ℘_{R}, &_{R}, &_{L}, ⊕_{R},!_{L}, w!_{L}, c!_{L}, ∀_{R}, ∀_{L}, ∃_{R}}

Thus, we can study how to normalize these proofs to obtain proof classes adapted to automated deduction by studying at first the permutability properties of the R_{0} rules (see Fig.1).

From these results and an analysis of non-determinism reduction, we are able to determinate the set of inferences I_{↓} = {℘_{R}, —∘_{R}, &_{R}, ∀_{R}, c!_{L}, ⊗_{L}} to move down and the set of inferences I_{↑} = { —∘_{L}, &_{L},!_{L}, w!_{L}, ∀_{L}, ⊗_{R}, ⊕_{R}, ∃_{R}} to move up. Thus, we can organize the inference movements in a proof with a view to defining specific classes of proofs, called canonical proofs, having in mind that a goal-oriented approach is fixed.

3) Canonical proofs design

We can determine different possibilities to define the more adapted subclasses of proofs for efficient goal-oriented search. In the proposal of [9], the choice is to move

R_{0} —∘_{L} ⊗_{R} ⊗_{L} —∘_{R} ℘_{R} &_{R} &_{L} ⊕_{R} !_{L} w!_{L} c!_{L} ∀_{R} ∀_{L} ∃_{R}
—∘_{L} p p p p p p p p p p p p p p
⊗_{R} p p p p p p p p p p p p p p
⊗_{L} np npr p p p p p p p p p p p p
—∘_{R} np np p p p p p p p p p p p p
℘_{R} np np p p p p p p p p p p p p
&_{R} np np np np np np np np np np np np np np
&_{L} p p p p p p p p p p p p p p
⊕_{R} p p p p p p p p p p p p p p
!_{L} p p p p p p p p p p p p p p
w!_{L} p p p p p p p p p p p p p p
c!_{L} np npr p p p p p p p p p p p p
∀_{R} p p p p p p p p p p p p np np
∀_{L} p p p p p p p p p p p p p p
∃_{R} p p p p p p p p p p p p p p

Fig. 1. Permutability properties

the right rules as upwards as possible. We can observe that, in this fragment, it is impossible to have proofs where the left inferences completely precede the right ones. There are two cases where a right rule in a permutation position, with the left rule that follows it, is not permutable: ⊗_{R} with ⊗_{L} and ⊗_{R} with c!_{L}. Moreover, we observe that a right rule immediately preceding the left rule —∘_{L} is not in permutation position. Moving the right rules at the maximum, we obtain what we call the locally LR proofs. Moreover, if we move up at the maximum the inferences of type —∘_{L} we obtain the simple proofs or uniform proofs. Consequently, these proof forms are only instances of canonical proofs we can define for this framework.

A point of discussion can be the actual necessity of the goal-oriented approach in this context and the possibilities to refine the existing or new proof strategies. Thus we have a general view about the possible extensions of logic programming based on Linear Logic, using other fragments with one or several conclusions, motivated by expressiveness and specification potentialities. We can apply these results to frameworks based on proof-construction as computation [12, 13]. Further work could be to consider transformation of linear logic programs through these results.

Remark. We can make a similar study of Hodas-Miller’s framework for the intuitionistic linear logic [12]. They propose weaker goal formulae than the previously defined ones but with a richer context and an adequate uniform proofs definition. The specific choice of this fragment has consequences on expressiveness and specification and resolution of problems. In [2] the approach is based on focusing proofs and Horn clauses so that the resulting language uses the multiple conclusion nature of LL.

4 Concluding remarks

This abstract focuses on a general and systematic approach to define canonical proof forms adequate for theorem proving and for linear logic programming languages. It allows to analyze the adequacy between a logic programming language issued from LL (motivated by expressiveness or concurrency aspects) and efficient and complete proof search or proof construction procedures. Thus, we can discuss about what is actually specific to linear logic programming and propose, from these results, improvements for more efficient implementations. Moreover, we can consider a linear logic programming framework as ACL [13] where computation is described in terms of proof construction and use the previous results not only for constructing proofs but mainly for the analysis, synthesis and transformations of concurrent programs.

References

1. S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3–58, 1993.

2. J.M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

3. D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver ’92, Logical Foundations of Computer Science Symposium, LNCS 620, pages 151–162, Tver, Russia, July 1992.

4. D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42–53, St. Petersburg, Russia, July 1992.

5. D. Galmiche and G. Perrier. On proof normalisation in linear logic. Research report 93-R-059, CRIN-CNRS, 1993. To appear in Theoretical Computer Science.

6. D. Galmiche and G. Perrier. Foundations of proof search strategies design in linear logic. In Logic at St Petersburg ’94, Symposium on Logical Foundations of Computer Science, to appear in LNCS, St Petersburg, Russia, July 1994.

7. J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

8. J. Harland. A proof-theoretic analysis of goal-directed provability. Journal of Logic and Computation, 4(1):69–88, 1994.

9. J. Harland and D. Pym. The uniform proof-theoretic foundation of linear logic programming. In International Symposium on Logic Programming, MIT Press, pages 304–318, San Diego, October 1991.

10. J. Harland and D. Pym. On resolution in fragments of classical linear logic. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 30–41, St. Petersburg, Russia, July 1992.

11. J. Harland and D. Pym. A synopsis on the identification of linear logic programming languages. LFCS Report Series ECS-LFCS-92-248, LFCS, University of Edinburg, November 1992.

12. J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

13. N. Kobayashi and A. Yonezawa. Acl - a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.

14. P. Lincoln and N. Shankar. Proof search in first-order linear logic and other cut-free sequent calculi. In 9th IEEE Symposium on Logic in Computer Science, Paris, France, July 1994.

15. J. Meseguer and N. Marti-Oliet. From petri nets to linear logic. Math. Struct. in Comp. Science, 1:69–101, 1991.

16. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

17. T. Tammet. Proof search strategies in linear logic. Programming Methodology Group Report 70, Chalmers University Group, University of Göteborg, 1993.

18. L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.

A The Linear sequent calculus

The inference system we use is the classical linear sequent calculus where, a sequent is an expression Γ ⊢ Δ where Γ and Δ are multisets of linear formulae, i.e, formulae built on the linear primitives 0, 1, ⊥, ⊤, ()^{⊥}, ⊗, ℘, &, ⊕, ∀, ∃,?,!. For a complete presentation of this system we refer to [7].

1) \underline{Identity Group}

\overline{⊢ A, A^{⊥}} Id  \frac{Γ ⊢ A, Δ A, Λ ⊢ Θ}{Γ, Λ ⊢ Δ, Θ} cut

2) \underline{Structural Group}

\frac{Γ ⊢ Δ}{!A, Γ ⊢ Δ} !w_{L}  \frac{Γ ⊢ Δ}{Γ ⊢ Δ,?A} ?w_{R}  \frac{!A,!A, Γ ⊢ Δ}{!A, Γ ⊢ Δ} !c_{L}  \frac{Γ ⊢ Δ,?A,?A}{Γ ⊢ Δ,?A} ?c_{R}

3) \underline{Logical Group}

\frac{A, B, Γ ⊢ Δ}{A ⊗ B, Γ ⊢ Δ} ⊗_{L}  \frac{Γ ⊢ Δ, A Λ ⊢ Θ, B}{Γ, Λ ⊢ Δ, Θ, A ⊗ B} ⊗_{R}  \frac{A, Γ ⊢ Δ B, Λ ⊢ Θ}{A℘B, Γ, Λ ⊢ Δ, Θ} ℘_{L}  \frac{Γ ⊢ Δ, A, B}{Γ ⊢ Δ, A℘B} ℘_{R}
\overline{⊢ 1} 1_{R}  \frac{Γ ⊢ Δ}{1, Γ ⊢ Δ} 1_{L}  \overline{⊥⊢} ⊥_{L}  \frac{Γ ⊢ Δ}{Γ ⊢ ΔΓ, ⊥} ⊥_{R}

\frac{Γ ⊢ Δ, A B, Λ ⊢ Θ}{A —∘B, Γ, Λ ⊢ Δ, Θ} —∘_{L}  \frac{A, Γ ⊢ Δ, B}{Γ ⊢ Δ, A —∘B} —∘_{R}  \frac{Γ ⊢ Δ, A}{A^{⊥}, Γ ⊢ Δ} ⊥_{L}  \frac{A, Γ ⊢ Δ}{Γ ⊢ Δ, A^{⊥}} ⊥_{R}

\frac{A, Γ ⊢ Δ}{A&B, Γ ⊢ Δ} &_{L}  \frac{B, Γ ⊢ Δ}{A&B, Γ ⊢ Δ} &_{L}  \frac{Γ ⊢ Δ, A Γ ⊢ ΔB}{Γ ⊢ Δ, A&B} &_{R}  \frac{A, Γ ⊢ Δ B, Γ ⊢ Δ}{A ⊕ B, Γ ⊢ Δ} ⊕_{L}
\frac{Γ ⊢ Δ, A}{Γ ⊢ Δ, A ⊕ B} ⊕_{R}  \frac{Γ ⊢ Δ, B}{Γ ⊢ Δ, A ⊕ B} ⊕_{R}  \overline{Γ ⊢ Δ, ⊤} ⊤_{R}  \overline{0, Γ ⊢ Δ} 0_{L}

\frac{A, Γ ⊢ Δ}{!A, Γ ⊢ Δ} !_{L}  \frac{!Γ ⊢ A,?Δ}{!Γ ⊢!A,?Δ} !_{R}  \frac{!Γ, A ⊢?Δ}{!Γ,?A ⊢?Δ} ?_{L}  \frac{Γ ⊢ Δ, A}{Γ ⊢ Δ,?A} ?_{R}

\frac{A[t/x], Γ ⊢ Δ}{∀xA, Γ ⊢ Δ} ∀_{L}  \frac{Γ ⊢ Δ, A}{Γ ⊢ Δ, ∀xA} ∀_{R}  \frac{A, Γ ⊢ Δ}{∃xA, Γ ⊢ Δ} ∃_{L}  \frac{Γ ⊢ Δ, A[t/x]}{Γ ⊢ Δ, ∃xA} ∃_{R}