Lambda kalkul je formální systém v matematické logice pro vyjádření výpočtů založených na abstrakci a aplikaci funkcí pomocí vazby a substituce proměnných. Jedná se o univerzální model, který lze aplikovat na konstrukci jakéhokoli Turingova stroje. Lambda kalkul byl poprvé představen Churchem, slavným matematikem, ve 30. letech 20. století.
Systém se skládá z budování lambda členů a provádění redukčních operací na nich.
Vysvětlení a aplikace
Řecké písmeno lambda (λ) se používá ve výrazech lambda a termínech lambda k označení vazby proměnné ve funkci.
Lambda kalkul může být netypizovaný nebo napsaný. V první variantě lze funkce použít pouze v případě, že jsou schopny přijímat data tohoto typu. Typizované lambda calculi jsou slabší, mohou vyjadřovat menší hodnotu. Ale na druhou stranu vám umožní dokázat více věcí.
Jedním z důvodů, proč existuje tolik různých typů, je touha vědců udělat více, aniž by se vzdali příležitosti prokázat silné lambda matematické teorémy.
Systém má aplikace v mnoha různých oblastech matematiky, filozofie, lingvistiky a informatiky. Za prvé, lambda kalkul je kalkul, který sehrál důležitou roli ve vývoji teorie programovacích jazyků. Systémy implementují styly funkční tvorby. Jsou také horkým tématem výzkumu v oblasti teorie těchto kategorií.
Pro figuríny
Lambda kalkul zavedl matematik Alonzo Church ve 30. letech 20. století jako součást svého výzkumu základů vědy. Původní systém se ukázal jako logicky nekonzistentní v roce 1935, kdy Stephen Kleen a J. B. Rosser vyvinuli Kleene-Rosserův paradox.
Později, v roce 1936, Church vyčlenil a zveřejnil pouze tu část, která je relevantní pro výpočty, čemuž se dnes říká netypový lambda kalkul. V roce 1940 také představil slabší, ale logicky konzistentní teorii známou jako systém primárního typu. Ve své práci vysvětluje celou teorii jednoduchými termíny, takže lze říci, že Church publikoval kalkul lambda pro figuríny.
Až do 60. let, kdy se jeho vztah k programovacím jazykům vyjasnil, byl λ jen formalismus. Díky aplikacím Richarda Montagu a dalších lingvistů v sémantice přirozeného jazyka zaujal kalkul čestné místo jak v lingvistice, tak v informatice.
Původ symbolu
Lambda neznamená slovo nebo zkratku, pochází z odkazu v Russell's Principal Mathematics, po kterém následují dvě typografické změny. Příklad zápisu: pro funkci f s f (y)=2y + 1 je 2ŷ + 1. A zde použijeme stříšku („klobouk“) nad y k označení vstupní proměnné.
Církev původně zamýšlela používat podobné symboly, ale sazeči nedokázali umístit symbol „klobouku“nad písmena. Místo toho to původně vytiskli jako "/\y.2y+1". V další epizodě úprav nahradili písaři „/ \“vizuálně podobným znakem.
Úvod do lambda kalkulu
Systém se skládá z jazyka termínů, které jsou voleny určitou formální syntaxí, a ze sady transformačních pravidel, které s nimi umožňují manipulovat. Poslední bod lze považovat za rovnicovou teorii nebo za operační definici.
Všechny funkce v lambda kalkulu jsou anonymní, což znamená, že nemají jména. Berou pouze jednu vstupní proměnnou a k implementaci grafů s více proměnnými se používá currying.
Lambda termíny
Syntaxe kalkulu definuje některé výrazy jako platné a jiné jako neplatné. Stejně jako různé řetězce znaků jsou platné programy C a některé ne. Skutečné vyjádření lambda kalkulu se nazývá "lambda termín".
Následující tři pravidla poskytují induktivní definici, která může býtplatí pro konstrukci všech syntakticky platných pojmů:
Proměnná x je sama o sobě platným výrazem lambda:
- pokud T je LT a x je nekonstantní, pak (lambda xt) se nazývá abstrakce.
- jestliže T a s jsou pojmy, pak (TS) se nazývá aplikace.
Nic jiného není termín lambda. Koncept je tedy platný tehdy a jen tehdy, když jej lze získat opakovaným použitím těchto tří pravidel. Některé závorky však mohou být vynechány podle jiných kritérií.
Definice
Lambda výrazy se skládají z:
- proměnné v 1, v 2, …, v n, …
- symboly abstrakce 'λ' a tečka '.'
- hranaté závorky ().
Sada Λ může být definována indukčně:
- Je-li x proměnná, pak x ∈ Λ;
- x není konstantní a M ∈ Λ, pak (λx. M) ∈ Λ;
- M, N ∈ Λ, pak (MN) ∈ Λ.
Označení
Aby byl zápis lambda výrazů přehledný, běžně se používají následující konvence:
- Vnější závorky vynechány: MN místo (MN).
- Předpokládá se, že aplikace zůstanou asociativní: místo ((MN) P lze napsat MNP).
- Tělo abstrakce sahá dále doprava: λx. MN znamená λx. (MN), nikoli (λx. M) N.
- Posloupnost abstrakcí je redukována: λx.λy.λz. N může být λxyz. N.
Volné a vázané proměnné
Operátor λ spojuje svou nekonstantu kdekoli v těle abstrakce. Proměnné, které spadají do rozsahu, se nazývají vázané. Ve výrazu λ x. M, část λ x je často označována jako pojivo. Jako by naznačoval, že se proměnné stanou skupinou s přidáním X x k M. Všechny ostatní nestabilní se nazývají volné.
Například ve výrazu λ y. x x y, y - vázané netrvalé a x - volné. A také stojí za zmínku, že proměnná je seskupena podle své „nejbližší“abstrakce. V následujícím příkladu je řešení lambda kalkulu reprezentováno jediným výskytem x, který souvisí s druhým členem:
λ x. y (λ x. z x)
Množina volných proměnných M je označena jako FV (M) a je definována rekurzí přes strukturu termínů takto:
- FV (x)={x}, kde x je proměnná.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Vzorec, který neobsahuje volné proměnné, se nazývá uzavřený. Uzavřené výrazy lambda jsou také známé jako kombinátory a jsou ekvivalentní termínům v kombinatorické logice.
Zkratka
Význam výrazů lambda je určen tím, jak je lze zkrátit.
Existují tři typy řezů:
- α-transformace: změna vázaných proměnných (alfa).
- β-redukce: použití funkcí na jejich argumenty (beta).
- η-transform: pokrývá pojem extenzionality.
Tady je to takémluvíme o výsledných ekvivalencích: dva výrazy jsou β-ekvivalentní, pokud je lze β-transformovat na stejnou složku, a α / η-ekvivalence je definována podobně.
Pojem redex, zkratka pro redukovatelný obrat, odkazuje na podtémata, která lze omezit jedním z pravidel. Lambda kalkul pro figuríny, příklady:
(λ x. M) N je beta redex ve výrazu pro nahrazení N x v M. Složka, na kterou se redex redukuje, se nazývá její redukt. Redukce (λ x. M) N je M [x:=N].
Pokud x není volné v M, λ x. M x také em-REDEX s regulátorem M.
α-transformation
Alfa přejmenování umožňují změnit názvy vázaných proměnných. Například x. x může dát λ y. y Pojmy, které se liší pouze v alfa transformaci, jsou považovány za α-ekvivalenty. Při použití lambda kalkulu se často α-ekvivalenty považují za vzájemné.
Přesná pravidla pro převod alfa nejsou zcela triviální. Za prvé, s touto abstrakcí jsou přejmenovány pouze ty proměnné, které jsou spojeny se stejným systémem. Například alfa transformace λ x.λ x. x může vést k λ y.λ x. x, ale to nemusí vést k λy.λx.y Ten druhý má jiný význam než originál. Toto je analogie konceptu programování proměnných stínování.
Zadruhé, alfa transformace není možná, pokud by vedla k zachycení netrvalou jinou abstrakcí. Pokud například nahradíte x za y v λ x.λ y. x, pak můžete získatλy.λy. u, což vůbec není totéž.
V programovacích jazycích se statickým rozsahem lze pro zjednodušení překladu názvů použít převod alfa. Zároveň dbejte na to, aby koncept proměnné nezakrýval označení v oblasti obsahující.
V zápisu indexu De Bruyne jsou libovolné dva alfa-ekvivalentní termíny syntakticky totožné.
Náhrada
Změny zapsané pomocí E [V:=R] jsou procesem nahrazení všech volných výskytů proměnné V ve výrazu E obratem R. Substituce ve smyslu λ je definována lambda rekurze počet na struktuře konceptu následovně (poznámka: x a y - pouze proměnné a M a N - libovolný λ-výraz).
x [x:=N] ≡ N
y [x:=N] ≡ y, pokud 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]), pokud x ≠ y, za předpokladu, že y ∉ FV (N).
Pro substituci do lambda abstrakce je někdy nutné α-transformovat výraz. Například není pravda, že (λ x. Y) [y:=x] má za následek (λ x. X), protože substituované x mělo být volné, ale skončilo jako vázané. Správná náhrada je v tomto případě (λ z. X) až do α-ekvivalence. Všimněte si, že substituce je jednoznačně definována až do lambda.
β-snížení
Snížení beta odráží myšlenku použití funkce. Beta-redukční je definován v pojmechsubstituce: ((X V. E) E ') je E [V:=E'].
Například za předpokladu nějakého kódování 2, 7, × existuje následující β-redukce: ((λ n. N × 2) 7) → 7 × 2.
Snížení beta lze chápat stejně jako koncept místní redukovatelnosti v rámci přirozené dedukce prostřednictvím Curryho-Howardova izomorfismu.
η-transform
Tato konverze vyjadřuje myšlenku extenzionality, která v tomto kontextu znamená, že dvě funkce jsou si rovny, když dávají stejný výsledek pro všechny argumenty. Tento převod se vyměňuje mezi λ x. (F x) a f vždy, když se x nezdá volné v f.
Tuto akci lze považovat za stejnou jako koncept místní úplnosti přirozené dedukce prostřednictvím Curryho-Howardova izomorfismu.
Normální formy a fúze
U netypizovaného lambda kalkulu není β-redukční pravidlo obecně ani silné, ani slabé normalizační.
Nicméně lze ukázat, že β-redukce splývá, když probíhá před α-transformací (tj. dvě normální formy lze považovat za rovnocenné, pokud je možná α-transformace z jedné na druhou).
Výrazně normalizující i slabě upravující výrazy proto mají jedinou normální formu. Pro první termíny je zaručeno, že jakákoli redukční strategie povede k typické konfiguraci. Zatímco u slabě se normalizujících podmínek to některé redukční strategie nemusí najít.
Další metody programování
Pro lambda kalkul existuje mnoho kreačních idiomů. Mnohé z nich byly původně vyvinuty v kontextu používání systémů jako základu pro sémantiku programovacího jazyka a efektivně je aplikovaly jako nízkoúrovňový konstrukt. Vzhledem k tomu, že některé styly obsahují lambda kalkul (nebo něco velmi podobného) jako úryvek, najdou tyto techniky využití také v praktické tvorbě, ale pak mohou být vnímány jako nejasné nebo cizí.
Pojmenované konstanty
V lambda kalkulu má knihovna podobu sady dříve definovaných funkcí, kde termíny jsou pouze konkrétní konstanty. Čistý počet nemá žádný koncept pojmenovaných neměnných, protože všechny atomové lambda termíny jsou proměnné. Ale lze je také napodobit tak, že jako název konstanty vezmeme proměnlivé, použijeme lambda abstrakci k navázání této těkavé látky v těle a použijeme tuto abstrakci na zamýšlenou definici. Pokud tedy použijete f k reprezentaci M v N, můžete říci
(λ f. N) M.
Autoři často zavádějí syntaktický koncept, jako je nechat, aby bylo možné věci psát intuitivnějším způsobem.
f=M až N
Zřetězením takových definic lze napsat „program“lambda kalkulu jako nula nebo více definic funkcí následovaných jedním členem lambda, s použitím definic, které tvoří většinu programu.
Významným omezením tohoto nechť je, že jméno f není definováno v M,protože M je mimo závazný rozsah lambda abstrakce f. To znamená, že atribut rekurzivní funkce nelze použít jako M s let. Pokročilejší syntaxe letrec, která vám umožňuje psát definice rekurzivních funkcí v tomto stylu, navíc místo toho používá kombinátory s pevnou řádovou čárkou.
Tištěné analogy
Tento typ je typizovaný formalismus, který používá symbol k reprezentaci anonymní abstrakce funkcí. V tomto kontextu jsou typy obvykle objekty syntaktické povahy, které jsou přiřazeny k lambda termínům. Přesná povaha závisí na příslušném počtu. Z určitého pohledu lze typizované LI považovat za upřesnění netypizovaného LI. Ale na druhou stranu je lze také považovat za fundamentálnější teorii a netypizovaný počet lambda je speciální případ pouze s jedním typem.
Typované LI jsou základem programovacích jazyků a páteří funkčních jazyků, jako jsou ML a Haskell. A nepřímo i imperativní styly tvorby. Typované lambda kalkuly hrají důležitou roli ve vývoji typových systémů pro programovací jazyky. Zde typovatelnost obvykle zachycuje požadované vlastnosti programu, například nezpůsobí narušení přístupu do paměti.
Typované lambda kalkuly úzce souvisejí s matematickou logikou a teorií důkazů prostřednictvím Curry-Howardova izomorfismu a lze je považovat za vnitřní jazyk tříd kategorií, např.prostě je to styl karteziánských uzávěrů.
