Rachunek lambda, lato 2019-20
Wykład 5
27 marca 2020
1
Last week: Observational equivalence
TermsM,NwithFV(M) ∪FV(N) = ~x, areobservationally equivalent(M ≡ N) when, for all closedP:
P(λ~x .M)is solvable ⇐⇒ P(λ~x .N)is solvable Put it differently: for any “context”C [ ]:
C [M]is solvable ⇐⇒ C [N]is solvable Note:IfM =ηNthenM ≡ N.
2
Böhm Trees
BT (λ~x .yP1. . . Pn) = λ~x . y
BT (P1) BT (P2) . . . BT (Pn)
IfMis unsolvable thenBT (M) = ⊥.
IfMhas a hnfNthenBT (M) = BT (N).
3
Example 1: any fixed-point combinator Z
SinceZf =βf (Zf )for a fresh variablef, it must be the case thatZ =βλf .f T, for some T . Therefore:
f T =βZf =βf (Zf ) = f ((λf .f T )f ) =βf (f T ).
Hencef T =βf (f T ) =βf (f (f T )) =βf (f (f (f T ))) · · · The termZunfolds into an “infinite term”λf .f (f (f (. . . Its Böhm tree has one infinite branch:
λf .f ——f ——f —— · · ·
4
Example 2: M = Y(λmx. x(mx)(mx))
LetM = Y(λmx . x (mx )(mx )). ThenM =βλx . x (Mx )(Mx ).
BT (M) = λx x
%%
yyx
x
x x x x
· · · ·
5
Example 3: J = Y(λfxy . x(fy ))
WriteΦforλfxy . x (fy ). Then:
J = YΦ =βΦJ =βλxy0. x (Jy0) =βλxy0. x (ΦJy0)
=βλxy0. x (λy1. y0(Jy1)) =βλxy0. x (λy1. y0(ΦJy1)) =β. . .
The treeBT (J)consists of one infinite path:
λxy0. x ——λy1. y0——λy2. y1——λy3. y2—— · · ·
6
Example 3: J = Y(λfxy . x(fy ))
The treeBT (J)consists of one infinite path:
λxy0. x ——λy1. y0——λy2. y1——λy3. y2—— · · ·
The treeBT (I)consists of a single node: λx x The first can be obtained from the second by means of an infinite sequence ofη-expansions:
λx x η← λxy0. x ——y0 η← λxy0. x ——λy1. y0——y1
When are terms observationally equivalent?
Böhm treesBiB0areη-equivalent(B ≈ηB0), if there are two (possibly infinite) sequences of η-expansions:
B = B0 η← B1 η← B2 η← B3 η← · · · B0= B0 η0 ← B1 η0 ← B2 η0 ← B3 η0 ← · · · converging to the same (possibly infinite) tree.
Theorem (Wadsworth)
TermsMandNare observationally equivalent
if and only ifBT (M) ≈ηBT (N).
Przerwa na reklamę
9
To Mock a Mockingbird
10
Logika kombinatoryczna Combinatory Logic
11
Combinatory Logic,
or the calculus of combinators
Terms:
I Variables;
I ConstantsKandS;
I Applications(FG ).
12
The “weak” reduction
I KFG →wF;
I SFGH →wFH(GH);
I IfF →wG, thenFH →wGHandHF →wHG.
Notationw,=wetc. used as usual.
13
Examples of combinators
I I = SKK
IF →wKF (KF ) →wF
I Ω = SII(SII)
Ω →wI(SII)(I(SII)) wΩ
I W = SS(KI)
WFG →wSF (KIF )G →wSF IG →wFG (IG ) wFGG
14
Examples of combinators
I B = S(KS)K
BFGH →wKSF (KF )GH →wS(KF )GH →w
→wKFH(GH) →wF (GH)
I C = S(BBS)(KK) CFGH wFHG
I B0= CB
B0FGH wG (FH)
Remark:Each of those can be added as a new constant.
15
Examples of combinators
I 0 = KI 0FG wG
I 1 = SB(KI) 1FG wFG
I 2 = SB(SB(KI)) 2FG wF (FG )
16
Fixed point combinators
Y = WS(BWB)
Θ = WI(B(SI)(WI))
17
Good and bad properties
I Church-Rosser;
I Standardization;
I Definability of computable functions;
I Undecidability.
18
From CL to lambda
I (x )Λ= x ;
I (K)Λ= λxy .x ;
I (S)Λ= λxyz.xz(yz);
I (FG )Λ= (F )Λ(G )Λ.
Properties:
I If F wG , then (F )Λβ(G )Λ.
I If F =wG , then (F )Λ=β(G )Λ.
19
From CL to lambda
IfF =wG, then(F )Λ=β(G )Λ.
This is a “morphism” fromCL/=w to Λ/=β.
Ale nie monomorfizm: (F )Λ=β(G )Λnie implikujeF =wG.
Na przykład (KI)Λ=βλxy . y =β(S(K(KI))I)Λ
20
From CL to lambda
Twierdzenie (Jarosław Tworek, 2010)
Istnieje efektywna redukcjaϕ : CL → Λo własności:F =wG, wtedy i tylko wtedy, gdy ϕ(F ) =βϕ(G ).
Sens: Relacja=w redukuje się do relacji=β.
21
From lambda to CL: combinatory abstraction
I λ∗x . F = KF, whenx 6∈FV(F );
I λ∗x . x = I;
I λ∗x . FG = S(λ∗x .F )(λ∗x .G ), otherwise.
Lemma 1:(λ∗x .F )G wF [x := G ].
Lemma 2:(λ∗x .F )Λ=βλx . (F )Λ.
22
Lemma 1:
(λ∗x .F )G wF [x := G ]Case 1: If x 6∈FV(F ) then
(λ∗x .F )G = KFG →wF = F [x := G ].
Case 2: If F = x then (λ∗x .F )G = IG wG = x [x := G ].
Case 3: If F = F0F00then
(λ∗x .F )G = S(λ∗x .F0)(λ∗x .F00)G →w
→w(λ∗x .F0)G ((λ∗x .F00)G ) wF0[x := G ]F00[x := G ].
Combinatory completeness
Lemma 1:(λ∗x .F )G wF [x := G ].
Theorem (Combinatory completeness)
Given anyxandF, there isH such that, for allG, HG wF [x := G ]
From lambda to CL
I (x )C= x ;
I (MN)C= (M)C(N)C;
I (λx .M)C= λ∗x .(M)C.
Good property: ((M)C)Λ=βM.
Proof: Induction with respect to M, using Lemma 2:
(λ∗x .F )Λ=βλx . (F )Λ.
Moral: Translation from CL to lambda is surjective.
25
Translation from CL to lambda is surjective
I Złożenie(( )C)Λjest identycznością.
I Złożenie(( )Λ)Cnie jest identycznością. Na przykład ((K)Λ)C= S(KK)I 6=wK.
26
Translation from CL to lambda is surjective
Corollary:TermsKandSare abasisof lambda-calculus:
every term (up to β-equality) can be obtained fromK,S, and variables, by means of application.
Proof: M =β((M)C)Λ.
27
Bad property
I M =βNdoesnotimply(M)C=w(N)C. For example:
(λx .KIx )C=wS(K(KI))I 6=wKI = (λx I)C. W rzeczy samej, boλx .KIx →βλx I, ale:
(λx .KIx )C= S(λ∗x . (KI)C)(λ∗x .x ) = S(K((K)C(I)C))I = S(K(S(KK)II))I =wS(K(KI))I 6=wKI = (λx I)C. Moral:
I This isnota morphism fromΛ/=βtoCL/=w.
I „Weak” equality isstrongerthan beta-equality.
28
The guilty one
The combinatory abstractionλ∗is not weakly extensional.
Rule(ξ)is not valid forλ∗and =w: M = N
λx .M = λx .N, (ξ)
Indeed,λ∗x .KIx = S(K(KI))I 6=wKI = λ∗x .I.
29
Extensional CL
I IfG =wH thenG =extH;
I IfGx =extHxandx 6∈FV(G ) ∪FV(H)thenG =extH;
I IfG =extG0thenGH =extG0H andHG =extHG0. Properties:
I G =extH if and only if (G )Λ=βη(H)Λ;
I M =βηN if and only if (M)C=ext(N)C.
I ((G )Λ)C=extG, for allG.
30
Open problem
Define a computable translationT from lambda to CL with:
M =βN ⇐⇒ T (M) =wT (N).
31
NCL - “Naive Combinatory Logic”
Terms: IfF,Gare terms thenPFGis a term.
WriteF ⇒ GforPFG.
Formulas:
– Every termF is a formula;
– EquationsF = Gare formulas.
32
NCL - Axioms and rules
Axioms:
F = F KFG = F SFGH = FH(GH)
F ⇒ F (F ⇒ (F ⇒ G )) ⇒ (F ⇒ G )
Rules:
M = N MQ = NQ
M = N QM = QN M = N
N = M
M = N, N = Q M = Q
M, M = N N
M, M ⇒ N N
33
Curry’s Paradox
Take any termFand defineN = Y(λ∗x . x ⇒ F ).
ThenN = N ⇒ Fin NCL.
Using axiomN ⇒ Nit follows thatN ⇒ (N ⇒ F ).
ThusN ⇒ F, using(N ⇒ (N ⇒ F )) ⇒ (N ⇒ F ).
This provesN, becauseN = N ⇒ F. Eventually,Ffollows by modus ponens.
Moral:System NCL is logically inconsistent.
34
