Peano Module Users' Manual

Purpose

This document provides information on using the predicates exported from the peano module.

The concept of Number is an interesting one: although used since antiquity, the formal definition of Number was not found until the very end of the 19th century.¹ Numbers can be represented in many different ways: the Roman numerals were a complex form of tallying, we currently use digits based on their Arabic antecedents, and computers agree to the string of binary digits as defined by the IEEE. Just as there are many different ways of expressing numbers in human- (or machine-) readable forms, mathematical philosophy allows different ways to express numbers: the Peano series mirrors (a simplified form of) the tallying under the Roman counting method;² Church numerals, expressed in terms of two variables using the pure lambda calculus, is a very different approach to tallying,³ and a third approach uses pure lambda terms of N variables to express base_N-1 numerals.⁵

Given the different representations, what makes one representation better than another? Or, why build a module around tallying when Prolog already has built-in predicates that handle their IEEE representation natively? The fundamental issue is determinism: the peano series is a binary type -- it's either zero or a successor; therefore, it's very easy to write predicates that fall into a binary division of labour using the Peano series, whereas in the IEEE representation such division is not natural. Not only is the declarative syntax more nature with the Peano series, but when such a binary relationship arises in predicates, using Peano numerals eliminates choice points -- predicates indexed with Peano numerals usually have a run-time advantage over IEEE ones by a factor of forty.

The caveat using Peano numerals is that converting to and from Peano numerals from their IEEE counterparts incurs the cost of nondeterminism (leaving choice points and incurring run-time costs); and, since Roman times, humans find the IEEE/Arabic numerals much easier to read than their Peano/tallying/Roman counterparts. As the Peano series maps directly to the Natural number series, its natural state is when working with zero or positive integers: negative and fractional numbers require programming effort and should therefore be avoided if possible. These costs must be considered to use the Peano series effectively.

:- module(peano)

Exported Predicates

The peano module exports the following predicates:

peano/2
increment/2

Exported Operators

This module does not export any operators.

peano/2

Synopsis: peano(?Integral, ?Peano)

Arguments:

Integral	<integer>	a non-negative integer
Peano	<term>	The term of the binary type 'peano'
where `:- type(peano) ---> zero; s(peano).`

Description:

This predicate converts between non-negative integers and Peano numerals.

Backtracking:

As for any nondeterministic goal.

Examples:

The first example is a result of tallying referrals in an ordered set of real-estate:

count_referrals([Sale|Sales], zero, Refs),
peano(Referrals, Refs).

We count the referrals in the sales (starting from zero) then convert that Peano term to an integral.

The next example takes an integral, converts it to a Peano term, then uses that Peano term to collect the elements requested:

% take/[3,4] returns the first N elements of a list

take(N, In, Out) :-
  peano(N, Peano),
  take(Peano, In, Out, []).
take(s(Peano), [H|T]) --> [H], take(Peano, T).
take(_, []) --> [].
take(zero, _) --> [].

The same method works for the foil to take/[3,4]:

% drop removes the first N elements ... its implementation is much
% simpler as there's no need for accumulating the first N elements (as
% in take/[3,4]).

drop(N) --> { peano(N, Peano) }, drop_aux(Peano).
drop_aux(s(Peano)) --> pop(_) -> drop_aux(Peano); [].
drop_aux(zero) --> [].

The latter two examples demonstrate a trade-off consideration in using the peano module: we pay the cost of non-determinism once at the beginning when the integral is converted to a peano term; and therefore eliminate the repetitive costs at each recursive call in the auxiliary predicate.

increment/2

Synopsis: increment(?Peano₀, ?Peano₁)

Arguments:

Peano₀	<term>	a term of type 'peano' described above; the predecessor of Peano₁
Peano₁	<term>	a term of type 'peano' described above; the successor to Peano₀

Description:

Useful predicate for tallying when the DCG (implicit in/out) arguments are peano numerals.

Backtracking:

Semideterimistic, except for the erroneous call increment(X, X); as most Prologs do not have automatic occurs-check, this will result in infinite regression.

Example:

This example demonstrates a predicate that, when given a real estate sale, increments the implicit Peano term if that sale came from a referral:

sale_referral_count(Sale) --> { referred(Sale) } -> increment; [].
%    Bumps the referral (peano) count on a referral
%    from another sale.

Endnotes

An engrossing retelling of the finding of the definition of Number, including the missteps made by Euclid up to Peano in that quest, can be found in [Rus1919], chapters 1 and 2.

As the Peano series has a simple one-to-one mapping to sets, it is used there (see, e.g., [Jec2002], § 4 "Natural Numbers"), and also in propositional logic, such as for Gödel's proof (see, e.g., [NNH2001]).

Church numerals are particularly popular in the functional programming community:⁴ they work by applying a function repeatedly to a (in the abstract) deferred value. So:

x^x = λx.(xx)

succ x = λa.λf.λx.(f ((a f) x))

a * b = λa.λb.λf.(a (b f))

a^b = λa.λb.(b a)

0 = λf.λx.x

1 = λf.λx.(fx)

2 = λf.λx.(f(fx))

3 = λf.λx.(f(f(fx)))

4 = 2²

5 = (succ 4)

6 = (2 * 3)

7 = (succ 6)

8 = 2³

9 = 3²

...

16 = λx.(((xx)x)2) ≡ (2² 2) ≡ 2⁴

...

256 = 4⁴

⁴

So much so that the higher-order function, power, is in the canon of functional programming libraries. The power function returns a function representing the Church numeral of the number input.

⁵

Base_N lambda representations (particularly binary ones) are demonstrated in [Kee96]. So, for example, an encoding of numerals similar in style to the IEEE standard can be done with a lambda expression of three variables (where the a-variable represents binary-1 and where the b-variable represents binary-0 and binary numerals are represented in an inverted fashion with the least significant bit first, where leading zeros are truncated):

101 = 9 = λa.λb.λx.(((ab)a)x)

100 = 8 = λa.λb.λx.(((bb)a)x)

10111101100001 = 12129 = λa.λb.λx.((abbbbaabaaaaba)x)

Works Consulted

[Jec2002]	"Basic Set Theory", Thomas Jech, Stanford Encyclopedia of Philosophy, http://plato.standford.edu/entries/set-theory/primer.html, 2002.
[Kee1996]	"To Dissect a Mockingbird: A Graphical Notation for the Lambda Calclus with Animated Reduction", David C. Keenan, http://up.net.au/~zzdkeena, 1996.
[NNH2001]	Gödel's Proof (Revised Edition), Ernest Nagel and James R. Newman, edited and with a new foreward by Douglas R. Hofstadter, New York University Press, NY, 2001.
[Rus1919]	Introduction to Mathematical Philosophy, Bertrand Russell, Dover Publications, Inc., NY, 1993.

author:	Douglas M. Auclair (doug at cotilliongroup dot com)
created:	August 22, 2005
last modified:	May 28, 2008
Copyright © 2005-8, Cotillion Group, Inc. All rights reserved.