- Built-in treatment of bindings
- Syntax and semantics of definitions
- Symmetry of finite success and finite failure
- The ∇ quantifier
- Proof search within 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.

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.

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`

.

Kindchtype.Typez ch.Types ch -> ch. % The predicate a holds for 3, 5, and 2.Definea : ch ->propbya (s (s (s z))) ; a (s (s (s (s (s z))))) ; a (s (s z)). % The less-than-or-equal relationDefineinductiveleq : ch -> ch ->propbyleq z N ; leq (s N) (s M) := leq N M. % Compute the maximum of aDefinemaxa : ch ->propbymaxa N := a N /\forallx, 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.

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*.

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.

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 *A*⇒ *B*,
prover-1 calls *prover-0* to enumerate all possible solutions
{θ* _{i}* |

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 (*A* ⇒ *A*) 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.