Lambda

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with all sections Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of the license is included in the file "fdl.txt" included in this distribution.

1 Commands

1.1 load

1.2 list

1.3 set

1.4 def

1.5 ext

1.6 lambda-expression

1.7 quit

2 Expressions

2.1 Syntax

2.2 Semantics

2.2.1 Definition of "free"

2.2.2 Definition of "bound"

2.2.3 Substitution Rules

2.2.4 Conversion Definitions

2.2.5 Variable Name Prefixes

3 Arithmetic

3.1 Basic Definitions

3.2 Proposition for Addition

3.3 Proposition for Multiplication

3.4 Proposition for Exponentiation.

3.5 Proposition for Predecessor

3.6 Examples

4 Lists

4.1 Nodes

4.2 Empty List

4.3 Appending

4.4 Mapping

5 Functional Completeness of Curry Algebras

5.1 Proposition 1 Abstractions in Schönfinkel Algebras.

5.2 Proposition 2. Existence of Curry Algebras.

5.3 Proposition 3 Curry Algebras ≡ Lambda Calculus.

5.4 Proposition 4 Fixed Points in Curry Algebras.

---

1 Commands

1.1 load

load <definition-filename>

When lambda first starts it prints the current directory. If the definition file is in this directory, <directory-filename> can be just the filename (so long as the filename is just one word). Otherwise, the filename should be enclosed in double quotes.

For example:

load definitions
load "../share/definitions"


1.2 list

list

List all current definitions in reverse order. That is, the more recent definitions are printed first.

1.3 set

set [<flag>]...
<flag> = trace | step | thru | app | body | brief | sym | eta | xapp | full | alpha

Set or clear flags. The flags govern the way in which expressions are evaluated and printed. The set command used without any flags or with a flag which it doesn't recognize will print a list the flags and their current state, after executing the commands. The meaning of each flag is as follows:

trace	If set, prints a sub-expression just before it is reduced. Default: not set.
step	if set, one reduction is done at a time, the result printed, and the user prompted to continue or stop reduction of this expression. Default: not set.
thru	Works the same as step, except that the expression is reduced to normal form without pausing between each reduction to print the expression and prompt the user. Setting one of these flags (step or thru) will cause the other to be cleared. If neither flag is set, the expression is reduced using a recursive descent method, which should be faster. This method should result in the reductions being performed in the same order as the one reduction at a time method used when step or thru are set. However, it may not always. Default: not set.
app	If set, do the reductions in "applicative order," which means reduce the "rand" of an application before reducing the application. If not set, perform the reductions in "normal order", which means, do the left-most reduction in the expression first. Default: not set.
body	If set reduce the body of a abstraction, even though it is not the rator of an application. Default: not set. Setting body is necessary in order to make arithmetic work correctly: MUL 2 2 ==> 4.
brief	If set, use a more compact method of printing an expression, in which unnecessary parenthesis or elided. If not set, extra parenthesis are printed to indicate the left-to-right association nature of applications. Default: set.
sym	If set, causes sub-expressions to be matched to definitions when printing an expression. Whenever a match is found, the name of the definition is printed in place of the value, which result in a more compact representation. No attempt is made to preform alpha conversions to match expression, although this would be a good idea for future versions of this program. (An "alpha" conversion allows the name of the argument of an abstraction to be changed.) Default: set.
eta	If set: ext x f x ==> f. If not set: ext x f x ==> S(K f)I.
xapp	If set: ext x f g ==>S(K f)(K g). If not set: ext x f g ==>K(f g).
full	If set, causes names to be completed expanded, by looping over the definitions until no more expansions can be done. May result in recursive loops. Default: set.
alpha	If set, causes expressions to be alpha converted into a canonically named form before matching them for output display with definitions in the environment (which are also so converted). Each lambda argument is re-assigned a unique name from the sequence ~~1, ~~2, ... , from left to right.

1.4 def

def <name> <lambda-exp>

Make a definition, associating <name> with <lambda-exp> in subsequent reductions. If the name is already in use in a previous definition, that definition is replaced with the new one. If the lambda expression contains unbound variables, they may be captured by arguments of abstractions when the lambda expression is substituted for the definition name in the reduction process.

1.5 ext

ext <var> <lambda-exp>

Extract the variable <var> from the lambda-exp <lambda-exp> so that

(ext <var> <lambda-exp>) <var> == <lambda-exp>


If instead of a variable name <var> is the character ^ or ~,

(ext ^ <lambda-exp>) == <lambda-exp>
(ext ~ <lambda-exp>) == <lambda-exp>


The <lambda-exp> is replaced by S, K, and I combinators, as follows:

expression	result	remark
ext x x	I
ext x A	K A	A is a single symbol other than x
ext x A	K (A)	x is not free in A and A is an application expression and xapp is off
ext x lambda-exp	ext x (ext lambda-exp.arg lambda-exp.body)
ext x exp1 exp2	S (ext x exp1)(ext x exp2)	exp1 and exp2 both constant and xapp is on or exp1 and ext2 not both constant and exp2 is not x or exp1 is x and eta is off))
ext x exp1 x	S (ext x exp1)(ext x exp2)	eta is on
ext ^ x	x
ext ^ lambda-exp	ext lambda-exp.arg lambda-exp.body
ext ^ exp1 exp2	(ext ^ exp1)(ext ^ exp2)

The definitions of S, K, and I are

I a = a
K a b = a
S a b c = a c( b c)


I is often defined as S K K.

For example,

<< set
>trace = 0
>step  = 0
>thru  = 0
>app   = 0
>body  = 0
>brief = 1
>sym   = 1
>eta   = 1
>xapp  = 0
>full  = 1
<< ext x E x
E
<< set eta
<< ext x E x
S(K E)I
<< ext x A B
K(A B)
<< set xapp
<< ext x A B
S(K A)(K B)
<< ext x ^y.x y
S(S(K S)(S(K K)I))(K I)
<< set eta
<< ext x ^y.x y
I
<< ext ^ ^x.^y.x y
I
<< ext ^ ^x.^y.y x
S(S(K S)(K I))K
<<

1.6 lambda-expression

<lambda-exp>

Reduce the lambda-expression. However, if the lambda expression is just a single variable, print its definition. When a expression is reduced, it is first parsed into an internal expression tree form, printed (in the "non-brief" format), and reduced again as directed by the flags. The final result (and any intermediate results, if the step flag is set) is printed as directed by the brief and sym flags. When in the step mode, for each intermediate or final result, an "B" is incorporated into the result cue to indicate a "beta" reduction was performed, and an "H" is incorporated to indicated a "eta" reduction was performed.

A user cue of

<<

used to indicate input is needed. An a command is terminated by a new line. However, if a lambda-expression is being reduced and a new line is encountered with parentheses unbalanced, the user is prompted to supply the missing right parentheses.

Parsed results are printed after the cue:

==>

In the step mode, intermediate and final results are printed after the cue:

=B==>

which indicates an "beta" reduction was peformed, or

=H==>

which means an "eta" reduction was performed. The cue

===> is used for final results when not in the step mode.

1.7 quit

quit

Quit.

2 Expressions

2.1 Syntax

<lambda-exp> = <variable>
| ^<variable>.<lambda-exp>
| <lambda-exp> <lambda-exp>
| (<lambda-exp>)


2.2 Semantics

The form ^<variable>.<lambda-exp> is called an "abstraction." The variable after the ^ and before the period is called the argument, and the lambda expression after the period is called the body. The body extends until the end of the expression, or until a right parenthesis is encountered which is unmatched by a corresponding left parenthesis in the body expression.

The form <lambda-exp> <lambda-exp> is called an application. The first lambda expression is called the operator (or rator for short) and the second is called the operand (or rand for short.) When an rator of an application is an abstraction, an application can be reduced by substituting the rand into the body of the abstraction in place of each occurrence of the abstraction's argument. This must be done in such a way as to avoid an name collisions with the arguments of other abstractions which might be embedded in the body of the abstraction. The application operation is left-associative, which means that the expression

a b c d

means

((a b) c) d.

2.2.1 Definition of "free"

Variable x occurs free in an expression:
1. x occurs free in x (but not in any other variable);
2. x occurs free in X Y if x occurs free in X or Y;
3. x occurs free in ^y.Y if x and y different and x occurs free in Y;
4. x occurs free in (X) if x occurs free in X.

2.2.2 Definition of "bound"

Variable x occurs bound in an expression:
1. No variable occurs bound in an expression consisting of just a single variable;
2. x occurs bound in ^y.Y if x and y are the same variable (and x occurs free in Y), or if x occurs bound in Y.
3. x occurs bound in X Y if it occurs bound in X or Y.
4. x occurs bound in (X) if it occurs bound in X.

2.2.3 Substitution Rules

Substitute expression M for variable x in expression X
[M/x]X

Case	Condition	Rule: [M/x]X ==>
1	X is a Variable
1.1	X == x	M
1.2	X != x	X
2	X is a Application: Y Z	([M/x]Y)([M/x]Z)
3	X is an Abstraction: ^y.Y
3.1	y == x	X
3.2	y != x
3.2.1	x doesn't occur free in Y or y doesn't occur free in M	^y.[M/x]Y
3.2.2	x does occur free in Y and y does occur free in M (a collision)	^z.[M/x]([z/y]Y) where z is the first variable in the sequence of variables such that z doesn't occur free in M or Y. That is, change all free occurrences of y in Y to z, then replace occurrences of x in Y with M. The argument of the abstraction is changed from y to z.

2.2.4 Conversion Definitions

Conversion	Definition
α	if y is not free in X, then ^x.X cnv(&alpha) ^y.[y/x]X
β	(^x.M)N cnv(β) [N/x]M
η	if x is not free in M, then ^x.M x cnv(η) M.

A reduction means going from left to right with a β or η conversion; that is, getting rid of a ^. Normal order means getting rid of the left most ^ first. Applicative order means reducing the rand before the rator.

2.2.5 Variable Name Prefixes

Prefix	Meaning
$	If the argument of an abstraction has $ as its first character, the abstraction, when it is being reduced as part of an application, will be reduced as though the step flag were off, and the body flag were on.
&	If the argument of an abstraction has & as its first character, the abstraction will be reduced as though the step and body flags are both off.

3 Arithmetic

3.1 Basic Definitions

Let

[m]	represent the lambda expression for the postive integer m,
[0]	^x.^y.y
[n+1]	^x.^y.x([n] x y) for all n > 0
ADD	^m.^n.^x.^y.m x(n x y)
MUL	^m.^n.^x.m(n x)
EXP	^n.^m.m n

3.2 Proposition for Addition

ADD [m][n] = [m+n]
Proof	By induction
1)	ADD [0] [n] = ^x.^y.[0] x.([n] x y) = ^x.^y.[n] x y = [n] = [0+n]
2)	Assume ADD [m][n] = [m+n]	induction hypothesis
3)	ADD [m+1][n] = ^x.^y.[m+1] x([n] x y) = ^x.^y.(^a.^b.a([m] a b)) x ([n] x y) = ^x.^y.x([m] x ([n] x y) = ^x.^y.x(ADD [m] [n] x y)
=>	= ^x.^y.x([m+n] x y)	by 2) induction hypothesis
	= [(m+1)+n]

3.3 Proposition for Multiplication

MUL [m][n] = [m*n]
Proof	By induction
1)	MUL [0] [n] = ^x.[0]([n] x) = ^x.(^a.^b.b)([n] x) = ^x.^b.b = ^x.^y.y = [0]
2)	Assume MUL [m][n] = [m*n]	induction hypothesis
3)	MUL [m+1] [n] = ^x.[m+1]([n] x) = ^x.(^a.^b.a([m] a b))([n] x) = ^x.^b.([n] x)([m] ([n] x) b) = ^x.^b.([n] x)(MUL [m] [n] x b)
=>	= ^x.^b.([n] x)([m*n] x b)	by 2) induction hypthesis
	= ^x.^b.ADD [n] [m*n] x b = ^x.^b.[n+m*n] x b = [n+m*n] = [(m+1)*n]

3.4 Proposition for Exponentiation.

EXP [n][m] = [n**m]
Proof	By induction
1)	EXP [n] [0] = [0] [n] = (^x.^y.y)[n] = ^y.y = ^y.^z.y z = [1]
2)	Assume EXP [n][m] = [n**m]	induction hypothesis
3)	EXP [n] [m+1] = [m+1] [n] = (^x.^y.x([m] x y))[n] = ^y.[n]([m] [n] y) = ^y.[n](EXP [n] [m] y)
=>	= ^y.[n]([n**m] y)	by 2) induction hypothesis
	= MUL [n] [n**m] = [n*(n**m)] = [n**(m+1)]

3.5 Proposition for Predecessor

pred [n] = [n-1] Let suc = ^n.^x.^y.x(n x y) pair = ^f.^s.^p.(p f s) false = ^f.^s.s true = ^f.^s.f and bump = ^p.pair (suc(p true)) (p true) pred_pair = ^n.n bump (pair 0 0) pred = ^n.pred_pair n false then pred_pair [n] = pair [n] [n-1] hence pred [n] = [n-1]
Proof	By induction
1)	pred_pair [1] = 1 bump (pair 0 0) = bump (pair 0 0) = pair (suc((pair 0 0) true)) ((pair 0 0) true)) = pair 1 0
2)	Assume pred_pair [n] = pair [n] [n-1]	induction hypothesis
3)	pred_pair [n+1] = ^n. (n bump (pair 0 0))[n+1] = [n+1] bump (pair 0 0) = bump ([n] bump (pair 0 0)) = bump (pred_pair [n])
=>	= bump (pair [n] [n-1]) = pair [n+1] [n]	by 2) induction hypothesis
4)	pred [n] = pred_pair [n] false = pair [n] [n-1] false = false [n] [n-1] = [n-1]

3.6 Examples

def 0 ^m.^n.n
def true ^p.^q.p
def def false ^p.^q.q
def suc ^p.^m.^n.m(p m n)
def pred ^$k.$k(^p.(mpair(suc(p true))(p true)))(mpair 0 0)false
def mpair ^a.^b.^u.u a b
def def iszero ^n. n (true false) true
def ADD ^m.^n.^x.^y.m x(n x y)
def MUL ^m.^n.^f.m(n f)
def EXP ^m.^n.n m
def GT ^m.^n.not(iszero (n pred m))
def EQ ^m.^n.and (iszero (m pred n)) (iszero (n pred n))
def LT ^m.^n.not(iszero(m pred n))
def GE ^m.^n.not(LT m n)
<< iszero 0
==> iszero 0
====>true
<< iszero 5
==> iszero 5
====>false
<< suc 0
==> suc 0
====>I
<< suc 1
==> suc 1
====>2
<< suc 2
==> suc 2
====>3
<< pred 3
==> pred 3
====>2
<< pred 2
==> pred 2
====>I
<< pred 1
==> pred 1
====>0
<< pred 0
==> pred 0
====>0
<< ADD 1 2
==> (ADD 1) 2
====>3
<< MUL 2 3
==> (MUL 2) 3
====>6
<< EXP 2 3
==> (EXP 2) 3
====>8
<< EXP 3 2
==> (EXP 3) 2
====>9
<< GT 2 3
==> (GT 2) 3
====>false
<< GT 3 2
==> (GT 3) 2
====>true
<< EQ 4 (ADD 2 2)
==> (EQ 4)((ADD 2) 2)
====>true
<< EQ 5 (ADD 3 3)
==> (EQ 5)((ADD 3) 3)
====>false
<<

4 Lists

4.1 Nodes

The basis of a list is the triple:

def mtriple ^a.^b.^c.^u.u a b c
def 1st ^a.^b.^c.a
def 2nd ^a.^b.^c.b
def 3rd ^a.^b.^c.c

So

==> abc 2nd
====>b
<< abc 3rd
==> abc 3rd
====>c
<<

A list node is a triple whose first component is the first element of the list, the second component is the rest of the list, and the third component is a boolean that is true if the triple is the last node of the list and false otherwise.

def true ^p.^q.p
def false ^p.^q.q
def mknode (^a.^b.^u.u a b false)
def is_end (^n.n sel_3)

4.2 Empty List

A special node, end is constructed to serve as the empty list, and to be the last node of a list.

def renda ^e.^&u.&u e e true
def def rend (^x.renda(x x))(^x.renda(x x))
def head (^n.n sel_1)
def tail (^n.n sel_2)
def end ^&u.&u rend rend true

We see that:

<< Y renda
==> Y renda
====>end
<< renda rend
==> renda rend
====<end
<< head end
==> head end
====>end
<< tail end
==> tail end
====>end
<< is_end end
==> is_end end
====>true
<<

We define Y, the fixed-point operator, in the next section, "Function Complete of Curry Algebras."

So end

• is the fixed point of renda,
• answers true to is_end, and
• is its own head and tail.

4.3 Appending

The form append adds and element to the end of a list.

def Appenda ^h.^n.^list.(is_end list)(mknode n end)(mknode(head list)(h n(tail list)))
def append (^x.Appenda(x x))(^x.Appenda(x x))

It is easy to see that

	append = Y Appenda

As an example of a list, we have:

<< def abc append c (append b (append a end)))
<< head abc
==> head abc
====>a
<< head (tail abc)
==> head(tail abc)
====>b
<< head (tail (tail abc))
==> head(tail(tail abc))
====>c
<< head (tail (tail (tail abc)))
==> head(tail(tail(tail abc)))
====>end
<<

4.4 Mapping

Finally define the form map which applies its first argument to each node of its second argument, if the second argument is a list, anyway.

def Mapa ^h.^f.^list.(is_end list)(end)(mknode(f (head list))(h f (tail list)))
def map (^x.Mapa(x x))(^x.Mapa(x x))

So, for example,

<< def n01234 append 4 (append 3 (append 2 (append 1 (append 0 end))))
<< head n01234
==> head n01234
====>0
<< head (tail n01234)
==> head(tail n01234)
====>I
<< head (tail (tail n01234))
==> head(tail(tail n01234))
====>2
<< head (tail (tail (tail n01234)))
==> head(tail(tail(tail n01234)))
====>3
<< head(tail(tail(tail(tail n01234))))
==> head(tail(tail(tail(tail n01234))))
====>4
<< head(tail(tail(tail(tail(tail n01234)))))
==> head(tail(tail(tail(tail(tail n01234)))))
====>end
<< def s01234 map suc n01234
<< head s01234
==> head s01234
====>I
<< head (tail s01234)
==> head(tail s01234)
====>2
<< head (tail (tail s01234))
==> head(tail(tail s01234))
====>3
<< head(tail(tail(tail s01234)))
==> head(tail(tail(tail s01234)))
====>4
<< head(tail(tail(tail(tail s01234))))
==> head(tail(tail(tail(tail s01234))))
====>5
<< head(tail(tail(tail(tail(tail s01234)))))
==> head(tail(tail(tail(tail(tail s01234)))))
====>end
<<

5 Functional Completeness of Curry Algebras

The course of reasoning followed here is adapted from "FROM λ-CALCULUS TO CARTESIAN CLOSED CATEGORIES", J Lambek, McGill University, Montreal, P.Q. H3A 2K6, Canada.

[Note: To read this section your browser must be able to render the greek character entities: &alpha;(α), &beta;(β), ..., &equiv;(≡), &isin;(∈), &forall;(∀), &deg;(°).]

A Schönfinkel Algebra A consists of a set of symbols |A|, a left associative binary operation |A|x|A|->|A| (denoted here by juxtaposition), and three constants in |A|: I, K, and S such that:

for all a, b, c, f, and g in |A|
(1)	I a = a
(2)	K a b = a
(3)	S f g c = (f c)(g c)

We call (a b) a combination. So we can form expressions of combinations of the symbols in |A|, and these will correspond to other symbols in |A|. Mostly, we are interested in just those symbols that can be expressed by combinations of S, K and I.

We can say that a polynomial in A with unknown x is an element of the Schönfinkel Algebra A[x], (which is A with an extra element x attached to |A|) and a mapping

	hx: A -> A[x]

such for all algebra's B and mappings A->B and b ∈ |B|, there is an f' such that

	f = f'°hx

and

	f'(x) = b. 

If

	B = A and
	f is the identity morphism,

then f' is the substitution map that replaces x with b=a∈A.

If

	B =  A[x], and
	f = hx

then f' is the substitution map that replaces x with b=ψ(x)∈A[x].

5.1 Proposition 1 Abstractions in Schönfinkel Algebras.

Every polynomial φ(x) over a Schönfinkel Algebra A can be written in the form

	f x

where

	f ∈ |A|

Polynomials in A are formed as words in an indeterminate x and satisfy the same three identities. In particular equality =_x between polynomials is the smallest equivalence relation ≡ that satisfies:

(0x)	φ(x) ≡ ψ(x) and α(x) ≡ β(x) implies φ(x)ψ(x) ≡ α(x) β(x)
(1x)	I(α(x)) ≡ α(x)
(2x)	K(α(x))(β(x)) ≡ α(x)
(3x)	S(α(x))(β(x))(γ(x)) ≡ (α(x))(γ(x))((β(x))(γ(x))

Proof:

By induction on the length of the word φ(x), which must be one of

	x,
	some constant expression (without x), or
	ψ(x) χ(x)

We have for these three cases:

	φ(x) =x I x
	φ(x) =x (K a ) x,
	φ(x) =x (g x) (h x) = (S g h x)

This proof yields an algorithm for converting every polynomial into the form f x, where the word f is free of any occurrence of x. This is equivalent to the lambda command

	ext x φ(x)

with the flag eta toggled off (1) and xapp toggle on, With eta on, we still can make ext x work like this algorithm if we replace all occurrences of x not already in the combination (I x) with (I x).

Starting with eta on, such a lambda session might look like:

<< ext x x
I
<< ext x I x
I
<< ext x A
K A
<< ext x A B
K(A B)
<< ext x (A x)(B x)
S A B
<< ext x A x
A
<< ext x A (I x)
S(K A)I
<< ext x x A
S I(K A)
<< ext x I x A
S I(K A)
<<

A Curry Algebra is a Schönfinkel Algebra subject to certain additional equations or identities whose conjunction is equivalent to the following statement:

(4)	If f x =x g x in A[x] then f = g in A.

For example,

	S K I x =x (K x)(I x) =x I x,

so, (4) implies

	S K I = I

a result that can't be obtained from (1) through (3) alone.

5.2 Proposition 2. Existence of Curry Algebras.

It is possible to add a finite collection of equations or identities to the definition of a Schönfinkel Algebra to form a Curry Algebra: Every polynomial φ(x) over a Curry Algebra A may be written uniquely in the form (f x) with f ∈ |A|.

Proof

We need to demonstate a collection of (universally quantified) equations, or better, identities, in |A| whose conjunction, together with (1), (2), and (3), imply (4).

Define the function λ_x by induction on the length of the word representing the polynomial, φ(x).

(i)	λxx = I;
(ii)	λxx = K a, when a is a constant; and
(iii)	λx(φ(x))(ψ(x)) = S(λxφ(x))(λxψ(x)), when φ(x) and ψ(x) are not both constant.

The restriction on (iii) is necessary so that λ_x is not ambiguous: if both parts of a combination are constant then (ii) applies. The lambda command ext x works like λ_x if the both the flags eta and xapp are off. With xapp on, constant applications will be extracted by (iii) instead of (ii).

λ_x maps every polynomial φ(x) in A[x] to an element of f of A such that (f x) =_x φ(x). So the existence of f is assured.

We must now show that f is unique. We first prove that

(*)		φ(x) =x ψ(x) implies λx(φ(x)) = λx(ψ(x)).

That is, if two polynomials are equal in A[x], their lambda abstractions are equal in A .

To prove this assertion, we show that the equality

	λx(φ(x)) = λx(ψ(x))

defines an equivalence relation over the polynomials in A[x] that satisfies  (ix), (iix), and (iiix) above, when certain additional universally quantified equations in A  are assumed. Since =_x is assumed to be the smallest (finest grained) such equivalence, the assertion must hold.

(Adding such equations can only unify partitions of an equivalence relation, but never divide. That is, two members of |A[x]| (or |A|) that were equal without the additional equations will still be equal with them. So if =_x was the finest equivalence relation satisfying (ix), (iix), and (iiix) before the addition, it will remain such after the addition.)

So we must have, for all polynomials α(x), β(x), γ(x) in A[x]:

(1''')	λxI(α(x)) = λxα(x)
(2''')	λxK(α(x))(β(x)) = λx(α(x))
(3''')	λxS(α(x))(β(x))(γ(x)) = λx(α(x))(γ(x))((β(x))(γ(x))

For uniqueness of f, suppose we have

	(g x) =x φ(x).

But, using (*), this would imply that for all g∈A

	λx(g x) = λxφ(x) = f.

So we impose the condition, for all g∈A

(4''')	λx(g x) = g.

We would like to remove the restriction on (iii) above. That is, for all f, and g∈A , λx(f g)  using (iii) must equal λx(f g)  using (ii). So we have:

(5''')	S(K f)(K g) = K(f g)

Let

	a = λxα(x)
	b = λxβ(x)
	c = λxγ(x)

If we replace α(x), β(x), and γ(x) in (1'''), (2'''), and (3''') above with: (a x), (b x), and (c x) then we can use the lambda  command ext x  to calculate the corresponding equations in A

(1'')	S(K I)a = a
(2'')	S(S(K K)a)b = a
(3'')	S(S(S(K S)a)b)c = S(S a c)(S b c)
(4'')	S(K g)I = g
(5'')	S(K f)(K g) = K(f g)

Such a lambda  session might look like:

<< ext x I(a x)
S(K I)a
<< ext x (a x)
a
<< ext x K(a x)(b x)
S(S(K K)a)b
<< ext x (a x)
a
<< ext x S(a x)(b x)(c x)
S(S(S(K S)a)b)c
<< ext x (a x)(c x)((b x)(c x))
S(S a c)(S b c)
<< ext x g (I x)
S(K g)I
<<

These equations are universally quantified in α(x), β(x), γ(x), f, and g. Because every occurrence of the polynomials are bound by λx, and in light of (4'''), every expression a∈A has a corresponding polynomial in A[x]: (a x). So instead of qualifying the equations in terms of polynomials in |A[x]|, we can qualify them in terms of elements in |A|. So we have

(1')	∀a.S(K I)a = a
(2')	∀a.∀b.S(S(K K)a)b = a
(3')	∀a.∀b.∀c.S(S(S(K S)a)b)c = S(S a c)(S b c)
(4')	∀g.S(K g)I = g
(5')	∀f.∀g.S(K f)(K g) = K(f g)

Using the lambda  ext ^  command, we can turn these equations into identities in A

(1i)	S(K I) = I
(2i)	S(K S)(S(K K)) = K
(3i)	S(K(S(K S)))(S(K S)(S(K S))) = S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S)
(4i)	S(S(K S)K)(K I) = I
(5i)	S(S(K S)(S(K K)(S(K S)K)))(K K) = S(K K)

Such a lambda  session might look like:

<< ext ^ ^a.^x.I(a x)
S(K I)
<< ext ^ ^a.^x.a x
I
<< ext ^ ^a.^b.^x.K(a x)(b x)
S(K S)(S(K K))
<< ext ^ ^a.^b.^x.a x
K
<< ext ^ ^a.^b.^c.^x.S(a x)(b x)(c x)
S(K(S(K S)))(S(K S)(S(K S)))
<< ext ^ ^a.^b.^c.^x.(a x)(c x)((b x)(c x))
S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S)
<< ext ^ ^g.S(K g)I
S(S(K S)K)(K I)
<< ext ^ ^g.g
I
<< ext ^ ^f.^g.S(K f)(K g)
S(S(K S)(S(K K)(S(K S)K)))(K K)
<< ext ^ ^f.^g.K(f g)
S(K K)
<<

Let's check our work:

<< load definitions
<< S(K I) a x
==> ((S(K I)) a) x
====>a x
<< I a x
==> (I a) x
====>a x
<< S(K S)(S(K K)) a b x
==> ((((S(K S))(S(K K))) a) b) x
====>a x
<< K a b x
==> ((K a) b) x
====>a x
<< S(K(S(K S)))(S(K S)(S(K S))) a b c x
==> (((((S(K(S(K S))))((S(K S))(S(K S)))) a) b) c) x
====>a x(c x)(b x(c x))
<< S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S) a b c x
==> (((((S((S(K S))((S(K K))((S(K S))((S(K(S(K S)))) S)))))(K S)) a) b) c) x
====>a x(c x)(b x(c x))
<< S(S(K S)K)(K I) g x
==> (((S((S(K S)) K))(K I)) g) x
====>g x
<< I g x
==> (I g) x
====>g x
<< S(S(K S)(S(K K)(S(K S)K)))(K K) f g x
==> ((((S((S(K S))((S(K K))((S(K S)) K))))(K K)) f) g) x
====>f g
<< S(K K) f g x
==> (((S(K K)) f) g) x
====>f g
<<

5.3 Proposition 3 Curry Algebras ≡ Lambda Calculus.

A Curry Algebra is equivalent to the lambda calculus.

Proof

The identities of Curry algebra are equivalent to the following equations in the LC:

(1e) I = λxx
(2e) K = λxλyx
(3e) S = λxλyλzx z(y z)
(4e) ∀f.f = λxf x
(5e) ∀φ(x).∀a.φ(a) = (λxφ(x))a

First, show that, the identities of Curry algebra imply (1e)..(5e). Now (1e)..(4e) follow directly from the definition of λx and equation (4) in the definition of a Curry Algebra. Condition (5e) is true because we have by Proposition 2,

	 (λxφ(x))x = φ(x)

and by the substitution property, we can substitute a∈A for the unbound occurrences of x on both sides of the equation.

Second, show that (1e)..(5e) imply the identities (1)..(4) of Curry Algebra. It is clear that the definition (1e)..(3e) above will satify the behavior of I, K, and S for Curry Algebra. (4) above is η reduction. (5) above is β reduction (removing any name collisions by the appropriate α conversions). In the LC, two expressions are equal if one can be converted to the other by a finite number of α β and η conversions. So

(*e)	if φ(x) = ψ(x) then λxφ(x) = λxψ(x).

(Convert the body one lambda expression to the body of the other.) So any polynomial φ(x) can be expressed uniquely as ((λxφ(x)) x). Because if (g x) = ((λxφ(x)) x) then by (4) and g = λ_x(g x) = λ_xφ(x) (by (4e) and (*e)).

Any lambda expression with no free variables can be converted to an expression involving only S, K, and I. (Or S, K, if we replace I with (S K K)). This convertion is performed by the lambda command ext ^.

5.4 Proposition 4 Fixed Points in Curry Algebras.

Every element of a Curry Algebra has a fixed point.

Proof

The fixed point is

	Y g,

where

	Y = λg((λxg(x x))(λxg(x x))).

We have

	Y f
	= (λxf(x x))(λxf(x x))
	= f((λxf(x x))(λxf(x x)))
	= f(Y f)

so (Y f) is indeed a fixed point of f.