Normalizációs tulajdonság (absztrakt átírás) - Normalization property (abstract rewriting)

A matematikai logikában és az elméleti informatikában az átírási rendszer rendelkezik az ( erős ) normalizálási tulajdonsággal, vagy megszűnik, ha minden tag erősen normalizálódik ; vagyis ha az újraírások minden sorozata végül egy redukálhatatlan , normál formának is nevezett kifejezéssel fejeződik be . Az átírási rendszernek a gyenge normalizálási tulajdonsága is lehet , ami azt jelenti, hogy minden kifejezés esetében létezik legalább egy meghatározott átírási sorozat, amely végül normál formát, azaz redukálhatatlan kifejezést eredményez.

Lambda számítás

Gépelés nélküli lambda számítás

A tiszta, tipizálatlan lambda -számítás nem elégíti ki az erős normalizálási tulajdonságot, és még a gyenge normalizálási tulajdonságot sem. Vegye figyelembe a kifejezést . A következő átírási szabályt tartalmazza: Bármilyen kifejezésre , ${\ displaystyle \ lambda x.xxx}$${\ displaystyle t}$

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

De fontolja meg, mi történik, ha önmagára alkalmazunk : ${\ displaystyle \ lambda x.xxx}$

${\ displaystyle {\ 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 \ \ ldots \, \ end {aligned }}}$

Ezért a kifejezés sem erősen, sem gyengén nem normalizálódik. ${\ displaystyle (\ lambda x.xxx) (\ lambda x.xxx)}$

Gépelt lambda számítás

Különböző rendszerek gépelt lambda kalkulus beleértve az egyszerűen begépelt lambda-kalkulus , Jean-Yves Girard „s F-rendszer , és Thierry Coquand ” s kalkulus konstrukciók erősen normalizálódik.

A normalizálási tulajdonsággal rendelkező lambda -számítási rendszer programozási nyelvnek tekinthető azzal a tulajdonsággal, hogy minden program leáll . Bár ez egy nagyon hasznos tulajdonság, van egy hátránya: a normalizáló tulajdonsággal rendelkező programozási nyelv nem lehet Turing teljes , ellenkező esetben a leállási problémát úgy lehetne megoldani, ha megnézzük, hogy a program típus-ellenőrzi-e. Ez azt jelenti, hogy vannak számítható függvények, amelyeket nem lehet definiálni az egyszerűen begépelt lambda -számításban (és hasonlóképpen vannak olyan számítható függvények, amelyeket nem lehet kiszámítani a konstrukciók számításában vagy az F rendszerben ).

Önértelmezés a begépelt lambda-számításban

Példaként lehetetlen önmagyarázót definiálni a fent hivatkozott számítások egyikében sem.

Itt "önértelmező" alatt olyan programot értünk, amely valamilyen egyszerű formátumú forráskifejezést (például karaktersorozatot) vesz fel, és a megfelelő normalizált kifejezés reprezentációját adja vissza. Ez a lehetetlen eredmény nem vonatkozik az "önértelmező" más definícióira. Például egyes szerzők a típusfunkciókat önértelmezőként emlegették , ahol a típusú kifejezések reprezentációi vannak . A félreértések elkerülése érdekében ezeket a funkciókat önfelismerőként fogjuk használni . Brown és Palsberg azt mutatták, hogy az önálló felismerők lehetne meghatározni, több erősen normalizáló nyelven, köztük F-rendszer és a System F _ω . Ez lehetségesnek bizonyult, mert a kódolt kifejezések típusai, amelyek tükröződnek az ábrázolásuk típusaiban, megakadályozzák az átlós argumentum létrehozását . Brown és Palsberg cikkükben cáfolják azt a "hagyományos bölcsességet", amely szerint az önértelmezés lehetetlen (és éppen erre a Wikipédia-oldalra hivatkoznak a hagyományos bölcsesség példájaként), de valójában cáfolják az önképtelenséget felismerők, teljesen más fogalom. Követő munkájuk során áttértek az általunk használt specifikusabb "önfelismerő" terminológiára, nevezetesen megkülönböztetve ezeket az "önértékelőktől" . Felismerik azt is, hogy az önértékelés végrehajtása nehezebbnek tűnik, mint az önismeret, és az előbbi végrehajtását erősen normalizáló nyelven nyitott problémaként hagyják. ${\ displaystyle \ pi \, \ tau \ to \ tau}$${\ displaystyle \ pi \, \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ pi \, \ tau \ to \ pi \, \ tau}$

Lásd még

• Gépelt lambda számítás
• Átírás
• Teljes funkcionális programozás
• Barendregt – Geuvers – Klop sejtés
• Newman -féle lemma
• Normalizálás értékeléssel

Megjegyzések

Hivatkozások

• Baader, Franz ; Nipkow, Tobias (1999). Kifejezések átírása és minden . Cambridge University Press. ISBN 0-521-77920-0. 316 oldal.