• Nie Znaleziono Wyników

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

N/A
N/A
Protected

Academic year: 2021

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

Copied!
5
0
0

Pełen tekst

(1)

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.

(2)

“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

(3)

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.

(4)

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

(5)

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

Cytaty

Powiązane dokumenty

We investigate some radius results for various geometric properties con- cerning some subclasses of the class S of univalent functions.. This work was supported by KOSEF

Aplikacją będziemy nazywać działanie, które funkcji f i argumentowi x przypisu- je – w przypadku funkcji jednej zmiennej – wartość funkcji f dla argumentu x, czyli coś, co

[2] Uszczegółowienie Małopolskiego Regionalnego Programu Operacyjnego na lata 2007-2013 Zarząd Województwa Małopolskiego, Kraków, styczeń 2008 r..

Functional Languages Based on the λ-Calculus, treat computation as the evaluation of mathematical functions and typically avoids state and mutable data. LISP family Lisp is the

In this note we establish an advanced version of the inverse func- tion theorem and study some local geometrical properties like starlikeness and hyperbolic convexity of the

In view of the well-known connection between the classes of starlike and convex functions this radius of convexity is equal to the radius of star- likeness of the

Recently, Juneja and Srivastava[9| have obtained the classical interpretation of convergence in the space r F,,(p) of all entire functions whose index pair does not

O sumach częściowych pewnej klasy funkcji jednolistnych Об отрезках ряда Тейлора одного класса однолистных функций.. Subsequently the