Rachunek lambda - ci¡g dalszy

(1)

Rachunek lambda - ci¡g dalszy

18 marca 2013

(2)

Siªa wyrazu: logika zdaniowa

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.

◦

(3)

Ordered pair

Pair = Boolean selector:

hM, Ni = λx.xMN;

π_i = λx1x2.xi (i = 1, 2);

Π_i = λp. pπ_i (i = 1, 2).

It works:

Π₁hM, Ni →β hM, Niπ1 β M.

◦

(4)

Ordered pair

Pair = Boolean selector:

hM, Ni = λx.xMN;

π_i = λx1x2.xi (i = 1, 2);

Π_i = λp. pπ_i (i = 1, 2).

It works:

Π₁hM, Ni →β hM, Niπ₁ β M.

◦

(5)

Church's numerals

c

n

= n = λfx.f

ⁿ

( x),

0 = λfx.x;

1 = λfx.fx;

2 = λfx.f (fx);

3 = λfx.f (f (fx)), etc.

(6)

Some denable functions

I Successor: succ = λnfx.f (nfx);

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;

◦

(7)

Some denable functions

◦

(8)

Some denable functions

◦

(9)

Some denable functions

◦

(10)

Some denable functions

◦

(11)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

Step = λp.hsucc(pπ₁),pπ₁i pred = λn. (n Steph0, 0i)π2

How it works:

Steph0, 0i β h1, 0i Steph1, 0i β h2, 1i Steph2, 1i β h3, 2i, and so on.

◦

(12)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

◦

(13)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

◦

(14)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

Steph0, 0i β h1, 0i

Steph1, 0i β h2, 1i Steph2, 1i β h3, 2i, and so on.

◦

(15)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

Steph0, 0i β h1, 0i Steph1, 0i β h2, 1i

Steph2, 1i β h3, 2i, and so on.

◦

(16)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

Steph0, 0i β h1, 0i Steph1, 0i β h2, 1i Steph2, 1i β h3, 2i,

and so on.

◦

(17)

Predecessor is denable too

p(n + 1) = n, p(0) = 0

How it works:

(18)

Undecidability

The following are undecidable problems:

I Given M and N, does M β N hold?

I Given M and N, does M =β N hold?

I Given M, does M normalize?

I Given M, does M strongly normalize?

◦

(19)

Undecidability

◦

(20)

Undecidability

◦

(21)

Undecidability

(22)

The standard theory

◦

(23)

Adding equational axioms

Example

Add the axiom K = Sto the equational theory of λ-calculus.

Then, for every M, one proves: M = SI(KM)I = KI(KM)I = I. This extension is inconsistent.

Böhm Theorem

Let M, N be β-normal combinators withM 6=βη N. ThenM~P =β trueand N~P =β false, for some ~P.

◦

(24)

Adding equational axioms

Example

Add the axiom K = Sto the equational theory of λ-calculus. Then, for every M, one proves:

M = SI(KM)I = KI(KM)I = I.

This extension is inconsistent.

Böhm Theorem

Let M, N be β-normal combinators withM 6=βη N. ThenM~P =β trueand N~P =β false, for some ~P.

◦

(25)

Adding equational axioms

Example

Add the axiom K = Sto the equational theory of λ-calculus. Then, for every M, one proves:

M = SI(KM)I = KI(KM)I = I.

This extension is inconsistent.

Böhm Theorem

Let M, N be β-normal combinators withM 6=βη N.

ThenM~P =β trueand N~P =β false, for some ~P.

(26)

Böhm Trees (nite case)

λxy. x

zzzzzzzzz

@@

@ λxy. x

xxxxxxxxx

;;

λz. x

BB BB BB

BB y λzv. x

DD DD DD DD

D y

z y z x v

M = λxy.x(λz.xzy)y N = λxy.x(λzv.xzxv)y

◦

(27)

Böhm Trees: the dierence

λxy. x

zzzzzzzzz zzzzzzzzz

@@

@ λxy. x

xxxxxxxxx xxxxxxxxx

;;

λz. x

BB BB BB BB

BB BB BB

BB y λzv. x

DD DD DD DD

D y

z y z x v

M = λxy.x(λz.xzy)y N = λxy.x(λzv.xzxv)y Trick: Applying M to λuv. hu, vi gives λy. hλz.hz, yi, yi.

And components can be extracted from a pair.

(28)

Discriminating terms

M = λxy.x(λz.xzy)y N = λxy.x(λzv.xzxv)y

Applying M and N toP = λuv. hu, vi, then to any Q yields: hλz.hz, Qi, Qi hλzv.hz, Piv, Qi

Next appply both to true, I, false to obtain:

Q P = λuv.hu, vi

ChooseQ = λuvw. true and apply both sides tofalse, I, true:

true false.

◦

(29)

Discriminating terms

M = λxy.x(λz.xzy)y N = λxy.x(λzv.xzxv)y Applying M and N toP = λuv. hu, vi, then to any Q yields:

hλz.hz, Qi, Qi hλzv.hz, Piv, Qi

Next appply both to true, I, false to obtain:

Q P = λuv.hu, vi

true false.

◦

(30)

Discriminating terms

hλz.hz, Qi, Qi hλzv.hz, Piv, Qi Next appply both to true, I, false to obtain:

Q P = λuv.hu, vi

true false.

◦

(31)

Discriminating terms

hλz.hz, Qi, Qi hλzv.hz, Piv, Qi Next appply both to true, I, false to obtain:

Q P = λuv.hu, vi

true false.

(32)

The Meaning of Value and Undened

First idea: Value = Normal form.

Undened = without normal form.

Can we identify all such terms?

No: for instance λx.xKΩ = λx.xSΩ implies K = S (apply both to K).

Moral: A term without normal form can still behave in a well-dened way. In a sense it has a value.

Better idea: Value = Head normal form. Undened = without head normal form.

◦

(33)

The Meaning of Value and Undened

◦

(34)

The Meaning of Value and Undened

◦

(35)

The Meaning of Value and Undened

◦

(36)

The Meaning of Value and Undened

Better idea: Value = Head normal form.

Undened = without head normal form.

◦

(37)

Solvability

A closed term is solvable i M~P =β I, for some closed ~P.

If FV(M) = ~x then M is solvable i λ~x M is solvable.

Theorem

A term is solvable i it has a head normal form. Proof for closed terms:

(⇒) If M~P =β I then M~P β I. If M~P head normalizes then also M must head normalize.

(⇐) If M =β λx1x2. . .xn.xiR1. . .Rm then MP . . . P = I, for P = λy1. . .ym.I.

◦

(38)

Solvability

Theorem

A term is solvable i it has a head normal form. Proof for closed terms:

◦

(39)

Solvability

Theorem

A term is solvable i it has a head normal form.

Proof for closed terms:

◦

(40)

Solvability

Theorem

◦

(41)

Solvability

Theorem

(⇐) If M =β λx₁x₂. . .x_n.x_iR₁. . .R_m then MP . . . P = I, for P = λy1. . .ym.I.

(42)

The standard theory

We identify all unsolvable terms as undened.

Which solvable terms may be now be consistently identied? We cannot classify terms by their head normal forms.

Too many of them!

We can onlyobserve their behaviour.

◦

(43)

The standard theory

Which solvable terms may be now be consistently identied?

We cannot classify terms by their head normal forms. Too many of them!

◦

(44)

The standard theory

We cannot classify terms by their head normal forms.

Too many of them!

◦

(45)

The standard theory

We cannot classify terms by their head normal forms.

Too many of them!

(46)

Observational equivalence

Terms M, N withFV(M) ∪FV(N) = ~x, are observationally equivalent (M ≡ N) when, for all closed P:

P(λ~x.M) is solvable ⇐⇒ P(λ~x.N) is solvable

Put it dierently:

C[M] is solvable ⇐⇒ C[N] is solvable Note: If M =η N then M ≡ N.

◦

(47)

Observational equivalence

P(λ~x.M) is solvable ⇐⇒ P(λ~x.N) is solvable Put it dierently:

C[M] is solvable ⇐⇒ C[N] is solvable

Note: If M =η N then M ≡ N.

◦

(48)

Observational equivalence

P(λ~x.M) is solvable ⇐⇒ P(λ~x.N) is solvable Put it dierently:

C[M] is solvable ⇐⇒ C[N] is solvable Note: If M =η N then M ≡ N.

◦

(49)

Böhm Trees

BT (λ~x.yP₁. . .P_n) = λ~x. y

xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

<<

BT (P₁) BT (P₂) . . . BT (P_n)

If M has a hnf N then BT (M) = BT (N).

If M is unsolvable then BT (M) = ⊥.

(50)

Example: J = Y(λfxy. x(fy))

Write Φ for λfxy. x(fy)). Then:

J = YΦ =β ΦJ

=β λxy. x(Jy) =β λxy0.x(ΦJy0)

=_β λxy0.x(λy1.y0(Jy1)) =_β λxy0.x(λy1.y0(ΦJy1)) =_β . . . The treeBT (J) consists of one innite path:

λxy0.xλy1.y0λy2.y1λy3.y2 · · ·

◦

(51)

Example: J = Y(λfxy. x(fy))

J = YΦ =β ΦJ =β λxy. x(Jy)

=β λxy0.x(ΦJy0)

◦

(52)

Example: J = Y(λfxy. x(fy))

J = YΦ =β ΦJ =β λxy. x(Jy) =β λxy0.x(ΦJy0)

◦

(53)

Example: J = Y(λfxy. x(fy))

=_β λxy0.x(λy1.y0(Jy1))

=_β λxy0.x(λy1.y0(ΦJy1)) =_β . . . The treeBT (J) consists of one innite path:

◦

(54)

Example: J = Y(λfxy. x(fy))

=_β λxy0.x(λy1.y0(Jy1)) =_β λxy0.x(λy1.y0(ΦJy1)) =_β . . .

The treeBT (J) consists of one innite path: λxy0.xλy1.y0λy2.y1λy3.y2 · · ·

◦

(55)

Example: J = Y(λfxy. x(fy))

(56)

Example: J = Y(λfxy. x(fy))

The treeBT (J) consists of one innite path:

The treeBT (I) consists of a single node: λx x

The rst can be obtained from the second by means of an innite sequence of η-expansions:

λx x η← λxy0.xy0 η← λxy0.xλy1.y0y1

◦

(57)

Example: J = Y(λfxy. x(fy))

λxy0.xλy1.y0λy2.y1λy3.y2 · · · The treeBT (I) consists of a single node: λx x

◦

(58)

Example: J = Y(λfxy. x(fy))

◦

(59)

Example: J = Y(λfxy. x(fy))

λx x η← λxy0.xy0

η← λxy0.xλy1.y0y1

◦

(60)

Example: J = Y(λfxy. x(fy))

◦

(61)

When are terms observationally equivalent?

Böhm trees B i B⁰ are η-equivalent (B ≈η B⁰), if there are two (possibly innite) sequences of η-expansions:

B = B_{0 η}←B_{1 η}←B_{2 η}←B_{3 η}← · · · B⁰ =B_{0 η}⁰ ←B_{1 η}⁰ ←B_{2 η}⁰ ←B_{3 η}⁰ ← · · · converging to the same (possibly innite) tree.

Theorem

Terms M and N are observationally equivalent

if and only if BT (M) ≈η BT (N).

◦

(62)

When are terms observationally equivalent?

Böhm trees B i B⁰ are η-equivalent (B ≈η B⁰), if there are two (possibly innite) sequences of η-expansions:

B = B_{0 η}←B_{1 η}←B_{2 η}←B_{3 η}← · · · B⁰ =B_{0 η}⁰ ←B_{1 η}⁰ ←B_{2 η}⁰ ←B_{3 η}⁰ ← · · · converging to the same (possibly innite) tree.

Theorem

Terms M and N are observationally equivalent

if and only if BT (M) ≈η BT (N).

◦

(63)

Semantics

Goal: Interpret any term M as an element [[M]] of some structure A, so thatM =β N implies [[M]] = [[N]].

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

Write [[M]]_v, for the value of M under v.

◦

(64)

Semantics

Goal: Interpret any term M as an element [[M]] of some structure A, so thatM =β N implies [[M]] = [[N]].

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

v : Var → A.

Write [[M]]v, for the value of M under v.

◦

(65)

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

Application · is a binary operation in A;

[[ ]] : Λ ×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[x7→a], for any a ∈ A; (d) If v|FV(P)=u|FV(P), then [[P]]v = [[P]]u.

◦

(66)

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

[[ ]] : Λ ×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[x7→a], for any a ∈ A; (d) If v|FV(P)=u|FV(P), then [[P]]v = [[P]]u.

◦

(67)

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

[[ ]] : Λ ×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[x7→a], for any a ∈ A;

(d) If v|FV(P)=u|FV(P), then [[P]]v = [[P]]u.

(68)

Extensionality

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

Extensional interpretation: a ≈ b implies a = b, for all a, 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 i [[M]]v[x7→a] = [[N]]v[x7→a], all a.)

◦

(69)

Extensionality

Extensional interpretation: a ≈ b implies a = b, for all a, 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.

◦

(70)

Extensionality

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

Meaning: Abstraction makes sense algebraically.

◦

(71)

Extensionality

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

Meaning: Abstraction makes sense algebraically.

(72)

Lambda-model

Lambda-model: Weakly extensional lambda-interpretation:

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

◦

(73)

Very Important Lemma

Lemma

In every lambda-model,

[[M[x := N]]]v = [[M]]v[x7→[[N]]v].

Proof: Induction wrt M. Case of λ with x 6∈FV(N). [[(λy P)[x := N]]]_v[x7→[[N]]_v]·a = [[λy.P[x := N]]]_v ·a

= [[P[x := N]]]v[y7→a] = [[P]]v[y7→a][x7→[[N]]_v[y7→a]]

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

◦

(74)

Very Important Lemma

Lemma

In every lambda-model,

[[M[x := N]]]v = [[M]]v[x7→[[N]]v].

Proof: Induction wrt M. Case of λ with x 6∈FV(N).

[[(λy P)[x := N]]]_v[x7→[[N]]_v]·a = [[λy.P[x := N]]]_v ·a

= [[P[x := N]]]v[y7→a] = [[P]]v[y7→a][x7→[[N]]_v[y7→a]]

= [[P]]v[y7→a][x7→[[N]]v] = [[λy.P]]v[x7→[[N]]v]·a, for all a.

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

◦

(75)

Soundness

Proposition

Every lambda-model is a lambda-algebra:

M =β N implies [[M]]_v = [[N]]_v

Proof:

Induction wrt M =β N. Non-immediate cases are two:

(Beta)

[[(λx.P)Q]]v = [[λx.P]]v· [[Q]]v = [[P]]v[x7→[[Q]]v] = [[P[x := Q]]]v.

(Xi)

Let P =β Q and let M = λx.P, N = λx.Q. Then [[M]]v·a = [[P]]v[x7→a] = [[Q]]v[x7→a] = [[N]]v ·a, for all a.

◦

(76)

Soundness

Proposition

Every lambda-model is a lambda-algebra:

M =β N implies [[M]]_v = [[N]]_v

Proof:

Induction wrt M =β N. Non-immediate cases are two:

(Beta)

[[(λx.P)Q]]v = [[λx.P]]v· [[Q]]v = [[P]]v[x7→[[Q]]v] = [[P[x := Q]]]v. (Xi)

Let P =β Q and let M = λx.P, N = λx.Q. Then [[M]]v·a = [[P]]v[x7→a] = [[Q]]v[x7→a] = [[N]]v ·a, for all a.

◦

(77)

Completeness

Theorem

The following are equivalent:

1) M =β N;

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

Proof.

(1)⇒(2) By soundness.

(2)⇒(1) Because term model is a lambda-model.

(78)

Complete partial orders

Let hA, ≤i be a partial order.

A subset B ⊆ A is directed when for every a, b ∈ B there is c ∈ B with a, b ≤ c.

The set A is acomplete partial order (cpo) when every directed subset has a supremum.

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

◦

(79)

Complete partial orders

◦

(80)

Complete partial orders

◦

(81)

Complete partial orders

Let hA, ≤i and hB, ≤i be cpos, and f : A → B.

Then f ismonotone if a ≤ a⁰ implies f (a) ≤ f (a⁰).

And f iscontinuous 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

◦

(82)

Complete partial orders

Then f ismonotone if a ≤ a⁰ implies f (a) ≤ f (a⁰). And f iscontinuous if sup f (C) = f (sup C)

for every nonempty directed C ⊆ A.

Fact: Every continuous function is monotone.

◦

(83)

Complete partial orders

◦

(84)

Complete partial orders

◦

(85)

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 i a ≤ a⁰ and b ≤ b⁰.

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

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

(86)

Continuous functions

Lemma

A function f : A × B → C is continuous i it is continuous wrt both arguments, i.e. all functions of the form λλa. f (a, b) and λλb. f (a, b) are continuous.

Proof.

(⇐)Take X ⊆ A × B directed. Let Xi = π_i(X ) for i = 1, 2. Step 1: If ha, bi ∈ X1×X2 then ha, bi ≤ ha⁰,b⁰i ∈X . Step 2: Therefore sup X = hsup X₁,sup X₂i = ha₀,b₀i. We show that hf (a0),f (b0)iis the supremum of f (X ). Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2. Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀).

Fix b0, to get c ≥ sup_af (a, b0) =f (a0,b0).

◦

(87)

Continuous functions

Lemma

Proof.

(⇐)Take X ⊆ A × B directed. Let Xi = π_i(X ) for i = 1, 2.

Step 1: If ha, bi ∈ X1×X2 then ha, bi ≤ ha⁰,b⁰i ∈X . Step 2: Therefore sup X = hsup X₁,sup X₂i = ha₀,b₀i. We show that hf (a0),f (b0)iis the supremum of f (X ). Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2. Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀).

◦

(88)

Continuous functions

Lemma

Proof.

Step 1: If ha, bi ∈ X1×X2 then ha, bi ≤ ha⁰,b⁰i ∈X .

Step 2: Therefore sup X = hsup X₁,sup X₂i = ha₀,b₀i. We show that hf (a0),f (b0)iis the supremum of f (X ). Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2. Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀).

◦

(89)

Continuous functions

Lemma

Proof.

Step 1: If ha, bi ∈ X1×X2 then ha, bi ≤ ha⁰,b⁰i ∈X . Step 2: Therefore sup X = hsup X₁,sup X₂i = ha₀,b₀i. We show that hf (a0),f (b0)iis the supremum of f (X ).

Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2. Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀).

◦

(90)

Continuous functions

Lemma

Proof.

Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2.

Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀). Fix b0, to get c ≥ sup_af (a, b0) =f (a0,b0).

◦

(91)

Continuous functions

Lemma

Proof.

Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X X .

◦

(92)

Continuous functions

Lemma

Proof.

Let c ≥ f (X ), then c ≥ f ha, bi for all ha, bi ∈ X1×X2. Fix a, to get c ≥ sup_bf (a, b) = f (a, b₀).

◦

(93)

Continuous functions

Lemma

The application App : [A → B] × A → B is continuous.

Proof:

Uses the previous lemma.

Lemma

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

(94)

Reexive cpo

The cpo D is reexive i there are continuous functions F : D → [D → D] and G : [D → D] → D,

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

Then F must be onto and G is injective. The following are equivalent conditions:

G ◦ F = idD, G onto, F injective.

◦

(95)

Reexive cpo

with F ◦ G = id[D→D]. Then F must be onto and G is injective.

The following are equivalent conditions:

◦

(96)

Reexive cpo

with F ◦ G = id[D→D]. Then F must be onto and G is injective.

The following are equivalent conditions:

◦

(97)

Reexive cpo

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

Dene application asa · b = F (a)(b)so that G(f ) · a = f (a). Dene interpretation as

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

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

I [[λx.P]]_v =G(λλa.[[P]]_v[x7→a]).

Fact: This is a (well-dened) lambda interpretation. (Use continuity of App and Abs.)

◦

(98)

Reexive cpo

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

Dene application asa · b = F (a)(b)so that G(f ) · a = f (a).

Dene interpretation as

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

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

I [[λx.P]]_v =G(λλa.[[P]]_v[x7→a]).

◦

(99)

Reexive 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[x7→a]).

◦

(100)

Reexive 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[x7→a]).

Fact: This is a (well-dened) lambda interpretation.

(Use continuity of App and Abs.)

◦

(101)

Reexive cpo

Theorem

A reexive cpo is a lambda-model.

Proof.

Prove weak extensionality: let [[λx.M]]v·a = [[λx.N]]v·a, all a. Note that [[λx.M]]_v ·a = G(λλa.[[M]]_v[x7→a]) ·a = [[M]]_v[x7→a], and thus λλa.[[M]]v[x7→a] = λλa.[[N]]v[x7→a]. By the injectivity of G, it follows that [[λx.M]]v = [[λx.N]]v.

◦

(102)

Reexive cpo

Theorem

A reexive cpo is a lambda-model.

Proof.

Prove weak extensionality: let [[λx.M]]v·a = [[λx.N]]v·a, all a.

Note that [[λx.M]]_v ·a = G(λλa.[[M]]_v[x7→a]) ·a = [[M]]_v[x7→a], and thus λλa.[[M]]v[x7→a] = λλa.[[N]]v[x7→a]. By the injectivity of G, it follows that [[λx.M]]v = [[λx.N]]v.

◦

Rachunek lambda - ci¡g dalszy