Church numerals in Haskell
"Jerzy" == Jerzy Karczmarczuk [EMAIL PROTECTED] writes: Somebody tried to suggest that lambda provides a kind of logarithm... In defense of it I can offer the following laws, which follow from the eta-rule of lambda calculus. Just regard log_x ... as alternative notation for \ x - ... log_x (a * b) = log_x a + log_x b log_x 1 = 0 log_x x = 1 log_x (a ^ b) = (log_x a) * b , x not free in b . I only meant that if abstraction and application are somehow inverse, and if application is exponentiation, then abstraction must be some kind of logarithm, and in a strange formal sense it does seem to satisfy some of the crucial laws. -- Peter
Church numerals in Haskell
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.
Re: Church numerals in Haskell
"Hans" == Hans Aberg [EMAIL PROTECTED] writes: In real life though, it is very difficult to translate an arbitrarily given lambda expression into a combination of the given primitive set. I cannot resist illustrating Hans's point. This is the sort of thing that comes up... (((V "^" :*: V "0" :^: V "*" :+: (V "^" :*: V "0" :^: V "*") :^: V "+" :*: V "*") :+: (V "Junk" :^: V "^") :^: V "^") :+: V "*") :+: (V "Junk" :^: V "^") :^: V "^" So for practical purposes, there is no real gain in attempting to use a primitive set as a replacement for lambda expressions. Maybe it isn't entirely futile to think about it though. Reduction to combinators is the sort of thing that compilers do. I sometimes wonder if there is any interest for compilers in the fact that the only non-affine combinator (i.e. duplicating an argument) is +. Maybe there is a garbage-collection angle. By the way, I'm not wild about Hans's term "constant variables". In Church's lambda-I calculus, you aren't allowed abstractions where the bound variable doesn't occur in the body. It would be better to distinguish linear (exactly once), affine (at most once), and general abstraction. All 0, 1, * and ^ are affine, but + is not. All 1, * and ^ are linear, but 0 is not. Reduction of affine combinators needs essentially no new space, I think. It is amusing to think of an arithmetic machine (a bit like the G-machine maybe) that spends most of its time collecting the garbage generated by an occassional addition. -- Peter
Re: Church numerals in Haskell
At 13:39 +0100 1999/06/03, Jerzy Karczmarczuk wrote:
... I don't understand
the Hans remark about making from +, * etc. the primitive basis
for the set theory. What's so primitive about them?
A set of lambda expressions is called primitive if all other lambda
expressions can be generated from it by finite combinations. Church also
requires that the members of the set are not themselves finite combinations
(of the form AB), and that they contain no free variables. (So this is the
same use of the word when constructing data bases and the like: One has
some kind of algebra, and a primitive set is what generates it.)
So if one has the set S = { I, +, *, ^ }, then the lambda is not needed for
the purpose of constructing formulas with only non-constant variables. If
you want to allow formulas with constant variables, then Peter Hancock
[EMAIL PROTECTED] says that { O, +, *, ^ } suffices.
In real life though, it is very difficult to translate an arbitrarily given
lambda expression into a combination of the given primitive set. So for
practical purposes, there is no real gain in attempting to use a primitive
set as a replacement for lambda expressions.
Hans Aberg
* Email: Hans Aberg mailto:[EMAIL PROTECTED]
* Home Page: http://www.matematik.su.se/~haberg/
* AMS member listing: http://www.ams.org/cml/
Re: Church numerals in Haskell
At 13:46 +0100 1999/06/03, Peter Hancock wrote:
Just regard log_x ... as alternative
notation for \ x - ...
log_x (a * b) = log_x a + log_x b
log_x 1 = 0
log_x x = 1
log_x (a ^ b) = (log_x a) * b , x not free in b .
These are interesting relations in some sense, even though it is hard to
immediately see what to do with them.
What one can do though is to take say the primitive set S = { I, +, *, ^ }
plus the obvious relations R they satisfy (like associativity, and some
other such relations). Then is the question is, is (S; R) equivalent to the
set of all lambda expressions? -- The difference is that when using the
primitive set S only, we subsume the relations in the algebra of lambda
expressions, but here we try to express these relations explicitly.
Hans Aberg
* Email: Hans Aberg mailto:[EMAIL PROTECTED]
* Home Page: http://www.matematik.su.se/~haberg/
* AMS member listing: http://www.ams.org/cml/
Re: Church numerals in Haskell
Jerzy Karczmarczuk wrote: 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). Compared to using equality, I think the following is really better: dec n = fst (n (\(_,b)-(b,inc b)) (zer,zer)) where zer s z = z Of course, you wouldn't really use built-in pairing, would you? Christian Sievers
Re: Church numerals in Haskell
At 15:37 +0100 1999/06/03, Peter Hancock wrote: By the way, I'm not wild about Hans's term "constant variables". In Church's lambda-I calculus, you aren't allowed abstractions where the bound variable doesn't occur in the body. It would be better to distinguish linear (exactly once), affine (at most once), and general abstraction. All 0, 1, * and ^ are affine, but + is not. All 1, * and ^ are linear, but 0 is not. Reduction of affine combinators needs essentially no new space, I think. I think Church's restriction that a bound variable must occur in the bound expression is more technical in nature, but not essential in a practical application. The thing is that the lambda-calculus does not come with an interpretation of the symbols. So if one adds (in an interpreation of the lambda-calculus) a symbol O such that O(f)(x) = x, then lambda x.O(x)(f) where f does not contain x is a legal expression in Church's calculus, but this expresion becomes equivalent to lambda x.f when O(x)(f) = f is substituted. Here O lambda a b . b, as before. Hans Aberg * Email: Hans Aberg mailto:[EMAIL PROTECTED] * Home Page: http://www.matematik.su.se/~haberg/ * AMS member listing: http://www.ams.org/cml/
