Natural numbers and Peano

No types in logic programming

In pure logic programming, 3 and + are just symbols, with no specific meaning attached, and the same holds in pure Prolog. So how do we deal with, say, natural numbers? Giuseppe Peano shows us the way.

Peano axioms

The five Peano axioms, also known as Peano's postulates, were introduced in 1889 by the Italian mathematician Giuseppe Peano. Like Euclid's axioms for geometry, they were meant to provide a rigorous foundation for the natural numbers (0, 1, 2, 3, ...) used in arithmetic, number theory and set theory. In particular, they enable an infinite set to be generated by a finite set of symbols and rules.

1. Zero is a natural number.
2. Every natural number has a successor in the natural numbers.
3. Zero is not the successor of any natural number.
4. If the successor of two natural numbers is the same, then the two original numbers are the same.
5. If a set contains zero and the successor of every number is in the set, then the set contains the natural numbers (induction).

Natural numbers in logic programming

In logic programming, the Herbrand universe represents the elements of the domain of discourse, and the Herbrand base represents the elementary propositions over the domain of discourse. To represent natural numbers we therefore use constants and functors for the numbers, and predicates for relations such as n ∈ ℕ.

Our domain of discourse is ℕ, so our Herbrand universe needs to express the elements of ℕ. From the Peano axioms we understand that:

• zero is essential: we use z as the constant symbol for zero. This is not something belonging to the language, it is just our (pre-)interpretation of the symbol z for our current purposes;
• the notion of successor is essential, too: we use s/1 (s with arity 1) as the functor symbol for successor. If N is a natural number, then s(N) is another natural number, precisely the successor of N. This is a recursive data structure: the successor of s(N) is s(s(N)), which is another natural number.

In our pre-interpretation, z is zero, s(z) is one, s(s(z)) is two, and so on.

We focus on the simple relation n ∈ ℕ, that is, "n is a natural number", and we use nat/1 as its predicate symbol. If N is a variable, the atom nat(N) represents the proposition "N is a natural number", according to our current interpretation. For instance, nat(s(s(z))) means that two is a natural number.

Natural numbers in Prolog

A first program, the extensional representation: one fact per number.

nat(z).         % zero is a natural number
nat(s(z)).      % one is a natural number
nat(s(s(z))).   % two is a natural number
...

It needs an infinite number of clauses (facts) for infinite numbers, which is not exactly in the spirit of axiomatic systems, in particular of Peano's one: we just used facts. Rules are what trigger the intensional representation, with universal variables: a finite representation for (potentially) infinite propositions.

A second program (naturals.pl) uses a recursive rule for the intensional representation: one fact and one rule for infinitely many numbers.

Remarks:

• z is zero, 0 is not zero. 0 is an integer, a different term altogether.
• Recursive data structures are powerful and expressive, yet unreadable for humans, and generally impractical. This is why Prolog is actually impure logic programming, with predicates like ?- X is 1 + 3.
• Logic programming allows for the generation of data, e.g. the set of natural numbers, or the set of positive numbers (nat(s(N))).
• There is an unlimited number of SLD refutations: an infinite branch of the proof tree.
• The order of clauses matters in Prolog. What if we exchange the fact with the rule?

Checking a given number still works, but asking for any nat2(N) dives into the recursive rule forever without ever reaching the fact: with the clauses swapped, the generator never produces a first answer. The fact for the base case must come before the recursive rule.

Computing with naturals: sum/3

File naturals.pl continues with the sum, based on the same representation of ℕ:

sum(z, N, N).                   % zero plus N is N
sum(s(M), N, s(P)) :- sum(M, N, P).  % if M plus N is P, then adding N to
                                     % the successor of M returns the successor of P

sum/3 actually represents an equation in the form of a ternary relation: sum(X, Y, Z) means that X + Y = Z.

Remarks:

• again, z is zero and 0 is not zero (so goal 2 fails);
• there are no predefined input/output parameters for the sum/3 procedure: atoms represent equations;
• the system can generate possible solutions (goal 5 lists all 7 ways to split 6);
• equations can be combined in systems of equations (goal 6). It finds X = 2, Y = 4, and then keeps searching for more solutions forever: the notebook stops it after a bounded number of steps.