Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 6

3 kwietnia 2020

1

(2)

Modele

(3)

Semantics

Goal: Interpret any termM as an element [[M]] of some structureA, so that M =_β N implies [[M]] = [[N]].

More precisely, [[M]] may depend on avaluation: v : Var → A.

Write [[M]]_v for the value of M underv.

3

(4)

Semantics

Goal: Interpret any termM as an element [[M]] of some structureA, so that M =_β N implies [[M]] = [[N]].

More precisely, [[M]] may depend on avaluation:

v : Var → A.

Write [[M]]_v for the value of M underv.

(5)

Lambda-interpretation: A = hA, ·, [[ ]] i

Application · is a binary operation inA;

[[ ]] : Λ × A^Var → 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) If v |_FV(P)= u|_FV(P), then [[P]]_v = [[P]]_u.

4

(6)

Lambda-interpretation: A = hA, ·, [[ ]] i

[[ ]] : Λ × A^Var → A.

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) If v |_FV(P)= u|_FV(P), then [[P]]_v = [[P]]_u.

(7)

Lambda-interpretation: A = hA, ·, [[ ]] i

[[ ]] : Λ × A^Var → A.

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) If v |_FV(P)= u|_FV(P), then [[P]]_v = [[P]]_u.

4

(8)

Dygresja

Jeśli znamy[[P]]_v i [[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]}, dla a ∈ A.

(9)

Dygresja

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]}, dla a ∈ A.

5

(10)

Dygresja

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]}, dla a ∈ A.

(11)

Dygresja

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]}, dla a ∈ A.

5

(12)

Dygresja

Warunek ∀v ([[P]]_v = [[Q]]_v) to trochę za dużo.

Należy wymagać [[P]]_{v [x 7→a]} = [[Q]]_{v [x 7→a]}, dla a ∈ A.

(13)

Dygresja

Warunek ∀v ([[P]]_v = [[Q]]_v) to trochę za dużo.

Należy wymagać [[P]]_{v [x 7→a]} = [[Q]]_{v [x 7→a]}, dla a ∈ A.

5

(14)

Extensionality

Write a ≈ b whena · c = b · c, for all c.

Extensional interpretation: a ≈ b implies a = b, for alla, b. Weakly extensional interpretation:

[[λx .M]]v ≈ [[λx.N]]v implies[[λx .M]]v = [[λx .N]]v, for all N, v. Meaning: Abstraction makes sense algebraically.

(N.B.[[λx .M]]_v ≈ [[λx.N]]_v iff [[M]]_{v [x 7→a]} = [[N]]_{v [x 7→a]}, all a.)

(15)

Extensionality

Extensional interpretation: a ≈ b implies a = b, for alla, b.

Weakly extensional interpretation:

[[λx .M]]v ≈ [[λx.N]]v implies[[λx .M]]v = [[λx .N]]v, for all N, v. Meaning: Abstraction makes sense algebraically.

6

(16)

Extensionality

[[λx .M]]v ≈ [[λx.N]]v implies [[λx .M]]v = [[λx .N]]v, for all N, v.

Meaning: Abstraction makes sense algebraically.

(17)

Extensionality

[[λx .M]]v ≈ [[λx.N]]v implies [[λx .M]]v = [[λx .N]]v, for all N, v.

Meaning: Abstraction makes sense algebraically.

6

(18)

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

(19)

Lambda-algebra and lambda-model

Lambda-algebra: a lambda-interpretation satisfying beta:

Lambda-model : Weakly extensional lambda-interpretation:

[[λx .M]]_v ≈ [[λx.N]]_v implies [[λx .M]]_v = [[λx .N]]_v

7

(20)

“Trivial” examples

M(λ) = hΛ/₌_β, ·, [[ ]] i,

where[[M]]_v = [M[~x := v (~x )]]_β and [M]_β· [N]_β = [MN]_β

Similarly:

M(λη) = hΛ/₌_β_η, ·, [[ ]] i; M⁰(λ) = hΛ⁰/₌_β, ·, [[ ]] i; M⁰(λη) = hΛ⁰/₌_β_η, ·, [[ ]] i.

(21)

“Trivial” examples

M(λ) = hΛ/₌_β, ·, [[ ]] i,

where[[M]]_v = [M[~x := v (~x )]]_β and [M]_β· [N]_β = [MN]_β

Similarly:

M(λη) = hΛ/₌_β_η, ·, [[ ]] i;

M⁰(λ) = hΛ⁰/₌_β, ·, [[ ]] i;

M⁰(λη) = hΛ⁰/₌_β_η, ·, [[ ]] i.

8

(22)

“Trivial” examples

Fact

StructuresM(λ) and M(λη) are lambda-models.

StructuresM⁰(λ) and M⁰(λη) are lambda-algebras,

but not lambda-models. It may happen that MP =_β NP for all closed P,

(i.e. [λx . Mx ] ≈ [λx . Nx ]), but Mx 6=_β Nx

(i.e. [λx . Mx ] 6= [λx . Nx ]).

(23)

“Trivial” examples

Fact

but not lambda-models.

It may happen that MP =_β NP for all closed P, (i.e. [λx . Mx ] ≈ [λx . Nx ]),

but Mx 6=_β Nx

(i.e. [λx . Mx ] 6= [λx . Nx ]).

9

(24)

“Trivial” examples

Fact

but not lambda-models.

It may happen that MP =_β NP for all closed P, (i.e. [λx . Mx ] ≈ [λx . Nx ]),

but Mx 6=_β Nx

(i.e. [λx . Mx ] 6= [λx . Nx ]).

(25)

Very Important Lemma

Lemma

In every lambda-model, [[M[x := N]]]_v = [[M]]v [x 7→[[N]]v].

Proof: Induction wrt M. First assume that x 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 all a. Therefore[[(λy P)[x := N]]]_v = [[(λy .P)]]v [x 7→[[N]]v].

10

(26)

Very Important Lemma

Lemma

In every lambda-model, [[M[x := N]]]_v = [[M]]v [x 7→[[N]]v]. Proof: Induction wrt M. First assume that x 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

(27)

Very Important Lemma

Lemma

= [[P[x := N]]]_{v [y 7→a]} =

[[P]]v [y 7→a][x 7→[[N]]v [y 7→a]]

10

(28)

Very Important Lemma

Lemma

(29)

Very Important Lemma

Lemma

= [[P]]v [y 7→a][x 7→[[N]]v]=

[[λy .P]]v [x 7→[[N]]v]· a, for all a. Therefore[[(λy P)[x := N]]]_v = [[(λy .P)]]v [x 7→[[N]]v].

10

(30)

Very Important Lemma

Lemma

= [[P]]v [y 7→a][x 7→[[N]]v]= [[λy .P]]v [x 7→[[N]]v]· a, for all a.

Therefore[[(λy P)[x := N]]]_v = [[(λy .P)]]v [x 7→[[N]]v].

(31)

Very Important Lemma

Lemma

= [[P]]v [y 7→a][x 7→[[N]]v]= [[λy .P]]v [x 7→[[N]]v]· a, for all a.

Therefore[[(λy P)[x := N]]]_v = [[(λy .P)]]v [x 7→[[N]]v].

10

(32)

Very Important Lemma

Lemma

In every lambda-model, [[M[x := N]]]_v = [[M]]v [x 7→[[N]]v]

Proof.

In case x ∈FV(N) take fresh z and 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].

(33)

Very Important Lemma

Lemma

Proof.

In case x ∈FV(N) take fresh z and 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

(34)

Very Important Lemma

Lemma

Proof.

[[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].

(35)

Very Important Lemma

Lemma

Proof.

[[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

(36)

Very Important Lemma

Lemma

Proof.

[[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].

(37)

Very Important Lemma

Lemma

Proof.

[[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

(38)

Very Important Lemma

Lemma

Proof.

[[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].

(39)

Soundness

Proposition

Every lambda-model is a lambda-algebra:

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 =β Q and let M = λ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

(40)

Soundness

Proposition

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 =β Q and let M = λx .P, N = λx .Q. Then [[M]]_v · a = [[P]]_{v [x 7→a]} = [[Q]]_{v [x 7→a]} = [[N]]_v · a, for alla.

(41)

Soundness

Proposition

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 =β Q and let M = λ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

(42)

Completeness

Theorem

The following are equivalent:

1) M =β N;

2) A |= M = N, for every lambda-algebraA;

3) A |= M = N, for every lambda-model A.

Proof.

(1)⇒(2) Obvious.

(2)⇒(3) By soundness.

(3)⇒(1) BecauseM(λ) is a lambda-model.

(43)

Modele Scotta

14

(44)

Complete partial orders

LethA, ≤i be a partial order.

A subsetB ⊆ A is directed (skierowany) when

for every a, b ∈ B there isc ∈ B with a, b ≤ c.

The setAis a complete partial order (cpo) when

every directed subset has a supremum. It follows that every cpo has a least element⊥ = sup ∅.

(45)

Complete partial orders

every directed subset has a supremum.

It follows that every cpo has a least element⊥ = sup ∅.

15

(46)

Complete partial orders

every directed subset has a supremum.

It follows that every cpo has a least element⊥ = sup ∅.

(47)

Complete partial orders

LethA, ≤i and hB, ≤i be cpos, and f : A → B. Thenf is monotone if a ≤ a⁰ implies f (a) ≤ f (a⁰).

Andf is continuous if sup f (C ) = f (sup C )

for every nonempty directed C ⊆ A. Fact: Every continuous function is monotone.

[A → B]is the set of all continuous functions from A to B

16

(48)

Complete partial orders

for every nonempty directed C ⊆ A.

Fact: Every continuous function is monotone.

(49)

Complete partial orders

16

(50)

Complete partial orders

(51)

Complete partial orders

If hA, ≤i and hB, ≤i are cpos then:

I The productA × B is a cpo with

ha, bi ≤ ha⁰, b⁰i iff a ≤ a⁰ and b ≤ b⁰.

I The function space[A → B] is a cpo with

f ≤ g iff ∀a. f (a) ≤ g (a).

17

(52)

Continuous functions

Lemma

A functionf : A × B → C is 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.

(53)

Continuous functions

Lemma

The applicationApp : [A → B] × A → B is continuous.

Proof hint:

Use the previous lemma.

Lemma

The abstractionAbs : [(A × B) → C ] → [A → [B → C ]], given by Abs(F )(a)(b) = F (a, b), is continuous.

19

(54)

Reflexive cpo

The cpoD is reflexive iff there are continuous functions F : D → [D → D] and G : [D → D] → D,

with F ◦ G = id_[D→D].

ThenF must be onto and G is injective.

The following are equivalent conditions:

“G ◦ F = id_D”, “G onto”, “F injective”.

(55)

Reflexive cpo

20

(56)

Reflexive cpo

(57)

Reflexive cpo

F : D → [D → D], G : [D → D] → D, F ◦ G = id.

Define application asa · b = F (a)(b) so that G (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 of App and Abs.)

21

(58)

Reflexive cpo

F : D → [D → D], G : [D → D] → D, F ◦ G = id.

Define application asa · b = F (a)(b)so that G (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]}).

(59)

Reflexive cpo

F : D → [D → D], G : [D → D] → D, F ◦ G = id.

I [[x ]]_v = v (x );

I [[PQ]]v = [[P]]v · [[Q]]v;

I [[λx .P]]_v = G (λλa.[[P]]_{v [x 7→a]}).

21

(60)

Reflexive cpo

F : D → [D → D], G : [D → D] → D, F ◦ G = id.

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 of App and Abs.)

(61)

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

(62)

Reflexive cpo

Theorem

Proof.

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]}.

(63)

Reflexive cpo

Theorem

Proof.

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]}.

22

(64)

Reflexive cpo

Theorem

Proof.

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:

(65)

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 all a ∈ P_ω.

Moral: A continuous function is fully determined by its values on finite arguments.

23

(66)

A reflexive cpo: Model P

_ω

= hP(N), ⊆i

NotationPω = P(N).

Lemma

(67)

A reflexive cpo: Model P

_ω

= hP(N), ⊆i

NotationPω = P(N).

Lemma

23

(68)

A reflexive cpo: Model P

_ω

= hP(N), ⊆i

NotationPω = P(N).

Lemma

Moral: A continuous function is fully determined

(69)

Encodings in P

_ω

Pairs:

(m, n) = (n + m)(n + m + 1)

2 + m,

Finite sets: e₀ = ∅, and

e_n= {k₀, k₁, . . . , k_{r −1}}, forn =X

i <r

2^kⁱ.

24

(70)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

Lemma: Functions graph and fun are continuous, and fun ◦ graph = id_[P_ω→Pω].

Proof: fun(graph(f ))(x) =

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

(71)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

25

(72)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

(73)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

25

(74)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

(75)

P

_ω

is reflexive

graph(f ) = {(n, m) | m ∈ f (en)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

= {m | ∃n ∈ N(en⊆ x ∧ (n, m) ∈ graph(f ))}

= {m | ∃n ∈ N(eⁿ⊆ x ∧ m ∈ f (en))}

=S{f (en) | e_n⊆ x} = f (x).

25

(76)

Przykłady w P

_ω

(ćwiczenie)

I [[I]] = graph(id) = {(n, m) | m ∈ en};

I [[K]] = {(m, (k, `)) | ` ∈ em};

I [[ω]] = {(x , m) | ∃n(e_n⊆ e_x ∧ (n, m) ∈ e_x)};

I [[Ω]] = ∅ = ⊥.

(77)

P

_ω

is not a model of η-conversion

graph(f ) = {(n, m) | m ∈ f (e_n)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

Every nonempty graph(f ) is infinite:

If (n, m) ∈ graph(f )then also (k, m) ∈ graph(f ), for e_n⊆ e_k. (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, where a 6= ∅ is finite.

Then[[x ]]_v = a is finite. But [[λy .xy ]]_v = graph(. . . ) is infinite.

27

(78)

P

_ω

is not a model of η-conversion

graph(f ) = {(n, m) | m ∈ f (e_n)};

fun(a)(x) = {m | ∃n ∈ N(en ⊆ x ∧ (n, m) ∈ a)}.

Every nonempty graph(f ) is infinite:

If (n, m) ∈ graph(f )then also (k, m) ∈ graph(f ), for e_n⊆ e_k. (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, where a 6= ∅ is finite.

(79)

Theory of P

_ω

Theorem (Hyland)

P_ω |= M = N ⇐⇒ BT (M) = BT (N)

28

(80)

(81)

Trzy własności modeli denotacyjnych

I Poprawność: Jeśli M =_β N, to[[M]] = [[N]].

I Adekwatność: Jeśli[[M]] = [[N]], to M ≡ 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

(82)

Trzy własności modeli denotacyjnych

(83)

Trzy własności modeli denotacyjnych

29

(84)

Trzy własności modeli denotacyjnych

(85)

Trzy własności modeli denotacyjnych

Uwaga: Model P_ω jest poprawny i adekwatny, ale nie jest w pełni abstrakcyjny.

30

(86)

Towards a fully abstract model

A projection ofB onto Ais a pair of continuous functions ϕ : A → B and ψ : B → A,

such that

ψ ◦ ϕ = idA and ϕ ◦ ψ ≤ idB.

Thenϕ(⊥_A) = ⊥_B, because ϕ(⊥_A) ≤ ϕ(ψ(⊥_B)) ≤ ⊥_B.

ψ

yy ^ψoo

ϕ //

(87)

Towards a fully abstract model

A projection ofB onto Ais 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

(88)

Example

LetD be any cpo. For example D = {⊥, >}. 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] onto D.

(89)

Raising a projection

Let(ϕ, ψ) be a projection of B onto A.

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

A B

ψ

oo

33

(90)

Towards D

_∞

Take any fixedD₀, for instance D₀ = {⊥, >}.

Define by inductionDn+1 = [Dn → Dn].

Define projections(ϕ_n, ψ_n) of D_n+1 onto D_n by induction: (ϕ_n+1, ψ_n+1) = (ϕ^∗_n, ψ^∗_n).

Two-way transmission:

D₀ −→ D^ϕ⁰ ₁ −→ D^ϕ¹ ₂ −→ · · ·^ϕ² D₀ ←− D^ψ⁰ ₁ ←− D^ψ¹ ₂ ←− · · ·^ψ²

(91)

Towards D

_∞

Define projections(ϕ_n, ψ_n) of D_n+1 onto D_n by induction:

(ϕ_n+1, ψ_n+1) = (ϕ^∗_n, ψ^∗_n).

D₀ −→ D^ϕ⁰ ₁ −→ D^ϕ¹ ₂ −→ · · ·^ϕ² D₀ ←− D^ψ⁰ ₁ ←− D^ψ¹ ₂ ←− · · ·^ψ²

34

(92)

Towards D

_∞

Define projections(ϕ_n, ψ_n) of D_n+1 onto D_n by induction:

(ϕ_n+1, ψ_n+1) = (ϕ^∗_n, ψ^∗_n).

D₀ −→ D^ϕ⁰ ₁ −→ D^ϕ¹ ₂ −→ · · ·^ϕ² D₀ ←− D^ψ⁰ ₁ ←− D^ψ¹ ₂ ←− · · ·^ψ²