DEV Community

Cover image for Prolog Natural Numbers
Montegasppα Cacilhας
Montegasppα Cacilhας

Posted on • Edited on

Prolog Natural Numbers

#functional #logic #prolog

λ-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)))
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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).
Enter fullscreen mode Exit fullscreen mode

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.
Enter fullscreen mode Exit fullscreen mode

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).
Enter fullscreen mode Exit fullscreen mode

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).
Enter fullscreen mode Exit fullscreen mode

Or, using DCG:

to_int(z) --> '='. to_int(s(N)) --> succ, to_int(N).
Enter fullscreen mode Exit fullscreen mode

Casting from integer

For the backward casting, we’ll need a natural successor predicate for s(N):

nat_succ(N, s(N)) :- nat(N).
Enter fullscreen mode Exit fullscreen mode

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).
Enter fullscreen mode Exit fullscreen mode

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)))))))).
Enter fullscreen mode Exit fullscreen mode

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]).
Enter fullscreen mode Exit fullscreen mode

Then, compile it:

sh$ swipl -q :- [library(qsave), natural]. true. :- qsave_program(natural, [init_file('natural.pl'), goal(natural:go), toplevel(halt)]). true. :-
Enter fullscreen mode Exit fullscreen mode

Finally you can run:

sh$ ./natural 12 s(s(s(s(s(s(s(s(s(s(s(s(z)))))))))))) sh$
Enter fullscreen mode Exit fullscreen mode

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).
Enter fullscreen mode Exit fullscreen mode

Note: \+ means logic negation.

Top comments (1)

Collapse
 
miguelmj profile image
MiguelMJ •

I have actually enjoyed reading this