Peano arithmetic

Programming data types

A data type is a construction plus algorithms. The construction is defined by deciding the functors (name and arity) for the terms; the algorithms are predicates, with a mapping from functions to relations.

Recall the features of an algebraic data type: a name for the type; a set of values, expressed by sums of products; and a set of I/O pure functions, often using recursion.

In Prolog we have no types, hence no enforcement:

• the name can only impact the names of values and functions;
• values are expressed by a set of functors, e.g. cons/2 and nil/0;
• a function f : I1, I2, ..., In ↦ O becomes a predicate p(I1, I2, ..., In, O). Functions are defined (in the body) as a composition of goals: h(X) = f(g(X)) becomes h(X, Y) :- g(X, Z), f(Z, Y). ideally using matching on functors. Functions returning booleans might have special treatment.

Example: naturals by Peano numbers

Encoding natural numbers is traditionally the next step after booleans while studying a language's expressiveness. An easy encoding is the unary, Peano one: Z, SZ, SSZ, SSSZ, SSSSZ, ..., so for instance SSZ + SSSZ = SSSSSZ. (Prolog will actually have an ad-hoc management of numbers and booleans.)

The ideas:

• use the functors s/1 and zero/0, e.g. s(s(s(zero)));
• the succ function is easily obtained by s/1 construction;
• sum is obtained recursively from succ or s/1: a + 0 = a, a + s(b) = s(a + b);
• mul is obtained recursively from sum: a * 0 = 0, a * s(b) = a + (a * b);
• we should be able to implement factorial;
• the output is the last argument, as usual.

The solution (peano.pl):

How to read the specification in the relational interpretation:

• the successor of X is s(X);
• the sum of X and zero is X;
• the sum of X and the successor of Y is the successor of Z, provided the sum of X and Y is Z;
• et cetera.

The goals:

The last goal shows the relational nature of the encoding: sum run backwards enumerates every pair of naturals adding up to 3.

The resolution of sum(s(s(s(zero))), s(s(zero)), N) unfolds as:

sum(s(s(s(zero))), s(s(zero)), N)
sum(s(s(s(zero))), s(zero), Z') : {N/s(Z')}
sum(s(s(s(zero))), zero, Z'')   : {N/s(Z'), Z'/s(Z'')} ≡ {N/s(s(Z''))}
{N/s(Z'), Z'/s(Z''), Z''/s(s(s(zero)))} ≡ {N/s(s(s(s(s(zero)))))}

The factorial, which the program is built for:

Functions returning a boolean

File greater.pl. The typical Prolog approach is not to add an argument being b_true or b_false, but rather: f : I1, I2, ..., In ↦ bool becomes p(I1, I2, ..., In), and the result is whether the call to the predicate fails or succeeds. In fact, one such function is a predicate. This way, we can only implement what should happen in the positive cases.

Multiple output arguments

File nextprev.pl. Again, rather than an output of type pair: f : I1, ..., In ↦ O1 × O2 becomes p(I1, ..., In, O1, O2). In fact, we can conceptually have many inputs and many outputs.

Multiple results

File range.pl. Typically in Prolog, a function returning a lazy list, f : I1, ..., In ↦ LazyList, becomes p(I1, ..., In, O) such that it provides multiple solutions through the inherent resolution mechanism. We should always be prepared for goals to admit many solutions.

The resolution tree of range(zero, s(s(s(zero))), N) produces one solution per level, then fails on the last level because greater no longer holds:

range(zero, 3, N)
├── {N/zero}
└── greater(3, zero), range(s(zero), 3, N)
    ├── {N/s(zero)}
    └── greater(3, 1), range(s(s(zero)), 3, N)
        ├── {N/s(s(zero))}
        └── greater(3, 2), range(s(s(s(zero))), 3, N)
            ├── {N/s(s(s(zero)))}
            └── greater(3, 3), ...   → No