Lambda-kalkul

Kalkul lambda (nebo λ-kalkulu ) je formální systém vynalezl Alonzo Church v roce 1930 , která stanovuje koncepty funkce a aplikace . Manipulujeme s výrazy, které se nazývají výrazy λ, kde se k vázání proměnné používá řecké písmeno λ . Například pokud M je výraz λ, λx.M je také výrazem λ a představuje funkci, která x spojuje M.

Λ-kalkul byl prvním formalismem, který definoval a charakterizoval rekurzivní funkce : má proto velký význam v teorii vypočítatelnosti , srovnatelně s Turingovými stroji a modelem Herbrand-Gödel . Od té doby se používá jako teoretický programovací jazyk a jako metajazyk pro formální počítačovou demonstraci . Lambda-kalkul může být napsán nebo ne .

Lambda-kalkul souvisí s kombinatorické logice z Haskell Curry a je zobecnit do výpočtů explicitní substituce .

Neformální prezentace

V lambda-kalkulu je vše funkcí

Základní myšlenkou lambda-kalkulu je, že všechno je funkce . Funkce je zejména vyjádřena výrazem, který může obsahovat funkce, které ještě nejsou definovány: tyto jsou poté nahrazeny proměnnými. Existuje základní operace zvaná aplikace :

Je zaznamenáno použití výrazu (který popisuje funkci) na výraz (který popisuje funkci) . $NA$ $B$ $A ~ B$

Jak „vyrábět“ funkce?

Můžeme také vytvořit funkce tak, že řekneme, že pokud E je výraz, vytvoříme funkci, která odpovídá x výrazu E; Tuto novou funkci napíšeme λx.E.

Název proměnné není důležitější než ve výrazu jako ∀x P (x), který je ekvivalentní ∀y P (y) . Jinými slovy, pokud E [y / x] je výraz E, ve kterém byly všechny výskyty x přejmenovány na y , budeme uvažovat, že výrazy λx.E a λy.E [y / x] jsou ekvivalentní.

Použitím nástrojů, které jsme právě získali, získáváme pomocí aplikací a abstrakcí poměrně komplikované funkce, které můžeme chtít zjednodušit nebo vyhodnotit. Zjednodušilo uplatňování forma P (λx.E), vrátí se přetransformovala na alternativní expresní E kde každý výskyt bez z x je nahrazen P . Tato forma zjednodušení se nazývá kontrakce (nebo β- kontrakce, pokud si chceme pamatovat, že použijeme pravidlo β lambda-kalkulu).

Některé funkce

Na tomto základě můžeme vytvořit některé zajímavé funkce, jako je funkce identity , což je funkce, která odpovídá , jinými slovy funkce . Můžeme také sestrojit konstantní funkci rovnou , viz . $Já$ $X$ $X$ $\ lambda x. X$ $X$ $\ lambda y. X$

Odtud můžeme sestavit funkci, která dělá konstantní funkce, za předpokladu, že jí dáme konstantu jako parametr, jinými slovy funkci , to znamená funkci, díky které je funkce neustále stejná . $\ lambda x. (\ lambda y. x)$ $X$ $X$

Můžeme také například sestrojit funkci, která permutuje použití parametrů jiné funkce, přesněji pokud je to výraz, chtěli bychom, aby to fungovalo stejně . Funkce je funkce . Budeme-li aplikovat funkce na dostaneme , že můžeme zjednodušit do . $VS$ $M$ $((C ~ M) ~ x) ~ y$ $(M ~ y) ~ x$ $VS \,$ $\ lambda z. (\ lambda x. (\ lambda y. (z ~ y) ~ x))$ $VS \,$ $M \,$ $(\ lambda z. (\ lambda x. (\ lambda y. (z ~ y) ~ x))) \; M$ $(\ lambda x. (\ lambda y. (M ~ y) ~ x))$

Zatím jsme byli docela neformální. Myšlenkou lambda-kalkulu je poskytnout přesný jazyk k popisu funkcí a jejich zjednodušení.

Syntax

Kalkulus lambda definuje syntaktické entity, které se nazývají lambda-termíny (nebo někdy také lambda výrazy ) a které spadají do tří kategorií :

jsou proměnné : $x$ , $y$ ... jsou lambda výrazy;
aplikace : $UV$ je termín, lambda, jestliže $u$ a $v$ jsou lambda-výrazy;
je abstrakce : $λ x . v$ je lambda-termín, pokud $x$ je proměnná a $v je$ lambda-termín.

Mapa lze vidět tak, že pokud $u$ je funkce, a je-li $v$ je jeho tvrzení, pak $UV$ je výsledkem mapě do $V$ funkce $u$ .

Abstrakce $λ x . v$ lze interpretovat jako formalizaci funkce, která k $x$ spojuje $v$ , kde $v$ obvykle obsahuje výskyty $x$ .

Funkce $f,$ která bere lambda-termín $x$ jako parametr a přidá k němu 2 (tj. V aktuální matematické notaci funkce $f : x \mapsto x +2$ ), bude v lambda-kalkulu označena výrazem $λ x . x +2$ . Aplikace této funkce na číslo 3 je zapsána $( λ x . X +2) 3$ a je „hodnocena“ (nebo normalizována) ve výrazu 3 + 2 .

Původ λ

Alonzo Church znala vztah mezi jeho kalkul a že o Russell a Whitehead je Principia Mathematica . Nyní používají k označení abstrakce notaci , ale církev místo toho použila notaci, která se později stala . Peano také definoval abstrakci ve své matematické formě , používá zejména notaci, aby si všiml funkce jako . ${\ displaystyle {\ hat {x}} f (x)}$ ${\ displaystyle {\ hat {~~}} xf (x)}$ ${\ displaystyle \ lambda xf (x)}$ ${\ displaystyle a {\ bar {x}}}$ $F$ ${\ displaystyle fx = a}$

Zápisy, konvence a koncepty

Parenthesizing

K vymezení aplikací se používají závorky, ale pro přehlednost jsou některé závorky vynechány. Například napíšeme x 1 x 2 ... x n pro (( x 1 x 2 ) ... x n ).

Ve skutečnosti existují dvě konvence:

Asociace vlevo , výraz ((M 0 M 1 ) (M 2 M 3 )) je zapsán M 0 M 1 (M 2 M 3 ) . Když se aplikace vztahuje na jinou aplikaci, umístíme na ni pouze závorku vpravo. Formálně je gramatika závorek lambda kalkulu následující:Λ :: = Var | λ Var. L | Λ L  ; L :: = Var | λ Var. L | (Λ L)
V případě, že je nadřazený člen uveden v závorkách , je výraz ((M 0 M 1 ) (M 2 M 3 )) zapsán (M 0 ) M 1 (M 2 ) M 3 . Termín v závorkách je první v řadě aplikací. Argumenty výrazu jsou tedy snadno identifikovatelné. Formálně je potom gramatika závorek lambda-kalkulu:Λ :: = Var | λ Var. Λ | (Λ) Λ + .

Kari

Shönfinkel a Curry představili currying : jedná se o proces představující funkci s několika argumenty. Například funkce, která s dvojicí ( x , y ) spojuje u, je považována za funkci, která s x spojuje funkci, která s y sdružuje u . Proto se označuje: λx. (Λy.u) . Také je psáno λx.λy.u nebo λxλy.u nebo prostě λxy.u . Například funkce, která s dvojicí ( x , y ) spojuje x + y, bude označena λx.λy.x + y nebo jednodušeji λxy.x + y .

Volné proměnné a spojené proměnné

V matematických výrazech obecně a zejména v lambda kalkulu existují dvě kategorie proměnných: volné proměnné a spojené (nebo hloupé ) proměnné . V lambda-kalkulu je proměnná spojena pomocí λ. Vázaná proměnná má obor a tento obor je místní. Kromě toho můžete přejmenovanou vázanou proměnnou přejmenovat, aniž byste změnili celkový význam celého výrazu, ve kterém se objeví. Proměnná, která není vázána, je považována za volnou.

Související proměnné v matematice

Například ve výrazu je proměnná volná, ale proměnná je propojena (pomocí ). Tento výraz je „stejný“ jako, protože byl místní název, stejně jako je . Na druhou stranu neodpovídá stejnému výrazu, protože je zdarma. ${\ displaystyle \ textstyle \ int _ {a} ^ {b} {(x + y) ~ dy}}$ $X$ $y$ $dy$ ${\ displaystyle \ textstyle \ int _ {a} ^ {b} {(x + z) ~ dz}}$ $y$ $z$ ${\ displaystyle \ textstyle \ int _ {a} ^ {b} {(z + y) ~ dy}}$ $z$

Stejně jako integrál váže proměnnou integrace, tak váže i proměnnou, která ji následuje. $\ lambda$

Příklady :

V proměnná je propojena a proměnná je volná. Tento výraz je ekvivalentem α k tomuto výrazu . $\ lambda x.xy$ $X$ $y$ $\ lambda t.ty$

$\ lambda xyzt.z (xt) ab (zsy)$ je α-ekvivalent k . $\ lambda wjit. i (wt) ab (isj)$

${\ displaystyle \ lambda b. \ lambda nb}$ je α-ekvivalent k . ${\ displaystyle \ lambda p. \ lambda t}$

Formální definice volných proměnných v lambda kalkulu

Definujeme nastavenou VL (t) z volných proměnných z termínovaného t indukcí:

pokud je proměnná, pak VL (x) = {x} $X$
if and v are lambda-terms then VL (uv) = VL (u) ∪ VL (v) $u$
if je proměnná a u je lambda-termín, pak VL (λx.u) = VL (u) \ {x} $X$

Uzavřený termín a otevřený termín

Termín, který neobsahuje žádnou volnou proměnnou, je považován za uzavřený (nebo uzavřený). Tento lambda-termín je také považován za kombinátor (ze souvisejícího konceptu kombinatorické logiky ).

Termín, který není uzavřen, je považován za otevřený.

Substituce a α-přeměna

Nejdůležitějším nástrojem pro lambda-kalkul je substituce, která umožňuje nahradit v termínu proměnnou za termín. Tento mechanismus je základem redukce, která je základním mechanismem hodnocení výrazů, tedy „výpočtu“ termínů lambda.

Substituce v lambda období t variabilní x o termínu u je označena T [x: = u] . Aby bylo možné správně definovat substituci, je třeba učinit určitá opatření, abychom se vyhnuli fenoménu zachycení proměnné, který by mohl, pokud nejsme opatrní, vázat proměnnou, která byla před provedením substituce volná.

Například pokud u obsahuje volnou proměnnou y a pokud se x objeví v t jako výskyt dílčího termínu tvaru λy.v , může se objevit fenomén zachycení. Operace t [x: = u] se nazývá substituci v t o x o u a je definován indukcí podle t :

pokud t je proměnná, pak t [x: = u] = u , pokud x = t a t jinak
if t = vw then t [x: = u] = v [x: = u] w [x: = u]
if t = λy.v then t [x: = u] = λy. (v [x: = u]) pokud x ≠ y a t jinak

Poznámka : v posledním případě budeme věnovat pozornost tomu, že y není volná proměnná u . Ve skutečnosti by to pak „zajalo“ externí lambda. Pokud tomu tak je, přejmenujeme y a všechny jejich výskyty ve v proměnnou z, která se neobjeví v t ani v u .

Konverze α identifikuje λy.v a λz.v [y: = z] . Dva lambda termíny, které se liší pouze přejmenováním (bez zachycení) jejich spojených proměnných, jsou považovány za α-konvertibilní . Α-konverze je ekvivalenční vztah mezi lambda-podmínkami.

Příklady:

(λx.xy) [y: = a] = λx.xa
(λx.xy) [y: = x] = λz.zx (a ne λ x.xx , což je úplně jiné, viz poznámka výše)

Poznámka: α-převod musí být před nahrazením pečlivě definován. V termínu λx.λy.xyλz.z tedy nemůžeme najednou přejmenovat x na y (dostali bychom λy.λy.yyλz.z ), na druhou stranu můžeme přejmenovat x na z .

Definováno tedy, substituce je mechanismus mimo lambda-kalkul, říká se také, že je součástí meta-teorie. Všimněte si, že některé práce mají za cíl zavést substituci jako vnitřní mechanismus lambda-kalkulu, což vede k tomu, co se nazývá explicitní substituční výpočty .

Slevy

Jedním ze způsobů pohledu na pojmy lambda-kalkul je považovat je za stromy s binárními uzly (mapování), unárními uzly (λ-abstrakce) a listy (proměnné). Účelem redukcí je změna termínů nebo stromů, pokud je takto vidíme; například redukce (λx.xx) (λy.y) dává (λy.y) (λy.y) .

Redex nazýváme členem tvaru (λx.u) v , kde u a v jsou členy a x proměnná. Definujeme beta-kontrakci (nebo β-kontrakci) (λx.u) v jako u [x: = v] . Říkáme, že výraz C [u] se redukuje na C [u '], pokud u je redex, který β-kontrakty uzavře na u' , pak napíšeme C [u] → C [u '] , vztah → se nazývá kontrakce .

Příklad kontrakce :

(λx.xy) a dává (xy) [x: = a] = ay .

Označíme → * na tranzitivní reflexivní uzavření kontrakce vztahu → a říkáme, že snížení . Jinými slovy, redukce je konečná, možná prázdná posloupnost kontrakcí.

Definujeme = β jako symetrické a přechodné reflexní uzavření kontrakce a nazývá se to beta-konverze , β- konverze , nebo častěji beta-ekvivalence nebo β- ekvivalence .

B-ekvivalence umožňuje například srovnávat termíny, které nejsou navzájem redukovatelné, ale které po sérii β-kontrakcí dospějí ke stejnému výsledku. Například (λy.y) x = β (λy.x) z, protože dva výrazy se smršťují a dávají x .

Formálně máme M = β M 'právě tehdy, když ∃ N 1 , ..., N p takové, že M = N 1 , M' = N p a pro všechna i menší než p a větší než 0 , N i → N i + 1 nebo N i + 1 → N i .

To znamená, že při konverzi lze použít redukce nebo inverzní vztahy redukcí (tzv. Expanze ).

Definujeme také další operaci nazvanou eta-redukce , která je definována následovně: λx.ux → η u , když x se v u neobjeví jako volné. Ve skutečnosti, UX je interpretován jako obraz x použití funkce u . Proto je λx.ux interpretován jako funkce, která k x spojuje obraz x s u , tedy jako funkce u sama.

Normalizace: pojmy počet a člen v normální formě

Výpočet spojený s termínem lambda je sled redukcí, které generuje. Termín je popis výpočtu a výsledkem je běžná forma termínu (pokud existuje).

O lambda-termu t se říká, že je v normální formě, pokud na něj nelze aplikovat beta kontrakci, tj. Pokud t neobsahuje žádný redex, nebo pokud neexistuje lambda-termín u takový, že t → u . Syntaktická struktura termínů v normální formě je popsána níže.

Příklad:

λx.y (λz.z (yz))

Říkáme, že lambda-termín t je normalizovatelný, pokud existuje termín u, na který nelze aplikovat beta kontrakci a takový, že t = β u . Takové u se nazývá normální formu o t .

Řekneme, že lambda-term t je silně normalizable pokud všechny slevy z t jsou omezené .

Příklady:

Nechť delta ≡ λx.xx být nastavena .

Ukázkový příklad ne-silně normalizovatelného lambda-termu se získá aplikací tohoto termínu na sebe, jinými slovy: Ω = (λx.xx) (λx.xx) = ΔΔ . Lambda člen Ω není silně normalizovatelný, protože jeho redukce na sebe neurčitě navazuje. (λx.xx) (λx.xx) → (λx.xx) (λx.xx) .
(λx.x) ((λy.y) z) je silně normalizovatelný lambda-termín a jeho normální forma je . $z$
(λx.y) (ΔΔ) je normalizovatelný a jeho normální forma je , ale není silně normalizovatelný, protože redukce termínu (λx.y) (ΔΔ) může vést k termínu, ale také k termínu (λx.y ) (ΔΔ) zvažuje Δ ≡ λx.xx . $y$ $y$
(λx.xxx) (λx.xxx) → (λx.xxx) (λx.xxx) (λx.xxx) → (λx.xxx) (λx.xxx) (λx.xxx) (λx.xxx) → .. ... vytváří pojmy větší a větší.

Pokud je výraz silně normalizovatelný, pak je normalizovatelný.

Dvě základní věty

Church-Rosserova věta: nechť t a u jsou dva pojmy takové, že t = β u . Existuje termín v takový, že t → * v a u → * v .

Věta o kosočtverci (nebo soutoku): nechť t , u 1 a u 2 jsou lambda-termíny takové, že t → * u 1 a t → * u 2 . Pak existuje lambda-termín v takový, že u 1 → * v a u 2 → * v .

Díky Church-Rosserově teorému lze snadno ukázat jedinečnost normální formy i konzistenci lambda-kalkulu (tj. Existují alespoň dva odlišné pojmy, které nelze převést na beta verzi).

Struktura pojmů v normální formě

Můžeme popsat strukturu termínů v normální formě, která tvoří množinu . K tomu popíšeme takzvané neutrální pojmy, které tvoří množinu . Neutrální výrazy jsou výrazy, ve kterých se proměnná (například ) aplikuje na výrazy v normální formě. Například je neutrální, pokud ... jsou v normální formě. Termíny v normální formě jsou neutrální termíny, kterým předchází nula, jedno nebo více λ, jinými slovy, následné abstrakce termínů v normální formě. Tak je to v normální formě. Termíny můžeme popsat v normální formě gramatikou. ${\ displaystyle NF}$ ${\ displaystyle NE}$ $X$ ${\ displaystyle xN_ {1} ... N_ {p}}$ $N_ {1}$ ${\ displaystyle N_ {p}}$ ${\ displaystyle \ lambda x. \ lambda y.xN_ {1} ... N_ {p}}$

${\ displaystyle NF :: = NE \ mid \ lambda x.NF}$

${\ displaystyle NE :: = Var \ mid NE \ NF}$

Příklady : je neutrální, tedy také v normální formě. je v normální formě. je neutrální. je v normální formě. Na druhé straně není v normální formě, protože není neutrální a nejedná se o abstrakci termínu v normální formě, ale také proto, že je sám o sobě β-redex, tedy β-redukovatelný. $X$ ${\ displaystyle \ lambda xx}$ ${\ displaystyle xx}$ ${\ displaystyle \ lambda x.xx}$ ${\ displaystyle (\ lambda xx) y}$

Různé výpočty lambda

Na základě syntaxe a redukce lambda-kalkulu můžeme upravit různé výpočty omezením víceméně třídy výrazů. Můžeme tedy rozlišit dvě hlavní třídy výpočtů lambda: netypový výpočet lambda a výpočty typu lambda. Typy jsou anotacemi termínů, jejichž cílem je zachovat pouze termíny, které jsou normalizovatelné, případně přijetím redukční strategie. Doufáme tedy, že budeme mít lambda-kalkul, který splní Church-Rosserovy a normalizační vlastnosti.

Curry-Howard korespondence týká typované lambda k systému přirozené srážky. Uvádí, že typ odpovídá výroku a termín odpovídá důkazu, a naopak.

Netypický lambda-kalkul

Kódování simuluje běžné počítačové objekty včetně přirozených čísel, rekurzivních funkcí a Turingových strojů. Naopak lambda-kalkul může být simulován Turingovým strojem. Díky církevní tezi usuzujeme, že lambda-kalkul je univerzálním modelem kalkulu.

Booleovci

V části Syntaxe jsme viděli, že je praktické definovat primitiva. To je to, co tady budeme dělat.

true = λab.a

false = λab.b

Toto je pouze definice kódování a mohli bychom definovat další.

Všimli jsme si, že: true xy → * x a : false xy → * y

Poté můžeme definovat lambda-termín představující alternativu: if-then-else . Je to funkce se třemi argumenty, booleovským ba dvěma lambda výrazy u a v , která vrací první, pokud je booleovská hodnota pravdivá, a druhý jinak.

ifthenelse = λbuv. (buv) .

Naše funkce je ověřena: ifthenelse true xy = (λbuv. (buv)) true xy  ; ifthenelse true xy → (λuv. (true uv)) xy  ; ifthenelse true xy → * (true xy)  ; ifthenelse true xy → * ((λab.a) xy)  ; ifthenelse true xy → * x .

Uvidíme to stejným způsobem ifthenelse false xy → * y .

Odtamtud máme také lambda-termín pro klasické booleovské operace: no = λb.ifthenelse b false true  ; a = λab.ifthenelse ab false (nebo λab.ifthenelse aba ); kde = λab.ifthenelse a true b (nebo λab.ifthenelse aab ).

Celá čísla

Následující kódování celých čísel se po jejich návrháři nazývá Církevní celá čísla . Ptáme se: 0 = λfx.x , 1 = λfx.fx , 2 = λfx.f (fx) , 3 = λfx.f (f (fx)) a obecně: n = λfx.f (f (... (fx) ...)) = λfx.f n x s f opakována n krát.

Celé číslo n je tedy považováno za funkční, které k dvojici ≺f, x≻ sdružuje f n (x) .

Některé funkce

Existují dva způsoby, jak ke kódování nástupce funkce , a to buď přidáním f v čele nebo na ocasu. Na začátku máme n = λfx.f n x a chceme λfx.f n + 1 x . Je nutné mít možnost přidat f buď na začátek f („pod“ lambdas), nebo na konec.

Pokud se rozhodneme dát to do vedení, musíme být schopni vstoupit „pod“ lambdy. Za to, že pokud n je naše celé číslo, nejprve vytvoříme nfx , což dává f n x . Vložením f do hlavy získáme: f (nfx) → f (f n x) = f n + 1 x . Potom stačí dokončit záhlaví a rekonstruovat církevní celé číslo: λfx.f (nfx) = λfx.f n + 1 x . Nakonec, abychom měli nástupnickou „funkci“, je samozřejmě nutné brát celé číslo jako parametr, takže přidáme lambdu. Dostaneme λnfx.f (nfx) . Čtenář si může ověřit, že (λnfx.f (nfx)) 3 = 4 , s 3 = λfx.f (f (fx))) a 4 = λfx.f (f (f (fx)))) .

Pokud bychom naopak chtěli zařadit f do fronty, stačí použít nfx ne na x , ale na fx , konkrétně nf (fx) , což se redukuje na f n (fx) = f n + 1 x . Musíme jen předělat obal jako v předchozím případě a získáme λnfx.nf (fx) . Lze provést stejné ověření.

Ostatní funkce jsou postaveny na stejném principu. Například přidání „zřetězením“ dvou termínů lambda: λnpfx.nf (pfx) .

K kódování násobení použijeme f k „šíření“ funkce po celou dobu: λnpf.n (pf)

Předchůdce a odčítání nejsou přímočaré jeden. O tom si povíme později.

Test můžeme definovat na 0 následovně: if0thenelse = λnab.n (λx.b) a , nebo pomocí Boolean λn.n (λx.false) true .

Iterátory

Nejprve definujeme iterační funkci na celá čísla: iterates = λnuv.nuv

v je základní případ a u funkce. Pokud je n nula, vypočítáme v , jinak vypočítáme u n (v) .

Například dodatek, který pochází z následujících rovnic

přidat (0, p) = p
add (n + 1, p) = add (n, p + 1)

lze definovat následovně. Základní případ v je číslo p a funkce u je nástupnická funkce . Termín lambda odpovídající výpočtu součtu je tedy: přidat = λnp. iter n nástupce p . Všimněte si, že přidat np → * n nástupce p .

Páry

Můžeme kódovat páry pomocí c = λz.zab, kde a je první prvek ab druhý. Označíme tento pár (a, b) . Pro přístup ke dvěma částem používáme π 1 = λc.c (λab.a) a π 2 = λc.c (λab.b) . Rozpoznáme pravdivé a nepravdivé booleovské hodnoty v těchto výrazech a necháme na čtenáři, aby redukoval π 1 (λz.zab) na a .

Seznamy

Můžeme si všimnout, že celé číslo je seznam, ze kterého se nedíváme na prvky, když vezmeme v úvahu pouze délku. Přidáním informací odpovídajících prvkům můžeme sestavit seznamy analogickým způsobem jako celá čísla: [a 1 ; ...; a n ] = λgy. ga 1 (... (ga n y) ...). Tak : [] = λgy.y; [a 1 ] = λgy.ga 1 rok ; [a 1 ; a 2 ] = λgy.ga 1 (ga 2 y).

Iterátory v seznamech

Stejným způsobem, jakým jsme zavedli iteraci na celá čísla, zavedeme iteraci na seznamy. seznam funkcí je definován v λlxm.lxm jako pro celá čísla. Koncept je téměř stejný, ale existují malé nuance. Uvidíme na příkladu.

příklad: Délka seznamu je definována

délka ([]) = 0
délka (x :: l) = 1 + délka l

x :: l je seznam hlavy x a ocasu l (notace ML ). Funkce délky aplikovaná na seznam l je kódována pomocí: λl.liste_it l (λym.add (λfx.fx) m) (λfx.x) Nebo prostě λl.l (λym. přidat 1 m) 0.

Binární stromy

Princip konstrukce celých čísel, párů a seznamů je zobecněn na binární stromy:

konstruktor listu: sheet = λngy.yn
konstruktor uzlů: node = λbcgy.g (bgy) (cgy) (s b a b binárními stromy)
iterátor: tree_it = λaxm.axm

Strom je buď list, nebo uzel. V tomto modelu nejsou na úrovni uzlu uloženy žádné informace, data (nebo klíče) jsou uchovávána pouze na úrovni listů. Poté můžeme definovat funkci, která počítá počet listů stromu: nb_feuilles = λa.arbre_it a (λbc.add bc) (λn.1), nebo jednodušeji: nb_feuilles = λa.a add (λn.1)

Předchůdce

K definování předchůdce na celých číslech Církve je nutné použít páry. Cílem je rekonstruovat předchůdce iterací: pred = λn.π 1 (iteruje n (λc. (Π 2 c, nástupce (π 2 c))) (0,0)). Vzhledem k tomu, že předchůdce přirozených celých čísel není definován v 0, abychom definovali celkovou funkci, přijali jsme zde konvenci, že je 0.

Zkontrolujeme například, že pred 3 → * π 1 (iter 3 (λc. (Π 2 c, nástupce (π 2 c))) (0,0)) → * π 1 (2,3) → * 2.

Dedukujeme, že odčítání je definovatelné pomocí: sub = λnp. Iteruje p pred n s konvencí, že pokud je p větší než n, pak se sub np rovná 0.

Rekurze

Kombinací předchůdce a iterátoru získáme rekurzor . To se liší od iterátoru skutečností, že funkce předaná jako argument má přístup k předchůdci.

rec = λnfx.π 1 (n (λc. (f (π 2 c) (π 1 c), nástupce (π 2 c))) (x, 0))

Kombinátory pevných bodů

Kombinátor pevných bodů umožňuje konstruovat pro každé F řešení rovnice X = FX . To je užitečné pro programování funkcí, které nejsou vyjádřeny jednoduše iterací, jako je gcd, a je to obzvláště nutné pro programování dílčích funkcí.

Nejjednodušší kombinátor pevných bodů , díky Currymu, je: Y = λf. (Λx.f (xx)) (λx.f (xx)). Turing navrhl další kombinátor pevných bodů: Θ = (λx. Λy. (Y (xxy))) (λx. Λy. (Y (xxy))).

Zkontrolujeme, že cokoli g. Díky kombinátoru pevných bodů můžeme například definovat funkci, která bere funkci jako argument a testuje, zda tato funkce argumentu vrací true alespoň pro jedno celé číslo: teste_annulation = λg.Y (λfn.ou (gn) (f (nástupce) n))) 0. $Y \ g \ = _ \ beta \ g (Y \ g)$

Například pokud definujeme střídavou posloupnost pravdivých a nepravdivých Booleanů : alternates = λn.itère n není false, pak zkontrolujeme, že: teste_annulation alternates → * nebo (alternates 0) (Y (λfn.or (alternates n) ( f nástupce n)) (nástupce 0)) → * nebo (střídá 1) (Y (λfn. nebo (střídá n) (f nástupce n)) (nástupce 1)) → * true.

Můžeme také definovat gcd: pgcd = Y (λfnp.if0thenelse (sub pn) (if0thenelse (sub np) p (fp (sub np))) (fn (sub pn))).

Spojení s rekurzivními dílčími funkcemi

Rekurzor a pevný bod jsou klíčové ingredience, které ukazují, že jakoukoli rekurzivní částečnou funkci lze definovat v kalkulu λ, když jsou celá čísla interpretována církevními celými čísly. Naopak λ-pojmy lze kódovat celými čísly a redukce λ-pojmů je definovatelná jako (částečná) rekurzivní funkce. Λ-kalkul je tedy modelem vypočítatelnosti .

Jednoduše napsaný lambda-kalkul

Pojmy anotujeme výrazy zvanými typy . Děláme to tak, že poskytujeme způsob, jak napsat výraz. Pokud tato metoda uspěje, říkáme, že termín je dobře napsaný . Kromě toho, že to naznačuje, co funkce „dělá“, například transformuje objekty určitého typu na objekty jiného typu, pomáhá zajistit silnou normalizaci , to znamená - tedy pro všechny termíny, všechny Výsledkem redukcí je normální forma (která je pro každý počáteční termín jedinečná). Jinými slovy, všechny výpočty provedené v této souvislosti končí. Tyto jednoduché typy jsou konstruovány jako typy vlastností, funkcí funkce funkce funkce funkce na funkce, atd Ať se to může zdát jakkoli, expresivní síla tohoto počtu je velmi omezená (tedy v ní nelze definovat exponenciál, ani funkci ). $n \ rightarrow 2 ^ n$

Více formálně jsou jednoduché typy konstruovány následovně:

základní typ (pokud máme primitiva, můžeme si také dát několik typů základen, jako jsou celá čísla, booleovské hodnoty, znaky atd., ale to nemá žádný vliv na teorii). $\jota$
pokud a jsou typy, je typ. $\ tau_1$ $\ tau_2$ $\ tau_1 \ rightarrow \ tau_2$

Druhý případ intuitivně představuje typ funkcí, které přebírají prvek typu a vracejí prvek typu . $\ tau_1$ $\ tau_2$

Kontext je sada dvojic formuláře, kde je proměnná a typ. Úsudek psaní je trojice (můžeme tedy říci, že je dobře napsaný v ), které jsou definovány rekurzivně podle: $\ Gama$ $(x, \ tau)$ $X$ $\ tau$ $\ Gamma \ vdash t: \ tau$ $t$ $\ Gama$

ano , tedy . $(x, \ tau) \ v \ Gamma$ $\ Gamma \ vdash x: \ tau$
ano , tedy . $\ Gamma \ cup (x, \ tau_1) \ vdash u: \ tau_2$ $\ Gamma \ vdash \ lambda x \ !: \! \ Tau_1.u \ ,: \, \ tau_1 \ rightarrow \ tau_2$
jestli a pak $\ Gamma \ vdash u: \ tau_1 \ rightarrow \ tau_2$ $\ Gamma \ vdash v: \ tau_1$ $\ Gamma \ vdash uv: \ tau_2$

Pokud jsme do výpočtu lambda přidali konstanty, musíme jim dát typ (via ). $\ Gama$

Výpočty lambda vyššího řádu

Prostě zadaný lambda-kalkul je příliš omezující na to, aby vyjádřil všechny vypočítatelné funkce , které potřebujeme v matematice, a tedy v počítačovém programu. Jedním ze způsobů, jak překonat expresivitu lambda-kalkulu jednoduše zadaného typu, je umožnit proměnné typu a kvantifikovat je, jak je tomu v systému F nebo v počtu konstruktů .

Lambda kalkul a programovací jazyky

Lambda-kalkul tvoří teoretický základ funkčního programování a ovlivnil tak mnoho programovacích jazyků. Prvním z nich je Lisp, což je netypický jazyk. Později budou vyvinuty ML a Haskell , což jsou strojové jazyky.

De Bruijnovy stopy

De Bruijnovy indexy jsou zápisem lambda kalkulu, který umožňuje reprezentovat pomocí termínu každou třídu ekvivalence pro α-konverzi. Za tímto účelem de Bruijn navrhl nahradit každý výskyt proměnné přirozeným celým číslem. Každé přirozené číslo označuje počet λ, které musí být překročeny, aby se vztahoval výskyt k jeho linkeru.

Tedy termín λ x. xx je reprezentován termínem λ 0 0, zatímco termín λx. λy. λz .xz (yz) je reprezentováno λ λ λ 2 0 (1 0) , protože v prvním případě cesta od x k jeho linkeru nepřekročí žádné λ, zatímco ve druhém případě cesta od x na jeho linkeru kříží dvě λ (jmenovitě λy a λz ), cesta od y k jeho linkeru protíná λ (tj. λz ) a cesta od z k jeho linkeru nepřekračuje žádné λ.

Jako další příklad lze uvést termín (λ x λ y λ z λ u. (X (λ x λ y. X))) (λ x. (Λ x. X) x) a termín, který je jeho ekvivalentem α , jmenovitě (λ x λ y λ z λ u. (x (λ v λ w. v))) (λ u. (λ t. t) u) jsou reprezentovány (λ λ λ λ (3 (λ λ 1 ))) (λ (λ 0) 0) (viz obrázek).

Poznámky

AM Turing , „ Vyčíslitelnost a λ-definovatelnost “, The Journal of Symbolic Logic , sv. 2, n O 4,1937, str. 153–163 ( DOI 10.2307 / 2268280 , číst online , přistupováno 10. října 2017 )
který může případně obsahovat proměnnou x .
co by napsali matematici . $x \ mapsto E.$
Zejména jsme oslabili problém nahrazení proměnné výrazem, který představuje choulostivé problémy.
Zdá se, že toto vysvětlení zavádí celé konstanty a operace, jako + a *, ale není tomu tak, protože tyto koncepty lze popsat konkrétními lambda výrazy, z nichž jsou pouze zkratkami.
(in) J. Barkley Rosser , „ Highlights of the History of the Lambda Calculus “ , Annals of the History of Computing , Vol. 6, n O 4,Říjen 1984, str. 338.
G. Peano, Forma matematiky: Matematická logika , t. II, ( číst online ),
strana 58 .
V matematice jsou proměnné příbuzné vztahem ∀ nebo ∃ nebo ∫ ... dx .
Rozsah je část výrazu, kde má proměnná stejný význam.
Pozor, „zmenšení“ neznamená, že se velikost zmenší!
C [] se nazývá kontext .
Mnoho autorů tento vztah zaznamenává ↠.
Jako inverzní eta-expanzi
Termín vyplývající z redukce, z níž již nelze redukovat.
Naděje založená obecně, ale je stále nutné ji demonstrovat!
De Bruijn, Nicolaas Govert, „ Zápis lambda kalkulu s bezejmennými figurínami: nástroj pro automatickou manipulaci s formulemi s aplikací na Church-Rosserovu větu “, Elsevier , sv. 34,1972, str. 381–392 ( ISSN 0019-3577 , číst online )
Benjamin Pierce, Typy a programovací jazyk , MIT Press ,2002( ISBN 0-262-16209-1 , číst online ) , „Kapitola 6: Bezejmenné znázornění pojmů“
Jedná se o přístup zcela srovnatelný s přístupem Bourbaki, který používá „sestavy“ a „odkazy“ .

Bibliografie

(en) Henk Barendregt , The Lambda-Calculus , svazek 103, Elsevier Science Publishing Company, Amsterdam, 1984.
F Cardone a JR Hindley, Příručka dějin logiky ,2006( číst online ) , „Historie lambda-kalkulu a kombinační logiky“
Marcel Crabbé, Le calcul lambda , Cahiers du center de Logique , číslo 6, 1986.
Jean-Louis Krivine , Lambda-Calcul, types et models , Masson 1991, anglický překlad k dispozici na stránkách autora [1] .
(en) Steven Fortune , Daniel Leivant , Michael O'Donnell , „Expresivita jednoduchých struktur typu a řádu druhého řádu“ v Journal of the ACM vol. 30 (1983), str. 151-185.
(en) Jean-Yves Girard , Paul Taylor , Yves Lafont , Proofs and Types , Cambridge University Press, New York, 1989 ( ISBN 0-521-37181-3 ) .
Pierre Lescanne : „ A kdybychom začali s funkcemi! », Obrazy matematiky .
Hervé Poirier , „Pravá podstata inteligence“, Science et Vie n o 1013 (Únor 2002), s. 38-57.
Francis Renaud , Sémantika času a lambda-kalkul, Presses Universitaires de France , 1996 ( ISBN 2-13-047709 7 )

Lambda-kalkul

Neformální prezentace

V lambda-kalkulu je vše funkcí

Jak „vyrábět“ funkce?

Některé funkce

Syntax

Původ λ

Zápisy, konvence a koncepty

Parenthesizing

Kari

Volné proměnné a spojené proměnné

Uzavřený termín a otevřený termín

Substituce a α-přeměna

Slevy

Normalizace: pojmy počet a člen v normální formě

Dvě základní věty

Struktura pojmů v normální formě

Různé výpočty lambda

Netypický lambda-kalkul

Jednoduše napsaný lambda-kalkul

Výpočty lambda vyššího řádu

Lambda kalkul a programovací jazyky

De Bruijnovy stopy

Poznámky

Bibliografie

Dodatky

Související články

externí odkazy