• Nie Znaleziono Wyników

Beta-redukcja (λx P)Q → P[x := Q]

N/A
N/A
Protected

Academic year: 2021

Share "Beta-redukcja (λx P)Q → P[x := Q]"

Copied!
7
0
0

Pełen tekst

(1)

Rachunek lambda, lato 2019-20

Wykład 2

6 marca 2020

Beta-redeks (λx P)Q

...

@

} 

λx



Q

P

Beta-redukcja (λx P)Q → P[x := Q]

...

@

} 

λx



Q .

 P

x

33

x

jj

=⇒ ...

.

 P

Q Q

Beta-redeks w grafie

(1)

@

| 

λ



(3)

(2)

Beta-redukcja w grafie

(1)



@

| 

λ



(3)

(2)

 

33

jj

=⇒ (1)



(2)

 

(3) (3)

Beta-redukcja nieco wyidealizowana

(1)



@

| 

λx



(4)

(3)

@@

(2)

=⇒ (1)



(4)

(3)

&&

(2)

Kompozycjonalność

Lemat

(1) Jeśli M →βM0, to M[x := N] →βM0[x := N];

(2) Jeśli N →βN0, to M[x := N] βM[x := N0], Dowód: Indukcja ze względu na długość M.

Wniosek

Jeśli M βM0i N βN0, to M[x := N] βM0[x := N0].

Normalizacja

Postać normalnato term bez redeksów.

Nie da się go redukować.

Term Mma postać normalną(jest normalizowalny), gdy redukuje się do pewnej postaci normalnej.

Nazywamy jąpostacią normalnatermu M.

Term M jestsilnie normalizowalny(M ∈ SN), gdy nie istnieje nieskończony ciąg

M = M0βM1βM2β· · ·

Inaczej: każdy ciąg redukcji prowadzi do postaci normalnej.

(2)

Przykłady

I TermS = λxyz.xz(yz)jest w postaci normalnej.

I TermSKKjest silnie normalizowalny i ma postać normalnąI.

I TermΩ = (λx . xx )(λx . xx )nie ma postaci normalnej.

I Term(λx . y )Ωma postać normalnąy, ale nie jest silnie normalizowalny.

Własności redukcji

Abstrakcyjne systemy redukcyjne

Abstrakcyjny system redukcyjny:

parahA, →i, gdzie→jest relacją binarną wA.

Oznaczenia:

+ domknięcie przechodnie;

 domknięcie przechodnio-zwrotne;

= domknięcie zwrotne.

Postać normalna: takiea ∈ A, że∀b. a 6→ b.

Inne definicje stosują się odpowiednio.

Silna normalizacja (SN)

Każdy ciąg redukcjia0→ a1→ a2→ · · · jest skończony.

(Wtedy relacjajest dobrym ufundowaniem.)

Fakt:Beta-redukcja nie ma własności silnej normalizacji:

Ω →βΩ →βΩ →β· · ·

Własność Churcha-Rossera (CR)

Jeślia  bia  c, to istnieje takied, żeb  d ic  d.

a

  

b

 

c



d

Własność rombu (diamond property)

Jeślia → bia → c, to istnieje takied, żeb → dic → d.

a

 

b



c



d

Własność rombu implikuje CR

a1

 //.

 //.

 //a2

.



.

 //.

 //.

a3 //. //. //a4

Własność rombu?

Fakt:Beta-redukcja nie ma własności rombu.

(λx .xx )((λx .x )y )

xx ''

(λx .x )y ((λx .x )y )

&&

(λx .xx )y

ww

??

(3)

Słaba własność Churcha-Rossera (WCR)

Jeślia → bia → c, to istnieje takied, żeb  d ic  d.

a

 

b

 

c



d

Fakt: Beta-redukcja ma słabą własność Churcha-Rossera.

WCR nie implikuje CR

Przykład:

a ←− b ←→ c −→ d

Lemat Newmana:

WCR ∧ SN =⇒ CR

Twierdzenie Churcha-Rossera: Beta ma własność CR

Definicja(complete development):

TermMtopełne rozwinięcietermuM.

– x= x ;

– (λx M)= λx M;

– (MN)= MN, gdy M nie jest abstrakcją;

– ((λx M)N)= M[x := N].

Sens:jednoczesna redukcja wszystkich istniejących redeksów.

Relacja pomocnicza →

1

– x→ x, gdy x jest zmienną;1 – jeśli M→ M1 0, to λxM→ λxM1 0; – jeśli M→ M1 0i N→ N1 0, to:

MN→ M1 0N0, oraz (λxM)N→ M1 0[x := N0].

Sens:jednoczesna redukcja kilku redeksów

już obecnych w termie.

Własności relacji →

1

(1) JeśliM→ M1 0, toFV(M0) ⊆FV(M).

(2) Dla dowolnegoMzachodziM→ M1 orazM→ M1 .

(3) JeśliM→ M1 0iN→ N1 0, toM[x := N]→ M1 0[x := N0].

(4) JeśliM→ M1 0, toM0→ M1 .

Relacja → ma własność rombu

1

M

1

~~

1

!!

M0

1

M00 }} 1

M

Dowód twierdzenia Churcha-Rossera

1) Ponieważ relacja→ ma własność rombu, więc tym1 bardziej jej domknięcie przechodnio-zwrotne ma1 własność rombu.

M1

 //.

 //.

 //M2

.



.

 //.

 //.

M3 //. //. //M4

2) Ponieważ→β⊆→ ⊆ 1 β, więc1 iβsą równe.

3) Własność rombu dlato własność CR dla→.

Wnioski z twierdzenia Churcha-Rossera

(1)JeśliM =βN, toM βQβ N, dla pewnego Q.

Q1

  

Q2

  

Qn

}}}}  

M

 

M1



"" ""

M2 . . . Mn−1 N

{{{{

"" ""



(4)

Wnioski z twierdzenia Churcha-Rossera

(2)Każdy term ma co najwyżej jedną postać normalną (i do niej się redukuje).

Dowód:

JeśliM =βNiNnormalne, toM βQβ N. SkoroNnormalne, toN = Q.

JeśliMteż normalne, toM = Q = N.

Wnioski z twierdzenia Churcha-Rossera

(3)Beta-konwersja jest niesprzeczną teorią równościową

Dowód:Na przykład0 x = y, ponieważx 6=βy.

Eta-redukcja

Eta-reduction

The least relation →η, satisfying the conditions:

I λx .Mx →ηM, when x 6∈FV(M);

I jeśli M →ηM0, to MN →ηM0N, NM →ηNM0 oraz λxM →ηλxM0.

Symbol→βηstands for the union of relations →βand →η. Other definitions and notation are applicable respectively.

Eta-conversion

Axiom(η): λx .Mx = M, when x 6∈FV(M).

Rule(ext): Mx = Nx

M = N (when x 6∈FV(M) ∪FV(N))

Fakt

Axiom (η) and rule (ext) are equivalent.

Proof.

(1) Assume (η) and letMx = Nx. Thenλx Mx = λx Nx, by rule (ξ), whenceM = N.

(2) Since(λx .Mx )x = Mx, one hasλx .Mx = Mby (ext).

Ekstensjonalność i słaba ekstensjonalność

(ext)Mx = Nx

M = N (when x 6∈FV(M) ∪FV(N)) JeśliM = λx PiN = λx Q, to wystarczy:

(ξ) P = Q λx P = λx Q

Słaba ekstensjonalność dla zbiorów to taka zasada

` W (x) ↔ V (x) {x | W (x)} = {x | V (x)}

Eta-reduction graphically

λ

@

 

=⇒ M

M •

bb

Eta-reduction amounts to removing a small loop in a graph.

Eta-reduction

Fakt

Eta-reduction is strongly normalizing.

Proof.

Because terms shrink under eta.

Fakt

Eta-reduction is Church-Rosser.

Proof.

Because it is WCR (easy), Newman’s lemma applies.

(5)

Beta-eta-redukcja

Relacja→βηto suma→βi→η.

Notacjaβη,=βηitd. stosuje się odpowiednio.

Beta-eta critical pairs

@

| 

λ



[λ]



[@]

| 

@

}}

λ



dd

cc

(λx Mx )N λx (λy M)x

Critical pairoccurs when two redexes use the same resource.

Proving WCR amounts to resolving critical pairs.

Beta-eta critical pairs

(λx Mx )N → MN

λx (λy M)x → λy M = λx . M[y := x ]

Morał

Beta-eta reduction is weakly Church-Rosser.

Towards Church-Rosser

Lemma

If Pη← M →βQ then there is N such that P →=βN η Q.

M

η



β



P

β

=



Q

 η

N

Towards Church-Rosser

Lemma

Relations βand ηcommute:

if Pη M βQ then there is N such that P βNη Q.

M

η



β

 

P

β  

Q

 η

N

Beta-eta is Church-Rosser

M1 β



η // //.

β



β // //.

β



η// //M2

β

.

η

η // //.

η



β // //.

η



η // //.

η

M3 η // //. β // //. η// //M4

Beta-SN versus beta-eta-SN

Theorem 0: A term is βη-SN if and only if it is β-SN.

Proof: (⇒) Obvious.

(⇐) Ćwiczenia?

Eta-postponement (odkładanie eta-redukcji)

Theorem 1:If M βηN then M βP ηN, for some P.

Theorem 2:

A term has a β-normal form iff it has a βη-normal form.

Proofs:Omitted.

Uwaga: Thm. 2 nie wynikanatychmiastz Thm. 1.

(6)

Standaryzacja

Standard reduction:

Never reduce to the left of something already reduced.

Standard reduction:

(λx .xx )((λzy .z(zy ))(λu.u)(λw .w )) → (λx .xx )((λy .(λu.u)((λu.u)y ))(λw .w )) → (λx .xx )((λu.u)((λu.u)(λw .w ))) → (λx .xx )((λu.u)(λw .w )) → (λx .xx )(λw .w ).

Non-standard reduction:

(λx .xx )((λzy .z(zy ))(λu.u)(λw .w )) → (λx .xx )((λy .(λu.u)((λu.u)y ))(λw .w )) → (λx .xx )((λy .(λu.u)y)(λw .w )) → (λx .xx )((λy .y )(λw .w )) → (λx .xx )(λw .w ).

Standardization

Theorem:

If M βN then there is a standard reduction from M to N.

Corollary:

If M has a β-normal form then theleftmostreduction leads to the normal form.

Slogan:

The leftmostreduction strategy is normalizing.

Redukcje czołowe i wewnętrzne

A term λ~x .z ~R is inhead normal form.1

A term λ~x .(λy .P)Q ~R has ahead redex(λy .P)Q.

A reduction step of the form

M = λ~x .(λy .P)Q ~R →βλ~x .P[y := Q] ~R = N is calledhead reduction. Write M→ N.h

Other reductions areinternal. Write M→ N.i

1Postać normalna jest wtedy, gdy ~R są normalne.

Main Lemma

Lemma: If M βN then M Ph  N, for some P.i Warning:A naive proof attempt fails. The assumption:

λ~x .(λy .P)Q ~R λ~x.(λy .Pi 0)Q0R~0 h→ λ~x .P0[y := Q0] ~R0 does not imply

λ~x .(λy .P)Q ~R→ λ~h x .P[y := Q] ~R λ~x.Pi 0[y := Q0] ~R0. This diagram is wrong. ·

h

·

i @@ @@

h



·

·

i @@ @@

Dygresja

Lemat łatwy:

Jeśli M Ni → P, to Mh → Q h βP, dla pewnego Q.

Wniosek:If M has a reduction with infinitely many head steps then it has an infinite head reduction.

Standaryzacja:jeśliM βN, to istnieje standardowa redukcja

Lemma: IfM βNthenM Ph  Ni , for someP.

(Dowód lematu opuszczamy)

Dowód standaryzacji:Indukcja ze względu na długośćN.

Najpierw wykonujemy same redukcje czołowe. Dostajemy termP = λ~x . M1M2. . . Mk, i dalej wszystkie redukcje są wewnątrz termówM1, M2, . . . , Mk. Można je łatwo przepermutować tak, aby najpierw redukować wewnątrzM1, potem wewnątrzM2i tak dalej. Do tych redukcji można zastosować indukcję.

Redukcje quasi-lewostronne

Lemma:If M has a reduction with infinitely many head steps then it has an infinite head reduction.

Uogólnienie:

Aquasi-leftmost reductionis an infinite reduction sequence with infinitely many leftmost steps.

(7)

Redukcje quasi-lewostronne

Theorem: A normalizing term has no quasi-leftmost reduction sequence.

Proof: Induction wrt the length of the normal form ofM. SupposeMhas a quasi-leftmost reduction. If there is infinitely many head steps, thenMhas an infinite head (thus leftmost) reduction and cannot normalize.

Thus almost all reductions are internal. (W szczególności, od pewnego miejsca mamy czołowe postaci normalne.)

λ~z.yP1. . . Pk

→ λ~i z.yP10. . . Pk0

→ λ~i z.yP100. . . Pk00

→ · · ·i

Infinitely many leftmost steps are within the samePi. By induction,Picannot normalize.

But thenMcannot normalize.

Cytaty

Powiązane dokumenty

We are aware of the fact that for two parallel lines there are infinitely many centers of symmetry but it is convenient and consistent with our approach to declare the point they

Up till now we have dealt with number series, i.e. each series was a sum of infinitely many numbers. For each fixed x such a series is defined as the usual number series. However, it

According to a 2014 questionnaire conducted by the British Council, one of the many things British people are associated with is their unique sense of humourA. And indeed, the way the

(1) (c) State if the converse is true or false and give an example to justify your answer. (b) Only one of the statements in part(a)

have defined, for an elliptic curve defined over a local field of residue charac- teristic p with ordinary reduction, an analogue of the Weierstrass σ-function which is defined on

Taking the idea from the author’s paper [3] dealing with squarefull in- tegers, we first give a reduction of our problem, which connects (∗) with some exponential sums, but this

1. It is a fascinating problem to determine the elliptic curves with everywhere good reduction over k. It is well known that there is no such curve over the field of rational

Criteria for the uniform λ-property in Orlicz sequence spaces, with Luxemburg norm and Orlicz norm, are given.. The set of extreme points of A is denoted by