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
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).
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
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].