Forum: A Multiple-Conclusion Specification Logic

Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA

                dale@saul.cis.upenn.edu
            http://www.cis.upenn.edu/∼dale

Draft: January 3, 1996

Abstract

The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, λProlog and its linear logic refinement, Lolli [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Linear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logic programming presentation of all of linear logic that modularly extends λProlog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a programming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the objectlanguages specified in Forum.

This paper will appear in Theoretical Computer Science.

1 Introduction

In [25] a proof theoretic foundation for logic programming was proposed in which logic programs are collections of formulas used to specify the meaning of non-logical constants and computation is identified with goal-directed search for proofs. Using the sequent calculus, this can be formalized by having the sequent Σ : Δ ⟶ G denote the state of an idealized logic programming interpreter, where the current set of non-logical constants (the signature) is Σ, the current logic program is the set of formulas Δ, and the formula to be established, called the query or goal, is G. (We assume that all the non-logical constants in G and in the formulas of Δ are contained in Σ.) A goal-directed or uniform proof is then a cut-free proof in which every occurrence of a sequent whose right-hand side is non-atomic is the conclusion of a right-introduction rule. The bottom-up search for uniform proofs is goal-directed to the extent that if the goal has a logical connective as its head, that occurrence of that connective must be introduced: the left-hand side of a sequent is only considered when the goal is atomic. A logic programming language is then a logical system for which uniform proofs are complete. The logics underlying Prolog, λProlog, and Lolli [15] satisfy such a completeness result.

The description of logic programming above is based on single-conclusion sequents: that is, on the right of the sequent arrow in Σ : Δ ⟶ G is a single formula. This leaves open the question of how to define logic programming in the more general setting where sequents may have multiple formulas on the right-hand side [8]. When extending this notion of goal-directed search to multiple-conclusion sequents, the following problem is encountered: if the righthand side of a sequent contains two or more non-atomic formulas, how should the logical connectives at the head of those formulas be introduced? There seems to be two choices. One choice simply requires that one of the possible introductions be done [12]. This choice has the disadvantage that there might be interdependencies between right-introduction rules: thus, the meaning of the logical connectives in the goal would not be reflected directly and simply into the structure of a proof, a fact that complicates the operational semantics of the logic as a programming language. A second choice requires that all possible introductions on the right can be done simultaneously. Although the sequent calculus cannot deal directly with simultaneous rule application, reference to permutabilities of inference rules [16] can indirectly address simultaneity. That is, we can require that if two or more right-introduction rules can be used to derive a given sequent, then all possible orders of applying those right-introduction rules can, in fact, be done and the resulting proofs are all equal modulo permutations of introduction rules. This approach, which makes the operational interpretation of specifications simple and natural, is used in this paper.

We employ the logical connectives of Girard [9] (typeset as in that paper) and the quantification and term structures of Church’s Simple Theory of Types [6]. A signature Σ is a finite set of pairs, written c : τ, where c is a token and τ is a simple type (over some fixed set of base types). We assume that a given token is declared at most one type in a given signature. A closed, simply typed λ-term t is a Σ-term if all the non-logical constants in t are declared types in Σ. The base type o is used to denote formulas, and the various logical constants are given types over o. For example, the binary logical connectives have the type o → o → o and the quantifiers ∀_{τ} and ∃_{τ} have the type (τ → o) → o, for any type τ. Expressions of the form ∀_{τ} λx.B and ∃_{τ} λx.B will be written more simply as ∀_{τ} x.B and ∃_{τ} x.B, or as ∀x.B and ∃x.B when the type τ is either unimportant or can be inferred from context. A Σ-term B of type o is also called a Σ-formula. In addition to the usual connectives present in linear logic, we also add the infix symbol ⇒ to denote intuitionistic implication; that is, B ⇒ C is equivalent to ! B −∘ C. The expression B ≡ C abbreviates the formula (B −∘ C) & (C −∘ B): if this formula is provable in linear logic, we say that B and C are logically equivalent.

In the next section, the design of Forum is motivated by considering how to modularly extend certain logic programming languages that have been designed following proof theoretic considerations. In Section 3, Forum is shown to be a logic programming language using the multiple conclusion generalization of uniform proofs. The operational semantics of Forum is described in Section 4 so that the examples in the rest of the paper can be understood from a programming point-of-view as well as the declarative point-of-view. Sequent calculus proof systems for some object-level logics are specified in Section 5, and various imperative and concurrency features of a object-level programming language are specified and analyzed in Sections 6 and 7.

Although Forum extends some existing logic programming languages based on linear logic, there have been other linear logic programming languages proposed that it does not extend or otherwise relate directly. In particular, the language ACL by Kobayashi and Yonezawa [17, 18] captures simple notions of asynchronous communication by identifying the send and read primitives with two complementary linear logic connectives. Also, Lincoln and Saraswat have developed a linear logic version of concurrent constraint programming and used linear logic connectives to extend previous languages in this paradigm [19, 32].

2 Design issues

The following generalization of the definition of uniform proof was introduced in [23] where it was shown that a certain logic specification inspired by the π-calculus [27] can be seen as a logic program.

Definition 1 A cut-free sequent proof Ξ is uniform if for every subproof Ξ′ of Ξ and for every non-atomic formula occurrence B in the right-hand side of the end-sequent of Ξ′, there is a proof Ξ′′ that is equal to Ξ′ up to a permutation of inference rules and is such that the last inference rule in Ξ′′ introduces the top-level logical connective of B.

Definition 2 A logic with a sequent calculus proof system is an abstract logic programming language if restricting to uniform proofs does not lose completeness.

Below are several examples of abstract logic programming languages.

• Horn clauses, the logical foundation of Prolog, are formulas of the form ∀x̄(G ⇒ A) where G may contain occurrences of & and ⊤. (We shall use x̄ as a syntactic variable ranging over a list of variables and A as a syntactic variables ranging over atomic formulas.) In such formulas, occurrences of ⇒ and ∀ are restricted so that they do not occur to the left of the implication ⇒. As a result of this restriction, uniform proofs involving Horn clauses do not contain right-introduction rules for ⇒ and ∀.

• Hereditary Harrop formulas [25], the logical foundation of λProlog, result from removing the restriction on ⇒ and ∀ in Horn clauses: that is, such formulas can be built freely from ⊤, &, ⇒, and ∀. Some presentations of hereditary Harrop formulas and Horn clauses allow certain occurrences of disjunctions (⊕) and existential quantifiers [25]: since such occurrences do not add much to the expressiveness of these languages (as we shall see at the end of this section), they are not considered directly here.

• The logic at the foundation of Lolli is the result of adding −∘ to the connectives present in hereditary Harrop formulas: that is, Lolli programs are freely built from ⊤, &, −∘, ⇒, and ∀. As with hereditary Harrop formulas, it is possible to also allow certain occurrences of ⊕ and ∃, as well as the tensor ⊗ and the modal !.

• The formulas used in LO are of the form ∀x̄(G −∘ A_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{n}) where n ≥ 1 and G may contain occurrences of &, ⊤, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊥. Similar to the Horn clause case, occurrences of −∘ and ∀ are restricted so that they do not occur to the left of the implication −∘.

The reason that Lolli does not include LO is the presence of ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and ⊥ in the latter. This suggests the following definition for Forum, the intended superlanguage: allow formulas to be freely generated from ⊤, &, ⊥, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , −∘, ⇒, and ∀. For various reasons, it is also desirable to add the modal ? directly to this list of connectives. Clearly, Forum contains the formulas in all the above logic programming languages.

Since the logics underlying Prolog, λProlog, Lolli, LO, and Forum differ in what logical connectives are allowed, richer languages modularly contain weaker languages. This is a direct result of the cut-elimination theorem for linear logic. Thus a Forum program that does not happen to use ⊥, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , −∘, and ? will, in fact, have the same uniform proofs as are described for λProlog. Similarly, a program containing just a few occurrences of these connectives can be understood as a λProlog program that takes a few exceptional steps, but otherwise behaves as a λProlog program.

Forum is a presentation of all of linear logic since it contains a complete set of connectives. The connectives missing from Forum are directly definable using the following logical equivalences.

B^{⊥} ≡ B −∘ ⊥  0 ≡ ⊤ −∘ ⊥  1 ≡ ⊥ −∘ ⊥
! B ≡ (B ⇒ ⊥) −∘ ⊥  B ⊕ C ≡ (B^{⊥} & C^{⊥})^{⊥}  B ⊗ C ≡ (B^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥})^{⊥}
∃x.B ≡ (∀x.B^{⊥})^{⊥}

The collection of connectives in Forum are not minimal. For example, ? and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , can be defined in terms of the remaining connectives.

? B ≡ (B −∘ ⊥) ⇒ ⊥ and B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C ≡ (B −∘ ⊥) −∘ C

The other logic programming languages we have mentioned can, of course, capture the expressiveness of full logic by introducing non-logical constants and programs to describe their meaning. Felty in [7] uses a meta-logical presentation to specify full logic at the object-level. Andreoli [1] provides a “compilationlike” translation of linear logic into LinLog (of which LO is a subset). Forum has a more immediate relationship to all of linear logic since no non-logical symbols need to be used to provide complete coverage of linear logic. Of course, to achieve this complete coverage, many of the logical connectives of linear logic are encoded using negations (more precisely, using “implies bottom”), a fact that causes certain operational problems, as we shall see in Section 4.

As a presentation of linear logic, Forum may appear rather strange since it uses neither the cut rule (uniform proofs are cut-free) nor the dualities that follow from uses of negation (since negation is not a primitive). The execution of a Forum program (in the logic programming sense of the search for a proof) makes no use of cut or of the basic dualities. These aspects of linear logic, however, are important in meta-level arguments about specifications written in Forum. In Sections 5 and 6 we show some examples of how linear logic’s negation and cut-elimination theorem can be used to reason about Forum specifications.

The choice of these primitives for this presentation of linear logic makes it possible to keep close to the usual computational significance of backchaining, and the presence of the two implications, −∘ and ⇒, makes the specification of object-level inference rules natural. For example, the proof figure

(A) ; ⋮ ; B C ; D

Can be written at the meta-level using implications such as (A ⇒ B) −∘ C −∘ D. Since we intend to use Forum as a specification language for type checking rules, structured operational semantics, and proof systems, the presence of implications as primitives is desirable.

The logical equivalences

1 −∘ H ≡  H
1 ⇒ H ≡  H
(B ⊗ C) −∘ H ≡  B −∘ C −∘ H
B^{⊥} −∘ H ≡  B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} H
B^{⊥} ⇒ H ≡  ? B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} H
! B −∘ H ≡  B ⇒ H
! B ⇒ H ≡  B ⇒ H
(B ⊕ C) −∘ H ≡ (B −∘ H) & (C −∘ H)
(∃x.B(x)) −∘ H ≡  ∀x.(B(x) −∘ H)

can be used to remove certain occurrences of ⊗, ⊕, ∃, !, and 1 when they occur to the left of implications. (In the last equivalence above, assume that x is not free in H.) These equivalences are more direct than those that employ the equivalences mentioned earlier that use negation via the “implies bottom” construction. As a result, we shall allow their use in Forum specifications and employ these equivalences to remove them when necessary.

Formulas of the form

∀ȳ(G_{1} ↪ ⋯ ↪ G_{m} ↪ (A_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{p})), (m, p ≥ 0)

where G_{1}, … G_{m} are arbitrary Forum formulas and A_{1}, … A_{m} are atomic formulas, are called clauses. Here, occurrences of ↪ are either occurrences of −∘ or ⇒. An empty ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (p = 0) is written as ⊥. The formula A_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{p} is the head of such a clause. If p = 0 then we say that this clause has an empty head. The formulas of LinLog [1] are essentially clauses in which p > 0 and the formula G_{1}, …, G_{m} do not contain −∘ and ⇒ and where ? has only atomic scope.

3 Proof Search

In this section we consider the abstract character of cut-free proofs over the connectives of Forum. Let L_{1} be the set of all formulas over the logical connectives ⊥, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊤, &, −∘, ⇒, ?, and ∀. If C is a set or multiset of formulas, the notation ! C denotes the corresponding set or multiset that results from placing ! on each of the formula occurrences in C: the notation ? C is defined similarly.

Let F be the sequent proof system given in Figure 1. In this proof system, sequents have the form

Σ: Ψ; Δ ⟶ Γ; Υ and Σ: Ψ; Δ ⟶^{B} Γ; Υ,

where Σ is a signature, Δ is a multiset of formulas, Γ is a list of formulas, Ψ and Υ are sets of formulas, and B is a formula. All of these formulas are from L_{1} and are also Σ-formulas. (The introduction of signatures into sequents is not strictly necessary but is desirable when this proof system is used for logic programming specifications [22].) The intended meanings of these two sequents in linear logic are

! Ψ, Δ ⟶ Γ,? Υ and ! Ψ, Δ, B ⟶ Γ,? Υ,

respectively. In the proof system of Figure 1, the only right rules are those for sequents of the form Σ: Ψ; Δ ⟶ Γ; Υ. In fact, the only formula in Γ that can be introduced is the left-most, non-atomic formula in Γ. This style of selection is specified by using the syntactic variable A to denote a list of atomic formulas. Thus, the right-hand side of a sequent matches A, B & C, Γ if it contains a formula that is a top-level & for which at most atomic formulas can occur to its left. Both A and Γ may be empty. Left rules are applied only to the formula B that labels the sequent arrow in Σ: Ψ; Δ ⟶^{B} A; Υ. The notation A_{1} + A_{2} matches a list A if A_{1} and A_{2} are lists that can be interleaved to yield A: that is, the order of members in A_{1} and A_{2} is as in A, and (ignoring the order of elements) A denotes the multiset set union of the multisets represented by A_{1} and A_{2}.

As in Church’s Simple Theory of Types, we assume the usual rules of α, β, and η-conversion and we identify terms up to α-conversion. A term is λ-normal if it contains no β and no η redexes. All terms are λ-convertible to a term in λ-normal form, and such a term is unique up to α-conversion. All formulas in sequents are in λ-normal form: in particular, the notation B[t/x], used in ∀L and ∀R, denotes the λ-normal form of the β-redex (λx.B)t.

We use the turnstile symbol as the mathematics-level judgment that a sequent is provable: that is, Δ ⊢ Γ means that the two-sided sequent Δ ⟶ Γ has a linear logic proof. The sequents of F are similar to those used in the LU proof system of Girard [10] except that we have followed the tradition of [1, 14] in writing the “classical” context (here, Ψ and Υ) on the outside of the sequent and the “linear” context (here, Δ and Γ) nearest the sequent arrow: in LU these conventions are reversed.

Given the intended interpretation of sequents in F, the following soundness theorem can be proved by simple induction on the structure of F proofs.

Theorem 1 (Soundness) If the sequent Σ: Ψ; Δ ⟶ Γ; Υ has an F proof then ! Ψ, Δ ⊢ Γ,? Υ. If the sequent Σ: Ψ; Δ ⟶^{B} A; Υ has an F proof then ! Ψ, Δ, B ⊢ Γ,? Υ.

Completeness of the F proof system is a more difficult matter, largely because proofs can be built only in a greatly constrained fashion. In sequent proof systems generally, left and right introduction rules can be interleaved, where as,

\overline{Σ: Ψ; Δ ⟶ A, ⊤, Γ; Υ} ⊤R

\frac{Σ: Ψ; Δ ⟶ A, B, Γ; Υ Σ: Ψ; Δ ⟶ A, C, Γ; Υ}{Σ: Ψ; Δ ⟶ A, B & C, Γ; Υ} & R

\frac{Σ: Ψ; Δ ⟶ A, Γ; Υ}{Σ: Ψ; Δ ⟶ A, ⊥, Γ; Υ} ⊥R \frac{Σ: Ψ; Δ ⟶ A, B, C, Γ; Υ}{Σ: Ψ; Δ ⟶ A, B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C, Γ; Υ} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} R

\frac{Σ: Ψ; B, Δ ⟶ A, C, Γ; Υ}{Σ: Ψ; Δ ⟶ A, B −∘ C, Γ; Υ} −∘ R \frac{Σ: B, Ψ; Δ ⟶ A, C, Γ; Υ}{Σ: Ψ; Δ ⟶ A, B ⇒ C, Γ; Υ} ⇒ R

\frac{y: τ, Σ: Ψ; Δ ⟶ A, B[y/x], Γ; Υ}{Σ: Ψ; Δ ⟶ A, ∀_{τ} x.B, Γ; Υ} ∀R \frac{Σ: Ψ; Δ ⟶ A, Γ; B, Υ}{Σ: Ψ; Δ ⟶ A,? B, Γ; Υ} ? R

\frac{Σ: B, Ψ; Δ ⟶^{B} A; Υ}{Σ: B, Ψ; Δ ⟶ A; Υ} decide! \frac{Σ: Ψ; Δ ⟶ A, B; B, Υ}{Σ: Ψ; Δ ⟶ A; B, Υ} decide?

\frac{Σ: Ψ; Δ ⟶^{B} A; Υ}{Σ: Ψ; B, Δ ⟶ A; Υ} decide

\overline{Σ: Ψ; · ⟶^{A} A; Υ} initial \overline{Σ: Ψ; · ⟶^{A} ·; A, Υ} initial ?

\overline{Σ: Ψ; · ⟶^{⊥} ·; Υ} ⊥L  \frac{Σ: Ψ; Δ ⟶^{B_{i}} A; Υ}{Σ: Ψ; Δ ⟶^{B_{1}&B_{2}} A; Υ} & L_{i}  \frac{Σ: Ψ; B ⟶ ·; Υ}{Σ: Ψ; · ⟶^{? B} ·; Υ} ? L

\frac{Σ: Ψ; Δ_{1} ⟶^{B} A_{1}; Υ Σ: Ψ; Δ_{2} ⟶^{C} A_{2}; Υ}{Σ: Ψ; Δ_{1}, Δ_{2} ⟶^{B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C} A_{1} + A_{2}; Υ} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L \frac{Σ: Ψ; Δ ⟶^{B[t/x]} A; Υ}{Σ: Ψ; Δ ⟶^{∀_{τ} x.B} A; Υ} ∀L

\frac{Σ: Ψ; Δ_{1} ⟶ A_{1}, B; Υ Σ: Ψ; Δ_{2} ⟶^{C} A_{2}; Υ}{Σ: Ψ; Δ_{1}, Δ_{2} ⟶^{B−∘C} A_{1} + A_{2}; Υ} −∘ L

\frac{Σ: Ψ; · ⟶ B; Υ Σ: Ψ; Δ ⟶^{C} A; Υ}{Σ: Ψ; Δ ⟶^{B⇒C} A; Υ} ⇒ L

Figure 1: The F proof system. The rule ∀R has the proviso that y is not declared in the signature Σ, and the rule ∀L has the proviso that t is a Σ-term of type τ. In &L_{i}, i = 1 or i = 2. in F, occurrences of introduction rules are constrained so that (reading from the bottom up) right rules are used entirely until the linear part of the right-hand side (Γ) is decomposed to only atoms, and it is only when the right-hand side is a list of atoms that left introduction rules are applied. Completeness of F can be proved by showing that any proof in linear logic can be converted to a proof in F by permuting enough inference rules. Since there are many opportunities for such permutations, such a completeness proof has many cases. Fortunately, Andreoli has provided a nice packaging of the permutation aspects of linear logic within a single proof system [1]. We show that the F proof system is simply a variation of the proof system he provided.

Let L_{2} be the set of formulas all of whose logical connectives are from the list ⊥, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊤, &, ?, ∀ (those used in L_{1} minus the two implications) along with the duals of these connectives, namely, 1, ⊗, 0, ⊕, !, and ∃. Negations of atomic formulas are also allowed, and we write B^{⊥}, for non-atomic formula B, to denote the formula that results from giving negations atomic scope using the de Morgan dualities of linear logic. A formula is asynchronous if it has a top-level logical connective that is either ⊥, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊤, &, ?, or ∀, and is synchronous if it has a top-level logical connective that is either 1, ⊗, 0, ⊕, !, and ∃. Figure 2 contains the J proof system. Andreoli showed in [1] that this proof system is complete for linear logic. Although he proved this only for the first-order fragment of linear logic, it lifts to the higher-order case we are considering given Girard’s proof of cut-elimination for full, higher-order linear logic [9].

The following theorem shows that the F and J proof systems are similar, and in this way, the completeness for F is established. Before proving the completeness of F we state the following technical result used in the completeness theorem.

Lemma 2 Let A and A′ be lists of atoms that are permutations of each other. If the sequent Σ: Ψ; Δ ⟶ A, Γ; Υ has an F proof then so too does Σ: Ψ; Δ ⟶ A′, Γ; Υ. Similarly, if the sequent Σ: Ψ; Δ ⟶^{B} A; Υ has an F proof then so too does Σ: Ψ; Δ ⟶^{B} A′; Υ.

Proof Completed by induction on the structure of proofs in F.

Theorem 3 (Completeness) Let Σ be a signature, Δ be a multiset of L_{1} Σformulas, Γ be a list of L_{1} Σ-formulas, and Ψ and Υ be sets of L_{1} Σ-formulas. If ! Ψ, Δ ⊢ Γ,? Υ then the sequent Σ: Ψ; Δ ⟶ Γ; Υ has a proof in F.

Proof Assume that ! Ψ, Δ ⊢ Γ,? Υ. The main result of [1], extended to the higher-order case, implies that the sequent Σ: Ψ^{⊥}, Υ; Δ^{⊥} ⇑ Γ has a J proof. We now show how to convert such a proof into a proof of F.

When B is an L_{1} formula, we define B^{0} to be the L_{2} formula that results from replacing subformulas of B of the form C −∘ D with C^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D and of the form C ⇒ D with ? C^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D. The formula B^{0} is either asynchronous or atomic

\frac{Σ: Ψ; Δ ⇑ L}{Σ: Ψ; Δ ⇑ ⊥, L} [⊥]  \frac{Σ: Ψ; Δ ⇑ F, G, L}{Σ: Ψ; Δ ⇑ F ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G, L} [^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ]  \frac{Σ: Ψ, F; Δ ⇑ L}{Σ: Ψ; Δ ⇑ ? F, L} [?]

\overline{Σ: Ψ; Δ ⇑ ⊤, L} [⊤] \frac{Σ: Ψ; Δ ⇑ F, L Σ: Ψ; Δ ⇑ G, L}{Σ: Ψ; Δ ⇑ F & G, L} [&]

\frac{y : τ, Σ: Ψ; Δ ⇑ B[y/x], L}{Σ: Ψ; Δ ⇑ ∀_{τ} x.B, L} [∀] \overline{Σ: Ψ; · ⇓ 1} [1]

\frac{Σ: Ψ; Δ_{1} ⇓ F Σ: Ψ; Δ_{2} ⇓ G}{Σ: Ψ; Δ_{1}, Δ_{2} ⇓ F ⊗ G} [⊗] \frac{Σ: Ψ; · ⇑ F}{Σ: Ψ; · ⇓ ! F} [!]

\frac{Σ: Ψ; Δ ⇓ F_{i}}{Σ: Ψ; Δ ⇓ F_{1} ⊕ F_{2}} [⊕_{i}] \frac{Σ: Ψ; Δ ⇓ B[t/x]}{Σ: Ψ; Δ ⇓ ∃_{τ} x.B} [∃]

\frac{Σ: Ψ; Δ, F ⇑ L}{Σ: Ψ; Δ ⇑ F, L} [R ⇑] provided that F is not asynchronous

\frac{Σ: Ψ; Δ ⇑ F}{Σ: Ψ; Δ ⇓ F} [R ⇓] provided that F is either asynchronous or an atom

\overline{Σ: Ψ; A ⇓ A^{⊥}} [I_{1}] \overline{Σ: Ψ, A; · ⇓ A^{⊥}} [I_{2}]

\frac{Σ: Ψ; Δ ⇓ F}{Σ: Ψ; Δ, F ⇑ ·} [D_{1}] \frac{Σ: Ψ; Δ ⇓ F}{Σ: Ψ, F; Δ ⇑ ·} [D_{2}]

Figure 2: The J proof system. The rule [∀] has the proviso that y is not declared in Σ, and the rule [∃] has the proviso that t is a Σ-term of type τ. In [⊕_{i}], i = 1 or i = 2. while (B^{0})^{⊥} is either synchronous or the negation of an atom. Notice that if B^{0} is equal to E ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F, then there are formulas C and D of L_{1} so that D^{0} is F, and either B is C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D and E is C^{0}, B is C −∘ D and E is (C^{0})^{⊥}, or B is C ⇒ D and E is ?(C^{0})^{⊥}.

Let Ψ be a set of formulas of the form B^{0} and (B^{0})^{⊥}, where B is from L_{1}; let Δ be a multiset of formulas that are either atomic or of the form (B^{0})^{⊥}, where B is from L_{1}; let L be a list of formulas of the form B^{0}, where B is from L_{1}; and let F be (B^{0})^{⊥} where B is an L_{1} formula. Given these restrictions on Ψ and Δ, we define the following pair of functions on sets of such formulas:

[Ψ]_{−} = {B | (B^{0})^{⊥} ∈ Ψ} [Ψ]_{+} = {B | B^{0} ∈ Ψ}.

Clearly the resulting sets are sets of L_{1} formulas. We similarly define [Δ]_{−} to be the corresponding multiset of L_{1}. The corresponding value for [Δ]_{+} would be a multiset of atomic formulas, but in the proof below, we need to consider [Δ]_{+} to be a list, which is the underlying multiset put in some arbitrary but fixed order. We now prove by mutual induction on the heights of J proofs the following two facts.

• If Σ: Ψ; Δ ⇑ L has a J proof then Σ: [Ψ]_{−}; [Δ]_{−} ⟶ [Δ]_{+}, L; [Ψ]_{+} has an F proof.

• If Σ: Ψ; Δ ⇓ (B^{0})^{⊥} has a J proof then Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{B} [Δ]_{+}; [Ψ]_{+} has an F proof.

Consider the possible last rules in the proofs of Σ: Ψ; Δ ⇑ L and Σ: Ψ; Δ ⇓ (B^{0})^{⊥}.

Case: [⊤]. In this case, L has ⊤ as its first element. Thus the corresponding F proof is ⊤R.

Case: [1]. In this case, B is ⊥ and Δ is empty, and the corresponding F proof is ⊥L.

Case: [I_{1}]. Thus B is the atomic formula A and Δ is the multiset containing just one occurrence of A. The corresponding F proof is initial.

Case: [I_{2}]. Thus B is the atomic formula A, Δ is the empty multiset, and Ψ is a set containing A. The corresponding F proof is initial?.

Case: [⊥]. In this case, the corresponding F proof is built using ⊥R.

Case: [^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ]. In this case, L is a list with head E ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F and tail L′. Let B be the L_{1} formula so that B^{0} is E ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F. There are three subcases to consider depending on structure of B.

Subcase: B is C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D and E is C^{0}. In this case, the corresponding J

proof is built using ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} R.

Subcase: B is C −∘ D and E is (C^{0})^{⊥}. In this case,

Σ: Ψ; Δ ⇑ (C^{0})^{⊥}, D^{0}, L′

has a smaller proof. However, the only inference rule that can yield this sequent as a conclusion is [R ⇑]. Thus, Σ: Ψ; Δ, (C^{0})^{⊥} ⇑ D^{0}, L′ has a smaller J proof. Using the inductive hypothesis and the −∘R rule provides the desired F proof.

Subcase: B is C ⇒ D and E is ?(C^{0})^{⊥}. In this case,

Σ: Ψ; Δ ⇑ ?(C^{0})^{⊥}, D^{0}, L′

has a smaller proof. However, the only inference rule that can yield this sequent as a conclusion is [?]. Thus, Σ: Ψ, (C^{0})^{⊥}; Δ ⇑ D^{0}, L′ has a smaller J proof. Using the inductive hypothesis and the ⇒R rule provides the desired F proof.

Case: [?]. In this case, the list L is of the form ?(B^{0}), L′ for some B in L_{1} and the sequent Σ: Ψ, B^{0}; Δ ⇑ L′ has a smaller J proof. By the inductive hypothesis, we have that the sequent Σ: [Ψ]_{−}; Δ^{⊥} ⟶ [Δ]_{+}, L; B, [Ψ]_{+} is provable in F and by using ?R we can obtain a proof of the desired F proof.

Case: [!]. In this case, B is a formula of the form ? C and the sequent Σ: Ψ; Δ ⇓ (C^{0})^{⊥} is provable in J. But the only way this can be proved is by the [R ⇓], so the sequent Σ: Ψ; (C^{0})^{⊥} ⇑ · has a smaller J proof. By the inductive hypothesis, we have that the sequent Σ: [Ψ]_{−}; C ⟶ ·; [Ψ]_{+} is provable in F. Now using ?L, we have the desired F proof.

Case: [R ⇓]. Not possible.

Case: [&] and [∀]. A simple use of induction and the &R and ∀R rules yield the desired F proofs.

Case: [⊗]. In this case, B is either of the form C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D, C −∘ D, or C ⇒ D.

Subcase: B is C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D. In this case, the proof of Σ: Ψ; Δ ⇓ (C^{0})^{⊥}⊗(D^{0})^{⊥} has immediate subproofs of Σ: Ψ; Δ_{1} ⇓ (C^{0})^{⊥} and Σ: Ψ; Δ_{2} ⇓ (D^{0})^{⊥} where Δ is the multiset union of Δ_{1} and Δ_{2}. The inductive hypothesis provides us with proofs of the sequents

Σ: [Ψ]_{−}; [Δ_{1}]_{−} ⟶^{C} [Δ_{1}]_{+}; [Ψ]_{+} and Σ: [Ψ]_{−}; [Δ_{2}]_{−} ⟶^{D} [Δ_{2}]_{+}; [Ψ]_{+}.

Using^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L we obtain a proof of the sequent Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{C^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D} [Δ_{1}]_{+}+

[Δ_{2}]_{+}; [Ψ]_{+}. It might not be the case that the list [Δ_{1}]_{+} + [Δ_{2}]_{+} is the same list as [Δ]_{+} (remember the ordering here was arbitrary and fixed), so we might need to use Lemma 2 to finally obtain a proof of

Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{C^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D} [Δ]_{+}; [Ψ]_{+}.

Subcase: B is C −∘ D. In this case, the proof of Σ: Ψ; Δ ⇓ C^{0} ⊗ (D^{0})^{⊥} has immediate subproofs of Σ: Ψ; Δ_{1} ⇓ C^{0} and Σ: Ψ; Δ_{2} ⇓ (D^{0})^{⊥} where Δ is the multiset union of Δ_{1} and Δ_{2}. Since C^{0} is either asynchronous or atomic, the only inference rule that yields the first of these sequents is [R ⇓]. Thus the sequent Σ: Ψ; Δ_{1} ⇑ C^{0} has a smaller proof. Using the inductive hypotheses, we conclude that sequents

Σ: [Ψ]_{−}; [Δ_{1}]_{−} ⟶ [Δ_{1}]_{+}, C; [Ψ]_{+}

and

Σ: [Ψ]_{−}; [Δ_{2}]_{−} ⟶^{D} [Δ_{2}]_{+}; [Ψ]_{+}

have F proofs. Using −∘L we obtain a proof of the sequent

Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{C−∘D} [Δ_{1}]_{+} + [Δ_{2}]_{+}; [Ψ]_{+}.

As above, it might not be the case that the list [Δ_{1}]_{+} + [Δ_{2}]_{+} is the same list as [Δ]_{+}, so we might need to use Lemma 2 to finally obtain a proof of Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{C−∘D} [Δ]_{+}; [Ψ]_{+}.

Subcase: B is C ⇒ D. In this case, the proof of Σ: Ψ; Δ ⇓ !(C^{0})⊗(D^{0})^{⊥} has immediate subproofs of Σ: Ψ; Δ_{1} ⇓ !(C^{0}) and Σ: Ψ; Δ_{2} ⇓ (D^{0})^{⊥} where Δ is the multiset union of Δ_{1} and Δ_{2}. The only inference rule that yields the first of these sequents is [!], and this is only possible only if Δ_{1} is empty and Δ_{2} is equal to Δ. Thus the sequent Σ: Ψ; · ⇑ C^{0} has a smaller proof. Using the inductive hypotheses, we conclude that Σ: [Ψ]_{−}; · ⟶ C; [Ψ]_{+} and Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{D} [Δ]_{+}; [Ψ]_{+}. Using ⇒L we obtain a proof of the sequent Σ: [Ψ]_{−}; [Δ]_{−} ⟶^{C⇒D} [Δ]_{+}; [Ψ]_{+}.

Case: [⊕_{i}]. This case follows using the inference rule &L_{i}.

Case: [∃]. This case follows using the inference rule ∀L.

Case: [R ⇑]. The list L must have the atomic formula A as its first element and L′ as its tail and the sequent Σ: Ψ; Δ, A ⇑ L′ has a shorter proof. By the inductive hypothesis we know that Σ: [Ψ]_{−}; [Δ]_{−} ⟶ [Δ, A]_{+}, L′; [Ψ]_{+} has an F proof and by using Lemma 2 we know that

Σ: [Ψ]_{−}; [Δ]_{−} ⟶ [Δ]_{+}, A, L′; [Ψ]_{+}

has an F proof.

Case: [D_{1}] and [D_{2}]. The [D_{1}] case follows immediately from the use of the inductive hypothesis and the decide inference rules. The [D_{2}] case follows immediately from the use of the inductive hypothesis and either the decide! or decide? inference rules.

This proof actually describes an algorithm for converting a J proof into a corresponding F proof. The corresponding proofs are nearly the same — just different connectives and different bookkeeping is involved.

The completeness of F immediately establishes Forum as an abstract logic programming language.

Notice that the form of the ?L rule is different from the other left introduction rules in that none of the sequents in its premise contain an arrow labeled with a formula. Thus, using this rule causes the “focus” of proof construction, which for left rules is directed by the subformulas of the formula labeling the sequent arrow, to be lost. If we were to replace that rule with the rule

\frac{Σ: Ψ; · ⟶^{B} ·; Υ}{Σ: Ψ; · ⟶^{? B} ·; Υ} ? L′

that keeps the “focus”, then the resulting proof system is not complete. In particular, the linear logic theorems ? a −∘? a and ? a −∘?((a −∘ b) −∘ b) would not be provable. Section 5 contains an occasion (Lemma 7) when using ? L′ instead of ?L is complete.

4 Operational reading of programs

We shall not discuss the many issues involved with building an interpreter or theorem prover for Forum. Certainly, work done on the implementations of languages such as λProlog, Lolli, and LO would all be applicable here. For now, we attempt to give the reader an understanding of what the high-level operational behavior of proof search is like using Forum specifications. Clearly, that semantics is an extension of these other logic programming languages, so we shall focus on those features that are novel to Forum and which are needed for the examples in the following sections.

First we comment on how the impermutabilities of some inference rules of linear logic are treated in Forum. In particular, an analogy exists between the embedding of all of linear logic into Forum and the embedding of classical logic into intuitionistic logic via a double negation translation. In classical logic, contraction and weakening can be used on both the left and right of the sequent arrow: in intuitionistic logic, they can only be used on the left. The familiar double negation translation of classical logic into intuitionistic logic makes it possible for the formula B^{⊥⊥} on the right to be moved to the left as B^{⊥}, where contractions and weakening can be applied to it, and then moved back to the right as B. In this way, classical reasoning can be regained indirectly. Similarly, in linear logic when there are, for example, non-permutable right-rules, one of the logical connectives involved can be rewritten so that the non-permutability is transferred to one between a left rule above a right rule. For example, the bottom-up construction of a proof of the sequent ⟶ a ⊗ b, a^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b^{⊥} must first introduce the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} prior to the ⊗: the context splitting required by ⊗ must be delayed until after the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} is introduced. This sequent, written using the connectives of Forum, is ⟶ (a^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b^{⊥}) −∘ ⊥, a^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b^{⊥}. In this case, −∘ and .^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} can be introduced in any order, giving rise to the sequent a^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b^{⊥} ⟶ a^{⊥}, b^{⊥}. Introducing the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} now causes the context to be split, but this occurs after the right-introduction of ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} . Thus, the encoding of some of the linear logic connectives into the set used by Forum essentially amounts to moving any “offending” non-permutabilities to where they are allowed.

We shall use the term backchaining to refer to an application of either the decide or the decide! inference rule followed by a series of applcations of leftintroduction rules. This notion of backchaining generalizes the usual notion found in the logic programming literature.

Sequents in linear logic and F contain multisets as (part of) their right-hand and left-hand sides. If we focus on the right-hand side, then the generalization of backchaining contained in the F proof system can be used to do multiset rewriting. As is well known, multiset rewriting is a natural setting for the specification of some aspects of concurrent computation. Given that multiset rewriting is only one aspect of the behavior of linear logic, such concurrent specifications are greatly enriched by the rest of higher-order linear logic. In particular, Forum allows for the integration of some concurrency primitives and various abstractions mechanisms in one declarative setting (see Section 6 for such an example specification).

To illustrate how multiset rewriting is specified in Forum, consider the clause

a ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b ∘− c ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e.

When presenting examples of Forum code we often use (as in this example) ∘− and ⇐ to be the converses of −∘ and ⇒ since they provide a more natural operational reading of clauses (similar to the use of :- in Prolog). Here, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} binds tighter than ∘− and ⇐. Consider the sequent Σ: Ψ; Δ ⟶ a, b, Γ; Υ where the above clause is a member of Ψ. A proof for this sequent can then look like the following.

Σ: Ψ; Δ ⟶ c, d, e, Γ; Υ
Σ: Ψ; Δ ⟶ c, d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e, Γ; Υ
Σ: Ψ; Δ ⟶ c ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e, Γ; Υ

Σ: Ψ; · ⟶^{a} a; Υ Σ: Ψ; · ⟶^{b} b; Υ

Σ: Ψ; · ⟶^{a^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b} a, b; Υ

Σ: Ψ; Δ ⟶^{c^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e−∘a^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b} a, b, Γ; Υ

Σ: Ψ; Δ ⟶ a, b, Γ; Υ

We can interpret this fragment of a proof as a reduction of the multiset a, b, Γ to the multiset c, d, e, Γ by backchaining on the clause displayed above.

Of course, a clause may have multiple, top-level implications. In this case, the surrounding context must be manipulated properly to prove the sub-goals that arise in backchaining. Consider a clause of the form

G_{1} −∘ G_{2} ⇒ G_{3} −∘ G_{4} ⇒ A_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{2}

labeling the sequent arrow in the sequent Σ: Ψ; Δ ⟶ A_{1}, A_{2}, A; Υ. An attempt to prove this sequent would then lead to attempt to prove the four sequents

Σ: Ψ; Δ_{1} ⟶ G_{1}, A_{1}; Υ Σ: Ψ; · ⟶ G_{2}; Υ
Σ: Ψ; Δ_{2} ⟶ G_{3}, A_{2}; Υ Σ: Ψ; · ⟶ G_{4}; Υ

where Δ is the multiset union of Δ_{1} and Δ_{2}, and A is A_{1} + A_{2}. In other words, those subgoals immediately to the left of an ⇒ are attempted with empty bounded contexts: the bounded contexts, here Δ and A, are divided up and used in attempts to prove those goals immediately to the left of −∘.

Although the innermost right-hand context of sequents in F is formally treated as a list, the order in the list is not “semantically” important: that list structure is only used to allow for a more constrained notion of proof search. It is easy to prove that a more general version of Lemma 2 holds.

Corollary 4 Let Γ and Γ′ be lists of formulas that are permutations of each other. If Σ: Ψ; Δ ⟶ Γ; Υ has an F proof then so too does Σ: Ψ; Δ ⟶ Γ′; Υ.

Proof This corollary can be proved by either referring to the soundness and completeness of F and the commutativity of ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} or showing that all rightintroduction rules in F permute over each other.

A particularly difficult aspect of Forum to imagine implementing directly is backchaining over clauses with empty heads. For example, consider attempting to prove a sequent with right-hand side A and with the clause ∀x̄(G−∘⊥) labeling the sequent arrow. This clause can be used in a backchaining step, regardless of A’s structure, yielding the new right-hand side A, θG, for some substitution θ over the variables x̄. Such a clause provides no overt clues as to when it can be effectively used to prove a given goal: backchaining using a clause with an empty head is always successful. See [21] for a discussion of a similar problem when negated clauses are allowed in logic programming based on minimal or intuitionistic logic. As we shall see in the next section, the specification of the cut rule for an object-level logic employs just such a clause: the well known problems of searching for proofs involving cut thus apply equally well to the search for F proofs involving such clauses. Also, the encoding of various linear logic connectives into Forum involve clauses with empty heads. (Notice that clauses with empty heads are not allowed in LO.)

5 Specifying object-level sequent proofs

Given the proof-theoretic motivations of Forum and its inclusion of quantification at higher-order types, it is not surprising that it can be used to specify proof systems for various object-level logics. Below we illustrate how sequent calculus proof systems can be specified using the multiple conclusion aspect of Forum and show how properties of linear logic can be used to infer properties of the object-level proof systems. We shall use the terms object-level logic and meta-level logic to distinguish between the logic whose proof system is being specified and the logic of Forum.

Consider the well known, two-sided sequent proof systems for classical, intuitionistic, minimal, and linear logic. The distinction between these logics can be described, in part, by where the structural rules of thinning and contraction can be applied. In classical logic, these structural rules are allowed on both sides of the sequent arrow; in intuitionistic logic, only thinning is allowed on the right of the sequent arrow; in minimal logic, no structural rules are allowed on the right of the sequent arrow; and in linear logic, they are not allowed on either side of the arrow. This suggests the following representation of sequents in these four systems. Let bool be the type of object-level propositional formulas and let left and right be two meta-level predicates of type bool → o. Sequents in these four logics can be specified as follows.

Linear: The sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (n, m ≥ 0) can be represented by the meta-level formula

left B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} left B_{n} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right C_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right C_{m}.

Minimal: The sequent B_{1}, …, B_{n} ⟶ C (n ≥ 0) can be represented by the meta-level formula

? left B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? left B_{n} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right C.

Intuitionistic: Intuitionistic logic contains the sequents of minimal logic and sequents with empty right-hand sides, i.e., of the form B_{1}, …, B_{n} ⟶, where n ≥ 0. These additional sequents can represented by the meta-level formula

? left B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? left B_{n}.

Classical: The sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (n, m ≥ 0) can be represented by the meta-level formula

? left B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? left B_{n} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? right C_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? right C_{m}.

The left and right predicates are used to identify which object-level formulas appear on which side of the sequent arrow, and the ? modal is used to mark the formulas to which weakening and contraction can be applied.

We shall focus only on an object-logic that is minimal in this section. To denote first-order object-level formulas, we introduce the binary, infix symbols ∧, ∨, and ⊃ of type bool → bool → bool, and the symbols ˆ∀ and ˆ∃ of type

(⊃ R)  right (A ⊃ B) ∘− (?(left A) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right B).
(⊃ L)  ?(left (A ⊃ B)) ∘− right A ∘− ?(left B).
(∧R)  right (A ∧ B) ∘− right A ∘− right B.
(∧L_{1})  ?(left (A ∧ B)) ∘− ?(left A).
(∧L_{2})  ?(left (A ∧ B)) ∘− ?(left B).
(ˆ∀R)  right (ˆ∀B) ∘− ∀x(right (Bx)).
(ˆ∀L)  ?(left (ˆ∀B)) ∘− ?(left (Bx)).
(Initial) right B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(left B).
(Cut)  ⊥ ∘− ?(left B) ∘− right B.

Figure 3: Specification of the LM_{1} sequent calculus.

(i → bool) → bool: the type i will be used to denote object-level individuals. Figure 3 is a specification of minimal logic provability using the above style of sequent encoding for just the connectives ∧, ⊃, and ˆ∀. (The connectives ∨ and ˆ∃ will be addressed later.) Expressions displayed as they are in Figure 3 are abbreviations for closed formulas: the intended formulas are those that result by applying ! to their universal closure. The operational reading of these clauses is quite natural. For example, the first clause in Figure 3 encodes the right-introduction of ⊃: operationally, an occurrence of A ⊃ B on the right is removed and replaced with an occurrence of B on the right and a (modalized) occurrence of A on the left (reading the right-introduction rule for ⊃ from the bottom). Notice that all occurrences of the left predicate in Figure 3 are in the scope of ?. If occurrences of such modals in the heads of clauses were dropped, it would be possible to prove meta-level goals that do not correspond to any minimal logic sequent: such goals could contain left-atoms that are not prefixed with the ? modal.

We say that the object-level sequent B_{0}, …, B_{n} ⟶ B has an LM_{1}-proof if it has one in the sense of Gentzen [8] using the corresponding object-level inference rules (⊃ R), (⊃ L), (∧R), (∧L_{1}), (∧L_{2}), (ˆ∀R), (ˆ∀L), (Initial), (Cut).

Let LM_{1} be the set of clauses displayed in Figure 3 and let Σ_{1} be the set of constants containing object-logical connectives ˆ∀, ⊃, and ∧ along with the two predicates left and right and any non-empty set of constants of type i (denoting members of the object-level domain of individuals). Notice that object-level quantification is treated by using a constant of second order, ˆ∀ : (i → bool) → bool, in concert with meta-level quantification: in the two clauses (ˆ∀R) and (ˆ∀L), the type of B is i → bool. This style representation of quantification is familiar from Church [6] and has been used to advantage in computer systems such as λProlog [7], Isabelle [29], and Elf [30]. This style of representing object-level syntax is often called higher-order abstract syntax.

To illustrate how these clauses specify the corresponding object-level inference rule, consider in more detail the first two clauses in Figure 3. Backchaining on the F sequent

Σ_{1}: LM_{1}; · ⟶ right(B_{0} ⊃ C_{0}); left(B_{1}), …, left B_{n}

using the (⊃ R) clause in LM_{1} (i.e., use decide!, ∀L twice, and −∘L) yields the sequent

Σ_{1}: LM_{1}; · ⟶ ?(left B_{0}) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right C_{0}; left(B_{1}), …, left B_{n},

which in turns is provable if and only if the sequent

Σ_{1}: LM_{1}; · ⟶ right C_{0}; left B_{0}, …, left B_{n}

is provable. Thus, proving the object-level sequent B_{1}, …, B_{n} ⟶ B_{0} ⊃ C_{0} has been successfully reduced to proving the sequent B_{0}, …, B_{n} ⟶ C_{0}. Now consider the sequent

Σ_{1}: LM_{1}; · ⟶ right(C); left(C_{0} ⊃ B_{0}), left(B_{1}), …, left B_{n}.

Using the decide! inference rule to select the (⊃ L) clause, and using two instances of ∀L, we get the sequent whose right-hand and left-hand sides have not changed but where the sequent arrow is labeled with

? left B_{0} −∘ right(C_{0}) −∘? left(C_{0} ⊃ B_{0}).

Using −∘L twice yields the following three sequents:

Σ_{1}: LM_{1}; · ⟶ right(C); left(C_{0} ⊃ B_{0}), left B_{0}, …, left B_{n} Σ_{1}: LM_{1}; · ⟶ right(C_{0}); left(C_{0} ⊃ B_{0}), left(B_{1}), …, left B_{n}

Σ_{1}: LM_{1}; · ⟶^{? left(C_{0}⊃B_{0})} ·; left(C_{0} ⊃ B_{0}), left(B_{1}), …, left B_{n}

The last sequent is immediately provable using the ?L, decide, and initial? inference rules. Notice that the formula right(C_{0}) could have moved to either the first or second sequent: if it had moved to the first sequent, no proof in F of that sequent is possible (provable F sequents using LM_{1} contain at most one right formula in the right, inner-most context). Thus, we have succeeded in reducing the provability of the object-level sequent C_{0} ⊃ B_{0}, B_{1}, …, B_{n} ⟶ C to the provability of the sequents

C_{0} ⊃ B_{0}, B_{1}, …, B_{n} ⟶ C_{0} and C_{0} ⊃ B_{0}, B_{0}, …, B_{n} ⟶ C.

As we shall show in the proof of Proposition 5, these are the only possible reductions available using the clauses in LM_{1}.

In a similar fashion, we can trace the use of decide! on the (Initial) and (Cut) clauses to see these are equivalent to the inference rules

Σ_{1}: LM_{1}; · ⟶ right B; left B, L

and

\frac{Σ_{1}: LM_{1}; · ⟶ right C; L Σ_{1}: LM_{1}; · ⟶ right B; left C, L}{Σ_{1}: LM_{1}; · ⟶ right B; L},

respectively, where L is a syntactic variable denoting a finite set of left-atoms.

In many ways, this style presentation of inference rules for LM_{1} can be judged superior to the usual presentation using inference figures. For example, consider the following inference figures for ∧R and ⊃L taken from [8].

\frac{Γ ⟶ Θ, A Γ ⟶ Θ, B}{Γ ⟶ Θ, A ∧ B} ∧ R \frac{Γ ⟶ Θ, A B, Δ ⟶ Λ}{A ⊃ B, Γ, Δ ⟶ Θ, Λ} ⊃ L

In these inference rules, the context surrounding the formulas being introduced must be explicitly mentioned and managed: in the ∧R figure, the context is copied, while in the ⊃L, the context is split to different branches (again, reading these inference figure bottom up). In the Forum specification, the context is manipulated implicitly via the use of the meta-level conjunctions: context copying is achieved using the additive conjunction & and context splitting is achieved using iterated ∘− (i.e., using the multiplicative conjunction ⊗). Similarly, the structural rules of contraction and thinning can be captured together using the ? modal. Since the meta-logic captures so well many of the structural properties of the object-level proof system we can reason about properties of the object-level system using meta-level properties of Forum and linear logic. Of course, this approach to sequent calculus is also limited since Forum cannot naturally capture a number of features that are captured by conventional sequent figures: for example, the structural rule of exchange.

Notice that the well known problems with searching for proofs containing cut rules are transferred to the meta-level as problems of using a clause with ⊥ for a head within the search for cut-free proofs (see Section 3).

Proposition 5 (Correctness of LM_{1}) The sequent B_{1}, …, B_{n} ⟶ B_{0} (n ≥ 0) has an LM_{1}-proof if and only if Σ_{1}: LM_{1}; · ⟶ right B_{0}; left B_{1}, …, left B_{n} has a proof in F.

Proof For the forward direction, an LM_{1}-proof can be converted into a F proof of the corresponding meta-level formula by mapping the sequence of inference rules in the LM_{1}-proof into the sequence of clauses used in backchaining in the proof from F. Additionally, right-introductions for ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , &, ∀, and ? will need to be inserted in a straightforward fashion.

For the reverse direction we need to read off the series of decide! inference rules in a proof from F of Σ_{1}: LM_{1}; · ⟶ right C_{0}; left C_{1}, …, left C_{n} to construct an LM_{1}-proof of C_{1}, …, C_{n} ⟶ C_{0}. Using the multiset rewriting notion of proof construction given in Section 4 makes this reading from proofs in F particular simple. However, that multiset rewriting paradigm was only described for clauses with atoms in the head: clauses in LM_{1} contain formulas of the form ?(left B) in their head. We need to extend this notion of multiset rewriting to include such formulas. To do this, we first show the following two technical lemmas about the structure of proofs in F based on LM_{1}. The term LM_{1}-derivative is defined as follows:

1. If D ∈ LM_{1} then D is an LM_{1}-derivative.

2. If ∀_{τ} x.D is an LM_{1}-derivative and t is a Σ_{1}-term of type τ, then D[t/x] is an LM_{1}-derivative.

3. If D_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D_{2} is an LM_{1}-derivative then D_{1} and D_{2} are LM_{1}-derivatives.

4. If G −∘ D is an LM_{1}-derivative then D is an LM_{1}-derivative.

5. If ? D is an LM_{1}-derivative then D is an LM_{1}-derivative.

6. Nothing else is an LM_{1}-derivative.

Notice that all atoms of the form right A and left A are LM_{1}-derivatives and if ? D is an LM_{1}-derivative, then D is of the form left A.

Lemma 6 If n ≥ 0 and the sequent Σ_{1}: LM_{1}; · ⟶ right C_{0}; left C_{1}, …, left C_{n} has a proof in F, then every sequent in that proof is of the form

Σ: LM_{1}; L_{1} ⟶ Γ; L_{2} or Σ: LM_{1}; L_{1} ⟶^{D} Γ; L_{2}

where Σ is a signature containing Σ, L_{1} is a multiset of left-atoms containing at most one formula, L_{2} is a set of left-atoms containing {left C_{1}, …, left C_{n}}, D is an LM_{1}-derivative, and Γ is a list of formulas of the form ?(left A_{1}) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} right A_{2}, ∀x(right (Bx)), right A, ?(left A), left A, and ⊥. Here, A, A_{1}, and A_{2} are Σ-terms of type bool, and B is a Σ-term of type i → bool.

Proof This lemma can be proved by induction on the distance of sequents from the root sequent. Clearly the root itself satisfies the condition on sequents. Next, we need to show that if the conclusion of an inference rule satisfies these conditions, the premises of that inference rule also satisfies these conditions. The only inference rules that can have such a sequents as conclusions are &R, ⊥R, ∀R, ?R, decide?, decide!, decide, initial, initial? −∘L, ∀L, and ?L. An examination of these rules confirms the inductive step of the proof.

Lemma 7 Let L be a set of left-atoms, D be an LM_{1}-derivative, A be a list of Σ_{1}-atomic formulas, and A be a Σ_{1}-term of type bool. If either

Σ_{1}: LM; left A ⟶ A; L or Σ_{1}: LM; left A ⟶^{D} A; L

has a proof in F then A is the one element list containing left A or A is empty and left A ∈ L.

Proof Assume not. Then one of these sequents is provable but the conditions on A and L are not satisfied. Pick the proof in F that has the smallest height and consider the various inference rules that can terminate that proof. Clearly, that proof does not end in a right-introduction rule or an initial rule. If the last rule was any of the other rules (the decide rules or the left-introduction rules), then one of the premises would contain a sequent that similarly does not satisfy the conditions in the lemma. This is then a contradiction since that sequent has a proof of smaller height.

The implication of this lemma is that the inference rule ? L′ can be used in place of ?L (see the end of Section 3) when using the LM_{1} theory. More

specifically, if the sequent Σ_{1}: LM_{1}; · ⟶^{? left B} ·; L is provable then left B ∈ L. Given this result, the multiset rewriting paradigm can be extended to those clause in LM_{1}.

The correctness proof for LM_{1} is now easy to finish: given a proof in F of

Σ_{1}: LM_{1}; · ⟶ right C_{0}; left C_{1}, …, left C_{n},

just read off of it the series of decide! rules that are used to select members of the LM_{1} set of clauses. Applying the sequent inference rules that correspond to those clauses yields an LM_{1} proof of C_{1}, …, C_{n} ⟶ C_{0}.

So far we have only discussed the operational interpretation of the specification in Figure 3. It is delightful, however, to note that this specification has some meta-logical properties that go beyond its operational reading. In particular, the specifications for the initial and cut inference rules together imply the equivalences (right B)^{⊥} ≡ ?(left B) and (right B) ≡ !(right B). That is, we have the (not too surprising) fact that left and right are related by a meta-level negation, and that this is guaranteed by reference only to the specifications for the initial and cut rules. Given these equivalences, it is possible to eliminate references to left in the LM_{1} specification. The result would be a specification quite similar to one for specifying a natural deduction proof system for minimal logic. To this end, consider the specification of the NM_{1} natural deduction proof system given in Figure 4. The specification there is similar to those given using intuitionistic meta-logics [7, 29] and dependent typed calculi [3, 13].

Proposition 8 (Correctness of NM_{1}) The formula B_{0} has an NM_{1} proof from the assumptions B_{1}, …, B_{n} (n ≥ 0) if and only if

Σ_{1}: NM_{1}, right B_{1}, …, right B_{n}; · ⟶ right B_{0}; ·

has a proof in F.

Proof The correctness proof for natural deduction based on intuitionistic logic and type theories that can be found in [7, 13, 29] can be used here as well. The only difference is that in Figure 4, certain occurrences of ⇐ are replaced with occurrences of ∘−. This replacement can be justified using Proposition 6 of

(⊃ I) right (A ⊃ B) ∘− (right A ⇒ right B).
(⊃ E)  right B ∘− right A ∘− right (A ⊃ B).
(∧I) right (A ∧ B) ∘− right A ∘− right B.
(∧E_{1})  right A ∘− right (A ∧ B).
(∧E_{2})  right B ∘− right (A ∧ B).
(ˆ∀I)  right (ˆ∀B) ∘− ∀x(right (Bx)).
(ˆ∀E)  right (Bx) ∘− right (ˆ∀B).

Figure 4: Specification of the NM_{1} natural deduction calculus.

[15] in which it is shown that when translating an intuitionistic theory to linear logic, positive occurrences of intuitionistic implications can be translated using by −∘ while negative occurrences can be translated using ⇒. It follows that these two presentations of NM_{1} prove the same sequents of the form displayed in this Proposition.

We can now supply a meta-logical proof that NM_{1} and LM_{1} prove the same object-level theorems. The following two lemmas supply the necessary implications.

Lemma 9 ⊢ LM_{1} ≡ [(⊗NM_{1}) ⊗ Initial ⊗ Cut].

Proof As we remarked before the formulas Initial and Cut in LM_{1} entail the equivalences (right B)^{⊥} ≡ ?(left B) and (right B) ≡ !(right B). If we apply these two equivalences along with the linear logic equivalences

p^{⊥} ∘− q^{⊥} ≡ q ∘− p  (! p)^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} q ≡ p ⇒ q  (p^{⊥} & q^{⊥})^{⊥} ≡ p ⊕ q

to the first seven clauses in Figure 3, we get the seven clauses in Figure 4. (The last two clauses of LM_{1} become linear logic theorems.) Clearly, LM_{1} ⊢ (⊗NM_{1}). The proof of the converse entailment follows by simply reverse the steps taking above: we can work backwards from NM_{1} to LM_{1} by equivalences.

Before we establish that LM_{1} and NM_{1} prove the same object-level formulas (Theorem 13), we need a couple of technical lemmas.

Lemma 10 If Σ_{1}: NM_{1}; · ⟶ right B; · has a proof in F, then Σ_{1}: LM_{1}; · ⟶ right B; · has a proof in F.

Proof This follows directly from Lemma 9, cut-elimination for linear logic, and the soundness and completeness results for F.

Lemma 11 If Σ_{1}: NM_{1}, Cut, Initial; · ⟶ right B; · has a proof in F, then Σ_{1}: NM_{1}; · ⟶ right B; · has a proof in F.

Proof Let Ξ be a proof in F of Σ_{1}: NM_{1}, Cut, Initial; · ⟶ right B; ·. We show we can always eliminate occurrences of decide! rules in Ξ that select the Cut clause. Once they have all been eliminated, the Initial clause is also not selected.

Consider the sequent that occurs the highest in Ξ that is also the conclusion of a decide! rule that select Cut. As we noted earlier, that sequent is of the form

Σ: NM_{1}, Cut, Initial; · ⟶ right B; L

and it has above it subproofs Ξ_{1} and Ξ_{2} of the sequents

Σ: NM_{1}; · ⟶ right C; L and Σ: NM_{1}; · ⟶ right B; left C, L,

respectively. We can now transform Ξ_{2} into Ξ′_{2} as follows: first remove left C from the right-most context of all of its sequents and for every occurrence of the initial rule in Ξ_{2} of the form

\overline{Σ_{1}: NM_{1}; · ⟶ right C; left C, L},

replace that subproof in Ξ_{2} with Ξ_{1}. The resulting Ξ′_{2} is a proof of

Σ: NM_{1}, Cut, Initial; · ⟶ right B; L

and, since Ξ_{1} and Ξ_{2} do not contain occurrences of decide! that selected Cut, neither does Ξ′_{2}. In this way, we have reduced the number of backchainings using Cut in Ξ by one.

Continuing in this fashion, we can eliminate all such uses of the Cut clause in proving the sequent Σ_{1}: NM_{1}, Cut, Initial; · ⟶ right B; ·. Since backchaining on Cut introduces left-atoms and backchaining on Initial eliminates such atoms (reading from bottom-up), if there there are no such occurrences of Cut, then there are no such occurrences of Initial. Hence, we have described a proof in F of Σ_{1}: NM_{1}; · ⟶ right B; ·.

Lemma 12 If Σ_{1}: LM_{1}; · ⟶ right B; · has a proof in F, then Σ_{1}: NM_{1}; · ⟶ right B; · has a proof in F.

Proof Assume Σ_{1}: LM_{1}; · ⟶ right B; · has a proof in F. Using Lemma 9, cut-elimination for linear logic, and the soundness and completeness results for F, the sequent

Σ_{1}: NM_{1}, Cut, Initial; · ⟶ right B; ·

has a proof in F. Now using Lemma 11, we have that Σ_{1}: NM_{1}; · ⟶ right B; · has a proof in F.

The following theorem follows from results of Gentzen [8]. We supply a new proof here using linear logic as a meta-theory.

Theorem 13 The sequent ⟶ B has an LM_{1} proof if and only if B has an NM_{1}-proof (from no assumptions).

(∨R_{1}) right (A ∨ B) ∘− right A.
(∨R_{2}) right (A ∨ B) ∘− right B.
(∨L) ?(left (A ∨ B)) ∘− ?(left A) & ?(left B).
(ˆ∃R)  right (ˆ∃B) ∘− right (Bx).
(ˆ∃L)  ?(left (ˆ∃B)) ∘− ∀x(?(left (Bx))).

Figure 5: Sequent rules for disjunction and existential quantification.

(∨I_{1})′ right (A ∨ B) ∘− right A.
(∨I_{2})′ right (A ∨ B) ∘− right B.
(∨E)′  ⊥ ∘− right (A ∨ B)
∘− (right A ⇒ ⊥) & (right B ⇒ ⊥).
(ˆ∃I)′  right (ˆ∃B) ∘− right (Bx).
(ˆ∃E)′  ⊥ ∘− right (ˆ∃B)
∘− ∀x(right (Bx) ⇒ ⊥).

Figure 6: Equivalent forms of the clauses in Figure 5.

(∨I_{1}) right (A ∨ B) ∘− right A.
(∨I_{2}) right (A ∨ B) ∘− right B.
(∨E)  right E ∘− right (A ∨ B)

∘− (right A ⇒ right E) ∘− (right B ⇒ right E).

(ˆ∃I)  right (ˆ∃B) ∘− right (Bx).
(ˆ∃E)  right E ∘− right (ˆ∃B)

∘− ∀x(right (Bx) ⇒ right E).

Figure 7: Natural deduction rules for disjunction and existential quantification.

Proof This theorem follows immediately from Propositions 5 and 8 and Lemmas 10 and 12.

Now consider adding to our object-logic disjunction and existential quantification. Let Σ_{2} be Σ_{1} with the constants ∨ and ˆ∃ added. Let LM_{2} be the sequent system that results from adding the five clauses in Figure 5 to LM_{1}. Note the use of & in the specification of (∨L): this conjunction is needed since the right-hand of the object-level sequent is copied in this inference rule.

Applying the equivalences (right B)^{⊥} ≡ ?(left B) and (right B) ≡ !(right B) to the clauses displayed in Figure 5, we get the formulas in Figure 6. The clauses for (∨E)′ and (ˆ∃E)′ could also be written more directly as the linear logic formulas

(right A) ⊕ (right B) ∘− right (A ∨ B).
∃x(right (Bx)) ∘− right (ˆ∃B).

(using the equivalence (right B) ≡ !(right B)).

Figure 7 contains the usual introduction and elimination rules for natural deduction for ∨ and ˆ∃. The only difference between the clauses in that Figure and those in Figure 6 is that the natural deduction rules for disjunction and existential quantification use the atom right E instead of ⊥ in the elimination rules for ∨ and ˆ∃. While this difference does not allow us to directly generalize Lemma 9 to include these two connectives, it is possible to show that the clauses in Figure 6 or in Figure 7 prove the same object-level theorems. For example, let NM′_{2} be the set of clauses formed by adding the clauses in Figure 6 to NM_{1} and consider using decide! rule with the (∨E)′ clause to prove the F sequent

Σ_{2}: NM′_{2}, R; · ⟶ right E; ·.

This would lead to subproofs of the form

Σ_{2}: NM′_{2}, right A, R; · ⟶ right E; · and Σ_{2}: NM′_{2}, right A, R; · ⟶ right E; ·.

Here, we assume that R is a set of right-atoms containing right (A ∨ B). This is, of course, the same reduction in proof search if (∨E) (from Figure 7) was used instead. A similar observation holds for using either (∃E)′ or (∃E). Given these observations, we could prove the generalization of Theorem 13 using LM_{2} and NM_{2}. Notice that the specifications of NM_{1} and NM_{2} avoid using either ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} or ⊥, and as a result, they can be modeled using on intuitionistic linear logic, in fact, a simple subset of that like Lolli [15].

Most logical or type-theoretic systems that have been used for meta-level specifications of proof systems have been based on intuitionistic principles: for example, λProlog [7], Isabelle [29], and Elf [30]. Although these systems have been successful at specifying numerous logical systems, they have important limitations. For example, while they can often provide elegant specifications of natural deduction proof systems, specifications of sequent calculus proofs are often unachievable without the addition of various non-logical constants for the sequent arrow and for forming lists of formulas (see, for example, [7]). Furthermore, these systems often have problems capturing substructural logics, such as linear logic, that do not contain the usual complement of structural rules. It should be clear from the above examples that Forum allows for both the natural specification of sequent calculus and the possibility of handling some substructural object-logics.

6 Operational Semantics Examples

Evaluation of pure functional programs has been successfully specified in intuitionistic meta-logics [11] and type theories [4, 30] using structured operational semantics and natural semantics. These specification systems are less successful at providing natural specifications of languages that incorporate references and concurrency. In this section, we consider how evaluation incorporating references can be specified in Forum; specification of concurrency primitives will be addressed in the following section.

Consider the presentation of call-by-value evaluation given by the following inference rules (in natural semantics style).

\frac{M ⇓ (abs R)  N ⇓ U  (R U) ⇓ V}{(app M N) ⇓ V}  \overline{(abs R) ⇓ (abs R)}

Here, we assume that there is a type tm representing the domain of object-level, untyped λ-terms and that app and abs denote application (at type tm → tm → tm) and abstraction (at type (tm → tm) → tm). Object-level substitution is achieved at the meta-level by β-reduction of the meta-level application (R U) in the above inference rule. A familiar way to represent these inference rules in meta-logic is to encode them as the following two clauses using the predicate eval of type tm → tm → o (see, for example, [11]).

eval (app M N) V ∘− eval M (abs R)
∘− eval N U ∘− eval (R U) V.

eval (abs R) (abs R).

In order to add side-effecting features, this specification must be made more explicit: in particular, the exact order in which M, N, and (R U) are evaluated must be specified. Using a “continuation-passing” technique from logic programming [33], this ordering can be made explicit using the following two clauses, this time using the predicate eval at type tm → tm → o → o.

eval (app M N) V K ∘−
eval M (abs R) (eval N U (eval (R U) V K)).
eval (abs R) (abs R) K ∘− K.

From these clauses, the goal (eval M V ⊤) is provable if and only if V is the call-by-value value of M. It is this “single-threaded” specification of evaluation that we shall modularly extend with non-functional features.

Consider adding to this specification a single global counter that can be read and incremented. To specify such a counter we place the integers into type tm, add several simple functions over the integers, and introduce the two symbols get and inc of type tm. The intended meaning of these two constants is that evaluating the first returns the current value of the counter and evaluating the second increments the counter’s value and returns the counter’s old value. We also assume that integers are values: that is, for every integer i the clause ∀k(eval i i k ∘− k) is part of the evaluator’s specification.

Figure 8 contains three specifications, E_{1}, E_{2}, and E_{3}, of such a counter: all three specifications store the counter’s value in an atomic formula as the argument of the predicate r. In these three specifications, the predicate r is

E_{1} = ∃r[ (r 0)^{⊥} ⊗

! ∀K∀V (eval get V K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V)) ⊗ ! ∀K∀V (eval inc V K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r (V + 1))]

E_{2} = ∃r[ (r 0)^{⊥} ⊗

! ∀K∀V (eval get (−V) K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V) ⊗ ! ∀K∀V (eval inc (−V) K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r V ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r (V − 1))]

E_{3} = ∃r[ (r 0) ⊗

! ∀K∀V (eval get V K ∘− r V ⊗ (r V −∘ K)) ⊗ ! ∀K∀V (eval inc V K ∘− r V ⊗ (r (V + 1) −∘ K)]

Figure 8: Three specifications of a global counter.

existentially quantified over the specification in which it is used so that the atomic formula that stores the counter’s value is itself local to the counter’s specification (such existential quantification of predicates is a familiar technique for implementing abstract data types in logic programming [20]). The first two specifications store the counter’s value on the right of the sequent arrow, and reading and incrementing the counter occurs via a synchronization between an eval-atom and an r-atom. In the third specification, the counter is stored as a linear assumption on the left of the sequent arrow, and synchronization is not used: instead, the linear assumption is “destructively” read and then rewritten in order to specify the get and inc functions (counters such as these are described in [15]). Finally, in the first and third specifications, evaluating the inc symbol causes 1 to be added to the counter’s value. In the second specification, evaluating the inc symbol causes 1 to be subtracted from the counter’s value: to compensate for this unusual implementation of inc, reading a counter in the second specification returns the negative of the counter’s value.

The use of ⊗, !, ∃, and negation in Figure 8, all of which are not primitive connectives of Forum, is for convenience in displaying these abstract data types. The equivalence

∃r(R_{1}^{⊥} ⊗! R_{2} ⊗! R_{3}) −∘ G ≡ ∀r(R_{2} ⇒ R_{3} ⇒ G ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} R_{1})

directly converts a use of such a specification into a formula of Forum (given α-conversion, we may assume that r is not free in G).

Although these three specifications of a global counter are different, they should be equivalent in the sense that evaluation cannot tell them apart. Although there are several ways that the equivalence of such counters can be proved (for example, operational equivalence), the specifications of these counters are, in fact, logically equivalent.

Proposition 14 The three entailments E_{1} ⊢ E_{2}, E_{2} ⊢ E_{3}, and E_{3} ⊢ E_{1} are provable in linear logic.

Proof The proof of each of these entailments proceeds (in a bottom-up fashion) by choosing an eigen-variable to instantiate the existential quantifier on the left-hand specification and then instantiating the right-hand existential quantifier with some term involving that eigen-variable. Assume that in all three cases, the eigen-variable selected is the predicate symbol s. Then the first entailment is proved by instantiating the right-hand existential with λx.s (−x); the second entailment is proved using the substitution λx.(s (−x))^{⊥}; and the third entailment is proved using the substitution λx.(s x)^{⊥}. The proof of the first two entailments must also use the equations

{−0 = 0, −(x + 1) = −x − 1, −(x − 1) = −x + 1}.

The proof of the third entailment requires no such equations.

Clearly, logical equivalence is a strong equivalence: it immediately implies that evaluation cannot tell the difference between any of these different specifications of a counter. For example, assume E_{1} ⊢ eval M V ⊤. Then by cut and the above proposition, we have E_{2} ⊢ eval M V ⊤.

It is possible to specify a more general notion of reference from which a counter such as that described above can be built. Consider the specification in Figure 9. Here, the type loc is introduced to denote the location of references, and three constructors have been added to the object-level λ-calculus to manipulate references: one for reading a reference (read), one for setting a reference (set), and one for introducing a new reference within a particular lexical scope (new). For example, let m and n be expressions of type tm that do not contain free occurrences of r, and let F_{1} be the expression

(new (λr(set r (app m (read r)))) n).

This expression represents the program that first evaluates n; then allocates a new, scoped reference cell that is initialized with n’s value; then overwrites this new reference cell with the result of applying m to the value currently stored in that cell. Since m does not contain a reference to r, it should be the case that this expression has the same operational behavior as the expression F_{2} defined as

(app (abs λx(app m x)) n).

Below we illustrate the use of meta-level properties of linear logic to prove the fact that F_{1} and F_{2} have the same operational behaviors.

Let Ev be the set of formulas from Figure 9 plus the two formulas displayed above for the evaluation of app and abs. An object-level program may have both a value and the side-effect of changing a store. Let S be a syntactic variable for a store: that is, a formula of the form ref h_{1} u_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} … ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ref h_{n} u_{n} (n ≥ 0), where all the constants h_{1}, …, h_{n} are distinct. A store is essentially a finite function that maps locations to values stored in those locations. The domain of a store is the set of locations it assigns: in the above case, the domain of S is

read : loc → tm
set : loc → tm → tm
new : (loc → tm) → tm → tm
assign : loc → tm → o → o
ref : loc → tm → o
eval (set L N) V K ∘− eval N V (assign L V K).
eval (new R E) V K ∘− eval E U (∀h(ref h U ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} eval (R h) V K)).
eval (read L) V K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ref L V ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ref L V.
assign L V K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ref L U ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ref L V.

Figure 9: Specification of references.

{h_{1}, …, h_{n}}. A garbaged state is a formula of the form ∀h̄.S, where S is a state and ∀h̄ is the universal quantification of all the variables in the domain of S. Given the specification of the evaluation of new in Figure 9, new locations are modeled at the meta-level using the eigen-variables that are introduced by the ∀R inference rule of F.

Consider, for example, the program expression F_{3} given as

(new λr(read r) 5).

This program has the value 5 and the side-effect of leaving behind a garbaged store. More precisely, the evaluation of a program M in a store S yields a value V, a new store S′, and a garbaged store G if the formula

∀k[k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S′ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G −∘ eval M V k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S]

is provable from the clauses in Ev and the signature extended with the domain of S. An immediate consequence of this formula is that the formula eval M V ⊤ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S is provable: that is, the value of M is V if the store is initially S. The references specified here obey a block structured discipline in the sense that the domains of S and S′ are the same and any new references that are created in the evaluation of M are collected in the garbaged store G.

A consequence of the formulas in Ev is the formula

∀k[k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ∀h(ref h 5) −∘ eval F_{3} 5 k].

That is, evaluating expression F_{3} yields the value 5 and the garbaged store ∀h(ref h 5). An immediate consequence of this formula is the formula

∀k[k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ∀h(ref h 5) −∘ eval F_{3} 5 k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S];

in other words, this expression can be evaluated in any store without changing it. Because of their quantification, garbaged stores are inaccessible: operationally (but not logically) ∀h(ref h 5) can be considered the same as ⊥ in a manner similar to the identification of (x)x̄y with the null process in the π-calculus [27].

We can now return to the problem of establishing how the programs F_{1} and F_{2} are related. They both contain the program phrases m and n, so we first assume that if n is evaluated in store S_{0} it yields value v and mutates the store into S_{1}, leaving the garbaged store G_{1}. Similarly, assume that if m is evaluated in store S_{1} it yields value (abs u) and mutates the store into S_{2} with garbaged store G_{2}. That is, assume the formulas

∀k[k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{1} −∘ eval n v k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{0}] and
∀k[k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{2} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{2} −∘ eval m (abs u) k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{1}].

From these formulas and those in Ev, we can infer the following formulas.

∀W ∀k[eval (u v) W k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{2} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{2} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ∀h(ref h v) −∘ eval F_{1} W k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{0}]
∀W ∀k[eval (u v) W k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{2} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{2}  −∘ eval F_{2} W k ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} S_{0}]

That is, if the expression (u v) has value W in store S_{2} then both expressions F_{1} and F_{2} yield value W in store S_{1}. The only difference in their evaluations is that F_{1} leaves behind an additional garbaged store. Since the continuation k is universally quantified in these formulas, F_{1} and F_{2} have these behaviors in any evaluation context.

Clearly resolution at the meta-level can be used to compose the meaning of different program fragments into the meaning of larger fragments. Hopefully, such a compositional approach to program meaning can be used to aid the analysis of programs using references.

7 Specification of Concurrency primitives

Concurrency primitives similar to those found in the π-calculus were shown in [23] to be expressible naturally in a fragment of linear logic subsumed by Forum. Below we show how concurrency primitives, inspired by those found in Concurrent ML (CML) [31] can be specified in Forum. Consider the specification in Figure 10. The first eight clauses specify the straightforward evaluation rules for the corresponding eight data constructors. The next three clauses defined the meaning of the three special forms sync, spawn, and newchan. The remaining clauses specify the event predicate.

This specification allows for multiple threads of evaluation. Evaluation of the spawn function initiates a new evaluation thread. The newchan function causes the meta-logic to pick a new eigen-variable (via the ∀c quantification) and then to assume that that eigen-variable is a value (via the assumption ∀I(eval c c I ∘− I)): such a new value can be used to designate new channels for use in synchronization. The name-restriction operator of the π-calculus can be modeled using universal quantification in a similar fashion [23].

The sync primitive allows for synchronization between threads: its use causes an “evaluation thread” to become an “event thread.” The behaviors of event threads are described by the remaining clauses in Figure 10. The primitive events are transmit and receive and they represent two halves of a synchronization between two event threads. Notice that the clause describing their meaning is the only clause in Figure 10 that has a head with more than one atom. The non-primitive events choose, wrap, guard, and poll are reduced to other calls to event and eval. The choice event is implemented as a local, non-deterministic choice. (Specifying global choice, as in CCS [26], would be much more involved.) The wrap and guard events chain together evaluation and synchronization but in direct orders.

The only use of & and ⊤ in any of our evaluators is in the specification of polling: in an attempt to synchronize with (poll E) (with the continuation K) the goal (event E U ⊤) & K is attempted (for some unimportant term U). Thus, a copy of the current evaluation threads is made and (event E U ⊤) is attempted in one of these copies. This atom is provable if and only if there is a complementary event for E in the current environment, in which case, the continuation ⊤ brings us to a quick completion and the continuation K is attempted in the original and unspoiled context of threads. If such a complementary event is not present, then the other clause for computing a polling event can be used, in which case, the result of the poll is none, which signals such a failure. The semantics of polling, unfortunately, is not exactly as intended in CML since it is possible to have a polling event return none even if the event being tested could be synchronized. This analysis of polling is similar to the analysis of testing in process calculus as described in [23]. As is discussed there, this problem with polling can be addressed if the meta-logic allows certain forms of negation-as-failure.

About this specification, we shall not prove anything formal, although it should be clear that the approach to reasoning about object-level programs using meta-level resolution, as in the last section, should be applicable here as well.

In the [5], Chirimar presents a specification of a programming language motivated by Standard ML [28]. In particular, a specification for the call-by-value λ-calculus is provided, and then modularly extended with the specifications of references, exceptions, and continuations: each of these features is specified without complicating the specifications of other the features.

8 Conclusions

We have given a presentation of linear logic that modularly extends the proof theory of several known logic programming languages. The resulting specification language, named Forum, provides the abstractions and higher-order judgments available in intuitionistic-based meta-logics as well as primitives for

eval, event : tm → tm → o → o.
none : tm.
guard, poll, receive, some, sync : tm → tm.
choose, transmit, wrap : tm → tm → tm.
spawn, newchan : (tm → tm) → tm.
eval none none K ∘− K.
eval (guard E) (guard V) K ∘− eval E V K.
eval (poll E) (poll V) K ∘− eval E V K.
eval (receive E) (receive V) K ∘− eval E V K.
eval (some E) (some V) K ∘− eval E V K.
eval (choose E F) (choose U V) K ∘− eval E U (eval F V K).
eval (transmit E F) (transmit U V) K ∘− eval E U (eval F V K).
eval (wrap E F) (wrap U V) K ∘− eval E U (eval F V K).
eval (sync E) V K ∘− eval E U (event U V K).
eval (spawn R) unit K ∘− (eval (R unit) unit ⊥) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} K.
eval (newchan R) V K ∘− ∀c(∀I(eval c c I ∘− I) ⇒ eval (R c) V K).

event (receive C) V K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} event (transmit C V) unit L ∘− K ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L.

event (choose E F) V K ∘− event E V K.
event (choose E F) V K ∘− event F V K.
event (wrap E F) V K ∘− event E U (eval (app F U) V K).
event (guard F) V K ∘− eval (app F unit) U (event U V K).
event (poll E) (some E) K ∘− (event E U ⊤) & K.
event (poll E) none K ∘− K.

Figure 10: Specifications of some primitives similar to those found in Concurrent ML. synchronization and communications. We have illustrated the possible uses of Forum by providing example specifications of object-level sequent systems and of the operational semantics of programming languages. Since the resulting specifications are natural and simple, properties of the meta-logic can be meaningful employed to prove properties about the specified object-languages.

Forum appears to be useful for other kinds of semantic specifications as well. In [5], Chirimar specified the operation semantics of a prototypical RISC machine: he specified its sequential and pipelined operational semantics, along with optimizations such as call-forwarding and early branch resolution. He also proved that sequential and pipelined specification were equivalent, and he addressed the problem of code equivalence and analyzed the problem of code rescheduling. His proofs and analyses made use of familiar aspects of proof theory and linear logic.

Acknowledgments. This paper is an extended version of a paper that appeared as [24] and which was also presented at the 1994 Joint Meeting of ALP and PLILP, Madrid, September 1994. I benefited from discussions with Jawahar Chirimar and Bob Harper. Thanks also to Bow-Yaw Wang for his help in proofreading this paper. The author has been funded in part by ONR N00014-93-1-1324, NSF CCR-92-09224, NSF CCR-94-00907, and ARO DAAH04-95-1-0092. Papers by Miller listed in the bibliography are available via anony-

mous ftp from ftp.cis.upenn.edu in pub/papers/miller or using WWW at
http://www.cis.upenn.edu/~dale.

References

[1] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

[2] J.M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9(3-4):445–473, 1991.

[3] Arnon Avron, Furio Honsell, Ian A. Mason, and Robert Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309–354, 1992.

[4] R. Burstall and Furio Honsell. A natural deduction treatment of operational semantics. In Proceedings of the 8th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume LNCS, Vol. 338, pages 250–269. Springer-Verlag, 1988.

[5] Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995. Available as

    ftp://ftp.cis.upenn.edu/pub/papers/chirimar/phd.ps.gz.

[6] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[7] Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43–81, August 1993.

[8] Gerhard Gentzen. Investigations into logical deductions, 1935. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland Publishing Co., Amsterdam, 1969.

[9] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[10] Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

[11] John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123–152, April 1993.

[12] James Harland and David Pym. On goal-directed provability in classical logic. Technical Report 92/16, Dept of Comp Sci, Uni. of Melbourne, 1992.

[13] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.

[14] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic: Extended abstract. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 32–42, Amsterdam, July 1991.

[15] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994.

[16] Stephen Cole Kleene. Permutabilities of inferences in Gentzen’s calculi LK and LJ. Memoirs of the American Mathematical Society, 10, 1952.

[17] Naoki Kobayashi and Akinori Yonezawa. ACL - a concurrent linear logic programming paradigm. In Dale Miller, editor, Logic Programming - Proceedings of the 1993 International Symposium, pages 279–294. MIT Press, October 1993.

[18] Naoki Kobayashi and Akinori Yonezawa. Type-theoretic foundations for concurrent object-oriented programming. In Proceedings of OOPSLA’94, 1994. To appear.

[19] P. Lincoln and V. Saraswat. Higher-order, linear, concurrent constraint programming. Available as file://parcftp.xerox.com/pub/ccp/lcc/hlcc.dvi., January 1993.

[20] Dale Miller. Lexical scoping as universal quantification. In Sixth International Logic Programming Conference, pages 268–283, Lisbon, Portugal, June 1989. MIT Press.

[21] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79–108, January 1989.

[22] Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.

[23] Dale Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242–265. Springer-Verlag, 1993.

[24] Dale Miller. A multiple-conclusion meta-logic. In S. Abramsky, editor, Ninth Annual Symposium on Logic in Computer Science, pages 272–281, Paris, July 1994.

[25] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[26] Robin Milner. Communication and Concurrency. Prentice-Hall International, 1989.

[27] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part I. Information and Computation, pages 1–40, September 1992.

[28] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.

[29] Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.

[30] Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–321, Monterey, CA, June 1989.

[31] John H. Reppy. CML: A higher-order concurrent language. In ACM SIG-PLAN Conference on Programming Language Design and Implementation, pages 293–305, June 1991.

[32] V. Saraswat. A brief introduction to linear concurrent constraint programming. Available as file://parcftp.xerox.com/pub/ccp/lcc/lcc-intro.dvi.Z., 1993.

[33] Paul Tarau. Program transformations and WAM-support for the compilation of definite metaprograms. In Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, number 592 in LNAI, pages 462–473. Springer-Verlag, 1992.