Rachunek lambda, lato 2019-20
Wykład 6
3 kwietnia 2020
1
Modele
2
Semantics
Goal: Interpret any termMas an element[[M]]of some structureA, so thatM =βNimplies[[M]] = [[N]].
More precisely,[[M]]may depend on avaluation:
v : Var → A.
Write[[M]]vfor the value ofMunderv.
3
Lambda-interpretation: A = hA, ·, [[ ]] i
Application·is a binary operation inA;
[[ ]] : Λ × AVar→ A.
Write[[M]]v instead of[[ ]](M, v ).
Postulates:
(a) [[x]]v= v (x );
(b) [[PQ]]v= [[P]]v· [[Q]]v;
(c) [[λx.P]]v· a = [[P]]v [x 7→a], for anya ∈ A;
(d) Ifv |FV(P)= u|FV(P), then[[P]]v= [[P]]u.
4
Dygresja
Jeśli znamy[[P]]vi[[Q]]v, to znamy[[PQ]]v= [[P]]v· [[Q]]v. Znaczenie aplikacji zależy tylko od znaczenia jej składowych.
To samo chcemy mieć dla abstrakcji.
Kiedy powinno zachodzić([[λx P]]v= [[λx Q]]v)?
Równość[[P]]v= [[Q]]v to trochę za mało.
Warunek∀v ([[P]]v= [[Q]]v)to trochę za dużo.
Należy wymagać[[P]]v [x 7→a]= [[Q]]v [x 7→a], dlaa ∈ A.
5
Extensionality
Writea ≈ bwhena · c = b · c, for all c.
Extensional interpretation:a ≈ bimpliesa = b, for alla, b.
Weakly extensionalinterpretation:
[[λx .M]]v≈ [[λx.N]]vimplies[[λx .M]]v= [[λx .N]]v, for allN, v.
Meaning:Abstraction makes sense algebraically.
(N.B.[[λx .M]]v≈ [[λx.N]]viff[[M]]v [x 7→a]= [[N]]v [x 7→a], alla.)
6
Lambda-algebra and lambda-model
Lambda-algebra: a lambda-interpretation satisfying beta:
M =βN implies [[M]]v= [[N]]v
Lambda-model : Weakly extensional lambda-interpretation:
[[λx .M]]v≈ [[λx.N]]v implies [[λx .M]]v= [[λx .N]]v
“Trivial” examples
M(λ) = hΛ/=β, ·, [[ ]] i,
where[[M]]v= [M[~x := v (~x )]]βand[M]β· [N]β= [MN]β
Similarly:
M(λη) = hΛ/=βη, ·, [[ ]] i;
M0(λ) = hΛ0/=β, ·, [[ ]] i;
M0(λη) = hΛ0/=βη, ·, [[ ]] i.
“Trivial” examples
Fact
StructuresM(λ)andM(λη)are lambda-models.
StructuresM0(λ)andM0(λη)are lambda-algebras, but not lambda-models.
It may happen thatMP =βNPfor all closedP, (i.e. [λx . Mx ] ≈ [λx . Nx ]),
butMx 6=βNx
(i.e. [λx . Mx ] 6= [λx . Nx ]).
9
Very Important Lemma
Lemma
In every lambda-model, [[M[x := N]]]v= [[M]]v [x 7→[[N]]v]. Proof: Induction wrtM. First assume thatx 6∈FV(N).
Krok indukcyjny dla abstrakcjiM = λy P:
[[(λy P)[x := N]]]v [x 7→[[N]]v]· a = [[λy .P[x := N]]]v· a
= [[P[x := N]]]v [y 7→a]= [[P]]v [y 7→a][x 7→[[N]]v [y 7→a]]
= [[P]]v [y 7→a][x 7→[[N]]v]= [[λy .P]]v [x 7→[[N]]v]· a, for alla.
Therefore[[(λy P)[x := N]]]v= [[(λy .P)]]v [x 7→[[N]]v].
10
Very Important Lemma
Lemma
In every lambda-model, [[M[x := N]]]v= [[M]]v [x 7→[[N]]v]
Proof.
In casex ∈FV(N)take freshzand letw = v [z 7→ [[N]]v].
[[M[x := N]]]v= [[M[x := z][z := N]]]v= [[M[x := z]]]w= [[M]]w [x 7→[[z]]w]= [[M]]v [x 7→[[z]]w]= [[M]]v [x 7→[[N]]v].
11
Soundness
Proposition
Every lambda-model is a lambda-algebra:
M =βN implies [[M]]v= [[N]]v
Proof.
Induction wrtM =βN. Non-immediate cases are two:
(Beta)
[[(λx .P)Q]]v= [[λx .P]]v· [[Q]]v= [[P]]v [x 7→[[Q]]v]= [[P[x := Q]]]v. (Xi) LetP =βQand letM = λx .P,N = λx .Q. Then [[M]]v· a = [[P]]v [x 7→a]= [[Q]]v [x 7→a]= [[N]]v· a, for alla.
12
Completeness
Theorem
The following are equivalent:
1) M =βN;
2) A |= M = N, for every lambda-algebraA;
3) A |= M = N, for every lambda-modelA.
Proof.
(1)⇒(2) Obvious.
(2)⇒(3) By soundness.
(3)⇒(1) BecauseM(λ)is a lambda-model.
13
Modele Scotta
14
Complete partial orders
LethA, ≤ibe a partial order.
A subsetB ⊆ Aisdirected (skierowany)when
for everya, b ∈ Bthere isc ∈ Bwitha, b ≤ c.
The setAis acomplete partial order (cpo)when
every directed subset has a supremum.
It follows that every cpo has a least element⊥ = sup ∅.
15
Complete partial orders
LethA, ≤iandhB, ≤ibe cpos, andf : A → B.
Thenf ismonotone ifa ≤ a0impliesf (a) ≤ f (a0).
Andf iscontinuousifsup f (C ) = f (sup C )
for everynonemptydirectedC ⊆ A.
Fact: Every continuous function is monotone.
[A → B]is the set of all continuous functions fromAtoB
16
Complete partial orders
IfhA, ≤iandhB, ≤iare cpos then:
I The productA × Bis a cpo with
ha, bi ≤ ha0, b0iiffa ≤ a0andb ≤ b0.
I The function space[A → B]is a cpo with
f ≤ giff∀a. f (a) ≤ g (a).
17
Continuous functions
Lemma
A functionf : A × B → Cis continuous iff it is continuous wrt both arguments, i.e. all functions of the formλλa. f (a, b) andλλb. f (a, b)are continuous.
18
Continuous functions
Lemma
The applicationApp : [A → B] × A → Bis continuous.
Proof hint:
Use the previous lemma.Lemma
The abstractionAbs : [(A × B) → C ] → [A → [B → C ]], given byAbs(F )(a)(b) = F (a, b), is continuous.
19
Reflexive cpo
The cpoDisreflexiveiff there are continuous functions F : D → [D → D]andG : [D → D] → D,
withF ◦ G = id[D→D]. ThenFmust be onto andG is injective.
The following are equivalent conditions:
“G ◦ F = idD”, “Gonto”, “Finjective”.
20
Reflexive cpo
F : D → [D → D], G : [D → D] → D, F ◦ G = id.
Define application asa · b = F (a)(b)so thatG (f ) · b = f (b).
Define interpretation as
I [[x ]]v= v (x );
I [[PQ]]v= [[P]]v· [[Q]]v;
I [[λx .P]]v= G (λλa.[[P]]v [x 7→a]).
Fact: This is a (well-defined) lambda interpretation.
(Use continuity ofAppandAbs.)
21
Reflexive cpo
Theorem
A reflexive cpo is a lambda-model.
Proof.
Należy udowodnić słabą ekstensjonalność.
Załóżmy, że[[λx .M]]v· a = [[λx.N]]v· a, dla każdegoa.
Inaczej,λλa.[[M]]v [x 7→a]= λλa.[[N]]v [x 7→a]. Chcemy[[λx .M]]v= [[λx .N]]v. Ale:
[[λx .M]]v= G (λλa.[[M]]v [x 7→a]) [[λx .N]]v= G (λλa.[[N]]v [x 7→a]).
22
A reflexive cpo: Model P
ω= hP(N), ⊆i
NotationPω= P(N).
Every set is a directed union of its finite subsets.
Lemma
A functionf : Pω→ Pωis continuous iff f (a) =S{f (e) | e finite and e ⊆ a}, for alla ∈ Pω.
Moral: A continuous function is fully determined by its values on finite arguments.
Encodings in P
ωPairs:
(m, n) =(n + m)(n + m + 1)
2 + m,
Finite sets: e0= ∅, and
en= {k0, k1, . . . , kr −1}, forn =X
i <r
2ki.
P
ωis reflexive
graph(f ) = {(n, m) | m ∈ f (en)};
fun(a)(x) = {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ a)}.
Lemma: Functionsgraphandfunare continuous, and fun ◦ graph = id[Pω→Pω].
Proof: fun(graph(f ))(x) =
= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}
= {m | ∃n ∈ N(en⊆ x ∧ m ∈ f (en))}
=S{f (en) | en⊆ x} = f (x).
25
Przykłady w P
ω(ćwiczenie)
I [[I]] = graph(id) = {(n, m) | m ∈ en};
I [[K]] = {(m, (k, `)) | ` ∈ em};
I [[ω]] = {(x , m) | ∃n(en⊆ ex∧ (n, m) ∈ ex)};
I [[Ω]] = ∅ = ⊥.
26
P
ωis not a model of η-conversion
graph(f ) = {(n, m) | m ∈ f (en)};
fun(a)(x) = {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ a)}.
Every nonemptygraph(f )is infinite:
If(n, m) ∈ graph(f )then also(k, m) ∈ graph(f ), foren⊆ ek. (Thusgraph ◦ fun 6= idPω.)
Fact: Pωis not a model ofη-conversion: Pω6|= x = λy .xy.
In particular,Pωis not extensional.
Proof: Letv (x ) = a, wherea 6= ∅is finite.
Then[[x ]]v= ais finite. But[[λy .xy ]]v= graph(. . . )is infinite.
27
Theory of P
ωTheorem (Hyland)
Pω|= M = N ⇐⇒ BT (M) = BT (N)
28
Trzy własności modeli denotacyjnych
I Poprawność: JeśliM =βN, to[[M]] = [[N]].
I Adekwatność: Jeśli[[M]] = [[N]], toM ≡ N.
I Pełna abstrakcyjność: JeśliM ≡ N, to[[M]] = [[N]].
Uwaga: Adekwatność to „słaba pełność”, a pełna abstrakcyjność to „silna poprawność”.
29
Trzy własności modeli denotacyjnych
I Poprawność: JeśliM =βN, to[[M]] = [[N]].
I Adekwatność: Jeśli[[M]] = [[N]], toM ≡ N.
I Pełna abstrakcyjność: JeśliM ≡ N, to[[M]] = [[N]].
Uwaga: Model Pωjest poprawny i adekwatny, ale nie jest w pełni abstrakcyjny.
30
Towards a fully abstract model
A projection ofBontoAis a pair of continuous functions ϕ : A → B and ψ : B → A,
such that
ψ ◦ ϕ = idA and ϕ ◦ ψ ≤ idB.
Thenϕ(⊥A) = ⊥B, becauseϕ(⊥A) ≤ ϕ(ψ(⊥B)) ≤ ⊥B.
ψ yy ψoo
ϕ //
31
Example
LetDbe any cpo. For exampleD = {⊥, >}. Functions ϕ0: D → [D → D] i ψ0: [D → D] → D, given by
ϕ0(d )(a) = d, oraz ψ0(f ) = f (⊥) make a projection of[D → D]ontoD.
32
Raising a projection
Let(ϕ, ψ)be a projection ofBontoA.
Then (ϕ∗, ψ∗) is a projection of[B → B]onto[A → A]:
ϕ∗(f ) = ϕ ◦ f ◦ ψ and ψ∗(g ) = ψ ◦ g ◦ ϕ,
A ϕ //B A
ϕ //B
g
A
f
OO
ψ B
oo OO
Aoo ψ B
33
Towards D
∞Take any fixedD0, for instanceD0= {⊥, >}.
Define by inductionDn+1= [Dn→ Dn].
Define projections(ϕn, ψn)ofDn+1ontoDnby induction:
(ϕn+1, ψn+1) = (ϕ∗n, ψn∗).
Two-way transmission:
D0 ϕ0
−→ D1 ϕ1
−→ D2 ϕ2
−→ · · · D0
ψ0
←− D1 ψ1
←− D2 ψ2
←− · · ·
34