7. Examples

Source code for modules can be found in the subdirectories of directory `examples'. Signature have filenames ending in .sig and modules have filenames ending in .mod.

The directory

`examples/utility/'

has a module defining the usual list predicates, a module defining mapping predicates and a module defining the reverse predicate. The definition of the last predicate uses implication, universal quantification and a non-local variable and so it might be especially interesting to look at the bytecode that is generated for it.

The examples in the directory

`examples/handbook/logic'

illustrate the power of lambda Prolog in manipulating formulas and those in

`examples/handbook/progs' 

do the same relative to manipulating programs. The code in these directories is modeled on that presented in the paper Higher-Order Logic Programming by G. Nadathur and D. Miller.

Finally, the directory

`examples/ndprover'

contains code defining an interactive theorem prover for a first-order logic based on a natural deduction calculus.

The subsections below contain a catalogue of queries to try against some of the modules mentioned above.

7.1 Examples for lists

Queries to execute against module `lists':

append (2::nil) (3::nil) L.

append L1 L2 (a::b::c::d::e::nil).

This query will produce all possibilities if you answer yes at the prompt, More solutions (y/n)?.

append (F a) (b::nil) (a::a::b::nil).

append (F X) nil (a::b::a::c::nil).

append (a::nil) ((b:int)::a::nil) (F a).

These queries make use of higher-order unification. If you are not already familiar with this notion, you may get some insight into it by examining the answers that are generated by each of the queries.

pi (X \ (append (X::nil) ((b:int)::X::nil) (F X))).

This query makes use of both higher-order unification and explicit universal quantification. Try to understand the answer that is produced and also why there is only one answer. Also, contrast this query with the one immediately preceding it.

sigma X \ (append [b] [a,a] (F X)).

This query makes use of both higher-order unification and explicit existential quantification. Note that the quantification has no effect on the search space. However, Teyjus displays bindings for only the free variables in a query that, in this case, includes only F. If the variable F were also explicitly existentially quantified, only an indication of success is relevant and so the query would terminate after displaying the first answer.

memb a (b::b::nil).

memb a (b::a::nil).

memb X (b::a::nil).

These queries demonstrate that at least one more predicate in the module, in particular, the predicate memb, works!

7.2 Examples for reverse

The definition of reverse illustrates the use of scoping constructs. Specifically, implication is used to give clauses a scope and universal quantification is used to close off the lexical scope of the name of the predicate that is defined. There is also the use of a non-local variable in a nested definition. You may view the disassembled code to see what the compiler does in the translation of this predicate and to also appreciate the fact that the compiler is not entirely naive.

Queries to execute against module `reverse':

reverse (1::2::3::4::nil) L.

reverse L [4,3,2,1].

reverse (b::a::nil) (F X).

The second query will succeed the first time around as you would expect, but will not terminate if you ask for another solution. Try to understand why.

7.3 Examples for maps

Here are some queries to try against the module `maps':

mapfun [a,b] (X \ (g a X)) L.

mapfun [a] F [g a a].

mapfun [a,b] F [g a a, g a b].

The first query shows the use of beta reduction. In solving the second and third queries, higher-order unification will be used. Examine the solutions produced in response to the second query and try to understand the differences between each of them and why they are collectively exhaustive. Also try to understand why only one of these is a solution to the last query.

mapfun [X:i] F [(g:i -> i -> i) a a].

mapfun [X:int] F [(g:i -> i -> i) a a].

mapfun [X:i -> i] F [(g:i -> i -> i) a a].

In several programming languages, types do not affect the results of computations. This is not true in Lambda Prolog. The queries above bring out this fact. Once again try to understand how typing plays a role in determining the solutions produced.

mappred [jane,john,james] father L.

mappred [jane,james] (X1\X2\(sigma Y\((father X1 Y), (father X2 Y)))) L.

mappred [jane,james] (X1\X2\ ((father X1 Y), (father X2 Y))) L.

mappred [john,peter] (X \ Y \ ((father Y X) ; (father X Y))) L.

mappred [jane,james] P L.

These queries illustrate the higher-order programming aspects of Lambda Prolog. The second, third and fourth queries show that goals with a complicated logical structure can be created and invoked at run-time. In fact, the only kind of goal that cannot be so created is one that includes an implication. When you run these queries, contrast the results that you get for the second query with those that you obtain from the third and try to understand the differences between these queries from this. Also note the behavior relative to the last query.

reduce [1,2,3,4,5] ((A:int) \ B \ (A + B)) 0 X.

reduce_eval [1,2,3,4,5] ((A:int) \ B \ (A + B)) 0 X.

These queries illustrate a reduce predicate that is familiar from the functional programming context. Contrast the two queries to realize that reduction in Lambda Prolog does not also involve the simplification of arithmetic expressions. The latter form of `reduction' can be forced through the use of the (impure) predicate is.

7.4 Examples for assoc

There is nothing novel about the code in the module `assoc' if you have already seen that in the preceding modules. It may be illustrative, though, to examine the byte code produced for the predicate in this module; note, in particular, the treatment of types in the code.

Here are some queries that you may try against the module:

assoc (foo:i) (X:int) [pair bar 2, pair foo 1].

assoc (F:i) (X:int) [pair bar 2, pair foo 1].

assoc ((F:i -> i) Y) (X:int) [pair bar 2, pair foo 1].

7.5 Examples for funs

This module contains more examples of higher-order predicate definitions. One of these is the familiar mapfun predicate. In comparison with the definition of the predicate with the same name in the module maps this one has the order of its first two arguments reversed. Teyjus indexes on the first argument, so the byte code produced in the two cases would be quite different. Look at the disassembled versions of the byte code files to understand this.

Here are some queries to try against this module:

mapfun (X \ (g a X)) [a,b] L.

mapfun F [a] [g a a].

mapfun F [a,b] [g a a, g a b].

mapfun F [X:int] [(g:i -> i -> i) a a].

foldr F 5 [1,2,3,4] L.

foldl F 5 [1,2,3,4] L.

foldl F 5 [1,2,3,4] (5 + 4 + 3 + 2 + 1).

Note that foldr will fold a list to the right, while foldl will fold a list to the left.

7.6 Examples for pnf

The module `pnf', the source code for which resides in the directory

`examples/handbook/logic',

contains code for converting first-order formulas to prenex normal form. It's illustrative of the use of universal goals and implication goals in recursion over higher-order abstract syntax. Some examples of its use can be examined through the module pnf_examples.mod. In particular, you could compile the latter module, load it and then try the following queries:

test 1 F.

This query converts the formula given by ((all (X \ (path a X))) imp tru).

test 2 F.

This query converts the fomula given by ((some (X \ (path a X))) imp tru).

test 3 F.

This query converts the fomula given by ((all (X \ (path a X))) and (all (Y \ (path Y a)))).

test 4 F.

This query converts the fomula given by ((some (X \ (path a X))) imp ((all (Y \ (path a Y))))).

This document was generated by Gopalan Nadathur on October, 20 2007 using texi2html 1.76.