A lambdaszámítás a matematikai logika formális rendszere absztrakció alapú számítások kifejezésére és függvények alkalmazására kötés és változó helyettesítés segítségével. Ez egy univerzális modell, amely bármely Turing-gép tervezésére alkalmazható. A lambda-számítást először Church, egy híres matematikus vezette be az 1930-as években.
A rendszer lambda tagok felépítéséből és redukciós műveletek végrehajtásából áll.
Magyarázatok és alkalmazások
A görög lambda (λ) betű a lambda-kifejezésekben és a lambda-kifejezésekben használatos egy függvényben lévő változó összerendelésére.
A lambda-számítás lehet gépeletlen vagy gépelt. Az első változatban a függvények csak akkor használhatók, ha képesek ilyen típusú adatok fogadására. A típusos lambda-kövek gyengébbek, kisebb értéket tudnak kifejezni. De másrészt lehetővé teszik, hogy több dolgot bizonyítson.
Az egyik oka annak, hogy ilyen sokféle típus létezik, az az, hogy a tudósok többet akarnak tenni anélkül, hogy feladnák az erős lambda-számítási tételek bizonyításának lehetőségét.
A rendszer a matematika, filozófia, nyelvészet és számítástechnika számos területén alkalmazható. Először is, a lambda-számítás egy olyan kalkulus, amely fontos szerepet játszott a programozási nyelvek elméletének fejlődésében. A rendszerek megvalósítják a funkcionális alkotás stílusait. Ezek a kategóriák elméletének kutatási témája is.
Babáknak
A lambda-számítást Alonzo Church matematikus vezette be az 1930-as években, a tudomány alapjaival kapcsolatos kutatásának részeként. Az eredeti rendszer logikailag inkonzisztensnek bizonyult 1935-ben, amikor Stephen Kleen és J. B. Rosser kidolgozta a Kleene-Rosser paradoxont.
Később, 1936-ban Church csak azt a részt választotta ki és tette közzé, amely a számítások szempontjából releváns, amit ma tipizálatlan lambda-számításnak neveznek. 1940-ben egy gyengébb, de logikailag konzisztens elméletet is bevezetett, amelyet prímtípus-rendszerként ismerünk. Munkájában az egész elméletet egyszerű kifejezésekkel magyarázza, így elmondható, hogy Church kiadta a calculus lambda-t a babákhoz.
Az 1960-as évekig, amikor a programozási nyelvekkel való kapcsolata világossá vált, a λ csak formalizmus volt. Richard Montagu és más nyelvészek természetes nyelv szemantikában való alkalmazásainak köszönhetően a kalkulus mind a nyelvészetben, mind a számítástechnikában előkelő helyet fogl alt el.
A szimbólum eredete
A lambda nem egy szót vagy egy betűszót jelent, hanem Russell Principal Mathematics című könyvében található hivatkozásból származik, amelyet két tipográfiai változtatás követ. Példa a jelölésre: egy f függvénynél f (y)=2y + 1 értéke 2ŷ + 1. És itt a bemeneti változó címkézésére használunk egy caret („hat”) karaktert y felett.
Az egyház eredetileg hasonló szimbólumokat szándékozott használni, de a szedők nem tudták a "kalap" szimbólumot a betűk fölé helyezni. Ehelyett eredetileg "/\y.2y+1"-ként nyomtatták ki. A szerkesztés következő epizódjában a gépírók a "/ \" karaktert egy vizuálisan hasonló karakterre cserélték.
Bevezetés a lambda kalkulusba
A rendszer a kifejezések nyelvéből áll, amelyeket egy bizonyos formális szintaxis választ ki, és egy sor transzformációs szabályt, amelyek lehetővé teszik azok manipulálását. Az utolsó pont egyenletelméletnek vagy műveleti definíciónak tekinthető.
A lambda-kalkulus összes függvénye névtelen, vagyis nincs nevük. Csak egy bemeneti változót használnak, és a curryinget a többváltozós diagramok megvalósítására használják.
Lambda-feltételek
A számítási szintaxis egyes kifejezéseket érvényesnek, másokat pedig érvénytelennek határoz meg. Csakúgy, mint a különböző karakterláncok érvényes C programok, és néhány nem. A lambda-számítás tényleges kifejezését "lambda-tagnak" nevezik.
A következő három szabály egy induktív definíciót ad, amely lehetvonatkozik az összes szintaktikailag érvényes fogalom felépítésére:
Maga az x változó egy érvényes lambda kifejezés:
- ha T LT és x nem állandó, akkor (lambda xt) absztrakciónak nevezzük.
- ha T és s is fogalom, akkor a (TS)-t alkalmazásnak nevezzük.
Semmi más nem lambda kifejezés. Így egy fogalom akkor és csak akkor érvényes, ha e három szabály ismételt alkalmazásával nyerhető. Egyes zárójelek azonban más kritériumok szerint elhagyhatók.
Definíció
A lambda kifejezések a következőkből állnak:
- változók v 1, v 2, …, v n, …
- az absztrakció szimbólumai 'λ' és pont '.'
- zárójelek ().
A Λ halmaz induktív módon definiálható:
- Ha x egy változó, akkor x ∈ Λ;
- x nem állandó és M ∈ Λ, akkor (λx. M) ∈ Λ;
- M, N ∈ Λ, majd (MN) ∈ Λ.
Megjelölés
A lambda-kifejezések jelölésének zavartalan megőrzése érdekében a következő konvenciókat használják általában:
- Külső zárójelek kihagyva: MN helyett (MN).
- Feltételezzük, hogy az alkalmazások asszociatívak maradnak: ((MN) P helyett MNP írható).
- Az absztrakció teste tovább nyúlik jobbra: λx. MN jelentése λx. (MN), nem (λx. M) N.
- Az absztrakciók sorozata lecsökkent: λx.λy.λz. N lehet λxyz. N.
Szabad és kötött változók
A λ operátor összeköti a nem állandóját, bárhol is legyen az absztrakciós testben. A hatókörbe tartozó változókat kötöttnek nevezzük. A λ x kifejezésben. M, a λ x részt gyakran kötőanyagnak nevezik. Mintha arra utalna, hogy a változók egy csoporttá válnak az X x hozzáadásával M-hez. Az összes többi instabilt szabadnak nevezünk.
Például a λ y kifejezésben. x x y, y - kötött nem állandó, és x - szabad. És azt is érdemes megjegyezni, hogy a változó a "legközelebbi" absztrakciója szerint van csoportosítva. A következő példában a lambda-számítás megoldását x egyetlen előfordulása ábrázolja, amely a második taghoz kapcsolódik:
λ x. y (λ x. z x)
Az M szabad változók halmazát FV-ként (M) jelöljük, és a kifejezések szerkezetén át történő rekurzióval határozzuk meg a következőképpen:
- FV (x)={x}, ahol x egy változó.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
A szabad változókat nem tartalmazó képletet zártnak nevezzük. A zárt lambda kifejezéseket kombinátoroknak is nevezik, és egyenértékűek a kombinatorikus logika kifejezéseivel.
Rövidítés
A lambda kifejezések jelentését az határozza meg, hogyan lehet rövidíteni őket.
Három fajta vágás létezik:
- α-transzformáció: kötött változók megváltoztatása (alfa).
- β-redukció: függvények alkalmazása argumentumaikra (béta).
- η-transzformáció: lefedi az extenzionalitás fogalmát.
Itt is vana kapott ekvivalenciákról beszélünk: két kifejezés β-ekvivalens, ha β-transzformálható ugyanabba a komponenssé, és az α / η-ekvivalenciát is hasonlóan definiáljuk.
A redex kifejezés, a csökkenthető forgalom rövidítése, olyan altémákra vonatkozik, amelyek valamelyik szabály szerint csökkenthetők. Lambda kalkulus próbabábukhoz, példák:
(λ x. M) N egy béta redex az N-t x-re cserélő kifejezésben az M-ben. Azt a komponenst, amelyre a redex redukál, reduktjának nevezzük. A redukció (λ x. M) N M [x:=N].
Ha x nem szabad M-ben, λ x. M x szintén em-REDEX M szabályozóval.
α-átalakítás
Az alfa átnevezések lehetővé teszik a kötött változók nevének megváltoztatását. Például x. x megadhatja λ y-t. y. Azokat a kifejezéseket, amelyek csak az alfa transzformációban különböznek egymástól, α-egyenértékűnek mondják. A lambda-számítás használatakor gyakran az α-ekvivalenseket kölcsönösnek tekintjük.
Az alfa-konverzió pontos szabályai nem teljesen triviálisak. Először is, ezzel az absztrakcióval csak azokat a változókat nevezzük át, amelyek ugyanahhoz a rendszerhez vannak társítva. Például a λ x.λ x alfa transzformáció. x vezethet λ y-hoz.λ x. x, de ez nem vezethet λy-hoz.λx.y Ez utóbbinak más jelentése van, mint az eredetinek. Ez analóg a változó árnyékoló programozás koncepciójával.
Másodszor, az alfa transzformáció nem lehetséges, ha azt egy nem állandó más absztrakció fogja el. Például ha lecseréli x-et y-ra λ x.λ y-ban. x, akkor kaphatλy.λy. u, ami egyáltalán nem ugyanaz.
A statikus hatókörű programozási nyelvekben az alfakonverzió használható a névfeloldás egyszerűsítésére. Ugyanakkor ügyelve arra, hogy a változó fogalma ne takarja el a jelölést a tartalmazó területen.
A De Bruyne index jelölésében bármely két alfa-egyenértékű kifejezés szintaktikailag azonos.
Csere
Az E [V:=R] által írt változtatások a V változó minden szabad előfordulását az E kifejezésben az R forgalommal helyettesítik. A λ-ban kifejezett helyettesítést a rekurzió lambda-ja határozza meg. a fogalomszerkezetre vonatkozó számítást a következőképpen (megjegyzés: x és y - csak változók, és M és N - bármilyen λ-kifejezés).
x [x:=N] ≡ N
y [x:=N] ≡ y, ha x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]), ha x ≠ y, feltéve, hogy y ∉ FV (N).
A lambda-absztrakcióval való helyettesítéshez néha szükséges egy kifejezés α-transzformációja. Például nem igaz, hogy (λ x. Y) [y:=x] eredménye (λ x. X), mert a helyettesített x-nek szabadnak kellett volna lennie, de végül kötött. A helyes csere ebben az esetben (λ z. X) α-ekvivalenciáig. Vegye figyelembe, hogy a helyettesítés egyedileg definiált lambda-ig.
β-csökkentés
A béta-csökkentés egy függvény alkalmazásának gondolatát tükrözi. A béta-reduktív fogalmak meghatározásahelyettesítés: ((X V. E) E ') az E [V:=E'].
Például 2, 7, × kódolást feltételezve a következő β-redukció jön létre: ((λ n. N × 2) 7) → 7 × 2.
A béta-csökkentés azonosnak tekinthető a Curry-Howard izomorfizmuson keresztüli természetes dedukciós lokális redukálhatóság fogalmával.
η-transform
Ez a konverzió az extenzionalitás gondolatát fejezi ki, ami ebben az összefüggésben azt jelenti, hogy két függvény egyenlő, ha minden argumentumra ugyanazt az eredményt adják. Ez a konverzió λ x között változik. (F x) és f, amikor x nem tűnik szabadnak az f-ben.
Ez a művelet azonosnak tekinthető a Curry-Howard izomorfizmuson keresztüli természetes dedukció lokális teljességének fogalmával.
Normál formák és összeolvadás
Tipizálatlan lambda kalkulus esetén a β-redukciós szabály általában sem nem erős, sem nem gyenge normalizálás.
Mindazonáltal kimutatható, hogy a β-redukció összeolvad, amikor az α-transzformáció előtt fut (vagyis két normálalakot tekinthetünk egyenlőnek, ha lehetséges az α-transzformáció az egyikből a másikba).
Ezért mind az erősen normalizáló, mind a gyengén módosító tagoknak egyetlen normál alakjuk van. Az első ciklusokban minden redukciós stratégia garantáltan tipikus konfigurációt eredményez. Míg gyengén normalizálódó körülmények esetén előfordulhat, hogy egyes redukciós stratégiák nem találják meg.
További programozási módszerek
Sok teremtési idióma létezik a lambda kalkulushoz. Sokukat eredetileg azzal összefüggésben fejlesztették ki, hogy rendszereket használtak egy programozási nyelv szemantikájának alapjául, hatékonyan alkalmazva őket alacsony szintű konstrukcióként. Mivel egyes stílusok töredékként tartalmaznak lambda kalkulust (vagy valami nagyon hasonlót), ezek a technikák a gyakorlati alkotásban is használhatók, de ilyenkor homályosnak vagy idegennek tűnhetnek.
Elnevezett konstansok
A lambda-számításban a könyvtár korábban definiált függvények halmazaként jelenik meg, ahol a kifejezések csak konkrét állandók. A tiszta kalkulusnak nincs fogalma a nevesített megváltoztathatatlanokról, mivel minden atomi lambda tag változó. De úgy is utánozhatók, hogy a változót veszik az állandó nevének, lambda absztrakciót használnak az illékony anyag megkötésére a testben, és ezt az absztrakciót alkalmazzák a kívánt definícióra. Tehát ha f-et használ az M jelölésére N-ben, akkor azt mondhatja, hogy
(λ f. N) M.
A szerzők gyakran bevezetnek egy szintaktikai koncepciót, például a letet, hogy lehetővé tegyék a dolgok intuitívebb írását.
f=M - N
Az ilyen definíciók láncolásával egy lambda-számítási "program" írható nulla vagy több függvénydefinícióként, amelyet egyetlen lambda tag követ, a program nagy részét alkotó definíciók használatával.
Ennek egy figyelemre méltó korlátja, hogy az f név nincs definiálva M-ben,mivel M kívül esik az f lambda absztrakció kötelező hatókörén. Ez azt jelenti, hogy a rekurzív függvényattribútum nem használható M-ként let-vel. A fejlettebb letrec szintaxis, amely lehetővé teszi rekurzív függvénydefiníciók írását ebben a stílusban, emellett fixpontos kombinátorokat használ helyette.
Nyomtatott analógok
Ez a típus egy tipizált formalizmus, amely szimbólumot használ egy névtelen függvényabsztrakció megjelenítésére. Ebben az összefüggésben a típusok általában szintaktikai jellegű objektumok, amelyeket lambda kifejezésekhez rendelnek. A pontos jelleg a kérdéses kalkulustól függ. Egy bizonyos szempontból a tipizált LI a tipizálatlan LI finomításainak tekinthető. De másrészt alapvetőbb elméletnek is tekinthetők, és a tipizálatlan lambda-számítás csak egy típussal egy speciális eset.
A Typed LI a programozási nyelvek alapja és a funkcionális nyelvek, például az ML és a Haskell gerince. Közvetve pedig az alkotás imperatív stílusai. A típusos lambda kalkulusok fontos szerepet játszanak a programozási nyelvek típusrendszereinek fejlesztésében. Itt a tipizálás általában a program kívánt tulajdonságait rögzíti, például nem okoz memória-hozzáférési megsértést.
A beírt lambda kalkulusok a Curry–Howard izomorfizmuson keresztül szorosan kapcsolódnak a matematikai logikához és bizonyítási elmélethez, és például a kategóriaosztályok belső nyelveként is felfoghatók.egyszerűen a karteziánus zárások stílusa.
