Lambda kalkul - Lambda calculus

Lambda kalkul (také psaný jako λ-kalkul ) je formální systém v matematické logice pro vyjádření výpočtu založeného na abstrakci funkcí a aplikaci pomocí variabilní vazby a substituce . Jedná se o univerzální model výpočtu, který lze použít k simulaci jakéhokoli Turingova stroje . Byl představen matematikem Alonzem Churchem ve třicátých letech minulého století jako součást jeho výzkumu základů matematiky .

Lambda kalkul sestává z konstrukce lambda výrazů a provádění redukčních operací na nich. V nejjednodušší formě lambda kalkulu se termíny vytvářejí pouze podle následujících pravidel:

produkující výrazy jako: (λ x .λ y . (λ z . (λ x . zx ) (λ y . zy )) ( xy )). Závorky lze zrušit, pokud je výraz jednoznačný. U některých aplikací mohou být zahrnuty termíny pro logické a matematické konstanty a operace.

Redukční operace zahrnují:

Pokud je použito De Bruijnovo indexování , pak α-konverze již není nutná, protože nedojde ke kolizím jmen. Pokud opakovaná aplikace redukčních kroků nakonec skončí, pak Church-Rosserova věta vytvoří β-normální formu .

Názvy proměnných nejsou nutné, pokud používáte univerzální funkci lambda, jako je Iota a Jot , která může vytvořit jakékoli chování funkce tím, že ji sama v různých kombinacích vyvolá.

Vysvětlení a aplikace

Lambda kalkul je Turingův úplný , to znamená, že je to univerzální model výpočtu, který lze použít k simulaci jakéhokoli Turingova stroje . Jeho jmenovec, řecké písmeno lambda (λ), se ve výrazech lambda a lambda používá k označení vazby proměnné ve funkci .

Lambda kalkul může být netypický nebo přepsaný . V typovaném lambda kalkulu lze funkce použít pouze tehdy, jsou -li schopné akceptovat „typ“ dat daného vstupu. Typické lambda kameny jsou slabší než netypovaný lambda kalkul, který je hlavním předmětem tohoto článku, v tom smyslu, že typizované lambda kameny mohou vyjadřovat méně, než může netypový počet, ale na druhé straně typizované lambda kameny umožňují dokázat více věcí ; v jednoduše napsaném lambda kalkulu je to například věta, že každá vyhodnocovací strategie končí pro každý jednoduše napsaný lambda termín, zatímco hodnocení netypovaných lambda termínů nemusí končit. Jedním z důvodů, proč existuje mnoho různých typovaných lambda kalkulů, byla touha udělat více (toho, co dokáže netypový kalkul), aniž bychom se vzdali schopnosti dokázat silné věty o počtu.

Lambda kalkul má uplatnění v mnoha různých oblastech v matematice , filozofii , lingvistice a informatice . Lambda kalkul hraje důležitou roli ve vývoji teorie programovacích jazyků . Funkční programovací jazyky implementují lambda kalkul. Lambda kalkul je také aktuálním tématem výzkumu v teorii kategorií .

Dějiny

Lambda kalkul zavedl matematik Alonzo Church ve 30. letech 20. století jako součást vyšetřování základů matematiky . Původní systém byl logicky nekonzistentní v roce 1935, kdy Stephen Kleene a JB Rosser vyvinuli Kleene -Rosserův paradox .

Následně v roce 1936 Church izoloval a publikoval pouze část relevantní pro výpočet, která se nyní nazývá netypový lambda kalkul. V roce 1940 také představil výpočetně slabší, ale logicky konzistentní systém, známý jako jednoduše napsaný lambda kalkul .

Do 60. let, kdy byl objasněn jeho vztah k programovacím jazykům, byl lambda kalkul pouze formalismem. Díky Richardu Montagueovi a dalším lingvistickým aplikacím v sémantice přirozeného jazyka si lambda kalkul začal užívat úctyhodného místa v lingvistice i informatice.

Původ symbolu lambda

Existuje určitá nejistota ohledně toho, proč církev používala řecké písmeno lambda (λ) jako označení pro abstrakci funkcí v lambda kalkulu, možná částečně kvůli konfliktním vysvětlením samotnou církví. Podle Cardone a Hindley (2006):

Mimochodem, proč si církev zvolila notaci „λ“? V [nepublikovaném dopise Haraldovi Dicksonovi z roku 1964] jasně uvedl, že pochází z notace „ “ používané pro abstrakci tříd Whiteheadem a Russellem , nejprve změnou „ “ na „∧ “, aby se odlišila abstrakce funkcí od abstrakce třídy, a poté změnou „∧“ na „λ“ pro snadnější tisk. ${\ displaystyle {\ hat {x}}}$${\ displaystyle {\ hat {x}}}$${\ displaystyle x}$

Tento původ byl také popsán v [Rosser, 1984, s. 338]. Na druhou stranu, ve svých pozdějších letech Church řekl dvěma tazatelům, že volba byla náhodnější: byl zapotřebí symbol a λ právě náhodou byl vybrán.

Dana Scott se této otázce věnovala také na různých veřejných přednáškách. Scott vypráví, že kdysi položil otázku o původu symbolu lambdy církevnímu zeti Johnu Addisonovi, který poté napsal svému tchánovi pohlednici:

Vážený pane profesore,

Russell měl operátor iota , Hilbert měl operátor epsilon . Proč jste si pro svého operátora vybrali lambdu?

Podle Scotta celá Churchova odpověď spočívala v vrácení pohlednice s následující anotací: „ eeny, meeny, miny, moe “.

Neformální popis

Motivace

Vypočitatelné funkce jsou základním pojmem v oblasti počítačové vědy a matematiky. Lambda kalkul poskytuje jednoduchou sémantiku výpočtu a umožňuje formální studium vlastností výpočtu. Lambda kalkul zahrnuje dvě zjednodušení, díky nimž je tato sémantika jednoduchá. První zjednodušení je, že lambda kalkul zachází s funkcemi „anonymně“, aniž by jim dával explicitní jména. Například funkce

${\ displaystyle \ operatorname {square \ _sum} (x, y) = x^{2}+y^{2}}$

lze přepsat v anonymní podobě jako

${\ Displaystyle (x, y) \ mapsto x^{2}+y^{2}}$

(který se načte jako „ n-tice z x a y je mapována na “). Podobně funkce ${\ textstyle x^{2}+y^{2}}$

${\ displaystyle \ operatorname {id} (x) = x}$

lze přepsat v anonymní podobě jako

${\ displaystyle x \ mapsto x}$

kde je vstup jednoduše namapován na sebe.

Druhým zjednodušením je, že lambda kalkul využívá pouze funkce jednoho vstupu. Běžnou funkci, která vyžaduje dva vstupy, například funkci, lze přepracovat na ekvivalentní funkci, která přijímá jeden vstup, a jako výstup vrací jinou funkci, která zase přijímá jeden vstup. Například, ${\ textstyle \ operatorname {square \ _sum}}$

${\ Displaystyle (x, y) \ mapsto x^{2}+y^{2}}$

lze přepracovat do

${\ Displaystyle x \ mapsto (y \ mapsto x^{2}+y^{2})}$

Tato metoda, známá jako currying , transformuje funkci, která přebírá více argumentů do řetězce funkcí, z nichž každá má jeden argument.

Aplikace funkce na funkci argumenty (5, 2), výnosy najednou ${\ textstyle \ operatorname {square \ _sum}}$

${\ textstyle ((x, y) \ mapsto x^{2}+y^{2}) (5,2)}$

${\ textstyle = 5^{2}+2^{2}}$

${\ textstyle = 29}$,

vzhledem k tomu, že hodnocení curried verze vyžaduje ještě jeden krok

${\ textstyle {\ Bigl (} {\ bigl (} x \ mapsto (y \ mapsto x^{2}+y^{2}) {\ bigr)} (5) {\ Bigr)} (2)}$

${\ textstyle = (y \ mapsto 5^{2}+y^{2}) (2)}$// definice byla použita ve vnitřním výrazu. Je to jako redukce beta.${\ displaystyle x}$${\ displaystyle 5}$

${\ textstyle = 5^{2}+2^{2}}$// definice byla použita s . Opět podobně jako β-redukce.${\ displaystyle y}$${\ displaystyle 2}$

${\ textstyle = 29}$

dospět ke stejnému výsledku.

Lambda kalkul

Lambda kalkul se skládá z jazyka lambda termínů , které jsou definovány určitou formální syntaxí, a sady transformačních pravidel, která umožňují manipulaci s lambda termíny. Na tato transformační pravidla lze pohlížet jako na rovníkovou teorii nebo na operační definici .

Jak je popsáno výše, všechny funkce v lambda kalkulu jsou anonymní funkce, které nemají jména. Přijímají pouze jednu vstupní proměnnou, přičemž currying slouží k implementaci funkcí s několika proměnnými.

Lambda podmínky

Syntaxe lambda počtu definuje některé výrazy jako platné výrazy lambda počtu a některé jako neplatné, stejně jako některé řetězce znaků jsou platné programy C a některé nikoli. Platný výraz lambda kalkulu se nazývá „lambda termín“.

Následující tři pravidla dávají indukční definici, kterou lze použít k vytvoření všech syntakticky platných lambda termínů:

• proměnná, je sama o sobě platným lambda termínem${\ displaystyle x}$
• if je termín lambda a je proměnnou, pak (někdy zapsáno v ASCII jako ) je termín lambda (nazývá se abstrakce );${\ displaystyle t}$${\ displaystyle x}$${\ displaystyle (\ lambda xt)}$${\ displaystyle ({\ text {L}} xt)}$
• pokud a jsou lambda termíny, pak je lambda termín (nazývá se aplikace ).${\ displaystyle t}$${\ displaystyle s}$${\ displaystyle (ts)}$

Nic jiného není termín lambda. Termín lambda je tedy platný pouze tehdy, pokud jej lze získat opakovaným uplatňováním těchto tří pravidel. Některé závorky však lze podle určitých pravidel vynechat. Například krajní závorky obvykle nejsou zapsány. Viz notace níže.

Abstrakce je definice anonymní funkce, která je schopná přijímat jeden vstup a její nahrazení do výrazu . Definuje tedy anonymní funkci, která bere a vrací . Například je abstrakcí pro funkci pomocí výrazu pro . Definice funkce s abstrakcí pouze „nastavuje“ funkci, ale nevyvolává ji. Abstrakce váže proměnnou v termínu . ${\ displaystyle \ lambda xt}$${\ displaystyle x}$${\ displaystyle t}$${\ displaystyle x}$${\ displaystyle t}$${\ Displaystyle \ lambda xx^{2} +2}$${\ Displaystyle f (x) = x^{2} +2}$${\ displaystyle x^{2} +2}$${\ displaystyle t}$${\ displaystyle x}$${\ displaystyle t}$

Aplikace představuje použití funkce na vstupu , to znamená, že představuje akt volání funkce na vstupu do produktů . ${\ displaystyle ts}$${\ displaystyle t}$${\ displaystyle s}$${\ displaystyle t}$${\ displaystyle s}$${\ Displaystyle t (s)}$

V lambda kalkulu deklarace proměnné neexistuje žádný koncept. V definici, jako je (tj. ), Se lambda kalkul považuje za proměnnou, která ještě není definována. Abstrakce je syntakticky platná a představuje funkci, která přidává svůj vstup do dosud neznámého . ${\ Displaystyle \ lambda x.x+y}$${\ Displaystyle f (x) = x+y}$${\ displaystyle y}$${\ Displaystyle \ lambda x.x+y}$${\ displaystyle y}$

Může být použito bracketing a může být zapotřebí k disambiguaci termínů. Například a označují různé výrazy (i když shodou okolností snižují na stejnou hodnotu). Zde první příklad definuje funkci, jejíž lambda člen je výsledkem použití x na podřízenou funkci, zatímco druhý příklad je použití krajní funkce na vstup x, který vrací podřízenou funkci. Oba příklady se proto vyhodnotí jako funkce identity . ${\ Displaystyle \ lambda x. ((\ \ lambda xx) x)}$${\ Displaystyle (\ lambda x. (\ lambda xx)) x}$ ${\ Displaystyle \ lambda xx}$

Funkce, které fungují na funkcích

V lambda kalkulu jsou funkce považovány za „ hodnoty první třídy “, takže funkce mohou být použity jako vstupy nebo mohou být vráceny jako výstupy z jiných funkcí.

Například představuje funkci identity , a reprezentuje funkci identity aplikovaného na . Dále představuje konstantní funkci , funkci, která se vždy vrací , bez ohledu na vstup. V lambda kalkulu je aplikace funkcí považována za asociativní vlevo , to znamená . ${\ Displaystyle \ lambda xx}$${\ displaystyle x \ mapsto x}$${\ Displaystyle (\ lambda xx) y}$${\ displaystyle y}$${\ displaystyle (\ lambda xy)}$ ${\ displaystyle x \ mapsto y}$${\ displaystyle y}$${\ displaystyle stx}$${\ displaystyle (st) x}$

Existuje několik pojmů „ekvivalence“ a „redukce“, které umožňují lambda termíny „redukovat“ na „ekvivalentní“ lambda termíny.

Alfa ekvivalence

Základní formou ekvivalence, definovatelnou lambda, je alfa ekvivalence. Zachycuje intuici, že na konkrétní volbě vázané proměnné v abstrakci (obvykle) nezáleží. Například, a jsou alfa-ekvivalentní lambda termíny, a oba představují stejnou funkci (funkce identity). Termíny a nejsou alfa-ekvivalentní, protože nejsou vázány v abstrakce. V mnoha prezentacích je obvyklé identifikovat alfa-ekvivalentní lambda termíny. ${\ Displaystyle \ lambda xx}$${\ Displaystyle \ lambda yy}$${\ displaystyle x}$${\ displaystyle y}$

Aby bylo možné definovat β-redukci, jsou nutné následující definice:

Volné proměnné

Tyto volné proměnné z období jsou tyto proměnné nejsou vázány k abstrakci. Množina volných proměnných výrazu je definována indukčně:

• Volné proměnné jsou just${\ displaystyle x}$${\ displaystyle x}$
• Sada volných proměnných je množina volných proměnných , ale s odstraněnými${\ displaystyle \ lambda xt}$${\ displaystyle t}$${\ displaystyle x}$
• Množina volných proměnných je sjednocením množiny volných proměnných a množinou volných proměnných .${\ displaystyle ts}$${\ displaystyle t}$${\ displaystyle s}$

Například lambda výraz reprezentující identitu nemá žádné volné proměnné, ale funkce má jeden volný proměnné . ${\ Displaystyle \ lambda xx}$${\ Displaystyle \ lambda x.yx}$${\ displaystyle y}$

Substituce, které se vyhýbají zachycení

Předpokládejme , a jsou lambda termíny a jsou proměnné. Notace označuje substituci pro v v zachytávání-vyhnout způsobem. To je definováno tak, že: ${\ displaystyle t}$${\ displaystyle s}$${\ displaystyle r}$${\ displaystyle x}$${\ displaystyle y}$${\ Displaystyle t [x: = r]}$${\ displaystyle r}$${\ displaystyle x}$${\ displaystyle t}$

• ${\ Displaystyle x [x: = r] = r}$;
• ${\ Displaystyle y [x: = r] = y}$kdyby ;${\ Displaystyle x \ neq y}$
• ${\ Displaystyle (ts) [x: = r] = (t [x: = r]) (s [x: = r])}$;
• ${\ Displaystyle (\ lambda xt) [x: = r] = \ lambda xt}$;
• ${\ Displaystyle (\ lambda yt) [x: = r] = \ lambda y. (t [x: = r])}$pokud a není ve volných proměnných . Proměnná je prý „čerstvá“ pro .${\ Displaystyle x \ neq y}$${\ displaystyle y}$${\ displaystyle r}$${\ displaystyle y}$${\ displaystyle r}$

Například , a . ${\ Displaystyle (\ lambda xx) [y: = y] = \ lambda x. (x [y: = y]) = \ lambda xx}$${\ Displaystyle ((\ \ lambda xy) x) [x: = y] = ((\ lambda xy) [x: = y]) (x [x: = y]) = (\ lambda xy) y}$

Podmínka čerstvosti (vyžadující, aby nebyla ve volných proměnných ) je zásadní, aby se zajistilo, že substituce nezmění význam funkcí. Například, substituce je stanoveno, že ignoruje čerstvosti podmínku: . Tato substituce mění konstantní funkci na identitu substitucí. ${\ displaystyle y}$${\ displaystyle r}$${\ Displaystyle (\ lambda xy) [y: = x] = \ lambda x. (y [y: = x]) = \ lambda xx}$${\ Displaystyle \ lambda xy}$${\ Displaystyle \ lambda xx}$

Obecně platí, že nesplnění podmínky čerstvosti lze napravit alfa-přejmenováním pomocí vhodné čerstvé proměnné. Například přepnutí zpět na náš správný pojem substituce, v abstrakci lze přejmenovat na čerstvou proměnnou , abychom získali , a význam funkce je zachován substitucí. ${\ Displaystyle (\ lambda xy) [y: = x]}$${\ Displaystyle z}$${\ Displaystyle (\ lambda zy) [y: = x] = \ lambda z. (y [y: = x]) = \ lambda zx}$

β-redukce

Pravidlo β-redukce uvádí, že aplikace formuláře redukuje na výraz . Zápis se používá k označení, že β-redukuje na . Například pro každého , . To ukazuje, že to opravdu je identita. Podobně, což ukazuje, že je to konstantní funkce. ${\ Displaystyle (\ lambda xt) s}$${\ Displaystyle t [x: = s]}$${\ Displaystyle (\ lambda xt) s \ to t [x: = s]}$${\ Displaystyle (\ lambda xt) s}$${\ Displaystyle t [x: = s]}$${\ displaystyle s}$${\ Displaystyle (\ lambda xx) s \ to x [x: = s] = s}$${\ Displaystyle \ lambda xx}$${\ Displaystyle (\ lambda xy) s \ to y [x: = s] = y}$${\ Displaystyle \ lambda xy}$

Na lambda kalkul lze pohlížet jako na idealizovanou verzi funkčního programovacího jazyka, jako je Haskell nebo Standard ML . V tomto pohledu odpovídá β-redukce výpočetnímu kroku. Tento krok lze opakovat dalšími β-redukcemi, dokud nezbývají žádné další aplikace ke snížení. V netypickém lambda kalkulu, jak je zde uveden, tento redukční proces nemusí být ukončen. Zvažte například termín . Tady . To znamená, že se tento termín redukuje sám na sebe v jediné β-redukci, a proto proces redukce nikdy neskončí. ${\ Displaystyle \ Omega = (\ lambda x.xx) (\ lambda x.xx)}$${\ Displaystyle (\ lambda x.xx) (\ lambda x.xx) \ to (xx) [x: = \ lambda x.xx] = (x [x: = \ lambda x.xx]) (x [x : = \ lambda x.xx]) = (\ lambda x.xx) (\ lambda x.xx)}$

Dalším aspektem netypového lambda kalkulu je, že nerozlišuje mezi různými druhy dat. Například může být žádoucí napsat funkci, která funguje pouze na číslech. V netypickém lambda kalkulu však neexistuje způsob, jak zabránit tomu, aby byla funkce aplikována na pravdivostní hodnoty , řetězce nebo jiné nečíselné objekty.

Formální definice

Definice

Výrazy lambda se skládají z:

• proměnné v ₁ , v ₂ , ...;
• abstrakční symboly λ (lambda) a. (tečka);
• závorky ().

Množinu výrazů lambda Λ lze definovat indukčně :

1. Pokud x je proměnná, pak x ∈ Λ.
2. Pokud x je proměnná a M ∈ Λ, pak (λ x . M ) ∈ Λ.
3. Pokud M , N ∈ Λ, pak ( MN ) ∈ Λ.

Instance pravidla 2 jsou známé jako abstrakce a instance pravidla 3 jsou známy jako aplikace .

Zápis

Aby byl zápis výrazů lambda přehledný, obvykle se používají následující konvence:

• Nejvzdálenější závorky jsou vynechány: M N místo ( M N ).
• Použití se předpokládá, že se nechal asociativní: M N P může být zapsána namísto (( M N ) P ).
• Tělo abstrakce sahá co nejvíce doprava : λ x . MN znamená λ x . ( MN ) a nikoli (λ x . M ) N .
• Sekvence abstrakcí je zkrácena : λ x .λ y .λ z . N je zkráceně λ xyz . N .

Volné a vázané proměnné

Operátor abstrakce λ údajně váže svoji proměnnou, ať se vyskytuje kdekoli v těle abstrakce. Proměnné, které spadají do rozsahu abstrakce, jsou údajně vázány . Ve výrazu λ x . M , část λ x je často nazýván pojivo , jako náznak, že proměnná x je stále vázán připojí λ x na M . Všechny ostatní proměnné se nazývají volné . Například ve výrazu λ y . xxy , y je vázaná proměnná a x je volná proměnná. Proměnná je také vázána svou nejbližší abstrakcí. V následujícím příkladu je jediný výskyt x ve výrazu vázán druhou lambda: λ x . y (λ x . zx ).

Sada volných proměnných lambda výrazu, M , je označena jako FV ( M ) a je definována rekurzí na strukturu výrazů, a to následovně:

1. FV ( x ) = { x }, kde x je proměnná.
2. FV (λ x . M ) = FV ( M ) \ { x }.
3. FV ( MN ) = FV ( M ) ∪ FV ( N ).

Výraz, který neobsahuje žádné volné proměnné, je údajně uzavřen . Uzavřené lambda výrazy jsou také známé jako kombinátory a jsou ekvivalentní výrazům v kombinační logice .

Snížení

Význam výrazů lambda je definován tím, jak lze výrazy omezit.

Existují tři druhy redukce:

• α-konverze : změna vázaných proměnných;
• β-redukce : aplikace funkcí na jejich argumenty;
• η-redukce : která zachycuje pojem extenze.

Mluvíme také o výsledných ekvivalencích: dva výrazy jsou α-ekvivalentní , pokud je lze α převést na stejný výraz. β-ekvivalence a η-ekvivalence jsou definovány podobně.

Termín redex , zkratka redukovatelného výrazu , se vztahuje k podtermům, které lze omezit jedním z pravidel redukce. Například, (λ x . M ) N je β-REDEX vyjádřit substituci N pro x v M . Výraz, na který redex redukuje, se nazývá jeho redukce ; redukce (λ x . M ) N je M [ x  : = N ].

Pokud x není v M volné , λ x . M x je také η-REDEX s Redukce z M .

α-konverze

α-konverze, někdy známá jako α-přejmenování, umožňuje změnit názvy vázaných proměnných. Například α-konverze λ x . x může poskytnout λ y . y . Termíny, které se liší pouze α-konverzí, se nazývají α-ekvivalent . Při použití lambda kalkulu jsou často α-ekvivalentní termíny považovány za ekvivalentní.

Přesná pravidla pro α-konverzi nejsou úplně triviální. Za prvé, při α-převodu abstrakce jsou přejmenovány pouze výskyty proměnných, které jsou vázány na stejnou abstrakci. Například α-konverze λ x .λ x . x může mít za následek λ y .λ x . x , ale nemohlo to mít za následek λ y .λ x . y . Ten druhý má jiný význam než originál. To je analogické s programovacím pojmem variabilní stínování .

Za druhé, α-konverze není možná, pokud by to mělo za následek zachycení proměnné jinou abstrakcí. Například, pokud nahradíme x s y v λ x .λ y . x , dostaneme λ y .λ y . y , což není vůbec stejné.

V programovacích jazycích se statickým rozsahem lze α-převod použít ke zjednodušení rozlišení názvu zajištěním toho, že název proměnné nebude maskovat název v rozsahu (viz α-přejmenování, aby rozlišení názvu bylo triviální ).

V De Bruijnově indexové notaci jsou jakékoli dva α-ekvivalentní termíny syntakticky totožné.

Střídání

Substituce, které M [ V  : = N ], je proces, který nahrazuje všechny volné výskyty proměnné V v expresním M s expresním N . Substituce na termínech lambda kalkulu je definována rekurzí na strukturu termínů následovně (poznámka: x a y jsou pouze proměnné, zatímco M a N jsou libovolné lambda výrazy):

x [ x  : = N ] = N

y [ x  : = N ] = y , pokud x ≠ y

( M ₁ M ₂ ) [ x  : = N ] = ( M ₁ [ x  : = N ]) ( M ₂ [ x  : = N ])

(λ x . M ) [ x  : = N ] = λ x . M

(λ y . M ) [ x  : = N ] = λ y . ( M [ x  : = N ]), pokud x ≠ y a y ∉ FV ( N )

Abychom nahradili abstrakci, je někdy nutné α převést výraz. Například není správné, aby (λ x . Y ) [ y  : = x ] mělo za následek λ x . x , protože nahrazené x mělo být volné, ale skončilo svázané. Správná náhrada je v tomto případě λ z . x , až do α-ekvivalence. Substituce je definována jednoznačně až do α-ekvivalence.

β-redukce

β-redukce vystihuje myšlenku aplikace funkcí. β-redukce je definována v podmínkách substituce: ZAŘÍZENÍ β-redukce (λ V . M ) N je M [ V  : = N ].

Například za předpokladu nějakého kódování 2, 7, × máme následující redukci β: (λ n . N × 2) 7 → 7 × 2.

Je možné vidět, že β-redukce je stejná jako koncept lokální redukovatelnosti v přirozené dedukci , pomocí Curry-Howardova izomorfismu .

η-redukce

η-redukce vyjadřuje myšlenku extenzality , což v tomto kontextu je, že dvě funkce jsou stejné právě tehdy, když dávají stejný výsledek pro všechny argumenty. Redukce η převádí mezi λ x . f x a f, kdykoli se x ve f nezobrazí jako volné .

η-redukci lze vidět stejnou jako koncept lokální úplnosti v přirozené dedukci prostřednictvím izomorfismu Curry-Howarda .

Normální formy a soutok

Pro netypový lambda kalkul β-redukce jako přepisovací pravidlo není ani silně normalizující, ani slabě normalizující .

Lze však ukázat, že β-redukce je konfluentní při zpracování až k α-konverzi (tj. Považujeme dvě normální formy za stejné, pokud je možné α-převést jednu na druhou).

Silně normalizační termíny i slabě normalizační termíny mají proto jedinečnou normální formu. U silně normalizačních výrazů je zaručeno, že jakákoli redukční strategie poskytne normální formu, zatímco u slabě normalizačních podmínek ji některé redukční strategie nemusí najít.

Kódování datových typů

Základní lambda kalkul lze použít k modelování booleovských, aritmetických , datových struktur a rekurze, jak je znázorněno v následujících dílčích částech.

Aritmetika v lambda kalkulu

Existuje několik možných způsobů, jak definovat přirozená čísla v lambda kalkulu, ale zdaleka nejběžnější jsou církevní číslice , které lze definovat následovně:

0: = λ f .λ x . X

1: = λ f .λ x . f x

2: = λ f .λ x . f ( f x )

3: = λ f .λ x . f ( f ( f x ))

a tak dále. Nebo pomocí alternativní syntaxe uvedené výše v Notation :

0: = λ fx . X

1: = λ fx . f x

2: = λ fx . f ( f x )

3: = λ fx . f ( f ( f x ))

Církevní číslice je funkce vyššího řádu- přebírá funkci s jedním argumentem f a vrací další funkci s jedním argumentem. Církevní číslice n je funkce, která bere funkci f jako argument a vrací n -té složení f , tj. Funkce f složená sama se sebou nkrát . Toto je označeno f ^{( n )} a je ve skutečnosti n -tou mocninou f (považováno za operátor); f ⁽⁰⁾ je definována jako funkce identity. Takto opakovaná složení (jedné funkce f ) dodržují zákony exponentů , a proto lze tyto číslice použít pro aritmetiku. (V Churchově původním lambda kalkulu byl formální parametr výrazu lambda vyžadován, aby se vyskytoval alespoň jednou v těle funkce, což znemožnilo výše uvedenou definici 0. )

Jedním ze způsobů uvažování o církevní číslici n , která je často užitečná při analýze programů, je instrukce „opakujte n krát“. Například pomocí níže definovaných funkcí PAIR a NIL lze definovat funkci, která sestrojí (propojený) seznam n prvků, které se všechny rovnají x , opakováním 'prepend another x element' n times, počínaje prázdným seznamem. Termín lambda je

λ n .λ x . n (PÁR x ) NIL

Změnou toho, co se opakuje, a změnou argumentu, na který se tato funkce opakuje, lze dosáhnout mnoha různých efektů.

Můžeme definovat nástupnickou funkci, která vezme církevní číslo n a vrátí n + 1 přidáním další aplikace f , kde '(mf) x' znamená, že funkce 'f' je aplikována 'm' krát na 'x':

SUCC: = λ n .λ f .λ x . f ( n f x )

Protože m -tá kompozice f složená s n -tou kompozicí f dává m + n -tu kompozici f , adici lze definovat následovně:

PLUS: = λ m .λ n .λ f .λ x . m f ( n f x )

PLUS lze chápat jako funkci, která bere jako argumenty dvě přirozená čísla a vrací přirozené číslo; dá se to ověřit

PLUS 2 3

a

5

jsou β-ekvivalentní lambda výrazy. Protože přidání m k číslu n lze provést přidáním 1 m krát, alternativní definice je:

PLUS: = λ m .λ n . m SUCC n 

Podobně lze násobení definovat jako

MULT: = λ m .λ n .λ f . m ( n f )

Alternativně

MULT: = λ m .λ n . m (PLUS n ) 0

od násobení m a n jsou stejné, jako opakování add n funkce m -krát, a pak aplikovat na nulu. Umocňování má poměrně jednoduché vykreslování v církevních číslicích, konkrétně

POW: = λ b .λ e . e b

Funkce předchůdce definovaná PRED n = n - 1 pro kladné celé číslo n a PRED 0 = 0 je podstatně obtížnější. Vzorec

PRED: = λ n .λ f .λ x . n (λ g .λ h . h ( g f )) (λ u . x ) (λ u . u )

lze validovat ukázkovým ukázáním, že pokud T označuje (λ g .λ h . h ( g f )) , pak T ^{( n )} (λ u . x ) = (λ h . h ( f ^{( n −1)} ( x ))) pro n > 0 . Níže jsou uvedeny dvě další definice PRED , jedna pomocí podmíněných a druhá pomocí dvojic . S funkcí předchůdce je odčítání jednoduché. Definování

SUB: = λ m .λ n . n PRED m ,

SUB m n výnosy m - n , když m > n a 0 jinak.

Logika a predikáty

Podle konvence se pro booleovské hodnoty PRAVDA a NEPRAVDA používají následující dvě definice (známé jako booleovské církve) :

PRAVDA: = λ x .λ y . X

NEPRAVDA: = λ x .λ y . y

(Všimněte si, že NEPRAVDA je ekvivalentní nule církve definované výše)

Potom s těmito dvěma lambda termíny můžeme definovat některé logické operátory (to jsou jen možné formulace; ostatní výrazy jsou stejně správné):

AND: = λ p .λ q . p q p

NEBO: = λ p .λ q . p p q

NE: = λ str . p FALSE TRUE

IFTHENELSE: = λ p .λ a .λ b . p a b

Nyní jsme schopni vypočítat některé logické funkce, například:

A SKUTEČNĚ NEPRAVDIVÉ

≡ (λ p .λ q . P q p ) PRAVDA NEPRAVDA → _β PRAVDA NEPRAVDA PRAVDA

≡ (λ x .λ y . X ) FALSE TRUE → _β FALSE

a vidíme, že AND TRUE FALSE je ekvivalentní FALSE .

Predikát je funkce, která vrátí logickou hodnotu. Nejzákladnějším predikátem je ISZERO , který vrací TRUE, pokud je jeho argumentem církevní číslice 0 , a FALSE, pokud je jeho argumentem jakákoli jiná církevní číslice:

ISZERO: = λ n . n (λ x .FALSE) PRAVDA

Následující predikát testuje, zda je první argument menší než druhý nebo druhý:

LEQ: = λ m .λ n. ISZERO (SUB m n ) ,

a protože m = n , pokud LEQ m n a LEQ n m , je jednoduché vytvořit predikát pro numerickou rovnost.

Dostupnost predikátů a výše uvedená definice PRAVDA a NEPRAVDA usnadňují psaní výrazů „kdyby-pak-jinak“ v lambda kalkulu. Funkci předchůdce lze například definovat jako:

PRED: = λ n . n (λ g .λ k. ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) 0

což lze ověřit indukčně ukázáním, že n (λ g .λ k. ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) je funkce add n - 1 pro n > 0.

Páry

Dvojici (2-tice) lze definovat z hlediska TRUE a FALSE pomocí kódování Church pro páry . Například PAIR zapouzdřuje pár ( x , y ), FIRST vrací první prvek páru a SECOND vrací druhý.

PÁR: = λ x .λ y .λ f . f x y

PRVNÍ: = λ str . p PRAVDA

DRUHÁ: = λ str . p NEPRAVDA

NIL: = λ x. TRUE

NULL: = λ p . p (λ x .λ y. FALSE)

Propojený seznam lze definovat buď jako NIL pro prázdný seznam, nebo jako PÁR prvku a menšího seznamu. Predikát NULL testuje hodnotu NIL . (Alternativně, s NIL: = FALSE , konstrukt l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil) obejde potřebu explicitního NULL testu).

Jako příklad použití dvojic lze funkci posunu a přírůstku, která mapuje ( m , n ) až ( n , n + 1), definovat jako

Φ: = λ x. PAIR (SECOND x ) (SUCC (SECOND x ))

což nám umožňuje poskytnout možná nejtransparentnější verzi funkce předchůdce:

PRED: = λ n. PRVNÍ ( n Φ (PÁR 0 0)).

Další techniky programování

Pro lambda kalkul existuje značná část programovacích idiomů . Mnoho z nich bylo původně vyvinuto v kontextu použití lambda kalkulu jako základu pro sémantiku programovacího jazyka , efektivně pomocí lambda kalkulu jako programovacího jazyka nízké úrovně . Protože několik programovacích jazyků obsahuje lambda kalkul (nebo něco velmi podobného) jako fragment, vidí tyto techniky využití také v praktickém programování, ale pak mohou být vnímány jako temné nebo cizí.

Pojmenované konstanty

V lambda kalkulu by knihovna měla formu sbírky dříve definovaných funkcí, které jako lambda-termíny jsou pouze konkrétní konstanty. Čistý lambda kalkul nemá koncept pojmenovaných konstant, protože všechny atomové lambda termíny jsou proměnné, ale pojmenované konstanty lze emulovat tak, že jako název konstanty odložíte proměnnou stranou, pomocí abstrakce tuto proměnnou v hlavním těle spojíte. , a aplikovat tuto abstrakci na zamýšlenou definici. Takže použít f ve smyslu M (nějaký explicitní lambda-termín) v N (jiný lambda-termín, "hlavní program"), lze říci

(λ f . N ) M

Autoři často zavádějí syntaktický cukr , jako například let , aby umožnili psaní výše uvedeného v intuitivnějším pořadí

nechť f = M v N.

Zřetězením těchto definic lze zapsat „program“ lambda kalkulu jako nula nebo více definic funkcí, následovaný jedním lambda termínem s využitím funkcí, které tvoří hlavní část programu.

Pozoruhodným omezením této let je, že název f není definován v M , protože M je mimo rozsah abstrakční vazby f ; to znamená, že definici rekurzivní funkce nelze použít jako M s let . Pokročilejší syntaktická konstrukce cukru letrec, která umožňuje psaní definic rekurzivních funkcí v tomto naivním stylu, místo toho navíc využívá kombinátory s pevným bodem.

Rekurze a pevné body

Rekurze je definice funkce pomocí samotné funkce. Lambda kalkul to nemůže vyjádřit přímo jako některé jiné notace: všechny funkce jsou v lambda kalkulu anonymní, takže nemůžeme odkazovat na hodnotu, která má být ještě definována, uvnitř lambda výrazu definujícího stejnou hodnotu. Nicméně, rekurze může ještě být dosaženo uspořádáním pro lambda výrazu pro příjem sebe jako argument hodnotu, například v  (λ x . X x ) E .

Zvažte faktoriální funkci F ( n ) rekurzivně definovanou

F ( n ) = 1, pokud n = 0; jinak n × F ( n - 1) .

Ve výrazu lambda, který má tuto funkci reprezentovat, se předpokládá, že parametr (typicky první) bude přijímat samotný výraz lambda jako jeho hodnotu, takže jeho volání - použití na argument - bude znamenat rekurzi. Aby se tedy dosáhlo rekurze, musí být zamýšlený argument odkazující na sebe ( zde nazývaný r ) vždy předán sám sobě v těle funkce v místě volání:

G: = λ r . λ n . (1, pokud n = 0; jinak n × ( r r ( n −1)))

s  r r x = F x = G r x  držet, takže  {{{1}}}  a

F: = GG = (λ x . X x ) G

Vlastní aplikace zde dosahuje replikace a předává výraz lambda funkce dalšímu vyvolání jako hodnotu argumentu, čímž je k dispozici pro odkazování a volání tam.

To to řeší, ale vyžaduje přepsat každé rekurzivní volání jako vlastní aplikaci. Chtěli bychom mít obecné řešení bez nutnosti přepisování:

G: = λ r . λ n . (1, pokud n = 0; jinak n × ( r ( n −1)))

kde  r x = F x = G r x  platí, takže  r = G r =: FIX G  a

F: = FIX G  kde  FIX g  : = ( r kde r = g r ) = g (FIX g )

takže  FIX G = G (FIX G) = (λ n . (1, pokud n = 0; jinak n × ((FIX G) ( n −1))))

Vzhledem k lambda výrazu s prvním argumentem představujícím rekurzivní volání (např. G zde) vrátí kombinátor FIX s pevným bodem samoreplikující se lambda výraz představující rekurzivní funkci (zde, F ). Funkci není třeba v žádném okamžiku výslovně předávat sama sobě, protože vlastní replikace je uspořádána předem, když je vytvořena, a je třeba ji provést pokaždé, když je vyvolána. Původní lambda výraz (FIX G) je tedy znovu vytvořen uvnitř sebe, v call-pointu, čímž se dosáhne sebereference .

Ve skutečnosti existuje mnoho možných definic pro tento operátor FIX , nejjednodušší z nich je:

Y  : = λ g . (Λ x . G ( x x )) (λ x . G ( x x ))

V lambda kalkulu je Y g   pevný bod g , protože se rozšiřuje na:

Y g

(λ h . (λ x . h ( x x )) (λ x . h ( x x ))) g

(λ x . g ( x x )) (λ x . g ( x x ))

g ((λ x . g ( x x )) (λ x . g ( x x )))

g ( Y g )

Nyní, abychom provedli rekurzivní volání faktoriální funkce, jednoduše bychom zavolali ( Y G) n , kde n je číslo, pro které počítáme faktoriál. Vzhledem k n = 4 to například dává:

( Y G) 4

G ( Y G) 4

(λ r .λ n . (1, pokud n = 0; jinak n × ( r ( n −1)))) ( Y G) 4

(λ n . (1, pokud n = 0; jinak n × (( Y G) ( n −1)))) 4

1, je -li 4 = 0; else 4 × (( Y G) (4−1))

4 × (G ( Y G) (4−1))

4 × ((λ n . (1, pokud n = 0; jinak n × (( Y G) ( n −1)))) (4−1))

4 × (1, je -li 3 = 0; jinak 3 × (( Y G) (3−1)))

4 × (3 × (G ( Y G) (3−1)))

4 × (3 × ((λ n . (1, pokud n = 0; jinak n × (( Y G) ( n −1)))) (3−1)))

4 × (3 × (1, pokud 2 = 0; jinak 2 × (( Y G) (2−1))))

4 × (3 × (2 × (G ( Y G) (2-1))))

4 × (3 × (2 × ((λ n . (1, pokud n = 0; jinak n × (( Y G) ( n −1)))) (2−1))))

4 × (3 × (2 × (1, pokud 1 = 0; jinak 1 × (( Y G) (1−1)))))

4 × (3 × (2 × (1 × (G ( Y G) (1−1))))))

4 × (3 × (2 × (1 × ((λ n . (1, pokud n = 0; jinak n × (( Y G) ( n −1))))) (1−1)))))

4 × (3 × (2 × (1 × (1, pokud 0 = 0; jinak 0 × (( Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24

Každou rekurzivně definovanou funkci lze považovat za pevný bod nějaké vhodně definované funkce, která se uzavírá nad rekurzivním voláním s dalším argumentem, a proto pomocí Y lze každou rekurzivně definovanou funkci vyjádřit jako výraz lambda. Zejména nyní můžeme čistě rekurzivně definovat predikci odčítání, násobení a porovnávání přirozených čísel.

Standardní podmínky

Některé výrazy mají běžně přijímaná jména:

I  : = λ x . X

K  : = λ x .λ y . X

S  : = λ x .λ y .λ z . x z ( y z )

B  : = λ x .λ y .λ z . x ( y z )

C  : = λ x .λ y .λ z . x z y

W  : = λ x .λ y . x y y

U  : = λ x . x x

ω  : = λ x . x x

Ω  : = ω ω

Y  : = λ g . (Λ x . G ( x x )) (λ x . G ( x x ))

Některé z nich mají přímé aplikace při eliminaci abstrakce, která mění lambda termíny na termíny kombinatorického počtu .

Odstranění abstrakce

Pokud N je lambda-termín bez abstrakce, ale případně obsahuje pojmenované konstanty ( kombinátory ), pak existuje lambda-termín T ( x , N ), který je ekvivalentní λ x . N, ale postrádá abstrakci (kromě případů, kdy jsou součástí pojmenovaných konstant, pokud jsou považovány za neatomové). Na to lze také pohlížet jako na anonymizující proměnné, protože T ( x , N ) odstraní všechny výskyty x z N , a přitom umožní nahrazení hodnot argumentů do pozic, kde N obsahuje x . Převodní funkci T lze definovat:

T ( x , x ): = I

T ( x , N ): = K N, pokud x není v N volné .

T ( x , M N ): = S T ( x , M ) T ( x , N )

V obou případech lze termín ve formě T ( x , N ) P redukovat tím, že počáteční kombinátor I , K nebo S uchopí argument P , stejně jako by to dělala β-redukce (λ x . N ) P. I vrátí tento argument. K hází argument pryč, stejně jako (λ x . N ) by udělat, pokud x není volné výskyt v N . S předá argument oběma podtermům aplikace a poté použije výsledek prvního na výsledek druhého.

Tyto kombinátory B a C jsou podobné S , ale předat argument pouze k jedné subterm žádosti ( B na „argument“ subterm a C na „funkce“ subterm), čímž se šetří následnou K , pokud není výskyt o x v jednom subterm. Ve srovnání s B a C je S kombinátor skutečnosti směšuje dvě funkce: přeskupit argumenty, a duplikování argument tak, že může být použit na dvou místech. Kombinátor W dělá pouze to druhé, čímž poskytuje systém B, C, K, W jako alternativu k počtu kombinátorů SKI .

Psaný lambda kalkul

Zadaný lambda kalkulu je zadaný formalismus , který používá lambda-symbol ( ) k označení anonymní funkce abstrakci. V této souvislosti jsou typy obvykle objekty syntaktické povahy, které jsou přiřazeny výrazům lambda; přesná povaha typu závisí na uvažovaném počtu (viz Druhy typovaných lambda calculi ). Z určitého úhlu pohledu lze na typizované lambda kameny pohlížet jako na zdokonalení netypového lambda kalkulu, ale z jiného úhlu pohledu je lze také považovat za fundamentálnější teorii a netypovaný lambda kalkul za speciální případ pouze s jedním typem. ${\ Displaystyle \ lambda}$

Typové lambda kalkulátory jsou základními programovacími jazyky a jsou základem typovaných funkčních programovacích jazyků, jako jsou ML a Haskell , a nepříměji typovaných imperativních programovacích jazyků. Typické lambda kameny hrají důležitou roli při navrhování typových systémů pro programovací jazyky; zde typovatelnost obvykle zachycuje požadované vlastnosti programu, např. program nezpůsobí narušení přístupu do paměti.

Zadané lambda kameny úzce souvisí s matematickou logikou a teorií důkazů pomocí Curry -Howardova izomorfismu a lze je považovat za vnitřní jazyk tříd kategorií , např. Jednoduše napsaný lambda kalkul je jazykem karteziánských uzavřených kategorií (CCC).

Redukční strategie

To, zda se určitý termín normalizuje nebo ne, a kolik práce je třeba při jeho normalizaci vykonat, pokud ano, do značné míry závisí na použité strategii redukce. Mezi běžné strategie redukce počtu lambda patří:

Normální objednávka

Nejlevnější, nejzazší redex je vždy redukován jako první. To znamená, že kdykoli je to možné, jsou argumenty nahrazeny tělem abstrakce, než jsou argumenty redukovány.

Přihláška

Nejlevnější, nejvnitřnější redex je vždy redukován jako první. Intuitivně to znamená, že argumenty funkce jsou vždy redukovány před samotnou funkcí. Aplikační pořadí se vždy pokouší použít funkce na normální formuláře, i když to není možné.

Plné β-redukce

Jakýkoli redex lze kdykoli snížit. To v podstatě znamená nedostatek jakékoli konkrétní redukční strategie - s ohledem na redukovatelnost „všechny sázky jsou vypnuté“.

Slabé redukční strategie nesnižují pod lambda abstrakcí:

Volejte podle hodnoty

Redex se sníží pouze tehdy, když se jeho pravá strana sníží na hodnotu (proměnnou nebo abstrakci). Omezeny jsou pouze nejvzdálenější redexy.

Volejte jménem

Jako normální pořadí, ale uvnitř abstrakcí se neprovádí žádná redukce. Například λ x . (Λ x . X ) x je podle této strategie v normální formě, přestože obsahuje redex (λ x . X ) x .

Strategie se sdílením omezují paralelně "stejné" výpočty:

Optimální redukce

Jako normální pořadí, ale výpočty, které mají stejný štítek, jsou redukovány současně.

Volejte podle potřeby

Jako volání podle jména (tedy slabé), ale funkční aplikace, které by místo názvu duplikovaly argument, který se pak redukuje pouze „když je to potřeba“.

Vypočitatelnost

Neexistuje žádný algoritmus, který by přijímal jako vstup libovolné dva výrazy lambda a výstupy PRAVDA nebo NEPRAVDA v závislosti na tom, zda se jeden výraz redukuje na druhý. Přesněji řečeno, žádná vypočítatelná funkce nemůže otázku rozhodnout . To byl historicky první problém, u kterého bylo možné dokázat nerozhodnutelnost. Jako obvykle pro takový důkaz, přepočitatelný znamená spočítatelný jakýmkoli modelem výpočtu, který je Turing dokončen . Ve skutečnosti lze vyčíslitelnost sama definovat pomocí lambda kalkulu: funkce F : N → N přirozených čísel je vypočítatelná funkce tehdy a jen tehdy, existuje -li lambda výraz f takový, že pro každý pár x , y v N , F ( x ) = y právě tehdy, když f x  = _β  y , kde x a y jsou církevní číslice odpovídající x a y , a = _β znamená ekvivalenci s β-redukcí. Další přístupy k definování vyčíslitelnosti a jejich rovnocennosti najdete v práci Church -Turinga .

Churchův důkaz nevypočitatelnosti nejprve redukuje problém na určení, zda má daný výraz lambda normální formu . Poté předpokládá, že tento predikát je vyčíslitelný, a proto může být vyjádřen v lambda kalkulu. V návaznosti na dřívější práci Kleene a konstrukci Gödelova číslování pro výrazy lambda konstruuje výraz lambda e, který těsně následuje důkaz první Gödelovy věty o neúplnosti . Pokud je e aplikováno na vlastní Gödelovo číslo, dojde k rozporu.

Složitost

Pojem výpočetní složitosti pro lambda kalkul je trochu ošidný, protože náklady na redukci β se mohou lišit v závislosti na tom, jak je implementován. Abychom byli přesní, je třeba nějak najít umístění všech výskytů vázané proměnné V ve výrazu E , což znamená časové náklady, nebo je třeba určitým způsobem sledovat umístění volných proměnných, což znamená náklady na prostor. Naïve hledání o umístění V v E je O ( n ) v délce n z e . Řetězcové řetězce byly raným přístupem, který obchodoval tentokrát s náklady za kvadratické využití prostoru. Obecněji to vedlo ke studiu systémů, které používají explicitní substituci .

V roce 2014 bylo ukázáno, že počet kroků redukce β provedených redukcí normálního řádu za účelem redukce termínu je model s rozumnými časovými náklady, to znamená, že redukci lze simulovat na Turingově stroji v čase polynomiálně úměrném počtu kroků . Jednalo se o dlouhotrvající otevřený problém, kvůli explozi velikosti , existenci lambda termínů, které rostou exponenciálně ve velikosti pro každou β-redukci. Výsledkem je obcházení práce s kompaktní sdílenou reprezentací. Výsledek jasně ukazuje, že velikost prostoru potřebného k vyhodnocení lambda výrazu není úměrná velikosti termínu během redukce. V současné době není známo, co by bylo dobrým měřítkem složitosti vesmíru.

Nerozumný model nemusí nutně znamenat neefektivní. Optimální redukce redukuje všechny výpočty se stejným označením v jednom kroku, vyhýbá se duplicitní práci, ale počet paralelních kroků β-redukce ke snížení daného termínu na normální formu je ve velikosti termínu přibližně lineární. To je příliš malé na to, aby to bylo přiměřené nákladové opatření, protože jakýkoli Turingův stroj může být zakódován v lambda kalkulu ve velikosti lineárně úměrné velikosti Turingova stroje. Skutečné náklady na snížení lambda termínů nejsou způsobeny β-redukcí per se, ale spíše zpracováním duplikace redexů během β-redukce. Není známo, zda jsou optimální implementace redukce rozumné, pokud jsou měřeny s ohledem na model přiměřených nákladů, jako je počet nejzazších kroků do normální formy, ale u fragmentů lambda kalkulu bylo ukázáno, že optimální redukční algoritmus je účinný. a má nanejvýš kvadratickou režii ve srovnání s krajním krajním krajem. Kromě toho implementace optimálního snížení BOHM překonala Caml Light i Haskell z hlediska čistého lambda.

Lambda kalkul a programovací jazyky

Jak zdůraznil papír Petera Landina z roku 1965 „Korespondence mezi ALGOL 60 a církevní lambda-notací“, sekvenční procedurální programovací jazyky lze chápat jako lambda kalkul, který poskytuje základní mechanismy pro procedurální abstrakci a proceduru (podprogram) aplikace.

Anonymní funkce

Například v Lispu lze funkci „square“ vyjádřit jako výraz lambda takto:

(lambda (x) (* x x))

Výše uvedený příklad je výraz, který se vyhodnotí jako funkce první třídy. Symbol lambdavytváří anonymní funkci, která obsahuje seznam názvů parametrů (x)- v tomto případě pouze jeden argument a výraz, který je vyhodnocen jako tělo funkce (* x x). Anonymní funkce se někdy nazývají výrazy lambda.

Například Pascal a mnoho dalších imperativních jazyků již dlouho podporuje předávání podprogramů jako argumentů jiným podprogramům prostřednictvím mechanismu ukazatelů funkcí . Ukazatele funkcí však nejsou dostatečnou podmínkou toho, aby funkce byly datovými typy první třídy , protože funkce je datovým typem první třídy právě tehdy, když lze za běhu vytvořit nové instance funkce. A toto vytváření funkcí za běhu je podporováno mimo jiné v jazycích Smalltalk , JavaScript a Wolfram a v poslední době mimo jiné ve Scale , Eiffel („agenti“), C# („delegáti“) a C ++ 11 .

Paralelismus a souběžnost

Church-Rosserova vlastnost lambda znamená, že vyhodnocení (β-redukce) se může provádět v libovolném pořadí , a to i paralelně. To znamená, že jsou relevantní různé nedeterministické strategie hodnocení . Lambda kalkul však nenabízí žádné explicitní konstrukty pro paralelismus . Do lambda kalkulu lze přidat konstrukty, jako jsou Futures . Pro popis komunikace a souběžnosti byly vyvinuty další procesní kameny .

Sémantika

Skutečnost, že termíny lambda kalkulu fungují jako funkce pro jiné termíny lambda kalkulu a dokonce i pro ně samotné, vedla k otázkám ohledně sémantiky lambda kalkulu. Mohl by být výrazům lambda kalkulu přiřazen rozumný význam? Přirozenou sémantikou bylo najít množinu D izomorfních k funkčnímu prostoru D → D , funkcí na sobě. Žádný netriviální takový D však nemůže existovat, kvůli omezením mohutnosti, protože sada všech funkcí od D do D má větší mohutnost než D , pokud D není singletonová množina .

V 70. letech Dana Scott ukázala, že pokud by se uvažovalo pouze o spojitých funkcích , mohla by být nalezena množina nebo doména D s požadovanou vlastností, čímž by se vytvořil model pro lambda kalkul.

Tato práce také vytvořila základ pro denotační sémantiku programovacích jazyků.

Variace a rozšíření

Tato rozšíření jsou v lambda kostce :

• Typový lambda kalkul - lambda kalkul se zadanými proměnnými (a funkcemi)
• Systém F -Typový lambda kalkul s typovými proměnnými
• Kalkul staveb -Typický lambda kalkul s typy jako hodnotami první třídy

Tyto formální systémy jsou rozšířením lambda kalkulu, které nejsou v lambda kostce:

• Binární lambda kalkul - Verze lambda kalkulu s binárními I/O, binárním kódováním výrazů a určeným univerzálním strojem.
• Lambda-mu počet -Rozšíření počtu lambda pro léčbu klasické logiky

Tyto formální systémy jsou variacemi lambda kalkulu:

• Kappa kalkul -analog prvního řádu lambda kalkulu

Tyto formální systémy souvisejí s lambda kalkulem:

• Kombinační logika - Zápis pro matematickou logiku bez proměnných
• Kombinátor SKI - výpočetní systém založený na kombinátorech S , K a I , ekvivalentní lambda kalkulu, ale redukovatelný bez proměnných substitucí

Viz také

Poznámky

Reference

Další čtení

• Abelson, Harold a Gerald Jay Sussman. Struktura a interpretace počítačových programů . MIT Press . ISBN  0-262-51087-1 .
• Hendrik Pieter Barendregt Úvod do lambda kalkulu .
• Henk Barendregt , Dopad lambda kalkulu v logice a informatice . Bulletin symbolické logiky, svazek 3, číslo 2, červen 1997.
• Barendregt, Hendrik Pieter , The Type Free Lambda Calculus pp1091–1132 of Handbook of Mathematical Logic , North-Holland (1977) ISBN  0-7204-2285-X
• Cardone a Hindley, 2006. Historie lambda-kalkulu a kombinační logiky . In Gabbay and Woods (eds.), Handbook of the History of Logic , sv. 5. Elsevier.
• Church, Alonzo, Neřešitelný problém elementární teorie čísel , American Journal of Mathematics , 58 (1936), s. 345–363. Tento dokument obsahuje důkaz, že ekvivalence výrazů lambda není obecně rozhodnutelná.
• Alonzo Church, The Calculi of Lambda-Conversion ( ISBN  978-0-691-08394-0 )
• Frink Jr., Orrin, Recenze: The Calculi of Lambda-Conversion
• Kleene, Stephen, A theory of positive integer in formal logic , American Journal of Mathematics , 57 (1935), str. 153–173 a 219–244. Obsahuje definice lambda kalkulu několika známých funkcí.
• Landin, Peter , Korespondence mezi ALGOL 60 a Church's Lambda-Notation , Communications of the ACM , sv. 8, č. 2 (1965), strany 89–101. K dispozici na webu ACM . Klasický dokument zdůrazňující význam lambda kalkulu jako základu pro programovací jazyky.
• Larson, Jim, Úvod do lambda kalkulu a schématu . Jemný úvod pro programátory.
• Schalk, A. a Simmons, H. (2005) Úvod do λ-kalkulů a aritmetiky se slušným výběrem cviků . Poznámky ke kurzu z matematické logiky MSc na univerzitě v Manchesteru.
• de Queiroz, Ruy JGB (2008). „O pravidlech redukce, významu jako použití a důkazně teoretické sémantice“. Studia Logica . 90 (2): 211–247. doi : 10,1007/s11225-008-9150-5 . S2CID  11321602 . Dokument, který formálně podtrhuje myšlenku „smyslu je použití“, který, i když je založen na důkazech, je odlišný od důkazní teoretické sémantiky jako v tradici Dummett-Prawitz, protože jako pravidla dávající význam vyžaduje redukci.
• Hankin, Chris, Úvod do Lambda Calculi pro počítačové vědce, ISBN  0954300653

Monografie/učebnice pro postgraduální studenty:

• Morten Heine Sørensen, Paweł Urzyczyn, Přednášky o Curry-Howard izomorfismus , Elsevier, 2006, ISBN  0-444-52077-5 je nedávný monografie, která pokrývá hlavní témata lambda kalkulu z typu bez odrůdě, většina zadaný lambda calculi , včetně novějších vývojů, jako jsou systémy čistého typu a kostka lambda . Nezahrnuje rozšíření podtypů .
• Pierce, Benjamin (2002), Typy a programovací jazyky , MIT Press, ISBN 0-262-16209-1pokrývá kameny lambda z pohledu systému praktického typu; některá témata jako závislé typy jsou pouze zmíněna, ale podtypování je důležité téma.

Některé části tohoto článku jsou založeny na materiálu společnosti FOLDOC , který byl použit se svolením .

externí odkazy

• Graham Hutton, Lambda Calculus , krátké (12 minut) Počítačové video o Lambda Calculus
• Helmut Brandl, krok za krokem Úvod do lambda kalkulu
• „Lambda-calculus“ , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• Achim Jung, Krátký úvod do lambda kalkulu -( PDF )
• Dana Scott, Časová osa lambda kalkulu -( PDF )
• David C. Keenan, Dissect a Mockingbird: Graphical Notation for the Lambda Calculus with Animated Reduction
• Raúl Rojas, Tutorial Introduction to Lambda Calculus -( PDF )
• Peter Selinger, Přednášky o lambda kalkulu -( PDF )
• L. Allison, Některé spustitelné příklady λ-počtu
• Georg P. Loczewski, The Lambda Calculus a A ++
• Bret Victor, Alligator Eggs: Logická hra založená na lambda kalkulu
• Lambda kalkul na webu Safalra
• LCI Lambda Interpreter je jednoduchý, ale výkonný tlumočník čistého počtu
• Odkazy Lambda Calculus na Lambda-the-Ultimate
• Mike Thyer, Lambda Animator , grafický aplet Java demonstrující alternativní strategie redukce.
• Implementace Lambda kalkulu pomocí šablon C ++
• Marius Buliga, grafický lambda kalkul
• Lambda kalkul jako model pracovního postupu Peter Kelly, Paul Coddington a Andrew Wendelborn; zmiňuje redukci grafu jako běžný způsob hodnocení výrazů lambda a diskutuje použitelnost lambda kalkulu pro distribuované výpočty (kvůli vlastnosti Church – Rosser , která umožňuje paralelní redukci grafu pro výrazy lambda).
• Shane Steinert-Threlkeld, „Lambda Calculi“ , internetová encyklopedie filozofie
• Anton Salikhmetov, Macro Lambda Calculus