Hans Aberg haberg at math.su.se
Sun Dec 7 05:48:25 EST 2008

On 7 Dec 2008, at 11:34, Luke Palmer wrote:

> On Sun, Dec 7, 2008 at 3:05 AM, Hans Aberg <haberg at math.su.se> wrote:
> One can define operators
>  a ^ b := b(a)          -- Application in inverse.
>  (a * b)(x) := b(a(x))  -- Function composition in inverse.
>  (a + b)(x) := a(x) * b(x)
>  O(x) := I              -- Constant function returning identity.
>  I(x) := x              -- Identity.
> and use them to define lambda calculus (suffices with the first
> four; Church reverses the order of "*").
>
> The simple elegance of writing this encoding just increased my
>
> a .^ b = b a
> (a .* b) x = b (a x)
> (a .+ b) x = a x .* b x
> o x = i
> i x = x
>
> toNat x = x (+1) 0
> fromNat n = foldr (.) id . replicate n

I have some more notes on this that you might translate, if possible
(see below).

If one implements integers this way, time complexity of the operators
will be of high order, but it is in fact due to representing n in
effect as 1+...+1. If one represents them, using these operators, in
a positional notation system, that should be fixed, though there is a

Hans

Associativity: a*(b*c) = (a*b)*c, a+(b+c) = (a+b)+c

RHS Relations:
a^O = I, a^I = a
a^(b * c) = (a^b)^c
a^(b + c) = a^b * a^c
a*(b + c) = a*b + a*c

LHS Relations:
I * a = a, O + a = a, O * a = I ^ a
c functor (i.e., c(a*b) = c(a)*c(b), c(I) = I) =>
(a*b)^c = a^c * b^c
(a+b)*c = a*c + b*c
I^c = I

If n in Natural, f: A -> A an endo-function, define
f^n := I,              if n = 0
f * ... * f,    if n > 1
|-n times-|
The natural number functionals, corresponding to Church's number
functionals, are then defined by
\bar n(f) := f^k
If S(x) := x + 1 (regular integer addition), then
\bar n(S)(0) = n

Also write (following Hancock)
log_x b := \lambda x b
Then
log_x I = O
log_x x = I
log_x(a * b) = log_x a + log_x b
log_x(a ^ b) = (log_x a) * b,    x not free in b.