Kombinációs logika - Combinatory logic

A kombinációs logika olyan jelölés, amely megszünteti a matematikai logika számszerűsített változóinak szükségességét . Vezette be Mózes Schönfinkel és Haskell Curry , és újabban alkalmazott számítástechnika elméleti számítási modell és ennek alapján a tervezés funkcionális programozási nyelvek . Ez alapján combinators által bevezetett Schönfinkel 1920-ban az elképzelést, amely hasonló módon felépíteni funkciók-és eltávolítására vonatkozó említést változók-különösen elsőrendű logika . A kombinátor egy magasabb rendű függvény , amely csak függvényalkalmazást és korábban definiált kombinátorokat használ az argumentumok eredményének meghatározására.

A matematikában

A kombinációs logikát eredetileg „előlogikának” szánták, amely tisztázza a számszerűsített változók logikában betöltött szerepét , lényegében megszüntetve azokat. A számszerűsített változók kiküszöbölésének másik módja Quine predikátumfüggvény -logikája . Míg a kombinációs logika kifejezőereje jellemzően meghaladja az elsőrendű logikát , a predikátus functor logika kifejezőereje azonos az elsőrendű logikával ( Quine 1960, 1966, 1976 ).

A kombinációs logika eredeti feltalálója, Moses Schönfinkel semmit sem tett közzé a kombinációs logikáról eredeti 1924 -es dolgozata után. Haskell Curry 1927 végén a Princetoni Egyetem oktatójaként fedezte fel újra a kombinátorokat . Az 1930 -as évek végén Alonzo Church és tanítványai Princetonban feltalálták a funkcionális absztrakció rivális formalizmusát, a lambda -számítást , amely népszerűbbnek bizonyult, mint a kombinációs logika. A végeredmény ilyen történelmi előre az volt, hogy amíg az elméleti számítógép-tudomány elkezdte érdeke a kombinációs logika az 1960-as és 1970-es, szinte minden munkát, a téma által Haskell Curry és tanítványai, vagy Robert Feys a Belgiumban . Curry és Feys (1958), valamint Curry és mtsai. (1972) áttekinti a kombinációs logika korai történetét. A kombinációs logika és a lambda -számítás korszerűbb kezeléséről lásd Barendregt könyvét , amely áttekinti azokat a modelleket , amelyeket Dana Scott az 1960 -as és 1970 -es évek kombinációs logikájára kidolgozott.

A számítástechnikában

A számítástechnikában a kombinációs logikát használják a számítás egyszerűsített modelljeként , amelyet a kiszámíthatóság elméletében és a bizonyítás elméletében használnak . Egyszerűsége ellenére a kombinációs logika a számítás számos alapvető jellemzőjét rögzíti.

A kombinációs logika a lambda -számítás egyik változatának tekinthető, amelyben a (funkcionális absztrakciót képviselő) lambda -kifejezéseket a kombinátorok korlátozott halmaza, szabad változók nélküli primitív függvények váltják fel . Könnyű átalakítani a lambda kifejezéseket kombinátor kifejezésekké, és a kombinátor redukció sokkal egyszerűbb, mint a lambda redukció. Ezért kombinációs logikát alkalmaztak néhány nem szigorú funkcionális programozási nyelv és hardver modellezésére . Ennek a nézetnek a legtisztább formája az Unlambda programozási nyelv , amelynek egyetlen primitíve az S és K kombinátor, karakterbemenettel/kimenettel kiegészítve. Bár nem praktikus programozási nyelv, az Unlambda némi elméleti érdekesség.

A kombinációs logika sokféleképpen értelmezhető. Curry számos korai tanulmánya megmutatta, hogyan lehet a hagyományos logika axiómahalmazait kombinációs logikai egyenletekbe fordítani (Hindley és Meredith 1990). Dana Scott az 1960 -as és 1970 -es években megmutatta, hogyan kell összeházasodni a modellelmélettel és a kombinációs logikával.

A lambda számítás összefoglalása

A Lambda calculus a lambda-kifejezéseknek nevezett objektumokkal foglalkozik , amelyeket a következő három karakterlánc-formával lehet ábrázolni:

• ${\ displaystyle v}$
• ${\ displaystyle \ lambda v.E_ {1}}$
• ${\ displaystyle (E_ {1} E_ {2})}$

ahol egy változó neve levonni előre végtelen sok változó neveket és és a lambda-kifejezések. ${\ displaystyle v}$${\ displaystyle E_ {1}}$${\ displaystyle E_ {2}}$

Az űrlap feltételeit absztrakcióknak nevezzük . A változó v nevezik formális paraméter az absztrakció és a test a absztrakció. A kifejezés azt a függvényt reprezentálja, amely egy argumentumra vonatkoztatva a v formális paramétert az argumentumhoz köti , majd kiszámítja a kapott értéket - azaz visszatér , amikor a v minden előfordulását az argumentum helyettesíti. ${\ displaystyle \ lambda v.E_ {1}}$${\ displaystyle E_ {1}}$${\ displaystyle \ lambda v.E_ {1}}$${\ displaystyle E_ {1}}$${\ displaystyle E_ {1}}$

Az űrlap feltételeit alkalmazásoknak nevezzük . Az alkalmazások modellezik a függvényhívást vagy végrehajtást: az ábrázolt függvényt kell meghívni, annak argumentumával, és kiszámítani az eredményt. Ha (néha a applicand ) egy absztrakció, a kifejezés lehet csökkenteni : az érv, helyettesített lehet a szervezetben a helyett a formális paraméter az , és az eredmény egy új lambda kifejezés, amely egyenértékű a régi egy. Ha a lambda kifejezés nem tartalmaz alformákat, akkor nem redukálható, és normál formában van . ${\ displaystyle (E_ {1} E_ {2})}$${\ displaystyle E_ {1}}$${\ displaystyle E_ {2}}$${\ displaystyle E_ {1}}$${\ displaystyle E_ {2}}$${\ displaystyle E_ {1}}$${\ displaystyle E_ {1}}$${\ displaystyle ((\ lambda v.E_ {1}) E_ {2})}$

A kifejezés jelentése eredményeként figyelembe kifejezés E és cseréje minden szabad előfordulását v meg benne egy . Így írunk ${\ displaystyle E [v: = a]}$

${\ displaystyle ((\ lambda vE) a) \ Rightarrow E [v: = a]}$

Megegyezés szerint a rövidítést vesszük (azaz az alkalmazás balra asszociatív ). ${\ displaystyle (abc)}$${\ displaystyle ((ab) c)}$

A redukció ezen definíciójának motivációja az, hogy rögzíti az összes matematikai függvény alapvető viselkedését. Vegyük például azt a függvényt, amely kiszámítja a szám négyzetét. Lehet, hogy írunk

A tér X jelentése${\ displaystyle x*x}$

(A " " segítségével jelezzük a szorzást.) X itt a függvény formális paramétere . Annak érdekében, hogy a négyzetet egy adott argumentumra, például 3 -ra értékeljük, a formai paraméter helyett illesszük be a definícióba: ${\ displaystyle *}$

A 3 -as négyzet ${\ displaystyle 3*3}$

A kapott kifejezés értékeléséhez a szorzás és a 3. szám ismereteit kell igénybe vennünk. Mivel minden számítás egyszerűen a megfelelő függvények megfelelő primitív érvek alapján történő értékelésének összetétele, ez az egyszerű helyettesítési elv elegendő a lényegi mechanizmus rögzítéséhez. számítás. Ezenkívül a lambda -számításban az olyan fogalmak, mint a „3” és „ ”, megjeleníthetők anélkül, hogy szükség lenne külsőleg meghatározott primitív operátorokra vagy állandókra. Lehetőség van olyan kifejezések azonosítására a lambda számításban, amelyek megfelelően értelmezve a 3 -as számhoz hasonlóan és a szorzási operátorhoz hasonlóan qv Church kódolásként viselkednek . ${\ displaystyle 3*3}$${\ displaystyle *}$

Ismert, hogy a Lambda -számítás teljesítménye számítástechnikailag ekvivalens sok más valószínű számítási modellel (beleértve a Turing -gépeket ); azaz bármely számítást, amelyet ezen más modellek bármelyikében el lehet végezni, lambda -számítással lehet kifejezni, és fordítva. A Church-Turing tézis szerint mindkét modell bármilyen lehetséges számítást kifejezhet.

Talán meglepő, hogy a lambda-számítás bármilyen elképzelhető számítást képviselhet, amely csak a függvénykivonás és az alkalmazás egyszerű fogalmait használja, a változók egyszerű szöveges helyettesítése alapján. De még figyelemre méltóbb, hogy az absztrakció nem is szükséges. A kombinációs logika a lambda -számítással egyenértékű számítási modell, de absztrakció nélkül. Ennek előnye, hogy a kifejezések kiértékelése a lambda számításban meglehetősen bonyolult, mivel a helyettesítés szemantikáját nagy körültekintéssel kell megadni, hogy elkerüljük a változó rögzítési problémákat. Ezzel szemben a kifejezések kombinációs logikában történő értékelése sokkal egyszerűbb, mert nincs helyettesítés fogalma.

Kombinációs számítások

Mivel az absztrakció az egyetlen módja annak, hogy a lambda -számításban függvényeket állítsunk elő, valamit ki kell cserélni a kombinációs számításban. Az absztrakció helyett a kombinációs számítás korlátozott számú primitív függvényt biztosít, amelyekből más függvények is felépíthetők.

Kombinációs kifejezések

A kombinációs kifejezés az alábbi formák egyikével rendelkezik:

Szintaxis	Név	Leírás
x	Változó	Kombinációs kifejezést képviselő karakter vagy karakterlánc.
P	Primitív funkció	Az I , K , S kombinációs szimbólumok egyike .
(MN)	Alkalmazás	Függvény alkalmazása argumentumra. M és N kombinatív kifejezések.

A primitív függvények kombinátorok , vagy olyan függvények, amelyek lambda kifejezéseknek tekintve nem tartalmaznak szabad változókat .

A jelölések lerövidítése érdekében általános egyezmény, hogy vagy akár jelöli a kifejezést . Ez ugyanaz az általános konvenció (bal-asszociativitás), mint a lambda-számítás többszöri alkalmazása esetén. ${\ displaystyle (E_ {1} E_ {2} E_ {3} ... E_ {n})}$${\ displaystyle E_ {1} E_ {2} E_ {3} ... E_ {n}}$${\ displaystyle (... ((E_ {1} E_ {2}) E_ {3}) ... E_ {n})}$

A kombinációs logika csökkentése

A kombinációs logika szerint minden primitív kombinátorhoz tartozik a forma redukciós szabálya

( P x ₁ ... x _n ) = E

ahol E olyan kifejezés, amely csak az { x ₁ ... x _n } halmaz változóit említi . A primitív kombinátorok ilyen módon viselkednek funkcióként.

Példák kombinátorokra

A kombinátor legegyszerűbb példája az I , az identitáskombinátor, amelyet a

( I x ) = x

minden feltételre x . Egy másik egyszerű kombinátor a K , amely állandó függvényeket állít elő: ( K x ) az a függvény, amely minden argumentum esetén x -et ad vissza , tehát

(( K x ) y ) = x

minden x és y kifejezésre . Vagy a többszörös alkalmazásra vonatkozó egyezményt követve,

( K x y ) = x

A harmadik kombinátor az S , amely az alkalmazás általánosított változata:

( S x yz ) = ( XZ ( yz ))

S az x -et y -re alkalmazza , miután először mindegyiket z -be cserélte. Vagy másként fogalmazva, x -et y -re alkalmazzuk a z környezetben .

Mivel S és K , I önmagában felesleges, mert lehet építeni a két másik:

(( SKK ) x )

= ( SKK x )

= ( K x ( K x ))

= x

bármely kifejezésre x . Vegye figyelembe, hogy bár (( SKK ) x ) = ( I x ) bármely x esetében , maga az ( SKK ) nem egyenlő I -vel . Azt mondjuk, hogy a feltételek kiterjedten egyenlők . Az extenzív egyenlőség a függvények egyenlőségének matematikai fogalmát ragadja meg: hogy két függvény egyenlő, ha mindig ugyanazokat az eredményeket hozza ugyanazokhoz az érvekhez. Ezzel szemben maguk a kifejezések a primitív kombinátorok redukciójával együtt magukban foglalják a függvények intenzív egyenlőségének fogalmát : hogy két függvény csak akkor egyenlő , ha azonos megvalósításokkal rendelkeznek a primitív kombinátorok kiterjesztéséig. Az identitásfüggvény megvalósításának számos módja van; ( SKK ) és én ezen utak közé tartozunk. ( SKS ) egy másik. Az egyenértékű szót használjuk a kiterjesztési egyenlőség jelzésére, fenntartva az egyenlőt az azonos kombinatív kifejezésekre.

Érdekesebb kombinátor a fixpontos kombinátor vagy az Y kombinátor, amely a rekurzió megvalósítására használható .

Az SK alap teljessége

Az S és K összeállítható olyan kombinátorok előállítására, amelyek kiterjedten egyenlők bármely lambda kifejezéssel, és ezért Church tézise szerint bármilyen kiszámítható függvényhez. A bizonyíték egy T [] transzformáció bemutatása , amely egy tetszőleges lambda kifejezést ekvivalens kombinátorrá alakít.

T [] a következőképpen határozható meg:

1. T [ x ] => x
2. T [( E ₁ E ₂)] => ( T [ E ₁] T [ E ₂])
3. T [ λx . E ] => ( K T [ E ]) (ha x nem fordul elő szabadon E -ben )
4. T [ λx . x ] => Én
5. T [ λx . λy . E ] => T [ λx . T [ λy . E ]] (ha x szabadon fordul elő E -ben )
6. T [ λx . ( E ₁ E ₂)] => ( S T [ λx . E ₁] T [ λx . E₂ ]) (ha x fordul elő szabad E ₁ vagy E ₂)

Ne feledje, hogy a T [] a megadott módon nem jól beírt matematikai függvény, hanem inkább kifejezés-átíró: Bár végül kombinátort eredményez, az átalakítás olyan közvetítő kifejezéseket generálhat, amelyek nem lambda kifejezések és nem kombinátorok, az (5) szabályon keresztül.

Ezt a folyamatot absztrakció megszüntetésnek is nevezik . Ez a meghatározás kimerítő: minden lambda kifejezés pontosan az egyik szabály hatálya alá tartozik (lásd fent a lambda számítás összegzését ).

Ez függ a folyamat a konzol absztrakció , amely úgy expressziós E épült változók és alkalmazás során, és egy kombinátor kifejezés [x] E, amelyben a változó x nem szabad, úgy, hogy [ x ] E x = E tart. A zárójelek absztrakciójának nagyon egyszerű algoritmusát a kifejezések szerkezetének indukciója határozza meg a következőképpen:

1. [ x ] y  : = K y
2. [ x ] x  : = Én
3. [ X ] ( Ei E₂ ): = S ([ x ] Ei ) ([ x ] E₂ )

A zárójel-absztrakció a lambda-kifejezésekből a kombinátor kifejezésekbe történő fordítást indukálja, a lambda-absztrakciók értelmezésével a zárójel-absztrakciós algoritmus használatával.

A lambda kifejezés átalakítása ekvivalens kombinatorikus kifejezéssé

Például átalakítjuk a lambda λx kifejezést . λy . ( y x ) kombinatorikus kifejezésre:

T [ λx . λy . ( y x )]

= T [ λx . T [ λy . ( Y x )]] (5 -tel )

= T [ λx . ( S T [ λy . Y ] T [ λy . X ])] (6 -tal )

= T [ λx . ( SI T [ λy . X ])] (4 -szer )

= T [ λx . ( SI ( K T [ x ]))]] (3 -mal )

= T [ λx . ( SI ( K x ))]] (1 -gyel )

= ( S T [ λx . ( SI )] T [ λx . ( K x )]) (6 -tal )

= ( S ( K ( SI )) T [ λx . ( K x )]) (3 -mal )

= ( S ( K ( SI ))) ( S T [ λx . K ] T [ λx . X ])) (6 -tal )

= ( S ( K ( SI ))) ( S ( KK ) T [ λx . X ])) (3 -mal )

= ( S ( K ( SI )) ( S ( KK ) I )) (4 -gyel)

Ha ezt a kombinatorikus kifejezést bármely két x és y kifejezésre alkalmazzuk (ha sorba rendezett módon „jobbról” betápláljuk őket a kombinátorba), akkor ez a következőképpen csökken:

( S ( K ( S I )) ( S ( K K ) I ) xy)

= ( K ( S I ) x ( S ( K K ) I x) y)

= ( S I ( S ( K K ) I x) y)

= ( I y ( S ( K K ) I xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (y ( I x))

= (yx)

A kombinációs ábrázolás, ( S ( K ( SI )) ( S ( KK ) I )) sokkal hosszabb, mint az λx lambda kifejezés . λy . (yx). Ez jellemző. Általánosságban elmondható, hogy a T [] konstrukció az n hosszúságú lambda tagot egy Θ ( n ³ ) hosszúságú kombinatorikus tagra bővítheti .

A T [] transzformáció magyarázata

A T [] transzformációt az absztrakció megszüntetésének vágya motiválja. Két különleges eset, a 3. és a 4. szabály triviális: λx . x egyértelműen egyenértékű I -vel és λx . E egyértelműen egyenértékű a ( K T [ E ]) értékkel, ha x nem tűnik szabadnak E -ben .

Az első két szabály is egyszerű: a változók önmagukba konvertálódnak, és a kombinációban megengedett alkalmazásokat egyszerűen kombinálják az alkalmazást és az argumentumot kombinátorokká.

Az 5. és 6. szabály az érdekes. Az 5. szabály egyszerűen azt mondja, hogy ahhoz, hogy egy összetett absztrakciót kombinátorrá alakítsunk, először testét kell kombinátorrá alakítanunk, majd az absztrakciót megszüntetnünk. A 6. szabály valójában megszünteti az absztrakciót.

λx . ( E ₁ E ₂) egy olyan függvény, amely úgy egy érv, mondjuk egy , és a helyettesítő be a lambda kifejezés ( E ₁ E ₂) helyett x , így ( E ₁ E ₂) [ X  : = a ] . De ha az a helyébe ( E ₁ E ₂) behelyettesítjük az x helyét, az ugyanaz, mint az E ₁ és az E into helyettesítése , tehát

( E ₁ E ₂) [ x  : = a ] = ( E ₁ [ x  : = a ] E ₂ [ x  : = a ])

( Λx . ( E ₁ E ₂) a ) = (( λx . E ₁ a ) ( λx . E ₂ a ))

= ( S λx . E ₁ λx . E ₂ a )

= (( S λx . Ei λx . E ₂) a )

A kiterjedt egyenlőséggel,

λx . ( E ₁ E ₂) = ( S λx . E ₁ λx . E ₂)

Ezért, hogy megtalálja egy kombinátor egyenértékű λx . ( E ₁ E ₂), ez elegendő ahhoz, hogy megtalálja a kombinátor egyenértékű ( S λx . E ₁ λx . E ₂), és

( S T [ λx . E ₁] T [ λx . E ₂])

nyilvánvalóan megfelel a törvényjavaslatnak. E ₁ és E ₂ mindegyike szigorúan kevesebb alkalmazást tartalmaz, mint ( E ₁ E ₂), ezért a rekurziónak lambda taggal kell végződnie, anélkül, hogy egyáltalán alkalmaznának - akár változó, akár λx alakú kifejezés . E .

Az átalakítás egyszerűsítései

η-redukció

A T [] transzformáció által generált kombinátorok csökkenthetők, ha figyelembe vesszük a η-redukciós szabályt:

T [ λx . ( E x )] = T [ E ] (ha x nem szabad E -ben )

λx . ( E x) az a függvény, amely x argumentumot vesz fel , és az E függvényt alkalmazza rá; ez kiterjedésben egyenlő az E függvénnyel . Ezért elegendő E -t kombinatorikus formává alakítani.

Ezt az egyszerűsítést figyelembe véve a fenti példa a következő:

  T [ λx . λy . ( y x )]

= ...

= ( S ( K ( SI )) T [ λx . ( K x )])

= ( S ( K ( SI )) K ) (η-redukcióval)

Ez a kombinátor egyenértékű a korábbi, hosszabb:

  ( S ( K ( SI )) K x y )

= ( K ( SI ) x ( K x ) y )

= ( SI ( K x ) y )

= ( I y ( K x y ))

= ( y ( K x y ))

= ( yx )

Hasonlóképpen, a T [] transzformáció eredeti változata átalakította a λf azonosságfüggvényt . λx . ( f x ) ( S ( S ( KS )) ( S ( KK ) I )) ( KI )). A η-redukciós szabállyal λf . λx . ( f x ) átalakul I -vé .

Egypontos alapon

Vannak egypontos bázisok, amelyekből minden kombinátor kiterjesztően összeállítható bármely lambda taggal. Az ilyen alap legegyszerűbb példája { X }, ahol:

X ≡ λx . ((X S ) K )

Nem nehéz ellenőrizni, hogy:

X ( X ( X X )) = ^β K és

X ( X ( X ( X X ))) = ^β S .

Mivel { K , S } alap, ebből következik, hogy az { X } is alap. Az Iota programozási nyelv az X -et használja egyetlen kombinátorként.

Egy másik egyszerű példa az egypontos alapra:

X ' ≡ λx . (X K S K )

( X ' X' ) X ' = ^β K és

X ' ( X' X ' ) = ^β S

Valójában végtelen sok ilyen bázis létezik.

B, C kombinátorok

Schönfinkel papírja az S és K mellett két kombinátort is tartalmazott, amelyeket most B és C névre hallgatnak , a következő csökkentésekkel:

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

Azt is elmagyarázza, hogyan lehet őket kifejezni csak S és K használatával :

B = ( S ( KS ) K )

C = ( S ( S ( K ( S ( KS ) K ))) S ) ( KK ))

Ezek a kombinátorok rendkívül hasznosak, amikor predikátumlogikát vagy lambda -számítást kombinátor kifejezésekké alakítanak át. Curry is használta őket , és jóval később David Turner is , akinek a nevét számítástechnikai felhasználásukhoz kötötték. Használatukkal a következőképpen bővíthetjük az átalakítás szabályait:

1. T [ x ] ⇒ x
2. T [( Ei E₂ )] ⇒ ( T [ Ei ] T [ E₂ ])
3. T [ λx . E ] ⇒ ( K T [ E ]) (ha x nem szabad E -ben )
4. T [ λx . x ] ⇒ Én
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (ha x szabad az E -ben )
6. T [ λx . ( Ei E₂ )] ⇒ ( S T [ λx . Ei ] T [ λx . E₂ ]) (ha X jelentése szabad mind Ei és E₂ )
7. T [ λx . ( Ei E₂ )] ⇒ ( C T [ λx . Ei ] T [ E₂ ]) (ha x ingyenes a Ei de nem E₂ )
8. T [ λx . ( Ei E₂ )] ⇒ ( B T [ Ei ] T [ λx . E₂ ]) (ha x ingyenes a E₂ de nem Ei )

A B és C kombinátorok használatával λx transzformációja . λy . ( y x ) így néz ki:

   T [ λx . λy . ( y x )]

= T [ λx . T [ λy . ( Y x )]]

= T [ λx . ( C T [ λy . Y ] x )] (a 7. szabály szerint)

= T [ λx . ( C I x )]

= ( C I ) (η-redukció)

= (hagyományos kanonikus jelölés :)${\ displaystyle \ mathbf {C} _ {*}}$${\ displaystyle \ mathbf {X} _ {*} = \ mathbf {XI}}$

= (hagyományos kanonikus jelölés :)${\ displaystyle \ mathbf {I} '}$${\ displaystyle \ mathbf {X} '= \ mathbf {CX}}$

És valóban, ( C I x y ) redukálódik ( y x ) -ra :

   ( C I x y )

= ( Én y x )

= ( y x )

A motiváció az, hogy B és C az S korlátozott verziói . Míg az S értéket vesz fel, és az alkalmazás végrehajtása előtt behelyettesíti mind az alkalmazásban, mind az érvében, C a helyettesítést csak az alkalmazásban végzi, B pedig csak az argumentumban.

A kombinátorok modern nevei Haskell Curry 1930 -as doktori értekezéséből származnak (lásd B, C, K, W System ). A Schönfinkel „s eredeti papír, amit ma úgy hívunk S , K , I , B és C hívták S , C , I , Z és T volt.

A kombinátor méretének az új átalakítási szabályokból eredő csökkentése a B és C bevezetése nélkül is megvalósítható , amint azt a 3.2.

CL _K kontra CL _I számítás

Különbséget kell tenni az ebben a cikkben leírt CL _K és a CL _I számítás között. A különbség megfelel a λ _K és a λ _I számítás közötti különbségnek . A λ _K számítással ellentétben a λ _I számítás az alábbiakra korlátozza az absztrakciókat:

λx . E ahol x -nek legalább egy szabad előfordulása van E -ben .

Ennek következtében a K kombinátor nincs jelen a λ _I számításban és a CL _I számításban sem. A CL _I állandói a következők: I , B , C és S , amelyek alapot képeznek, amelyből az összes CL _I tag összeállítható (moduláris egyenlőség). Minden λ _I tag átalakítható egyenlő CL _I kombinátorrá a fentiekhez hasonló szabályok szerint a λ _K kifejezések CL _K kombinátorokká történő átalakítására . Lásd Barendregt (1984) 9. fejezetét.

Fordított konverzió

Az L [] átalakítás kombinatorikus kifejezésekből lambda kifejezésekbe triviális:

L [ I ] = λx . x

L [ K ] = λx . λy . x

L [ C ] = λx . λy . λz . ( x z y )

L [ B ] = λx . λy . λz . ( x ( y z ))

L [ S ] = λx . λy . λz . ( x z ( y z ))

L [( Ei E₂ )] = ( L [ Ei ] L [ E₂ ])

Ne feledje azonban, hogy ez az átalakítás nem a T [] egyik általunk látott verziójának fordított transzformációja .

A kombinatorikus számítás eldönthetetlensége

A normál forma bármilyen kombinatorikus kifejezés, amelyben a primitív combinators előforduló, ha van ilyen, nem alkalmazzák, hogy elég argumentum egyszerűsíteni kell. Nem eldönthető, hogy egy általános kombinációs kifejezésnek van -e normális formája; hogy két kombinált kifejezés egyenértékű -e stb. Ez egyenértékű a lambda kifejezések megfelelő feladatainak eldönthetetlenségével. Ennek közvetlen bizonyítéka azonban a következő:

Először is a kifejezés

Ω = ( S I I ( S I I ))

nincs normális formája, mert három lépés után önmagára redukál, az alábbiak szerint:

   ( S I I ( S I I ))

= ( I ( S I I ) ( I ( S I I ))))

= ( S I I ( I ( S I I ))))

= ( S I I ( S I I ))

és nyilvánvalóan semmilyen más redukciós sorrend nem rövidítheti a kifejezést.

Most tegyük fel, hogy az N kombinátor a normál formák kimutatására

${\ displaystyle (\ mathbf {N} \ x) = {\ begin {case} \ mathbf {T}, {\ text {if}} x {\ text {normál formájú}} \\\ mathbf {F} , {\ text {egyébként.}} \ end {tok}}}$

(Amennyiben T és F képviseli a hagyományos Church kódolások igaz és hamis, λx . Λy . X és λx . Λy . Y , átalakul a kombinációs logika. A kombinatorikus változat T = K és F = ( K I ) .)

Most engedd

Z = ( C ( C ( B N ( S I I )) Ω ) I )

most fontolja meg a kifejezést ( S I I Z ). Van -e normál formája ( S I I Z )? Akkor és csak akkor működik, ha a következők is:

  ( S I I Z )

= ( I Z ( I Z ))

= ( Z ( I Z ))

= ( Z Z )

= ( C ( C ( B N ( S I I ))) Ω ) I Z ) ( Z definíciója )

= ( C ( B N ( S I I )) Ω Z I )

= ( B N ( S I I ) Z Ω I )

= ( N ( S I I Z ) Ω I )

Most az N -t kell alkalmazni ( S I I Z ). Vagy ( S I I Z ) normális formája van, vagy nincs. Ha ez nem egy normális alakját, majd a fentiek csökkenti az alábbiak szerint:

  ( N ( S I I Z ) Ω I )

= ( K Ω I ) ( N definíciója )

= Ω

de Ω nem nem normális formában, tehát van egy ellentmondás. De ha az ( S I I Z ) formája nem normális, akkor az alábbiak szerint csökken:

  ( N ( S I I Z ) Ω I )

= ( K I Ω I ) ( N definíciója )

= ( Én I )

= Én

ami azt jelenti, hogy ( S I I Z ) normális formája egyszerűen én , egy másik ellentmondás. Ezért a hipotetikus normál alakú kombinátor N nem létezhet.

A Rice -tétel kombinációs logikai analógja azt mondja, hogy nincs teljes nem triviális predikátum. A predikátum kombinátor, amelyet alkalmazva T vagy F értéket ad vissza . A predikátum N jelentése nem triviális , ha két érv A és B olyan, hogy N A = T , és N B = F . A kombinátor N jelentése teljes , ha, és csak akkor, ha az N M van rendes formában minden érv M . A Rice -tétel analógja azt mondja, hogy minden teljes predikátum triviális. Ennek a tételnek a bizonyítása meglehetősen egyszerű.

Bizonyítás: Reductio ad absurdum. Tegyük fel, hogy van egy teljes, nem triviális állítmány, mondjuk N . Mivel N állítólag nem triviális, vannak olyan A és B kombinátorok , amelyek

( N A ) = T és

( N B ) = F .

Adjuk Negation ≡ λx . (Ha ( N x ), akkor B mást A ) ≡ λx . (( N x ) B A )

ABSURDUM ine ( Y NEGATION) meghatározása

A fixpontos tétel adja: ABSURDUM = (NEGATION ABSURDUM), for

ABSURDUM ≡ ( Y NEGATION) = (NEGATION ( Y NEGATION)) ≡ (NEGATION ABSURDUM).

Mivel N -nek teljesnek kell lennie:

1. ( N ABSURDUM) = F vagy
2. ( N ABSURDUM) = T

• 1. eset: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T , ellentmondás.
• 2. eset: T = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N B ) = F , ismét ellentmondás.

Ezért ( N ABSURDUM) sem T, sem F , ami ellentmond annak a feltételezésnek, hogy N teljes, nem triviális predikátum lenne. QED

Ebből a eldönthetetlenségi tételből rögtön az következik, hogy nincs teljes predikátum, amely megkülönböztetné a normális formájú kifejezéseket és a normál formájú kifejezéseket. Ebből az is következik, hogy nincs teljes predikátum, mondjuk az EQUAL, így:

(EQUAL AB ) = T, ha A = B és

(EQUAL AB ) = F , ha A ≠ B .

Ha az EQUAL létezne, akkor minden A , λx esetén. (EQUAL x A ) teljes, nem triviális predikátumnak kell lennie.

Alkalmazások

Funkcionális nyelvek összeállítása

David Turner kombinátoraival valósította meg a SASL programozási nyelvet .

Kenneth E. Iverson az APL utódjaként, J programozási nyelvén Curry kombinátorain alapuló primitíveket használt . Ez lehetővé tette, amit Iverson tacit programozásnak nevezett , azaz a változókat nem tartalmazó funkcionális kifejezésekbe történő programozást, valamint az ilyen programokkal való hatékony eszközöket. Kiderült, hogy a hallgatólagos programozás bármilyen APL-szerű nyelven lehetséges a felhasználó által definiált operátorokkal.

Logika

A Curry – Howard izomorfizmus összefüggést jelent a logika és a programozás között: az intuíciós logika tételének minden bizonyítéka megfelel a begépelt lambda kifejezés redukciójának, és fordítva. Ezenkívül a tételek azonosíthatók függvénytípus -aláírásokkal. Konkrétan a gépelt kombinációs logika megfelel a bizonyításelmélet Hilbert -rendszernek .

A K és S kombinátorok megfelelnek az axiómáknak

AK : A → ( B → A ),

AS : ( A → ( B → C )) → (( A → B ) → ( A → C )),

és a funkcióalkalmazás megfelel a leválás (modus ponens) szabálynak

MP : a A és A → B Infer B .

Az AK -ból , AS -ből és MP -ből álló számítás teljes az intuíciós logika implikatív töredékéhez, amely a következőképpen látható. Tekintsük az összes deduktívan zárt képletsor W halmazát, befogadás szerint rendezve . Aztán jön egy intuitív Kripke keret , és ebben a keretben definiálunk egy modellt${\ displaystyle \ langle W, \ subseteq \ rangle}$${\ displaystyle \ Vdash}$

${\ displaystyle X \ Vdash A \ iff A \ in X.}$

Ez a meghatározás megfelel a → kielégítés feltételeinek: egyrészt, ha , és olyan, hogy és akkor modus ponens. Másrészt, ha , akkor a levonása tétel , így a deduktív lezárása olyan elem olyan, hogy , , és a . ${\ displaystyle X \ Vdash A \ to B}$${\ displaystyle Y \ W} -ban}$${\ displaystyle Y \ supseteq X}$${\ displaystyle Y \ Vdash A}$${\ displaystyle Y \ Vdash B}$${\ displaystyle X \ not \ Vdash A \ to B}$${\ displaystyle X, A \ not \ vdash B}$${\ displaystyle X \ cup \ {A \}}$${\ displaystyle Y \ W} -ban}$${\ displaystyle Y \ supseteq X}$${\ displaystyle Y \ Vdash A}$${\ displaystyle Y \ not \ Vdash B}$

Legyen A bármilyen képlet, amely nem bizonyítható a számításban. Aztán egy nem tartozik a deduktív bezárása X az üres halmaz, így , és egy nem intuitionistically érvényes. ${\ displaystyle X \ not \ Vdash A}$

Lásd még

• Alkalmazható számítási rendszerek
• B, C, K, W rendszer
• Kategóriás absztrakt gép
• Kombinatív kategorikus nyelvtan
• Kifejezett helyettesítés
• Rögzített pont kombinátor
• Grafikoncsökkentő gép
• Lambda számítás és hengeres algebra , más módszerek a számszerűsítés modellezésére és a változók kiküszöbölésére
• SKI kombinátor számítás
• Szuperkombinátor
• Kigúnyolni egy gúnymadarat

Hivatkozások

További irodalom

• Barendregt, Hendrik Pieter (1984). A lambda -számítás, szintaxisa és szemantikája. Logikai tanulmányok és a matematika alapjai . Kötet 103. Észak -Hollandia . ISBN 0-444-87508-5. |volume=extra szöveget tartalmaz ( segítség )
• Curry, Haskell B .; Feys, Robert (1958). Kombinációs logika . Kt. I. Amszterdam: Észak -Hollandia. ISBN 0-7204-2208-6. |volume=extra szöveget tartalmaz ( segítség )
• Curry, Haskell B .; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Kombinációs logika . Kt. II. Amszterdam: Észak -Hollandia. ISBN 0-7204-2208-6. |volume=extra szöveget tartalmaz ( segítség )
• Field, Anthony J .; Harrison, Peter G. (1998). Funkcionális programozás . Addison-Wesley. ISBN 0-201-19249-7.
• Hindley, J. Roger ; Meredith, David (1990), "Principal type- systems and condensed desachment " , Journal of Symbolic Logic , 55 (1): 90–105, doi : 10.2307/2274956 , JSTOR  2274956 , MR  1043546
• Hindley, JR ; Seldin, JP (2008). λ-számítás és kombinátorok: Bevezetés . Cambridge University Press .
• Paulson, Lawrence C. (1995). A funkcionális programozás alapjai . Cambridge -i Egyetem.
• Quine, WV (1960). "A változókat elmagyarázták". Az Amerikai Filozófiai Társaság folyóirata . 104 (3): 343–347. JSTOR  985250 .Újranyomva a Quine's Selected Logic Papers (1966) 23. fejezete szerint , 227–235.
• Schönfinkel, Moses , 1924, " Über die Bausteine ​​der mathematischen Logik ", lefordítva "A matematikai logika építőköveiről" a Frege -től Gödelig: forráskönyv a matematikai logikában, 1879–1931 , Jean van Heijenoort , szerk. Harvard University Press , 1967. ISBN  0-674-32449-8 . A kombinációs logikát megalapozó cikk.
• Smullyan, Raymond , 1985. Egy gúnymadarat kigúnyolni . Knopf. ISBN  0-394-53491-3 . Gyengéd bevezetés a kombinációs logikába, szabadidős rejtvények sorozataként, madármegfigyelési metaforákkal.
• ______, 1994. Átlósítás és önreferencia . Oxford University Press . A 17–20. Fejezet formálisabb bevezetés a kombinációs logikába, különös hangsúlyt fektetve a fixpontos eredményekre.
• Sørensen, Morten Heine B. és Paweł Urzyczyn, 1999. Előadások a Curry – Howard izomorfizmusról . Koppenhágai Egyetem és a Varsói Egyetem , 1999-ben.
• Wolfengagen, V. E. (2003). Kombinációs logika a programozásban: Számítások objektumokkal példákon és gyakorlatokon keresztül (2. kiadás). Moszkva: "Center JurInfoR" Ltd. ISBN 5-89158-101-9.
• Wolfram, István (2021). Kombinátorok: Százéves nézet . Wolfram Media . ISBN 978-1-57955-043-1.e ISBN  978-1-57955-044-8 . A kombinátorok fejlődésének ünnepe, száz évvel azután, hogy Moses Schönfinkel bemutatta őket 1920 -ban.

Külső linkek

• Stanford Encyclopedia of Philosophy : " Kombinációs logika ", Bimbó Katalin .
• 1920–1931 Curry blokkjegyzetei.
• Keenan, David C. (2001) " Gúnymadarat boncolni: Grafikus jelölés a Lambda -számításhoz animált redukcióval. "
• Rathman, Chris, " Kombinátor madarak. " Egy asztal, amely a Smullyan lényegének nagy részét lepárolja (1985).
• Húzza össze a kombinációkat. (Java kisalkalmazás)
• Bináris lambda számítás és kombinációs logika.
• Kombinált logikai redukciós webszerver