λ-calculus is the calculus deals with only one data type: function. The simpliest (thus main) numeric type in it is the natural number.
Its sign might look strange at first sight, but it’s actually easy:
0 ≡ λsz.z
1 ≡ λsz.sz
2 ≡ λsz.s(sz)
3 ≡ λsz.s(s(sz))
4 ≡ λsz.s(s(s(sz)))
It goes like this: each function has two arguments, the first (s
) is the increment (or successor) function, and the second is the zero (z
).
- The zero function returns zero (
z
); - The one function return the zero’s successor (
sz
, 1); - The two function return the one’s successor (
s(sz)
, 2); - And so on.
Some programming languages brings natural numbers built-in. For example, Idris defines natural numbers like this:
data Nat : Type where
Z : Nat
S : Nat -> Nat
Z
is zero, S Z
is one, S $ S Z
is two, S $ S $ S Z
is three, and so on.
Prolog
It’s possible to emulate this behaviour using Prolog.
First we need a predicate to define natural numbers according to the λ-calculus. It could be nat/1
, like in Idris:
nat(z).
nat(s(N)) :- nat(N).
It’s solved!
Casting to integer
Hereat, we’ll convert into and from integer type.
An easy way of casting into integer is:
to_int(z, 0).
to_int(s(N), R) :- to_int(N, R1), R is R1 + 1.
It could be a solution, but there’s an issue: to_int/2
accumulates function stacks, perchange easily leading to a stack overflow.
We can solve it by tail-call optimisation: the to_int/2
must delegate the procedure to its accumulating version to_int/3
.
So to_int/2
becames:
to_int(N, R) :- nat(N), to_int(N, 0, R).
And the accumulating version to_int/3
should be:
to_int(z, A, A).
to_int(s(N), A, R) :- succ(A, A1), to_int(N, A1, R).
Or, using DCG:
to_int(z) --> '='.
to_int(s(N)) --> succ, to_int(N).
Casting from integer
For the backward casting, we’ll need a natural successor predicate for s(N)
:
nat_succ(N, s(N)) :- nat(N).
Here’s the from_int/2
(and its pair from_int/3
):
from_int(I, R) :- integer(I), I >= 0, from_int(I, z, R).
from_int(0) --> '='.
from_int(I) --> { I1 is I - 1 }, nat_succ, from_int(I1).
Let’s see it working
Save it all into natural.pl
, and then:
sh$ swipl -q
:- [natural].
true.
:- natural:to_int(z, X).
X = 0.
:- natural:to_int(s(s(s(z))), X).
X = 3.
:- natural:from_int(8, X).
X = s(s(s(s(s(s(s(s(z)))))))).
Making it executable
Append to the natural.pl
’s end:
go :- current_prolog_flag(argv, [Argv]),
atom_to_term(Argv, I, []),
from_int(I, N),
writeln(N), !.
go :- current_prolog_flag(os_argv, [_, '-x', Path | _]),
file_base_name(Path, Script),
format('use: ~w <integer>~n', [Script]).
Then, compile it:
sh$ swipl -q
:- [library(qsave), natural].
true.
:- qsave_program(natural, [init_file('natural.pl'), goal(natural:go), toplevel(halt)]).
true.
:-
Finally you can run:
sh$ ./natural 12
s(s(s(s(s(s(s(s(s(s(s(s(z))))))))))))
sh$
Bonus: even and odd
We can determinate if a natural number is even or odd by:
even(z).
even(s(N)) :- odd(N).
odd(N) :- \+ even(N).
Note: \+
means logic negation.
Top comments (1)
I have actually enjoyed reading this