## 5 Hypothetical reasoning

For those familiar with λProlog, a key difference between Bedwyr and λProlog
is that the latter allows for “hypothetical” reasoning and such
reasoning is central to the way that λProlog treats bindings in syntax.
Bedwyr treats implication and universals in goal formulas in a
completely different way: via the closed world assumption.

Sometimes, when dealing with λ-tree syntax in Bedwyr, one
wishes to program operations as one might do in λProlog. This is possible
in the sense that one can write in Bedwyr an interpreter for suitable
fragments of λProlog. This is done, for example, in the `seq.def`
definition file. There is a goal-directed proof search procedure for a
small part of hereditary Harrop formulas (in particular, the minimal
theory of the fragment based on ⊤, ∧, ⊃, and
∀). This interpreter is prepared to use a logic program that
is stored as a binary predicate. For example, in λProlog, one would write
type checking for simple types over the untyped λ-calculus
encoded using
`app`

and
`abs`

as in 2.
The hypothetical reasoning that is involved in typing the object-level
λ-binder in the second clause above is not available directly
in Bedwyr. One can, however, rewrite these clauses as simply
“facts” in Bedwyr (3).

Listing 2:

Simple typing in Teyjus.

typeof (app M N) B :- typeof M (arrow A B), typeof N A.
typeof (abs R) (arrow A B) :- **pi** x\ typeof x A => typeof (R x) B. |

Listing 3:

Simple typing in Bedwyr (from

examples/progs_small.def).

__Define__ simple : form -> form -> **prop** __by__
simple (type_of (app M N) Tb)
(type_of M (Ta ~> Tb) && type_of N Ta);
simple (type_of (abs R) (Ta ~> Tb))
(for_all x\ type_of x Ta --> type_of (R x) Tb).
__Define__ atom : form -> **prop** __by__
atom (type_of X T). |

The first definition describes a logic program called
`simple`

that directly encodes the above λProlog program; the second definition
tells the interpreter in
`seq.def`

how to recognize an
object-level atomic formula. A call to
`seq atom simple tt (type_of Term Ty)`

will now attempt to
perform simple type checking on
`Term`

. Specifically, it is
possible to prove in Bedwyr the goal

(**exists** Ty, seq atom simple tt (type_of (abs x\ app x x) Ty))
-> **false**. |

or, in other words, that the self-application λ *x*(*x x*) does not
have a simple type.

This “two-level approach” of specification uses Bedwyr as a
meta-language in which a simple intuitionistic logic is encoded as an
object logic: computations can then be specified in the object-logic in
the usual way and then Bedwyr can be used to reason about that
specification. This general approach has been described in more detail
in [Mil06, GMN10].