Adequacy of Linear Resource Management in Logic Programming

February 19, 2001

1 An operational semantics for proof search

It is clear that the refinement of a logic programming language to support linearity will have to address not only the declarative interpretation of logic programs, but also their operational meaning. Even in the “pure” logic programming fragment without extra-logical features such as side effects or cut, operational considerations arise because of the incompleteness of the standard search procedure. For example, the goals (r ( r) ) (g ( r ( fail) ) g and (r ( r) ) (g ( fail ( r) ) g are logically equivalent, but the first runs forever, while the second fails finitely.

The question is how to describe the operational semantics of Lolli in the most natural way, independent of the particular implementation strategy for resource management. While the various sequent calculus based presentations of Lolli which have appeared in the literature address the logical interpretation of Lolli programs, they do not address the operational distinction between finite failure and infinite search. For example, Cervesato et. al. present three different formulations of Lolli, and show that a successful derivation exists in the original Lolli if and only if a derivation exists in each of the other formulations [?]. But this does not address the behavior of the search procedure as it considers unsuccessful derivations. The problem grows even more acute as extra-logical constructs are added to the language, because the search for a derivation of a subgoal may have other observable effects besides its success, failure, or non-termination. (Note that “effects” might include the interaction of search with unification, or a constraint solver.)

The approach taken here is to describe the search for a Lolli derivation as a sequence of refinements of incomplete proofs. It is convenient to represent incomplete proofs by their associated proof terms from linear type theory. In order to remain as close as possible to the sequent calculus formulation, where left rules appear in the opposite order from the corresponding elimination forms of natural deduction, the proof terms use spines rather than the more familiar applications and projections. Of course, this representation is only available for intuitionistic sequent calculi; a different technique would be needed in a classical setting. For simplicity, this paper concentrates on the propositional case, so the only observable effects of proof search are success, finite failure, and non-termination. However, the methods of this paper can be generalized to account for additional “effects” such as the unifier computed by a first-order query.

The first fragment of propositional Lolli of interest is the so-called uniform fragment consisting of the formulas freely generated by the connectives ) ⊸ & ⊤.

A ::= A_{1} ) A_{2}  Unrestricted implication
| A_{1} ⊸ A_{2}  Linear implication
| A_{1} & A_{2}  Additive conjunction
| ⊤  Additive unit
M ::= λu. M  Unrestricted abstraction
| λu. M  Linear abstraction
| ⟨M_{1}, M_{2}⟩  Additive pair
| ⟨⟩  Additive unit
| u .S  Application
| X  Variable
S ::= nil  Empty spine
| M ; S  Unrestricted application
| M ;S  Linear application
| π_{i} S  Projections (i = 1, 2)
| Y  Spine variable

The typing judgement that defines a notion of well formed partial proof is more complex than the corresponding notion for complete proofs. This is because a complete proof determines unambiguously how linear resources are assigned to each of its branches, but an incomplete proof has not necessarily committed to an assignment of resources to its unfinished branches. All that we require is that there be some consistent assignment of resources to the branches of the unfinished proof. This idea is captured by an approximate typing judgement Γ ⊢ M ˜: A which checks that a partial proof is well typed without considering linearity, and a function [[Γ ⊢ M ˜: A]] which computes the set of possible resource assignments to an approximately well-typed term M. We presume that for each variable X, its type type(X) and the context context(X) in which it appears are fixed.

Γ, u : A_{1} ⊢ M ˜: A_{2} ; Γ ⊢ λu. M ˜: A_{1} ) A_{2}  {Γ, u :A_{1} ⊢ M ˜: A_{2} \atop Γ ⊢ λu. M ˜: A_{1} ⊸ A_{2}}

\begin{matrix}Γ ⊢ M_{1} ˜: A_{1} & Γ ⊢ M_{2} ˜: A_{2} \\ Γ ⊢ ⟨M_{1}, M_{2}⟩ ˜: A_{1} & A_{2} \end{matrix}  Γ ⊢ ⟨⟩ ˜: ⊤

\begin{matrix}Γ(u) = A & Γ ⊢ S ˜: A > a \\ Γ ⊢ u .S ˜: a \end{matrix} type(X) = Γ context(X) = A

Γ ⊢ X ˜: A

Γ ⊢ nil ˜: a > a

type(Y) = A context(Y) = Γ
Γ ⊢ Y ˜: A > a

\begin{matrix}Γ ⊢ M ˜: A_{1} & Γ ⊢ S ˜: A_{2} > a \\ Γ ⊢ M ; S ˜: A_{1} ) A_{2} > a \end{matrix}  \begin{matrix}Γ ⊢ M ˜: A_{1} & Γ ⊢ S ˜: A_{2} > A \\ Γ ⊢ M ;S ˜: A_{1} ⊸ A_{2} > a \end{matrix}

{Γ ⊢ S ˜: A_{i} > a \atop Γ ⊢ π_{i} S ˜: A_{1} & A_{2} > a}

[[Γ ⊢ λu. M ˜: A_{1} ) A_{2}]] = Abs_{Γ,u:A_{1}}^{u} ([[Γ, u : A_{1} ⊢ M ˜: A_{2}]])
[[Γ ⊢ λu. M ˜: A_{1} ⊸ A_{2}]] = Abs_{Γ,u:A_{1}}^{u} ([[Γ, u :A_{1} ⊢ M ˜: A_{2}]])
[[Γ ⊢ ⟨M_{1}, M_{2}⟩ ˜: A_{1} & A_{2}]] = Both([[Γ ⊢ M_{1} ˜: A_{1}]], [[Γ ⊢ M_{2} ˜: A_{2}]])
[[Γ ⊢ ⟨⟩ ˜: ⊤]] = Any_{Γ}
[[Γ ⊢ X ˜: A]] = Any_{Γ}
[[Γ ⊢ nil ˜: A > a]] = None
[[Γ ⊢ M ; S ˜: A_{1} ) A_{2} > a]] = Contr (Unr([[Γ ⊢ M ˜: A_{1}]]), [[Γ ⊢ S ˜: A_{2} > a]])
[[Γ ⊢ M ;S ˜: A_{1} ⊸ A_{2} > a]] = Contr ([[Γ ⊢ M ˜: A_{1}]], [[Γ ⊢ S ˜: A_{2} > a]])
[[Γ ⊢ π_{i} S ˜: A_{1} & A_{2} > a]] = [[Γ ⊢ S ˜: A_{i} > a]]
[[Γ ⊢ Y ˜: A > a]] = Any_{Γ}

where

Both(ℛ_{1}, ℛ_{2}) = ℛ_{1} ∩ ℛ_{2}
Any_{Γ} = {ϕ | ϕ ⊆ |Γ| }
Abs_{Γ}^{u} (ℛ) = {ϕ − {u} | ϕ ∈ ℛ and u ∈ ϕ ∪ |Γ|_{w} }
Contr (ℛ_{1}, ℛ_{2}) = {ϕ_{1} ∪ ϕ_{2} | ϕ_{1} ∈ ℛ_{1}, ϕ_{2} ∈ ℛ_{2} and ϕ_{1} ∩ ϕ_{2} ⊆ |Γ|_{c} }
None = {∅}
Unr(ℛ) = {ϕ ∈ ℛ | ϕ ⊆ |Γ|_{c} ∩ |Γ|_{w} }
|Γ| = {u | u : A ∈ Γ} ∪ {u | u :A ∈ Γ}
|Γ|_{c} = |Γ|_{w} = {u | u : A ∈ Γ}

Note that we restrict our attention to partial proof terms where each variable X occurs at most once within a term. This makes it unnecessary to concern ourselves with whether different occurrences of X must each be allocated the same resources. (This issue does arise in considering unification of linear terms, however.) We then say that a partial proof M is well typed, Γ ⊢ M : A, if Γ ⊢ M ˜: A and [[Γ ⊢ M ˜: A]] ≠ ∅. A well typed partial proof need not consume all the resources mentioned in its context Γ.

It remains to specify the control flow of the proof search procedure. The first issue is which unfinished branch of an incomplete proof to select for refinement; i.e., the treatment of don’t care nondeterminism. In Lolli this is always the leftmost unfinished position within the incomplete proof. Note that the order of application of right rules vs. left rules has already been established by the focusing structure of the sequent calculus, so in each unfinished proof position only a single kind of rule can be applied. We can describe the set of allowed refinements by a transition relation M_{1} ) M_{2}. A sequence of refinements

X = M_{0} ) M_{1} )^{∗} M_{n}

is valid if context(X) = Γ, type(X) = A, and Γ ⊢ M_{i} : A for each i. One might imagine that the transition relation should proceed to apply a single left or right rule. Alternatively, it could apply a sequence of inversion or focussing rules all at once, as an atomic step. We will call these two transition relations )^{1} and )^{IF} respectively.

Note that both relations have the “non-redundancy” property: an approximately well-typed partial proof M uniquely determines the sequence of refinements X = M_{0} )^{∗} M_{n} = M leading up to it, modulo renaming of proof term variables. Additionally, the transition relations are finitely branching: for each approximately well-typed M, there are only finitely many M′ such that M ) M′.

The other issue is how to select an alternate proof when refinement of the current proof fails; i.e., how to cope with don’t know nondeterminism. A standard Lolli interpreter will explore the search space in a particular order: more recently introduced assumptions will be focussed on before earlier ones, the left side of an assumption A_{1} & A_{2} will be focussed on before the right side, and so on. This is described here by a partial order M_{1} ≤ M_{2} on partial proofs, such that given a context Γ and a type A, the order is total on approximately well-typed terms Γ ⊢ M_{i} ˜: A, modulo renaming of proof term variables. We will also require that the order respects refinement: if M_{1} ≤ M_{2}, M_{1} ) M′_{1}, and M_{2} ) M′_{2}, then M′_{1} ≤ M′_{2}. The standard order is presented in Figure ??. It is easy to show that the standard order respects refinement for both of the transition relations presented above. We then extend the order to valid sequences of refinements by saying that one sequence is ≤ another if the corresponding partial proof terms are ≤ at the first position at which the two sequences differ. It is an easy consequence that the induced ordering on valid sequences is total.

Now we are in a position to characterize successful, finitely failing and infinitely failing proof searches for our simple propositional Lolli. A query Γ ⊢ X : A is successful if there is a valid sequence of refinements X = M_{0} )^{∗} M_{n} = M, M is ground (it contains no proof term variables), and there is no infinite sequence X = M′_{0} ) M′_{1} )^{∗} less than the terminating sequence according to the total order on sequences. The query fails finitely if it is unsuccessful and there is no infinite sequence of refinements. If neither of the preceding cases apply, the query fails to terminate. This definition is in accord with the behavior of an actual Lolli interpreter because of the finite branching property of the transition relations. The definition could be extended to handle an infinitely branching transition relation at the price of some additional complexity.

2 Equivalence of operational semantics

3 Residuation and operational semantics