ext x lambda-exp+ 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. + + |
+
+ For example: +
+
+ load definitions
+
+
+ load "../share/definitions"
+
+
+ List all current definitions in reverse order. + That is, the more recent definitions are printed first. + +
+ 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. + | +
+ 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.
+
+
+ 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) |
+ A is 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 + << +
+ 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.
+
+ +
+
+ <lambda-exp> = <variable>
+
+
+ | ^<variable>.<lambda-exp>
+ | <lambda-exp> <lambda-exp>
+ | (<lambda-exp>)
+
+ 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.
+
+
+
+ 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 |
+
+ ^y.[M/x]Y |
+
3.2.2 |
+
+ x does occur free in Y |
+
+ ^z.[M/x]([z/y]Y)
+ |
+
+ +
| 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. + +
+ +
| 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.
+ |
+
+ [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
+ |
+
+ ADD [m][n] = [m+n]
+ |
+ ||
Proof |
+ By induction | +|
| 1) | +
+
+ ADD [0] [n]
+ |
+ |
|---|---|---|
| 2) | +
+ Assume
+
+ ADD [m][n] = [m+n]
+
+ |
+ + induction hypothesis + | +
| 3) | +
+
+ ADD [m+1][n]
+ |
+ |
| => + |
+
+ = ^x.^y.x([m+n] x y)
+ |
+
+
+ by 2) induction hypothesis + |
+
| + |
+
+ = [(m+1)+n]
+ | + |
+ MUL [m][n] = [m*n]
+ |
+ |||
Proof |
+ By induction | +||
| 1) | +
+
+ MUL [0] [n]
+ |
+ + | |
|---|---|---|---|
| 2) | +
+ Assume
+
+ MUL [m][n] = [m*n]
+
+ |
+ induction hypothesis + |
+ |
| 3) | +
+
+ MUL [m+1] [n]
+ | + | + |
| => | +
+
+ = ^x.^b.([n] x)([m*n] x b)
+ |
+ by 2) induction hypthesis + |
+ |
| + |
+
+ = ^x.^b.ADD [n] [m*n] x b
+ |
+ + | +|
+
+ EXP [n][m] = [n**m]
+ |
+ ||
Proof |
+ By induction | +|
| 1) | +
+
+ EXP [n] [0]
+ |
+ + |
|---|---|---|
| 2) | +
+ Assume
+
+ EXP [n][m] = [n**m]
+
+ |
+
+ induction hypothesis + |
+
| 3) | +
+
+ EXP [n] [m+1]
+ |
+ |
| => | +
+
+ = ^y.[n]([n**m] y)
+
+ |
+
+ by 2) induction hypothesis + |
+
| + |
+
+ = MUL [n] [n**m]
+ | + | +
+
+
+ pred [n] = [n-1]
+
+
|
+ ||||||||||
Proof |
+ By induction | +|||||||||
| 1) | +
+
+ pred_pair [1]
+
+ |
+ + | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 2) | +
+ Assume
+
+ pred_pair [n] = pair [n] [n-1]
+ |
+
+ induction hypothesis + |
+ ||||||||
| 3) | +
+
+ pred_pair [n+1]
+ |
+ |||||||||
| => | +
+
+ = bump (pair [n] [n-1])
+ |
+
+ by 2) induction hypothesis + |
+ ||||||||
| 4) | +
+
+ pred [n]
+ |
+ + | ||||||||
+ 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 + << ++
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 ++
+ ==> abc 2nd + ====>b + << abc 3rd + ==> abc 3rd + ====>c + << ++
+ 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) ++
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 ++
+ << 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 + << ++
+ So end
+
renda,is_end, and+
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)) ++
+ 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 + << ++
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)) ++
+ << 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 + << ++
+ [Note: To read this section your browser must be able to render + the greek character entities: + α(α), + β(β), + ..., + ≡(≡), + ∈(∈), + ∀(∀), + °(°).] +
+ 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].
+
+ 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) &quiv; psi;(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)) ++ + +
+ 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. +
+ +
φ(x)
+ over a Curry Algebra A may be
+ written uniquely in the form (f x)
+ with f ∈ |A|.
+ |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) + (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). ++ By (*) this implies 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 + << ++
α(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) + << ++
+ << 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 + << + ++
+ (1) I = λxx + (2) K = λxλyx + (3) S = λxλyλzx z(y z) + (4) ∀f.f = λxf x = f + (5) ∀φ(x).∀a.φ(a) = (λxφ(x))a ++ Condition (5) 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.
+ + 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.
+
+
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,239 ----
+ #!/usr/bin/perl -w -I ./
+ #####!/usr/bin/perl -T -w -I ./
+ use IO::File;
+
+ # stdin: html
+ # stdout: html with toc
+ # replace a line with "| $1<\/td><\/tr><\/table>/g;
+ s/ |