Rachunek lambda, lato 2019-20

Rachunek lambda, lato 2019-20

Wykład 7

śrątek, 8 kwietnia 2020

1

W poprzednim odcinku: 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: A reflexive cpo is a lambda-model.

Projekcje

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

ϕ //

3

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.

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

5

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^ϕ0 ₁ −→ D^ϕ1 ₂ −→ · · ·^ϕ2 D₀ ←− D^ψ0 ₁ ←− D^ψ1 ₂ ←− · · ·^ψ2

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^ϕ0 ₁ −→ D^ϕ1 ₂ −→ · · ·^ϕ2 D₀ ←− D^ψ0 ₁ ←− D^ψ1 ₂ ←− · · ·^ψ2

6

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^ϕ0 ₁ −→ D^ϕ1 ₂ −→ · · ·^ϕ2 D₀ ←− D^ψ0 ₁ ←− D^ψ1 ₂ ←− · · ·^ψ2

Scott’s D

Thread: a sequence(x_n)_n∈N, with x_n ∈ D_n and x_n= ψ_n(x_n+1).

x₀ ←− x^ψ0 ₁ ←− x^ψ1 ₂ ←− · · ·^ψ2

Denote the set of all threads byD∞. Ordering:

x ≤ y iff ∀n ∈ N(xn ≤ y_n).

Fact: The setD∞ is a cpo.

Proof: For directed X ⊆ D∞ takeXn= {xn | x ∈ X }. Then(sup X_n)_n is a thread and (sup X_n)_n = sup X.

7

Scott’s D

Thread: a sequence(x_n)_n∈N, with x_n ∈ D_n and x_n= ψ_n(x_n+1).

x₀ ←− x^ψ0 ₁ ←− x^ψ1 ₂ ←− · · ·^ψ2

Denote the set of all threads byD∞. Ordering:

x ≤ y iff ∀n ∈ N(xn ≤ y_n).

Fact: The setD∞ is a cpo.

Proof: For directed X ⊆ D∞ takeXn= {xn | x ∈ X }. Then(sup X_n)_n is a thread and (sup X_n)_n = sup X.

Scott’s D

Thread: a sequence(x_n)_n∈N, with x_n ∈ D_n and x_n= ψ_n(x_n+1).

x₀ ←− x^ψ0 ₁ ←− x^ψ1 ₂ ←− · · ·^ψ2

Denote the set of all threads byD∞. Ordering:

x ≤ y iff ∀n ∈ N(xn ≤ y_n).

Fact: The setD∞ is a cpo.

Proof: For directed X ⊆ D∞ takeX_n= {x_n | x ∈ X }.

Then(sup X_n)_n is a thread and (sup X_n)_n = sup X.

7

Scott’s D

Forn < m define projections (ϕ_nm, ψ_nm) of D_m onto D_n: ϕnm = ϕm−1◦ · · · ◦ ϕn, ψnm= ψn◦ · · · ◦ ψm−1.

Define projections(ϕ_n∞, ψ_n∞) of D∞ onto D_n:

(ϕ_n∞(x ))_i =







ψ_in(x ), gdy i < n; x , gdy i = n; ϕ_ni(x ), gdy i > n.

ψ_n∞(y ) = y_n.

Convention:

D0 ⊆ D1 ⊆ D2 ⊆ · · · ⊆ D∞,

Element x ∈ D_n identified with an almost constant thread.

Scott’s D

Forn < m define projections (ϕ_nm, ψ_nm) of D_m onto D_n: ϕnm = ϕm−1◦ · · · ◦ ϕn, ψnm= ψn◦ · · · ◦ ψm−1. Define projections(ϕ_n∞, ψ_n∞) of D∞ onto D_n:

(ϕ_n∞(x ))_i =







ψ_in(x ), gdy i < n;

x , gdy i = n;

ϕni(x ), gdy i > n.

ψ_n∞(y ) = y_n.

Convention:

D0 ⊆ D1 ⊆ D2 ⊆ · · · ⊆ D∞,

Element x ∈ D_n identified with an almost constant thread.

8

Scott’s D

Forn < m define projections (ϕ_nm, ψ_nm) of D_m onto D_n: ϕnm = ϕm−1◦ · · · ◦ ϕn, ψnm= ψn◦ · · · ◦ ψm−1. Define projections(ϕ_n∞, ψ_n∞) of D∞ onto D_n:

(ϕ_n∞(x ))_i =







ψ_in(x ), gdy i < n;

x , gdy i = n;

ϕni(x ), gdy i > n.

ψ_n∞(y ) = y_n.

Convention:

D0 ⊆ D1 ⊆ D2 ⊆ · · · ⊆ D∞,

Element x ∈ D_n identified with an almost constant thread.

Application

x · y = sup{x_n+1(y_n) | n ∈ N}

Fact: Application is a continuous function.

Proof: One shows continuity wrt both arguments.

N.B.The sequence xn+1(yn)does not have to form a thread. But it is monotone: x_n(y_n−1) ≤ x_n+1(y_n), and has a supremum.

9

Application

x · y = sup{x_n+1(y_n) | n ∈ N}

Fact: Application is a continuous function.

Proof: One shows continuity wrt both arguments.

N.B.The sequence x_n+1(y_n)does not have to form a thread.

But it is monotone: x_n(y_n−1) ≤ x_n+1(y_n), and has a supremum.

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n). If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀. Proofs happily omitted.

10

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n). If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀. Proofs happily omitted.

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n).

If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀. Proofs happily omitted.

10

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n).

If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀. Proofs happily omitted.

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n).

If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀.

Proofs happily omitted.

10

Some properties

I Every thread is mononotone: x0 ≤ x1 ≤ x2 ≤ . . . and x = sup xn.

I The bottom is unique: ⊥D0 = ⊥Dn = ⊥D∞.

I If x ∈ D_n+1 then x · y = x (y_n).

If also y ∈ D_n, thenx · y = x (y ).

I If y ∈ D_n then (x · y )_n= x_n+1(y ).

I Always(x · ⊥)₀ = x₀. Proofs happily omitted.

Extensionality

Lemma

If x · z = y · z, for all z, then x = y.

Proof.

One shows that

if ∀z ∈ D∞(x · z ≤ y · z) then x_n ≤ y_n, for all n. Begin withx₀ = (x · ⊥)₀ ≤ (y · ⊥)₀ = y₀.

Thenxn+1(z) = (x · z)n≤ (y · z)n = yn+1(z), for z ∈ Dn.

11

Extensionality

Lemma

If x · z = y · z, for all z, then x = y.

Proof.

One shows that

if ∀z ∈ D_∞(x · z ≤ y · z) then x_n ≤ y_n, for all n.

Begin withx₀ = (x · ⊥)₀ ≤ (y · ⊥)₀ = y₀.

Thenxn+1(z) = (x · z)n≤ (y · z)n = yn+1(z), for z ∈ Dn.

Extensionality

Lemma

If x · z = y · z, for all z, then x = y.

Proof.

One shows that

if ∀z ∈ D_∞(x · z ≤ y · z) then x_n ≤ y_n, for all n.

Begin withx₀ = (x · ⊥)₀ ≤ (y · ⊥)₀ = y₀.

Thenxn+1(z) = (x · z)n≤ (y · z)n = yn+1(z), for z ∈ Dn.

11

Extensionality

Lemma

If x · z = y · z, for all z, then x = y.

Proof.

One shows that

if ∀z ∈ D_∞(x · z ≤ y · z) then x_n ≤ y_n, for all n.

Begin withx₀ = (x · ⊥)₀ ≤ (y · ⊥)₀ = y₀.

Thenxn+1(z) = (x · z)n≤ (y · z)n = yn+1(z), for z ∈ Dn.

Scott’s D

model

Theorem

The cpoD∞ is reflexive.

Proof.

DefineF : D∞→ [D∞→ D∞] by F (x )(y ) = x · y. We know that F is continuous and injective. Take anyf ∈ [D∞ → D∞].

Definef⁽ⁿ⁾ : Dn → Dn by f⁽ⁿ⁾(y ) = f (y )n, for y ∈ Dn. The sequencef⁽ⁿ⁾ is monotone. Define G (f ) = sup_nf⁽ⁿ⁾. ThenF (G (f )) = f. Details omitted.

12

Scott’s D

model

Theorem

The cpoD∞ is reflexive.

Proof.

DefineF : D∞→ [D∞→ D∞] by F (x )(y ) = x · y.

We know that F is continuous and injective.

Take anyf ∈ [D∞ → D∞].

Definef⁽ⁿ⁾ : Dn → Dn by f⁽ⁿ⁾(y ) = f (y )n, for y ∈ Dn. The sequencef⁽ⁿ⁾ is monotone. Define G (f ) = sup_nf⁽ⁿ⁾. ThenF (G (f )) = f. Details omitted.

Scott’s D

model

Theorem

The cpoD∞ is reflexive.

Proof.

DefineF : D∞→ [D∞→ D∞] by F (x )(y ) = x · y.

We know that F is continuous and injective.

Take anyf ∈ [D∞ → D∞].

Definef⁽ⁿ⁾ : D_n → D_n by f⁽ⁿ⁾(y ) = f (y )_n, for y ∈ D_n. The sequencef⁽ⁿ⁾ is monotone. Define G (f ) = sup_nf⁽ⁿ⁾. ThenF (G (f )) = f. Details omitted.

12

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Przykład: Co to jest [[λx x ]]?

To taki element e, że a = e · adla a ∈ D∞.

W szczególności dla a ∈ Dn jest a = an = (e · a)n= en+1(a). No toe_n+1 = id_Dn, czyli e = (⊥, id, id, ...

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Przykład: Co to jest [[λx x ]]?

To taki element e, że a = e · adla a ∈ D∞.

W szczególności dla a ∈ Dn jest a = an = (e · a)n= en+1(a). No toe_n+1 = id_Dn, czyli e = (⊥, id, id, ...

13

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Przykład: Co to jest [[λx x ]]?

To taki element e, że a = e · adla a ∈ D∞.

W szczególności dla a ∈ Dn jest a = an = (e · a)n= en+1(a). No toe_n+1 = id_Dn, czyli e = (⊥, id, id, ...

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Przykład: Co to jest [[λx x ]]?

To taki element e, że a = e · adla a ∈ D∞.

W szczególności dla a ∈ Dn jest a = an = (e · a)n= en+1(a).

No toe_n+1 = id_Dn, czyli e = (⊥, id, id, ...

13

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Przykład: Co to jest [[λx x ]]?

To taki element e, że a = e · adla a ∈ D∞.

W szczególności dla a ∈ Dn jest a = an = (e · a)n= en+1(a).

No toe_n+1 = id_Dn, czyli e = (⊥, id, id, ...

Przykład

Kombinator Y jest interpretowany jako operator najmniejszego punktu stałego, tj.:

[[Y ]] · a jest najmniejszym elementem b o własności a · b = b.

14

Wieloznaczność w D

Funkcje ciągłe

F : D∞ → [D∞ → D∞] i G : [D∞→ D∞] → D∞

są wzajemnie odwrotnymi izomorfizmami.

To znaczy, że każdy elementa ∈ D∞ można utożsamiać z funkcją ciągłą F (a) ∈ [D∞→ D_∞], a nawet z funkcją

F ◦ F (a) ◦ G ∈ [[D∞ → D∞] → [D∞ → D∞]]

Aplikacjaa · b to to samo co F (a)(b)i można pisać a(b).

I to samo co(F ◦ F (a) ◦ G )(F (b)) = F (F (a)(G (F (b))) = F (F (a)(b)) = F (a · b).

Scott’s D

model

Corollary

The cpoD∞ is an extensional lambda-model.

It is isomorphic to [D∞ → D∞].

Twierdzenie (Hyland, Wadsworth)

The modelD∞ is “adequate” and “fully abstract”:

TermsM i N are observationally equivalent iffD∞ |= M = N.

16

Ściślej:

Twierdzenie (Hyland, Wadsworth)

Następujące warunki są równoważne:

1. Termy M i N są obserwacyjnie równoważne.

2. BT (M) ≈_η BT (N).

3. D∞ |= M = N.

Implikacja (1) ⇒ (2)to w istocie twierdzenie Böhma.

Naszkicujemy(3) ⇒ (1) (adekwatność) i (2) ⇒ (3).

Definicje

NiechB, B⁰ będą drzewami Böhma. NapisB v B⁰ oznacza, że B⁰ powstaje z B przez wstawienie jakichś poddrzew w miejsca, w których w B występuje ⊥.

Relacja B _η B⁰ zachodzi gdy istnieje (skończony lub nie) ciąg eta-ekspansji

B = B_{0 η}← B_{1 η}← B_{2 η}← B_{3 η}← · · · zbieżny doB⁰. Zatem:

B ≈_η B⁰ ⇔ B _η B⁰⁰_η B⁰ dla pewnego B⁰⁰

18

Definicje

NiechB, B⁰ będą drzewami Böhma. NapisB v B⁰ oznacza, że B⁰ powstaje z B przez wstawienie jakichś poddrzew w miejsca, w których w B występuje ⊥.

Relacja B _η B⁰ zachodzi gdy istnieje (skończony lub nie) ciąg eta-ekspansji

B = B_{0 η}← B_{1 η}← B_{2 η}← B_{3 η}← · · · zbieżny doB⁰.

Zatem:

B ≈_η B⁰ ⇔ B _η B⁰⁰_η B⁰ dla pewnego B⁰⁰

Definicje

NiechB, B⁰ będą drzewami Böhma. NapisB v B⁰ oznacza, że B⁰ powstaje z B przez wstawienie jakichś poddrzew w miejsca, w których w B występuje ⊥.

Relacja B _η B⁰ zachodzi gdy istnieje (skończony lub nie) ciąg eta-ekspansji

B = B_{0 η}← B_{1 η}← B_{2 η}← B_{3 η}← · · · zbieżny doB⁰. Zatem:

B ≈_η B⁰ ⇔ B _η B⁰⁰_η B⁰ dla pewnego B⁰⁰

18

Aproksymanty

Aproksymant to skończone drzewo Böhma (term w postaci normalnej), w którym może występować stała ⊥).

Przyjmujemy, że [[⊥]] = ⊥_D∞

Zbiór aproksymantów drzewa/termu:

A(T ) = {A | A jest aproksymantem oraz A v T } A(M) = A(BT (M)).

Twierdzenie o aproksymacji:

[[M]]_ρ = sup{[[A]]_ρ | A ∈ A(M)}. Dowód: Opuszczamy.

Aproksymanty

Aproksymant to skończone drzewo Böhma (term w postaci normalnej), w którym może występować stała ⊥).

Przyjmujemy, że [[⊥]] = ⊥_D∞

Zbiór aproksymantów drzewa/termu:

A(T ) = {A | A jest aproksymantem oraz A v T } A(M) = A(BT (M)).

Twierdzenie o aproksymacji:

[[M]]_ρ = sup{[[A]]_ρ | A ∈ A(M)}. Dowód: Opuszczamy.

19

Aproksymanty

Aproksymant to skończone drzewo Böhma (term w postaci normalnej), w którym może występować stała ⊥).

Przyjmujemy, że [[⊥]] = ⊥_D∞

Zbiór aproksymantów drzewa/termu:

A(T ) = {A | A jest aproksymantem oraz A v T } A(M) = A(BT (M)).

Twierdzenie o aproksymacji:

[[M]]_ρ = sup{[[A]]_ρ | A ∈ A(M)}.

Dowód: Opuszczamy.

Intuicje (czyli machanie rękami)

Twierdzenie o aproksymacji:

[[M]]_ρ = sup{[[A]]_ρ | A ∈ A(M)}.

Znaczenie [[M]]_ρ to nić x ∈ D∞, czyli w istocie ciąg funkcjix_n+1 : D_n→ D_n, opisujących zachowanie [[M]]_ρ na skończonym zbiorze D_n elementów rzędu n.

To zachowanie jest zdeterminowane przez skończony fragment początkowy drzewa Böhma BT (M).

20

Tw. o aproksymacji: [[M]]_ρ= sup{[[A]]_ρ | A ∈ A(M)}.

Wniosek: Term M jest rozwiązalny wtedy i tylko wtedy, gdy[[M]]_ρ 6= ⊥, dla pewnego ρ.

Dowód: (⇒) Jeśli M =_β λx₁. . . x_n. y ~N, gdziey wolne, to [[M]]_%6= ⊥, dla ρ(y ) = λλ~a.d, gdzie d 6= ⊥.

JeśliM =_β λx1. . . x_n. x_iN, to~ [[M]]_ρ6= ⊥, dla każdego ρ. Należy użyćλλ~a.d jakoi-tego argumentu dla [[M]]_ρ. (⇐) Wtedy z tw. o aproksymacji istnieje nietrywialny aproksymant, czyli jest czołowa postać normalna.

Tw. o aproksymacji: [[M]]_ρ= sup{[[A]]_ρ | A ∈ A(M)}.

Wniosek: Term M jest rozwiązalny wtedy i tylko wtedy, gdy[[M]]_ρ6= ⊥, dla pewnego ρ.

Dowód: (⇒) Jeśli M =_β λx₁. . . x_n. y ~N, gdziey wolne, to [[M]]_%6= ⊥, dla ρ(y ) = λλ~a.d, gdzie d 6= ⊥.

JeśliM =_β λx1. . . x_n. x_iN, to~ [[M]]_ρ6= ⊥, dla każdego ρ. Należy użyćλλ~a.d jakoi-tego argumentu dla [[M]]_ρ. (⇐) Wtedy z tw. o aproksymacji istnieje nietrywialny aproksymant, czyli jest czołowa postać normalna.

21

Tw. o aproksymacji: [[M]]_ρ= sup{[[A]]_ρ | A ∈ A(M)}.

Wniosek: Term M jest rozwiązalny wtedy i tylko wtedy, gdy[[M]]_ρ6= ⊥, dla pewnego ρ.

Dowód: (⇒) JeśliM =_β λx₁. . . x_n. y ~N, gdzie y wolne, to[[M]]_%6= ⊥, dla ρ(y ) = λλ~a.d, gdzied 6= ⊥.

JeśliM =_β λx1. . . x_n. x_iN, to~ [[M]]_ρ6= ⊥, dla każdego ρ.

Należy użyćλλ~a.d jakoi-tego argumentu dla [[M]]ρ.

(⇐) Wtedy z tw. o aproksymacji istnieje nietrywialny aproksymant, czyli jest czołowa postać normalna.

Tw. o aproksymacji: [[M]]_ρ= sup{[[A]]_ρ | A ∈ A(M)}.

Wniosek: Term M jest rozwiązalny wtedy i tylko wtedy, gdy[[M]]_ρ6= ⊥, dla pewnego ρ.

Dowód: (⇒) JeśliM =_β λx₁. . . x_n. y ~N, gdzie y wolne, to[[M]]_%6= ⊥, dla ρ(y ) = λλ~a.d, gdzied 6= ⊥.

JeśliM =_β λx1. . . x_n. x_iN, to~ [[M]]_ρ6= ⊥, dla każdego ρ.

Należy użyćλλ~a.d jakoi-tego argumentu dla [[M]]ρ. (⇐) Wtedy z tw. o aproksymacji istnieje nietrywialny aproksymant, czyli jest czołowa postać normalna.

21

Adekwatność

Twierdzenie:

JeśliD_∞ |= M = N, to M ≡ N.

Dowód: Jeśli [[M]]ρ= [[N]]ρ to także [[C [M]]]ρ = [[C [N]]]ρ. Jeśli jedno jest różne od⊥, to i drugie. Zatem jeśli jedno rozwiązalne to i drugie.

Adekwatność

Twierdzenie:

JeśliD_∞ |= M = N, to M ≡ N.

Dowód: Jeśli [[M]]ρ= [[N]]ρ to także [[C [M]]]ρ = [[C [N]]]ρ. Jeśli jedno jest różne od⊥, to i drugie. Zatem jeśli jedno rozwiązalne to i drugie.

22

Lemat

Lemat: Niech T₁ _η T₂. Wtedy:

• JeśliA ∈ A(T₁), to istnieje takie B ∈ A(T₂), że B η A.

• JeśliB ∈ A(T2), to istnieje takie A ∈ A(T1), że B η A.

Dowód: W nieskończonym ciągu eta-ekspansji od T₁ do T₂ tylko skończenie wiele kroków dotyczy wierzchołków drzewaT₁ które należą do aproksymantaA. Te eta-ekspansje

przekształcają Aw pewnego aproksymanta drzewa T₂. W przeciwnym kierunku analogicznie.

Lemat

Lemat: Niech T₁ _η T₂. Wtedy:

• JeśliA ∈ A(T₁), to istnieje takie B ∈ A(T₂), że B η A.

• JeśliB ∈ A(T2), to istnieje takie A ∈ A(T1), że B η A.

Dowód: W nieskończonym ciągu eta-ekspansji od T₁ do T₂ tylko skończenie wiele kroków dotyczy wierzchołków drzewaT₁ które należą do aproksymantaA. Te eta-ekspansje

przekształcają Aw pewnego aproksymanta drzewa T₂. W przeciwnym kierunku analogicznie.

23

Wniosek

Lemat: Niech T₁ _η T₂. Wtedy:

• JeśliA ∈ A(T1), to istnieje takie B ∈ A(T2), że B η A.

• JeśliB ∈ A(T₂), to istnieje takie A ∈ A(T₁), że B η A.

Wniosek:

Jeśli przyjmiemy, że[[T ]]_ρ= sup{[[A]]_ρ | A ∈ A(T )}, to zT1 η T2 wynika [[T1]]ρ= [[T2]]ρ, dla każdegoρ.

Pełna abstrakcyjność

Twierdzenie: Jeśli M ≡ N, to[[M]] = [[N]]

Dowód: Skoro M ≡ N, to BT (M) ≈_η BT (N), czyli BT (M) _η T _η BT (N). (To w istocie tw. Böhma.) Z poprzedniego lematu wynika[[BT (M)]]ρ= [[BT (N)]]ρ. Ale[[M]]_ρ= [[BT (M)]]_ρ i [[N]]_ρ= [[BT (N)]]_ρ na mocy twierdzenia o aproksymacji.

Zatem także[[M]]_ρ i [[N]]_ρ muszą być równe.

25