Korisnik:Ognjenzivanovic/prevod2

U apstraktnom prepisivanju, objekat je u normalnom obliku ako se ne može dalje pisati, odnosno nesvodiv je. U zavisnosti od sistema prepisivanja, objekat može prepisati u nekoliko normalnih oblika ili uopšte nijednu. Mnoga svojstva sistema prepisivanja odnose se na normalne forme.

Definicije

Formalno rečeno, ako je (A,→) sistem apstraktnog prepisivanja, x∈A je u normalnom obliku ako ne postoji y∈A tako da je x→y tj. x je nesvodljiv termin.

Objekat a je slabo normalizovan ako postoji bar jedan određeni niz prepisa koji počinje od a koji na kraju daje normalan oblik. Sistem za ponovno pisanje ima svojstvo slabe normalizacije ili (slabo) normalizuje (WN) ako je svaki objekat slabo normalizovan. Objekat a se snažno normalizuje ako se svaki niz prepisa koji počinje od a na kraju završava normalnim oblikom. Sistem apstraktnog ponovnog pisanja je snažno normalizovan, završavajući, neterovski ili ima (jako) svojstvo normalizacije (SN), ako je svaki od njegovih objekata snažno normalizovan.

Sistem ponovnog pisanja ima svojstvo normalnog oblika (NF) ako se za sve objekte a i normalne forme b, b može doći iz a nizom ponovnih pisanja i inverznih prepisa samo ako se a svodi na b. Sistem ponovnog pisanja ima jedinstveno svojstvo normalnog oblika (UN) ako za sve normalne oblike a, b ∈ S, a može da se dostigne iz b nizom prepisivanja i inverznih prepisivanja samo ako je a jednako b. Sistem prepisivanja ima jedinstveno svojstvo normalnog oblika u odnosu na redukciju (UN^→) ako je za svaki termin koji se svodi na normalne oblike a i b, a jednako b.

Rezultati

Ovaj odeljak predstavlja neke dobro poznate rezultate. Prvo, SN implicira WN.

Konfluencija (skraćeno CR) implicira NF implicira UN implicira UN^→. Obrnute implikacije generalno ne važe. {a→b,a→c,c→c,d→c,d→e} je UN^→ ali nije UN jer su b=e i b,e normalni oblici. {a→b,a→c,b→b} je UN ali nije NF jer je b=c, c normalan oblik, a b se ne svodi na c. {a→b,a→c,b→b,c→c} je NF pošto nema normalnih oblika, ali ne i CR jer se a redukuje na b i c, a b,c nemaju zajednički redukt.

WN i UN^→ impliciraju konfluenciju. Otuda se CR, NF, UN, i UN^→ poklapaju ako važi WN.

Primeri

Jedan primer je da pojednostavljivanje aritmetičkih izraza proizvodi broj – u aritmetici, svi brojevi su normalni oblici. Izvanredna činjenica je da svi aritmetički izrazi imaju jedinstvenu vrednost, tako da je sistem ponovnog pisanja snažno normalizovan i konfluentan:

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

Primeri nenormalizujućih sistema (ne slabo ili jako) uključuju brojanje do beskonačnosti (1 ⇒ 2 ⇒ 3 ⇒ ...) i petlje kao što je funkcija transformacije Kolacove hipoteze (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., otvoren je problem da li postoje još neke petlje Kolacove transformacije). Još jedan primer je sistem sa jednim pravilom { r(x,y) → r(y,x) }, koji nema normalizujuća svojstva pošto iz bilo kog pojma, npr. r(4,2) počinje jedna sekvenca ponovnog pisanja, tj. r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., koja je beskonačno duga. Ovo dovodi do ideje da se prepiše "modulo komutativnosti" gde je termin u normalnom obliku ako se ne primenjuju nikakva pravila osim komutativnosti.

Slabo, ali ne i snažno normalizujući sistem prepisivanja

Sistem {b → a, b → c, c → b, c → d} (na slici) je primer slabo normalizovanog, ali ne i jako normalizovanog sistema. a i d su normalni oblici, i b i c se mogu redukovati do a ili d ali beskonačna redukcija b → c → b → c → ... znači da ni b ni c nisu strogo normalizovani.

Netipski lambda račun.

Čisti netipski lambda račun ne zadovoljava jako svojstvo normalizacije, pa čak ni slabo svojstvo normalizacije. Razmotrimo termin $\lambda x.xxx$ (levo-asocijativni). Ima sledeće pravilo prepisivanja: Za bilo koji termin $t$,

$(\mathbf {\lambda } x.xxx)t\rightarrow ttt$

Ali razmislite šta se dešava kada primenimo $\lambda x.xxx$ na sebe:

${\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}$

Dakle, termin $(\lambda x.xxx)(\lambda x.xxx)$ nije snažno normalizovan. I ovo je jedini redosled redukcije, stoga nije ni slabo normalizovan.

Tipski lambda račun

Različiti sistemi tipskog lambda računa uključujući jednostavno otkucani lambda račun, Sistem F Žan-Iva Žirara i račun konstrukcija Tijerija Kokvanda snažno se normalizuju.

Sistem lambda računa sa svojstvom normalizacije može se posmatrati kao programski jezik sa svojstvom da svaki program završava. Iako je ovo veoma korisno svojstvo, ono ima nedostatak: programski jezik sa svojstvom normalizacije ne može biti Tjuring potpun, inače bi se halting problem mogao rešiti tako što ćemo videti da li program proverava tipove. To znači da postoje izračunljive funkcije koje se ne mogu definisati u jednostavnom tipskom lambda računu, i slično za račun konstrukcija, i Sistem F. Tipičan primer je samo-tumač u totalnom programskom jeziku.