Previous Up Next

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

Previous Up Next