Laszlo Nemeth wrote:
> I somehow managed to delete Hans's earlier post in which he gives the
> definitions for + and ^. So I wanted to fetch them from the
> archive...which was last updated on the 28 May. Is the archive broken
> or just rarely updated?
>
> Thanks,
> Laszlo Nemeth
Somebody tried to suggest that lambda provides a kind of logarithm...
Well no, we are still within a classical arithmetics, far from the
Analysis. Here you are some definitions, much more sexy than those
written by Hans. Sorry if you know already all this.
0. Introduction. Andante moderato.
Within the Peano minimalistic philosophy, there are two
primitive objects, the successor (we will call it s) and the
zero (called z).
For example z = 0; or z=""
s x = 1+x; or s x = '*' : x
2. Generic Church numerals. Allegro ma non troppo.
Numbers are functions accepting two parameters, s and z.
For example:
zero s z = z
This is the const combinator.
one s z = s z
This is the id combinator. Cool, non?
two s z = s (s z); three s z = s (s (s z)); etc.
but we can't go too far in such a a way
3. Simple operations. Alegretto.
in general the intuitive definition of the number n is:
"Act n times with s upon z"
In order to add two numbers n1 and n2, act with n1 upon n2:
(n1 + n2) s z = n1 s (n2 s z)
(Transform this yourself into combinators. It is awful!)
4. Multiplication. Vivace.
The partially applied form (n s) where n is <<some>> number, is
a "super-successor"; s iterated n times.
So, in order to multiply n1 by n2, pass the n2 super-successor
to n1 as <<the>> successor.
(n1 * n2) s z = n1 (n2 s) z
But now we see that this is
(n1 * n2) s = n1 (n2 s) = (n1 . n2) s; or n1 * n2 = n1 . n2
5. Exponentiation. Allegro furioso.
(Personal comment. Always when I came here, my students cried,
jumped through the window, or turned green. I don't know why...)
First the solution:
(n1 ^ n2) s z = n2 n1 s z; or n1 ^ n2 = n2 n1
The <<intuitive>> justification is quite venerable. If you take
two finite discrete sets A and B, and if you compute the cardinality
of the function space A -> B, you will get B^A. This is not an
accident that this notation is used in the set theory. Differently,
we have to iterate the base n1 : n2 times, so (n2 n1) is the
answer. You may punish your students asking them to prove it
by recurrence.
6. Subtraction. Largo.
According to some folklore Church himself thought for some time
that it is not possible to define the subtraction using pure
lambdas.
In fact it is possible to subtract Church numerals (but never
getting negative numbers, of course) The following solution is
silly, but please find a *really* better one...
First the incrementation: inc n s z = n s (s z)
(You may use it also to define the addition.)
Then the iteration defining the decrement
dec n = d zer where
zer s z = z
v = n s z -- global constants
d m = let h = inc m
in if h s z == v then m else d (inc m)
and the subtraction is the iterated decrement. Its complexity
is really bad (n^2).
===
That's it, I don't think you should ever use it. I don't understand
the Hans remark about making from +, * etc. the primitive basis
for the set theory. What's so primitive about them? Oh, to compute
the cardinals, etc. maybe.
But it is nice for teaching.
Best regards
Jerzy Karczmarczuk
Caen, France.
