Beta formă normală - Beta normal form

În calculul lambda , un termen este în formă beta normală dacă nu este posibilă reducerea beta . Un termen este în formă normală beta-eta dacă nu este posibilă nici o reducere beta și nici o reducere eta . Un termen este în formă normală a capului dacă nu există beta-redex în poziția capului .

Reducerea beta

În calculul lambda, un beta redex este un termen de forma:

${\ displaystyle (\ mathbf {\ lambda} xA) M}$ .

Un redex este în poziția capului într-un termen , dacă are următoarea formă (rețineți că aplicația are o prioritate mai mare decât abstractizarea și că formula de mai jos este menită să fie o abstractizare lambda, nu o aplicație): ${\ displaystyle r}$${\ displaystyle t}$${\ displaystyle t}$

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n}. \ underbrace {(\ lambda xA) M_ {1}} _ {{\ text {the redex}} r} M_ {2} \ ldots M_ {m}}$ , unde și . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

O reducere beta este o aplicație a următoarei reguli de rescriere la un beta redex conținut într-un termen:

${\ displaystyle (\ mathbf {\ lambda} xA) M \ longrightarrow A [x: = M]}$

unde este rezultatul înlocuirii termenului cu variabila în termen . ${\ displaystyle A [x: = M]}$${\ displaystyle M}$${\ displaystyle x}$${\ displaystyle A}$

O reducere beta a capului este o reducere beta aplicată în poziția capului, adică sub următoarea formă:

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n}. (\ lambda xA) M_ {1} M_ {2} \ ldots M_ {m} \ longrightarrow \ lambda x_ {1} \ ldots \ lambda x_ {n} .A [x: = M_ {1}] M_ {2} \ ldots M_ {m}}$ , unde și . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

Orice altă reducere este o reducere beta internă .

O formă normală este un termen care nu conține beta redex, adică care nu poate fi redus în continuare. O formă normală a capului este un termen care nu conține un beta redex în poziția capului, adică care nu poate fi redus în continuare printr-o reducere a capului. Când se ia în considerare calculul lambda simplu (și anume fără adăugarea de simboluri constante sau funcționale, menite să fie reduse prin regulă delta suplimentară), formele normale ale capului sunt termenii următoarei forme:

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n} .xM_ {1} M_ {2} \ ldots M_ {m}}$ , unde este o variabilă și . ${\ displaystyle x}$${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 0}$

O formă normală de cap nu este întotdeauna o formă normală, deoarece argumentele aplicate nu trebuie să fie normale. Cu toate acestea, inversul este adevărat: orice formă normală este, de asemenea, o formă normală. De fapt, formele normale sunt exact formele normale de cap în care subtermele sunt ele însele forme normale. Aceasta oferă o descriere sintactică inductivă a formelor normale. ${\ displaystyle M_ {j}}$${\ displaystyle M_ {j}}$

Există, de asemenea, noțiunea de formă normală a capului slab : un termen în formă normală a capului slab este fie un termen în formă normală a capului, fie o abstractizare lambda. Aceasta înseamnă că un redex poate apărea în interiorul unui corp lambda.

Strategii de reducere

În general, un termen dat poate conține mai multe redexuri, prin urmare ar putea fi aplicate mai multe reduceri beta diferite. Putem specifica o strategie pentru a alege ce redex să reducem.

• Reducerea ordinii normale este strategia în care se aplică continuu regula reducerii beta în poziția capului până când nu mai sunt posibile astfel de reduceri. În acel moment, termenul rezultat este în formă normală. Se continuă apoi aplicarea reducerii capului în subtermi , de la stânga la dreapta. În caz contrar, reducerea ordinii normale este strategia care reduce întotdeauna cel mai la stânga cel mai exterior cel mai redex. ${\ displaystyle M_ {j}}$
• În schimb, în reducerea ordinii aplicative , se aplică mai întâi reducerile interne și apoi se aplică reducerea capului numai atunci când nu mai sunt posibile reduceri interne.

Reducerea ordinii normale este completă, în sensul că, dacă un termen are o formă normală a capului, atunci reducerea ordinii normale va ajunge în cele din urmă. Prin descrierea sintactică a formelor normale de mai sus, aceasta implică aceeași afirmație pentru o formă normală „pe deplin” (aceasta este teorema standardizării ). În schimb, reducerea aplicativă a ordinii nu se poate termina, chiar și atunci când termenul are o formă normală. De exemplu, folosind reducerea aplicativă a comenzii, este posibilă următoarea secvență de reduceri:

${\ displaystyle {\ begin {align} & (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w .www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www)) \\ & \ ldots \ end {align}}}$

Dar folosind reducerea ordinii normale, același punct de plecare se reduce rapid la forma normală:

${\ displaystyle (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www))}$

${\ displaystyle \ rightarrow z}$

Șirurile director Sinot sunt o metodă prin care complexitatea de calcul a reducerii beta poate fi optimizată.

Vezi si

• Calcul Lambda
• Formă normală (dezambiguizare)

Referințe