Rachunek lambda, lato 2019-20
Wykład 3
13 marca 2020
1
Rachunek λ-I
2
The λI-calculus
The λI-terms:
– variables;
– applications (MN), where M and N are λI-terms;
– abstractions (λx M), where M is a λI-term, andx ∈FV(M).
TermsS = λxyz.xz(yz)andI = λx.xare λI-terms, butK = λxy .xis not.
3
Question
Are λI-terms closed under reductions?
Yes, ifM →βηN, andMis a λI-term, then so is N.
4
Theorem:
If a λI-term has a normal form then it is SN.
(Write→`for leftmost beta-reduction.)
Lemma: IfM ∈ λIandM →`N ∈ SNthenM ∈ SN.
Proof: Induction wrt the length of the normal form ofN. Case 1: M = λ~x . yR1R2. . . Rk. ThenN = λ~x . yR10. . . Rk0, withRi→ Ri0, for somei, andRi= Ri0, otherwise.
SinceN ∈ SN, alsoRi0∈ SN, with shorter normal form.
Thus allRiare SN, and so isM.
5
Theorem:
If a λI-term has a normal form then it is SN.
Lemma:IfM ∈ λIandM →`N ∈ SNthenM ∈ SN.
Proof:Induction wrt the length of the normal form ofN.
Case 2:
M = λ~x . (λy P)QR1. . . Rk→βλ~x . P[y := Q]R1. . . Rk= N.
All termsP, Q, R1, . . . , Rkare SN. Therefore internal reductions ofMmust terminate, and otherwise we have:
M λ~x. (λy Pi 0)Q0R10...Rk0 → λ~h x . P0[y := Q0]R10. . . Rk0 · · · ButN βλ~x . P0[y := Q0]R10. . . Rk0, andNis SN.
6
Question
Does the proof use the assumption thatMis a lambda-I-term?
Where?
Yes, otherwiseQis not necessarily normal.
Theorem:
If a λI-term has a normal form then it is SN.
Proof:LetM ∈ λIhave normal formM0. ThenM `M0∈ SN.
By induction wrt number of steps show thatMis SN.
Siła wyrazu / Expressive power
9
Curry’s fixed point combinator Y
Y = λf . (λx .f (xx ))(λx .f (xx ))
Fact: YF =βF (YF ), for everyF.
Proof:YF →β(λx .F (xx ))(λx .F (xx )) →β
F ((λx .F (xx ))(λx .F (xx )))β← F (YF )
10
Comment
Lambda calculus is a fantastic world: every function has a fixpoint (every equationX = Anything (X )has a solution)!
The moral sense is: every recursive definition is well-formed.
The price we pay for it is non-termination.
11
YF =
βF (YF )
Example: Find anMsuch thatMxy =βMxxyM.
Solution:No problem,M = Y(λm λxy . mxxym).
12
Turing’s fixed-point combinator
Θ = (λxf . f (xxf ))(λxf . f (xxf ))
Fact: ΘF βF (ΘF ), for all F .
Proof: ΘF = (λxf . f (xxf ))(λxf . f (xxf ))F →β
(λf . f ((λxf . f (xxf ))(λxf . f (xxf ))f )F →β
F ((λxf . f (xxf ))(λxf . f (xxf ))F ) = F (ΘF )
Note the βrather than =β.
13
Example
Consider a combinatorday = hour hour · · · hour, where eachhouris defined as
λabcdefghijklmnopstuwyzr . r (itisafikspointcombinator ).
How manyhours should adayhave to be a fixpoint combinator, i.e., to satisfy hour F =βF (hour F )?
Define a Polish or Spanish example.
14
Problems
1. Is there a termM such thatM =βMSM? 2. Can you solve non-fix-point equations like
MxxM =βMxM?
3. Can you solve systems of equations with 2 or more unknowns like{P = QSP, Q = PKQP}?
4. Can you solve any equation at all?
5. What are the fixpoints of the operatorSI (whereSandIare the standard combinators)?
6. Is there a fixpoint combinator in normal form?
7. IsYbeta-equal toΘ?
Conditional
true = λxy .x false = λxy .y if P then Q else R = PQR.
It works:
if true then Q else R βQ if false then Q else R βR.
Ćwiczenie: Zdefiniować operacje logiczne
Define Boolean logic conjectives: ∨,∧,→,¬as λ-terms.
For example, define a termCso that
C true false =βC false true =βC false false = false C true true =βtrue
Possible solution: C = λpd . p(d true false)false
17
A generalization: finite sets
Coding elements of a finite set {a1, . . . , an}:
ai:= λx1. . . xn. xi
Selection operator:
case a of (F1, . . . , Fn) := aF1. . . Fn
It works:
case aiof (F1, . . . , Fn) βFi
18
Ordered pair
Pair = Boolean selector:
hM, Ni = λx .xMN;
πi = λx1x2.xi (i = 1, 2);
Πi = λp. pπi (i = 1, 2).
It works:
Π1hM, Ni →βhM, Niπ1βM.
19
Question
Will this work:hΠ1M, Π2Mi =βM?
Not when M is not a pair; take e.g.M = x.
Comment: This pairing is not surjective. And one cannot do better: Church-Rosser fails with surjective pairing!
Note the similarity with eta.
20
Ordered tuples
Tuple = Selector:
hM1, . . . , Mni = λx .xM1. . . Mn;
πi = λx1. . . xn.xi (i = 1, . . . , n);
Πi = λt. tπi (i = 1, . . . , n).
It works:
ΠihM1, . . . , Mni βMi
21
Church’s numerals
cn= n = λfx .fn(x ),
0 = λfx .x ; 1 = λfx .fx ; 2 = λfx .f (fx );
3 = λfx .f (f (fx )), etc.
22
Definable functions
A partial functionf : Nk−◦ Nisλ-definable if there is a termFsuch that for alln1, . . . , nk∈ N:
I Iff (n1, . . . , nk) = m, thenF n1. . . nk=βm;
I Iff (n1, . . . , nk)is undefined
thenF n1. . . nkdoes not normalize.
FunctionFiswell-definablewhen, in addition:
I Iff (n1, . . . , nk)is defined thenF n1. . . nk∈ SN.
Comment
1. There are other definitions of lambda-definability.
They may slightly differ in the undefined case.
But the main results are the same.
2. The notion of “well definable” is not as common, but it proves technically useful.
Some well-definable functions
I Successor: succ = λnfx.f (nfx);
We have succ n βn + 1, please check.
Now try to define addition!
I Addition: add = λmnfx.mf (nfx);
I Multiplication: mult = λmnfx.m(nf )x;
I Exponentiation: exp = λmnfx.mnfx;
I Test for zero: zero = λm.m(λy .false)true;
I Constant zero (with k arguments):Zk= λm1. . . mk.0;
I Projection on the i -th coordinate:Πik= λm1. . . mk.mi. 25
A challenge: predecessor
p(n + 1) = n, p(0) = 0
Diggression: They say Kleene invented this definition while his tooth was being extracted.
And that Church formulated Church Thesis when Kleene came back from the dentist’s.
Because this construction generalizes to all primitive recursive functions.
26
Predecessor is definable
p(n + 1) = n, p(0) = 0
Step = λp.hsucc(pπ1), pπ1i pred = λn. (n Steph0, 0i)π2
How it works:
Steph0, 0i βh1, 0i Steph1, 0i βh2, 1i Steph2, 1i βh3, 2i,
and so on. (Evaluate pred 4.)
27
Problems
Some of the problems have solutions in the file zadlam.
Try them without looking at the solutions.
1. Define the functionn 7→ 2n2+ 2n + 4.
2. Letf (0, x ) = g (x )andf (n + 1, x ) = h(n, x , f (n, x )).
Assumehandgare lambda-definable, show how to lambda-definef.
3. Define the functionn 7→ 2n2− 2n + 4.
4. Define equalityEqso thatEq m n =β0iffm = n.
5. LetC = (λFxy . xF (λz. 1)(yF (λz. 0)))(λfg .gf ).
What is the function fromN2toNdefined byC?
28
Nierozstrzygalność / Undecidability
29
Turing machine
We consider deterministic single-tape Turing Machines computing functions fromNtoN. The input number is the length of input word and the output number is represented by the head position.
It is convenient to represent machine IDs so that we can have a direct access to head position,
and to the symbol at the left of tape head.
So if the tape contents isabrakadabra, with machine scanning the letterd(at position 6) in stateq, we represent it as the quadruplehakarba, q, dabra, 6i.
30
Turing machine
“Superkonfiguracja”.
hwR, q, v , `i,
(NotationwRiswwritten backwards, e.g. 011R= 110.)
I The tape contents is “wv BB. . . ” (whereBis blank);
I The head reads the first cell afterw.
I The machine state isq;
I The length ofwis`.
Final configuration whenq ∈ Final. Theresultis`.
Initial configuration: Cn= hε, q0, •n, 0i.
Assumptions about machines
I The machine is deterministic.
I There is one tape infinite to the right.
I The machine never writes a blank.
I The machine head never moves beyond the left tape end.
Encoding a Turing Machine
The set of states{q0, q1, . . . , qr}is finite.
States are encoded as projections: qi= λx0. . . xr.xi.
The alphabet{a0, a1, . . . , am}is finite.
Symbols are encoded as projections: ai= λx0. . . xm.xi.
Empty wordεis encoded asnil = hB, Ii.
Blank-free wordaw (lista :: w) is encoded asha, wi.
Word manipulation:head = Π1,tail = Π2. (Check how it works)
33
Encoding a Turing Machine
SuperconfigurationhwR, q, v , niis encoded
as a quadruplehwR, q, v, ni.
Initial configuration: Init = λx. hnil , q0, x (λy . h•, y i)nil , 0i.
ThenInit n hnil, q0, •n, 0i.
Stop test:Halt = λc. Π2cd1. . . dr= case Π2c of (d1, . . . , dr), wheredi= true, forqi∈ Final, anddi= false, otherwise.
Result extraction:Out = λc. Π4c. (Check how it works)
34
Encoding a machine step
(Superconfiguration: hwR, q, v, ni.)
We need a termNexts.t.Next(code of C1) β(code of C2) whenever the machine can move fromC1toC2. We take:
Next = λc. case Π2c of (R0, . . . , Rr) = λc. Π2c R0. . . Rr, whereRi codes the configuration to be obtained if the machine state in the given configurationc isqi.
35
Encoding a machine step
(Superconfiguration:hwR, q, v, ni.)
We takeNext = λc. Π2c R0. . . Rr, whereRicodes the next configuration when the machine state incisqi.
How to defineRi? As a case selector on the scanned symbol:
Ri= λc. head (Π3c)R1i. . . Rmi,
whereRjiis obtained according to the transitionδ(qi, aj) determined by stateqiand symbolaj.
36
Encoding transitions
Given codecof configurationC = hwR, qi, ajv , ni, we need a termRjirepresenting the next configuration, depending on the transition tableδ.
Ifδ(qi, aj) = hb, 0, pi(no move) then take Rji= hΠ1c, p, hb, tail (Π3c)i, Π4ci
Ifδ(q, a) = hb, +1, pi(right move) then take Rji= hhb, (Π1c)i, p, tail (Π3c), succ(Π4c)i,
Ifδ(q, a) = hb, −1, pi(left move) then take
Rji= htail (Π1c), p, hhead (Π1c), hb, (tail (Π3c))ii, pred(Π4c)i.
(The head never goes beyond the left tape end.)
37
Special case: a
j= B
LetC = hwR, qi, ajv , nioraz aj= B.
Thenajv is “empty”, i.e.Π3c = nil = hblank, Ii.
Ifδ(qi, aj) = hb, 0, pi(no move) then take Rji= hΠ1c, p, hb, nil i, Π4ci
Ifδ(q, a) = hb, +1, pi(right move) then take Rji= hhb, (Π1c)i, p, nil , succ(Π4c)i,
Ifδ(q, a) = hb, −1, pi(left move) then take
Rji= htail (Π1c), p, hhead (Π1c), hb, nil ii, pred(Π4c)i.
38
Encoding a Turing Machine
We have a termNexts.t.
Next(code of C1) β(code of C2), whenever the machine can move fromC1toC2. The function computed by the machine is λ-definable as:
λx .W (Init x )W, where
W = λc.ifHalt cthenλw .Out c elseλw .w (Next c)w .
Computing: C
0⇒ C
1⇒ C
2⇒ · · · ⇒ C
mF = λx .W (Init x )W,
W = λc.ifHalt cthenλw .Out celseλw .w (Next c)w . F n → W (Init n)W W C0W →
[if Halt C0thenλw .Out C0elseλw .w (Next C0)w ]W [λw .w (Next C0)w ]W [λw .w C1w ]W → W C1W → [if Halt C1thenλw .Out C1elseλw .w (Next C1)w ]W [λw .w (Next C1)w ]W [λw .w C2w ]W → W C2W →
· · · W CmW → [if Halt Cmthenλw .Out Cmelseλw .w (Next Cm)w ]W [λw .Out Cm]W → Out Cm f(n).
Question
We have definedF = λx .W (Init x )W, and
W = λc.ifHalt cthenλw .Out c elseλw .w (Next c)w . Suppose we replace this definition by:
W = λcw .ifHalt cthenOut celsew (Next c)w . Will anything change?
41
