Online Otter-λ

Examples

This example demonstrates the basic facilities for lambda calculus that are built into Otter-λ, and it also demonstrates how beta reduction is combined with ordinary demodulation. With this latter aim in mind, the file provides one demodulator:

x *x = x.

List(sos) then contains the disjunction of several negated goals, so that all the examples can run at once. In this commentary we consider them one at a time, and take the negation signs off so that we can consider the true form of the goal.

Example 1: ap(ap(lambda(x,lambda(y,x)),c*c),y) = c.

ap(lambda(x,lambda(y,x)),c*c) is reduce by substituting c*c for x in lambda(y,x), so we get lambda(y,c*c). Now when we apply that term to y, we get c*c, which is then demodulated to c. This demonstrates the combination of demodulation with beta-reduction. The beta reduction is actually performed before the demodulation, as indicated here.

Example2: ap(lambda(x,lambda(y,x)),y) = lambda(z,y)

If we were to simply textually replace x by y when reducing the left side, we would get lambda(y,y), which is wrong. The bound variable y on the left must first be renamed to avoid capturing the free variable y when it is substituted. This does happen as it should.

Example 3: lambda(x,x) = lambda(z,z)

These two terms differ by renaming a bound variable, so they should be equal. Indeed they unify.

Example 4: lambda(z,a) = lambda(z,x)

This is proved with the substitution x = a.

Example 5: lambda(w,a) = lambda(z,x).

Works the same as the previous example, even though the names of the bound variables are different.

Example 6: lambda(x,a) = lambda(z,x) would be illegal input, since x occurs both free and lambda-bound in the same clause.
The bound x would have to be renamed first. As of June 10, 2004, Otter-λ does not check the input file to enforce this condition, so it is possible to enter illegal input. The principle "garbage in, garbage out" applies. Eventually we will write code to detect and refuse such input.