Previous Up Next

7  The logic LINC

The logic behind Bedwyr, named LINC, is an extension to a higher-order version of intuitionistic logic that has been developed over the past few years. The acronym LINC, which stands for “lambda, induction, nabla, and co-induction”, lists the main novel components of the logic. In particular, λ-terms are supported directly (and, hence, the λ-tree syntax approach to higher-order abstract syntax is supported [Mil00]). Induction and co-induction are also available. The nabla (∇) quantifier has been added to this logic in order to increase the expressiveness of programs using λ-tree syntax in negated situations. The proof theory of LINC is given in [MT05, Tiu04]. Since this earlier work on LINC, more recent work on the logic G [GMN10, GMN11] and with fixed points in linear logic [Bae08a, Bae12] has further improved our understanding of using fixed points, induction, co-induction, and ∇-quantification.

Below we provide a high-level overview of the logical aspects of Bedwyr. More explicit information on this system can be found in [TNM05]. (N.b. the name “Level 0/1” in that paper has now been replaced by Bedwyr) Next, we describe the two orthogonal extensions to higher-order intuitionistic logic that have been incorporated into Bedwyr.

7.1  Built-in treatment of bindings

Bedwyr treats λ-abstractions within terms as primitives as well as allowing for variables of function type and quantifiers within formulas (∀, ∃, ∇). The system implements “higher-order pattern unification” (see 8). This kind of unification appears to be the weakest extension to first-order unification that treats bindings as a primitive. A number of automated deduction systems implement this kind of unification (e.g. Twelf, Teyjus, Coq, and Minlog). Full β-conversion is implemented by Bedwyr as well.

7.2  Syntax and semantics of definitions


Listing 7: Computing the maximum of a defined predicate (λProlog).

% The predicate a holds for 3, 5, and 2. a (s (s (s z))). a (s (s (s (s (s z))))). a (s (s z)). % The less-than-or-equal relation leq z N. leq (s N) (s M) :- leq N M. % Compute the maximum of a maxa N :- a N, pi x\ a x => leq x N.

Some systems implementing aspects of higher-order logic programming, such as λProlog, accept the “open-world assumption”: any conclusion drawn in their logic will hold in any extension of the underlying logic programming language. For example, consider the λProlog program in 7 (the signature has been left out), where the last clause has an implication => in the goal. During proof search, this implication causes λProlog to add a new eigenvariable, say c, to the runtime signature and to extend the current program with an atomic fact about it: (a c). In such a new world, however, the leq relation does not have any information about this “non-standard” number c.


Listing 8: Computing the maximum of a defined predicate (Bedwyr).

Kind ch type. Type z ch. Type s ch -> ch. % The predicate a holds for 3, 5, and 2. Define a : ch -> prop by a (s (s (s z))) ; a (s (s (s (s (s z))))) ; a (s (s z)). % The less-than-or-equal relation Define inductive leq : ch -> ch -> prop by leq z N ; leq (s N) (s M) := leq N M. % Compute the maximum of a Define maxa : ch -> prop by maxa N := a N /\ forall x, a x -> leq x N.

Bedwyr on the contrary accepts the “closed-world assumption”: the notion of programs is replaced by definitions that capture the “if-and-only-if” closure of logic programs (8). One of the syntactic difference between the syntax of clauses and that used in λProlog is that the head and body of clauses are separated from each other using the := instead of the :- (turnstile). The former symbol is used to remind the Bedwyr user of that “if and only if” completion of specifications.

Bedwyr takes the assumption (a c) and asks “Given the assumption that (a c) is true, how could have it been proved?” The natural answer to this is that that assumption could have been proved if c was either 3 or 5 or 2. Thus, this will cause a case analysis: in particular, the query (maxa N) will cause the following goals to be considered:

(a N)     (leq 3 N)     (leq 5 N)     (leq 2 N)

Here we use the numeric symbols ‘2’, ‘3’, etc., as abbreviations of the corresponding terms formed using z and s. The usual approach to unification and depth-first proof search will now produce the proper maximum value. This change allows Bedwyr to give a computational interpretation to finite failure and to do deduction that encodes model checking.

7.3  Symmetry of finite success and finite failure

The underlying logic of fixed points (also known as definitions) [Gir92, SH93, MMP03, MT03] contains an inference rule that allows for failure in unification (and, hence, in simple proof search) to be turned into a success. Thus, simple forms of “negation-as-failure” can be naturally captured in Bedwyr and the underlying logic. It is also possible to describe both may and must behaviors in process calculi. For example, not only can one code reachability in process calculus but bisimulation is also possible. One way to view this enhancement to proof search is the following: Let A and B be two atomic formulas. Then, finite success is captured by proving the sequent —→ A, finite failure is captured by proving the sequent A—→, and simulation is captured by proving the sequent A—→ B.

7.4  The ∇ quantifier

In order to treat specifications using λ-tree syntax properly, it appears that a new quantifier, called ∇, is necessary. If finite success is all that is needed, the ∇ can be replaced with the universal quantifier. When finite failure is involved, however, the ∇ quantifier plays an independent role. See [MT05, Tiu04, Tiu05] for more on this quantifier. It is worth pointing out that we know of no examples involving ∇ that do not also involve λ-tree syntax.

7.5  Proof search within LINC

Bedwyr is a proof search engine for a small fragment of the LINC logic. In principle, Bedwyr uses two provers. Prover-1 is similar to the depth-first interpreter used in λProlog. The main difference is in the proof of an implication. To prove an implication AB, prover-1 calls prover-0 to enumerate all possible solutions {θi | i=1,…,n} for A, and then prover-1 tries to prove Bθ1∧…∧ Bθn. If A has no solution (that is, if n=0), the implication is true. The substitutions generated by prover-1 are for existential1 variables, as usual in logic programming. On the other hand, the substitutions generated by prover-0 are for universal variables.

To illustrate this, consider the following goal:

∀ x  .  (∃ y  .  x=s y) ⇒ x=0 ⇒ false

(This formula formalizes the fact that if x is the successor of some number then x is not zero.) Bedwyr will call prover-1 on it. The prover introduces a universal variable and reaches the first implication. It then calls prover-0 on (∃ y   .  x = s y). Prover-0 introduces an existential variable y, and the unification instantiates x to get the only solution. Back to prover-1, we have to prove (s y = 0 ⇒ false) where y is still an existential variable. Prover-0 is given s y=0 to prove and fails to do so: that failure is a success for prover-1.

We’ve seen in 7 with the maxa example (8) how this treatment of the implication allows Bedwyr to check formulas which are not provable in traditional (pure) logic programming languages such as λProlog. As often, this novelty has a price. The systematic enumeration leads to infinite search for simple formulas like (AA) as soon as A does not have a finite number of solutions. Further development of Bedwyr may provide real support for induction and co-induction.

Prover-0 is similar to prover-1. The first difference is this dual treatment of variables; soundness requires another one. Because it needs to completely destruct formulas in order to enumerate solutions, prover-0 requires its connectives to be asynchronous on the left: they can be immediately destructed (introduced, in sequent calculus terminology) without restricting provability. This means that implication and universal quantification are forbidden on the left of implications.

Prover-1 instantiates existential variables, and considers universal variables as (scoped) constants. Prover-0 produces substitutions for universal variables, considers existential variables introduced in prover-0 as constants, but we have no satisfactory answer for existential variables introduced in prover-1. As a consequence, in prover-0, unification raises an run-time error when the instantiation of an existential variable is needed. More details about that can be found in Section 13.2.


Previous Up Next