Calcul Lambda

Litera lambda minusculă, unsprezecea din alfabetul grecesc este simbolul calculului lambda.

Calculul Lambda sau λ-calculul este un sistem formal definit de matematicianul Alonzo Church , dezvoltat pentru a analiza formal funcțiile și calculul acestora. Primele sunt exprimate prin intermediul unui limbaj formal , care stabilește regulile pentru formarea unui termen, acesta din urmă cu un sistem de rescriere , care definește modul în care termenii pot fi reduși și simplificați.

Descriere

Combinația de simplitate și expresivitate a făcut din calculul lambda un instrument frecvent în mai multe domenii științifice:

În domeniul matematicii și informaticii , în special în teoria calculabilității, a fost dezvoltat pentru studiul funcțiilor recursive ca fiind efectiv calculabile.
În informatică și în teoria limbajelor de programare este principalul prototip al limbajelor de programare funcționale și recursive .
În teoria dovezilor , calculul lambda tastat este unul dintre cele mai utilizate sisteme formale pentru reprezentarea dovezilor, datorită corespondenței Curry-Howard care leagă dovezile de termeni și tipuri de formule logice.
În modelarea semanticii (ramura lingvisticii ), calculul lambda este formalismul folosit pentru a descrie compoziția sensului în cadrul unei propoziții .

Termeni

Termenul calculului lambda sau, mai pe scurt, termenul lambda sau expresia lambda este definit ca orice șir bine format care începe de la următoarea gramatică , în forma Backus-Naur :

$T\quad ::=\quad V\quad |\quad \lambda V.T\quad |\quad (T\quad T)$ ${\ displaystyle T \ quad :: = \ quad V \ quad | \ quad \ lambda VT \ quad | \ quad (T \ quad T)}$ $T \ quad :: = \ quad V \ quad | \ quad \ lambda V.T \ quad | \ quad (T \ quad T)$

unde metavariabila $V.$ ${\ displaystyle V}$ $V.$ denotă o variabilă aparținând unui set infinit de variabile numărabile .

Parafrazând definiția formală, un termen lambda poate fi, respectiv, un nume de variabilă , abstractizarea unui termen față de o variabilă sau aplicarea unui termen ca argument (sau parametru real) al altuia.

Variabile

Având un termen generic lambda $M.$ ${\ displaystyle M}$ $M.$ , este definit $\mathrm {Var} (M)$ ${\ displaystyle \ mathrm {Var} (M)}$ ${\ mathrm {Var}} (M)$ setul care conține toate variabilele menționate în $M.$ ${\ displaystyle M}$ $M.$ . Dintre acestea distingem două partiții : setul de variabile libere, scrise $\mathrm {Libere} (M)$ ${\ displaystyle \ mathrm {Gratuit} (M)}$ ${\ mathrm {Gratuit}} (M)$ , și setul de variabile legate, indicate cu $\mathrm {Legate} (M)$ ${\ displaystyle \ mathrm {Legate} (M)}$ ${\ mathrm {Legate}} (M)$ . Setul de variabile libere este definit recursiv după cum urmează:

$\mathrm {Libere} (x)=\{x\}$ ${\ displaystyle \ mathrm {Free} (x) = \ {x \}}$ ${\ mathrm {Free}} (x) = \ {x \}$ ;
$\mathrm {Libere} (\lambda x.M)=\mathrm {Libere} (M)\setminus \{x\}$ ${\ displaystyle \ mathrm {Free} (\ lambda xM) = \ mathrm {Free} (M) \ setminus \ {x \}}$ ${\ mathrm {Free}} (\ lambda x.M) = {\ mathrm {Free}} (M) \ setminus \ {x \}$ ;
$\mathrm {Libere} (MN)=\mathrm {Libere} (M)\cup \mathrm {Libere} (N)$ ${\ displaystyle \ mathrm {Free} (MN) = \ mathrm {Free} (M) \ cup \ mathrm {Free} (N)}$ ${\ mathrm {Free}} (MN) = {\ mathrm {Free}} (M) \ cup {\ mathrm {Free}} (N)$ .

Prin urmare, setul de variabile legate poate fi obținut prin diferență:

\mathrm {Legate} (M)=Var(M)\setminus \mathrm {Libere} (M)

{\ displaystyle \ mathrm {Legate} (M) = Var (M) \ setminus \ mathrm {Free} (M)}

{\ mathrm {Legate}} (M) = Var (M) \ setminus {\ mathrm {Free}} (M)

.

Punctul 2 al definiției implică faptul că construcția sintactică a abstractizării este un liant variabil: dacă $x\in {\textrm {Libere}}(M)$ ${\ displaystyle x \ in {\ textrm {Free}} (M)}$ $x \ in {\ textrm {Free}} (M)$ , asa de $x\in {\textrm {Legate}}(\lambda x.M)$ ${\ displaystyle x \ in {\ textrm {Legate}} (\ lambda xM)}$ $x \ in {\ textrm {Legate}} (\ lambda x.M)$ .

Un nume de variabilă se spune că este proaspăt , relativ la un termen, dacă nu este inclus în numele variabilelor din același termen.

Câteva exemple care se obțin pur și simplu prin aplicarea definițiilor date mai sus:

{\textrm {Var}}(\lambda z.\lambda x.(xy))=\{z,x,y\}

{\ displaystyle {\ textrm {Var}} (\ lambda z. \ lambda x. (xy)) = \ {z, x, y \}}

{\ textrm {Var}} (\ lambda z. \ lambda x. (xy)) = \ {z, x, y \}

;

{\textrm {Libere}}(\lambda z.\lambda x.(xy))=\{y\}

{\ displaystyle {\ textrm {Free}} (\ lambda z. \ lambda x. (xy)) = \ {y \}}

{\ textrm {Gratuit}} (\ lambda z. \ lambda x. (xy)) = \ {y \}

;

{\textrm {Legate}}(\lambda z.\lambda x.(xy))=\{x,z\}

{\ displaystyle {\ textrm {Legate}} (\ lambda z. \ lambda x. (xy)) = \ {x, z \}}

{\ textrm {Legate}} (\ lambda z. \ lambda x. (xy)) = \ {x, z \}

;

Rescrie reguli

Înlocuire

O substituție este înlocuirea tuturor aparițiilor unui sub-termen cu altul, într-un al treilea termen care reprezintă contextul substituției în sine. Este indicat cu $M[N/v]$ ${\ displaystyle M [N / v]}$ $M [N / v]$ înlocuirea termenului $Nu.$ ${\ displaystyle N}$ $Nu.$ in loc de $v$ ${\ displaystyle v}$ $v$ în termen $M.$ ${\ displaystyle M}$ $M.$ : orice apariție liberă a variabilei $v$ ${\ displaystyle v}$ $v$ în $M.$ ${\ displaystyle M}$ $M.$ este înlocuit cu $Nu.$ ${\ displaystyle N}$ $Nu.$ . Un exemplu simplu de înlocuire este după cum urmează:

(zx)[\lambda x.x/z]\equiv ((\lambda x.x)x)

{\ displaystyle (zx) [\ lambda xx / z] \ equiv ((\ lambda xx) x)}

(zx) [\ lambda x.x / z] \ equiv ((\ lambda x.x) x)

.

O definiție recursivă a algoritmului de înlocuire este următoarea:

$x[N/x]\equiv N$ ${\ displaystyle x [N / x] \ equiv N}$ $x [N / x] \ echiv N$ ;
$y[N/x]\equiv y$ ${\ displaystyle y [N / x] \ equiv y}$ $y [N / x] \ echiv y$ , de sine $x\neq y$ ${\ displaystyle x \ neq y}$ $x \ neq y$ ;
$(\lambda y.M)[N/y]\equiv \lambda y.M$ ${\ displaystyle (\ lambda yM) [N / y] \ equiv \ lambda yM}$ $(\ lambda y.M) [N / y] \ equiv \ lambda y.M$ ;
$(\lambda y.M)[N/x]\equiv \lambda y.(M[N/x])$ ${\ displaystyle (\ lambda yM) [N / x] \ equiv \ lambda y. (M [N / x])}$ $(\ lambda y.M) [N / x] \ equiv \ lambda y. (M [N / x])$ , de sine $y\neq x$ ${\ displaystyle y \ neq x}$ $y \ neq x$ Și $y\notin FV(N)$ ${\ displaystyle y \ notin FV (N)}$ $y \ notin FV (N)$ ;
$(\lambda y.M)[N/x]\equiv \lambda z.(M[z/y][N/x])$ ${\ displaystyle (\ lambda yM) [N / x] \ equiv \ lambda z. (M [z / y] [N / x])}$ $(\ lambda y.M) [N / x] \ equiv \ lambda z. (M [z / y] [N / x])$ , de sine $y\neq x$ ${\ displaystyle y \ neq x}$ $y \ neq x$ , $y\in FV(N)$ ${\ displaystyle y \ în FV (N)}$ $y \ în FV (N)$ , Și $z$ ${\ displaystyle z}$ $z$ este un nume mișto;
$(M_{1}M_{2})[N/x]\equiv (M_{1}[N/x])(M_{2}[N/x])$ ${\ displaystyle (M_ {1} M_ {2}) [N / x] \ equiv (M_ {1} [N / x]) (M_ {2} [N / x])}$ $(M_ {1} M_ {2}) [N / x] \ equiv (M_ {1} [N / x]) (M_ {2} [N / x])$ .

Câteva exemple de substituție:

(zx)[(\lambda x.x)/z]\equiv ((\lambda x.x)x)

{\ displaystyle (zx) [(\ lambda xx) / z] \ equiv ((\ lambda xx) x)}

(zx) [(\ lambda x.x) / z] \ equiv ((\ lambda x.x) x)

;

(\lambda z.(zx))[(\lambda x.x)/z]\equiv (\lambda z.(zx))

{\ displaystyle (\ lambda z. (zx)) [(\ lambda xx) / z] \ equiv (\ lambda z. (zx))}

(\ lambda z. (zx)) [(\ lambda x.x) / z] \ equiv (\ lambda z. (zx))

;

(\lambda z.(zx))[(zx)/x]\equiv \lambda w.((zx)[w/z][(zx)/x])\equiv \lambda w.((wx)[(zx)/x])\equiv \lambda w.w(zx)

{\ displaystyle (\ lambda z. (zx)) [(zx) / x] \ equiv \ lambda w. ((zx) [w / z] [(zx) / x]) \ equiv \ lambda w. (( wx) [(zx) / x]) \ equiv \ lambda ww (zx)}

(\ lambda z. (zx)) [(zx) / x] \ equiv \ lambda w. ((zx) [w / z] [(zx) / x]) \ equiv \ lambda w. ((wx) [ (zx) / x]) \ equiv \ lambda ww (zx)

, unde este

w

{\ displaystyle w}

w

este un nume mișto.

Verificările de apariție din punctele 4 și 5 sunt necesare pentru a evita un fenomen nedorit numit captură variabilă . Fără aceste controale, operațiunea de substituție ar duce la o variabilă liberă a unui termen ca legătură ca urmare a substituției în sine, ceea ce este, de asemenea, intuitiv incorect.

Conversia alfa

$\lambda x.M\rightarrow _{\alpha }\lambda y.(M[y/x])$ ${\ displaystyle \ lambda xM \ rightarrow _ {\ alpha} \ lambda y. (M [y / x])}$ $\ lambda x.M \ rightarrow _ {{\ alpha}} \ lambda y. (M [y / x])$ .

Conversia alfa se aplică termenilor care sunt abstracții. Având în vedere o abstracție, este posibilă rescrierea acesteia prin înlocuirea variabilei abstracte ( $X$ ${\ displaystyle x}$ $X$ ) cu altul ( $y$ ${\ displaystyle y}$ $y$ ), cu condiția ca, în întregul sub-termen, în loc de fiecare apariție a primului, să scrie al doilea.

Regula de conversie alfa nu se preocupă de a face nicio distincție între aparițiile libere sau legate de variabile, deoarece operațiunea de substituire face deja acest lucru. Câteva exemple de conversie alfa:

\lambda x.(xy)\rightarrow _{\alpha }\lambda z.(zy)

{\ displaystyle \ lambda x. (xy) \ rightarrow _ {\ alpha} \ lambda z. (zy)}

\ lambda x. (xy) \ rightarrow _ {{\ alpha}} \ lambda z. (zy)

\lambda x.(x(\lambda z.(zw)))\rightarrow _{\alpha }\lambda z.(z(\lambda z.(zw)))

{\ displaystyle \ lambda x. (x (\ lambda z. (zw))) \ rightarrow _ {\ alpha} \ lambda z. (z (\ lambda z. (zw)))}

\ lambda x. (x (\ lambda z. (zw))) \ rightarrow _ {{\ alpha}} \ lambda z. (z (\ lambda z. (zw)))

Reducerea beta

Reducerea beta este cea mai importantă regulă de rescriere a calculului lambda, deoarece implementează etapa de calcul. Prescripția sa este definită după cum urmează, în cazul în care orice context actual este omis:

(\lambda x.M)N\rightarrow _{\beta }M[N/x]

{\ displaystyle (\ lambda xM) N \ rightarrow _ {\ beta} M [N / x]}

(\ lambda x.M) N \ rightarrow _ {{\ beta}} M [N / x]

.

(Înlocuiți N, pentru aparițiile variabilelor legate, în M)

Regula are ca obiect aplicarea unei abstracții lambda în formă $\lambda x.M$ ${\ displaystyle \ lambda xM}$ $\ lambda x.M$ la un al doilea termen $Nu.$ ${\ displaystyle N}$ $Nu.$ . Configurația sintactică reductibilă se numește tocmai redex , o contracție a englezei "red-ucible ex -pression", la rândul său rar trasată în italiană ca "redesso", rezultatul său fiind numit redus.

Continuând analogia cu limbajele de programare, regula se referă la o funcție aplicată unui argument. Prin urmare, corespunde unei etape de calcul, care returnează corpul funcției $M.$ ${\ displaystyle M}$ $M.$ unde parametrul curent (efectiv) $Nu.$ ${\ displaystyle N}$ $Nu.$ este substituit parametrului formal $X$ ${\ displaystyle x}$ $X$ a funcției. În acest context, prin urmare, substituția reprezintă tocmai trecerea parametrului .

Câteva exemple de reducere beta sunt:

(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda y.y)(\lambda y.y)\rightarrow _{\beta }\lambda y.y

{\ displaystyle (\ lambda x. (xx)) (\ lambda yy) \ rightarrow _ {\ beta} (\ lambda yy) (\ lambda yy) \ rightarrow _ {\ beta} \ lambda yy}

(\ lambda x. (xx)) (\ lambda y.y) \ rightarrow _ {{\ beta}} (\ lambda y.y) (\ lambda y.y) \ rightarrow _ {{\ beta}} \ lambda y.y

(\lambda x.\lambda y.(xy))(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }\dots \rightarrow _{\beta }\lambda y.y

{\ displaystyle (\ lambda x. \ lambda y. (xy)) (\ lambda x. (xx)) (\ lambda yy) \ rightarrow _ {\ beta} (\ lambda x. (xx)) (\ lambda yy ) \ rightarrow _ {\ beta} \ dots \ rightarrow _ {\ beta} \ lambda yy}

(\ lambda x. \ lambda y. (xy)) (\ lambda x. (xx)) (\ lambda yy) \ rightarrow _ {{\ beta}} (\ lambda x. (xx)) (\ lambda yy) \ rightarrow _ {{\ beta}} \ dots \ rightarrow _ {{\ beta}} \ lambda yy

Conversia vârstei

$\lambda x.(Mx)\rightarrow _{\eta }M$ ${\ displaystyle \ lambda x. (Mx) \ rightarrow _ {\ eta} M}$ $\ lambda x. (Mx) \ rightarrow _ {{\ eta}} M$ , de sine $x\notin FV(M)$ ${\ displaystyle x \ notin FV (M)}$ $x \ notin FV (M)$ .

Intuitiv, importanța acestei reguli constă în faptul că permite declararea a doi termeni lambda identici pe baza principiului că, dacă aceștia se comportă în același mod (odată aplicat unui parametru), trebuie, prin urmare, să fie considerați, exact, identici .

Spune asta $\lambda x.(Mx)$ ${\ displaystyle \ lambda x. (Mx)}$ $\ lambda x. (Mx)$ Și $M.$ ${\ displaystyle M}$ $M.$ se comportă la fel, este să spunem că pentru fiecare $Nu.$ ${\ displaystyle N}$ $Nu.$ : $(\lambda x.(Mx))N\rightarrow _{\beta }(Mx)[N/x]\equiv (MN)$ ${\ displaystyle (\ lambda x. (Mx)) N \ rightarrow _ {\ beta} (Mx) [N / x] \ equiv (MN)}$ $(\ lambda x. (Mx)) N \ rightarrow _ {{\ beta}} (Mx) [N / x] \ equiv (MN)$ . Cu alte cuvinte, conversia eta axiomatizează probabilitatea egalității în $\lambda$ ${\ displaystyle \ lambda}$ $\ lambda$ - calcul extensional ^[1] .

Termeni echivalenți

Regulile de conversie pot fi extinse la relații de echivalență reale, presupunând că poate fi rescrisă în sensul săgeților tocmai definite (de la stânga la dreapta) și că rescrierile în direcția opusă sunt, de asemenea, valabile (de la dreapta la stânga, prin urmare) . În mod formal, se aplică următoarele relații:

$\lambda x.M\Leftrightarrow _{\alpha }\lambda y.(M[y/x])$ ${\ displaystyle \ lambda xM \ Leftrightarrow _ {\ alpha} \ lambda y. (M [y / x])}$ $\ lambda x.M \ Leftrightarrow _ {{\ alpha}} \ lambda y. (M [y / x])$ ,
$\lambda x.(Mx)\Leftrightarrow _{\eta }M$ ${\ displaystyle \ lambda x. (Mx) \ Leftrightarrow _ {\ eta} M}$ $\ lambda x. (Mx) \ Leftrightarrow _ {{\ eta}} M$ , de sine $x\notin FV(M)$ ${\ displaystyle x \ notin FV (M)}$ $x \ notin FV (M)$ .

Cele două implicații duble se numesc echivalența alfa și, respectiv, echivalența eta. Se spune că doi termeni t și s sunt echivalenți alfa-eta atunci când relația este satisfăcută:

$t\Leftrightarrow _{x_{1}}t_{1}\Leftrightarrow _{x_{2}}t_{2}\Leftrightarrow _{x_{3}}\dots \Leftrightarrow _{x_{n}}t_{n}\Leftrightarrow _{x_{n+1}}s\qquad \forall i.x_{i}\in \{\alpha ,\eta \}$ ${\ displaystyle t \ Leftrightarrow _ {x_ {1}} t_ {1} \ Leftrightarrow _ {x_ {2}} t_ {2} \ Leftrightarrow _ {x_ {3}} \ dots \ Leftrightarrow _ {x_ {n}} t_ {n} \ Leftrightarrow _ {x_ {n + 1}} s \ qquad \ forall i.x_ {i} \ in \ {\ alpha, \ eta \}}$ ${\ displaystyle t \ Leftrightarrow _ {x_ {1}} t_ {1} \ Leftrightarrow _ {x_ {2}} t_ {2} \ Leftrightarrow _ {x_ {3}} \ dots \ Leftrightarrow _ {x_ {n}} t_ {n} \ Leftrightarrow _ {x_ {n + 1}} s \ qquad \ forall i.x_ {i} \ in \ {\ alpha, \ eta \}}$ .

Cu alte cuvinte, doi termeni sunt alfa-eta-echivalenți dacă există un lanț finit de rescrieri care utilizează doar regulile alfa-echivalență și echivalență vârstă.

Codificări

Prin calculul λ au fost formulate diferite codificări. Câteva exemple sunt codificarea Bisericii și codificarea Mogensen-Scott . Există, de asemenea, codificări care utilizează calculul lambda tastat, cum ar fi sistemul F.

Numerotare

Numerotarea bisericii poate exprima ansamblul numerelor naturale $\mathbb {N}$ ${\ displaystyle \ mathbb {N}}$ $\ mathbb {N}$ prin axiomele lui Peano . Fiecare număr este exprimat ca următorul celui precedent, în timp ce zero este singurul care nu este următorul din orice număr.

$n:=\lambda sz.s_{0}\circ s_{1}\circ \cdots \circ s_{n}(z)$ ${\ displaystyle n: = \ lambda sz.s_ {0} \ circ s_ {1} \ circ \ cdots \ circ s_ {n} (z)}$ $n: = \ lambda s z. s_0 \ circ s_1 \ circ \ cdots \ circ s_n (z)$

Toate numerele aparținând setului de naturale pot fi exprimate în mod analog.

$\mathbb {N} \ni {\begin{cases}0:=\lambda sz.z\\1:=\lambda sz.s(z)\\2:=\lambda sz.s(s(z))\\3:=\lambda sz.s(s(s(z)))\\4:=\lambda sz.s(s(s(s(z))))\\\cdots \end{cases}}$ ${\ displaystyle \ mathbb {N} \ ni {\ begin {cases} 0: = \ lambda sz.z \\ 1: = \ lambda sz.s (z) \\ 2: = \ lambda sz.s (s ( z)) \\ 3: = \ lambda sz.s (s (s (z))) \\ 4: = \ lambda sz.s (s (s (s (z)))) \\\ cdots \ end {cazuri}}}$ $\ mathbb {N} \ ni \ begin {cases} 0: = \ lambda sz.z \\ 1: = \ lambda sz.s (z) \\ 2: = \ lambda sz.s (s (z)) \ \ 3: = \ lambda sz.s (s (s (z))) \\ 4: = \ lambda sz.s (s (s (s (z)))) \\ \ cdots \ end {cases}$

Operatii aritmetice

În ceea ce privește numerotarea anterioară a numerelor naturale, este posibil să se exprime unele calcule enumerate mai jos.

Funcţie	Definiție aritmetică	Definiția according to Church
Succesor	$n+1$ ${\ displaystyle n + 1}$ $n + 1$	$\lambda wxy.x(wxy)$ ${\ displaystyle \ lambda wxy.x (wxy)}$ $\ lambda wxy. x (wxy)$
Plus	$x+y$ ${\ displaystyle x + y}$ $x + y$	$\lambda xyfg.xf(yfg)\equiv \lambda xy.x\;SUC\;y$ ${\ displaystyle \ lambda xyfg.xf (yfg) \ equiv \ lambda xy.x \; SUC \; y}$ $\ lambda xyfg.xf (yfg) \ equiv \ lambda xy. X \; SUC \; y$
Multiplicare	$xy$ ${\ displaystyle x y}$ $X y$	$\lambda xyf.x(yf)$ ${\ displaystyle \ lambda xyf.x (yf)}$ $\ lambda xyf. x (yf)$
Putere	$x^{y}$ ${\ displaystyle x ^ {y}}$ $x ^ y$	$\lambda xy.y(x)$ ${\ displaystyle \ lambda xy.y (x)}$ $\ lambda xy. y (x)$

Exemple

$SUC\;0=\lambda wxy.x(wxy)(\lambda sz.z)=\lambda xy.x((\lambda sz.z)xy)=\lambda xy.x((\lambda z.z)y)=\lambda xy.x(y)=1$ ${\ displaystyle SUC \; 0 = \ lambda wxy.x (wxy) (\ lambda sz.z) = \ lambda xy.x ((\ lambda sz.z) xy) = \ lambda xy.x ((\ lambda zz ) y) = \ lambda xy.x (y) = 1}$ $SUC \; 0 = \ lambda wxy. x (wxy) (\ lambda sz.z) = \ lambda xy. x ((\ lambda sz.z) xy) = \ lambda xy. x ((\ lambda z.z) y) = \ lambda xy. x (y) = 1$

$1\;ADD\;2=\lambda fg.(\lambda sz.s(z))f((\lambda sz.s(s(z)))fg)=\lambda fg.(\lambda z.f(z))(f(f(g))=\lambda fg.f(f(f(g)))=3$ ${\ displaystyle 1 \; ADD \; 2 = \ lambda fg. (\ lambda sz.s (z)) f ((\ lambda sz.s (s (z))) fg) = \ lambda fg. (\ lambda zf (z)) (f (f (g)) = \ lambda fg.f (f (f (g))) = 3}$ $1 \; ADĂUGA \; 2 = \ lambda fg. (\ lambda sz. s (z)) f ((\ lambda sz. s (s (z))) fg) = \ lambda fg. (\ lambda z. f (z)) (f (f (g)) = \ lambda fg. f (f (f (g))) = 3$

$1\;MUL\;3=(\lambda sz.s(z))(\lambda xyf.x(yf))(\lambda sz.s(s(s(z))))=\lambda f.(\lambda sz.s(z))((\lambda z.f(f(f(z)))))=\lambda f.\lambda z.f(f(f(z)))=3$ ${\ displaystyle 1 \; MUL \; 3 = (\ lambda sz.s (z)) (\ lambda xyf.x (yf)) (\ lambda sz.s (s (s (z)))) = \ lambda f. (\ lambda sz.s (z)) ((\ lambda zf (f (f (z))))) = \ lambda f. \ lambda zf (f (f (z))) = 3}$ ${\ displaystyle 1 \; MUL \; 3 = (\ lambda sz.s (z)) (\ lambda xyf.x (yf)) (\ lambda sz.s (s (s (z)))) = \ lambda f. (\ lambda sz.s (z)) ((\ lambda zf (f (f (z))))) = \ lambda f. \ lambda zf (f (f (z))) = 3}$

Logică booleană

Logica booleană sau algebra booleană este o formalizare a logicii bazată pe două valori, și anume adevărat și fals, care pot fi exprimate după cum urmează.

$V:=\lambda vf.v=\lambda v.\lambda f.v$ ${\ displaystyle V: = \ lambda vf.v = \ lambda v. \ lambda fv}$ $V: = \ lambda vf.v = \ lambda v. \ Lambda f.v$

$F:=\lambda vf.f=\lambda v.\lambda f.f$ ${\ displaystyle F: = \ lambda vf.f = \ lambda v. \ lambda ff}$ $F: = \ lambda vf. F = \ lambda v. \ lambda f.f$

Rețineți că $F.$ ${\ displaystyle F}$ $F.$ reprezintă atât valori zero, cât și valori false.

Operații logice

Mai jos, vor fi exprimate câteva dintre operațiile mai simple legate de logica booleană.

Funcția logică	Simbol	Definiție
E (ȘI)	$\land$ ${\ displaystyle \ land}$ $\ teren$	$\lambda p.\lambda p'.p\,p'p$ ${\ displaystyle \ lambda p. \ lambda p'.p \, p'p}$ $\ lambda p. \ lambda p '. p \, p'p$
O (SAU)	$\lor$ ${\ displaystyle \ lor}$ $\ lor$	$\lambda p.\lambda p'.p\,p\,p'$ ${\ displaystyle \ lambda p. \ lambda p'.p \, p \, p '}$ $\ lambda p. \ lambda p '. p \, p \, p '$
NU NU)	$\neg$ ${\ displaystyle \ neg}$ $\ neg$	$\lambda p.p\,F\,V$ ${\ displaystyle \ lambda pp \, F \, V}$ $\ lambda p. p \, F \, V$

Exemple

$V\;AND\;F=(\lambda vf.v)(\lambda pp'.p\,p'p)(\lambda vf.f)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=\lambda f.\lambda f.f=\lambda vf.f=Falso$ ${\ displaystyle V \; AND \; F = (\ lambda vf.v) (\ lambda pp'.p \, p'p) (\ lambda vf.f) = (\ lambda vf.v) (\ lambda vf .f) (\ lambda vf.v) = \ lambda f. \ lambda ff = \ lambda vf.f = False}$ $V \; ȘI \; F = (\ lambda vf.v) (\ lambda pp'.p \, p'p) (\ lambda vf.f) = (\ lambda vf.v) (\ lambda vf.f) (\ lambda vf.v ) = \ lambda f. \ lambda f. f = \ lambda vf. f = Fals$

$V\;OR\;V=(\lambda vf.v)(\lambda pp'.p\,p\,p')(\lambda vf.v)=(\lambda vf.v)(\lambda vf.v)(\lambda vf.v)=\lambda vf.v=Vero$ ${\ displaystyle V \; OR \; V = (\ lambda vf.v) (\ lambda pp'.p \, p \, p ') (\ lambda vf.v) = (\ lambda vf.v) (\ lambda vf.v) (\ lambda vf.v) = \ lambda vf.v = Adevărat}$ $V \; SAU \; V = (\ lambda vf.v) (\ lambda pp'.p \, p \, p ') (\ lambda vf.v) = (\ lambda vf.v) (\ lambda vf. V) (\ lambda vf .v) = \ lambda vf.v = Adevărat$

$NOT\;V=(\lambda p.p(\lambda vf.f)(\lambda vf.v))(\lambda vf.v)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=(\lambda f.\lambda vf.f)(\lambda vf.v)=\lambda vf.f=Falso$ ${\ displaystyle NOT \; V = (\ lambda pp (\ lambda vf.f) (\ lambda vf.v)) (\ lambda vf.v) = (\ lambda vf.v) (\ lambda vf.f) ( \ lambda vf.v) = (\ lambda f. \ lambda vf.f) (\ lambda vf.v) = \ lambda vf.f = False}$ $NU \; V = (\ lambda pp (\ lambda vf.f) (\ lambda vf.v)) (\ lambda vf.v) = (\ lambda vf.v) (\ lambda vf.f) (\ lambda vf.v) = (\ lambda f. \ lambda vf.f) (\ lambda vf.v) = \ lambda vf.f = False$

Forme normale

Un termen al calculului lambda se găsește în formă normală dacă nu este regrababil prin intermediul regulii de reducere beta. Dacă reducerea beta reprezintă un pas de calcul al unui termen lambda care descrie un program, atunci închiderea sa tranzitivă reprezintă orice calcul al acestuia. Când o reducere este finită și maximă , termenul redus în formă normală reprezintă rezultatul final al calculului.

De exemplu, să presupunem că îmbogățiți calculul adăugând numere naturale (pur și simplu notate ca $1,2,\ldots$ ${\ displaystyle 1,2, \ ldots}$ $1,2, \ ldots$ ) și operația de adăugare binară pe ele (scrise în formă prefixată ca $(+xy)$ ${\ displaystyle (+ xy)}$ $(+ xy)$ ), ambele putând fi codate direct ca termeni lambda. Acum ia în considerare un termen care se adaugă $2$ ${\ displaystyle 2}$ $2$ la argumentul său, și anume $(\lambda x.((+\ 2\ x))$ ${\ displaystyle (\ lambda x. ((+ \ 2 \ x))}$ $(\ lambda x. ((+ \ 2 \ x))$ și folosiți valoarea ca argument $5$ ${\ displaystyle 5}$ $5$ . Această aplicație converge la o formă normală $7$ ${\ displaystyle 7}$ $7$ , intr-adevar: $(\lambda x.((+\ 2\ x))5)\rightarrow _{\beta }(+\ 2\ 5)\rightarrow _{\beta }7\not \rightarrow _{\beta }$ ${\ displaystyle (\ lambda x. ((+ \ 2 \ x)) 5) \ rightarrow _ {\ beta} (+ \ 2 \ 5) \ rightarrow _ {\ beta} 7 \ not \ rightarrow _ {\ beta}}$ $(\ lambda x. ((+ \ 2 \ x)) 5) \ rightarrow _ {{\ beta}} (+ \ 2 \ 5) \ rightarrow _ {{\ beta}} 7 \ not \ rightarrow _ { {\ beta}}$ .

Nu toți termenii lambda au formă normală, iar reducerea beta nu are întotdeauna o lungime finită. Acest fenomen reprezintă faptul că calculul unui program poate continua la nesfârșit și diferă și permite să reprezinte funcții parțiale .

Exemplul clasic de divergență poate fi construit pornind de la termenul de duplicator $\delta =_{def}\lambda x.(xx)$ ${\ displaystyle \ delta = _ {def} \ lambda x. (xx)}$ $\ delta = _ {{def}} \ lambda x. (xx)$ , care nu face altceva decât să ia un termen limită și să returneze două exemplare, unul aplicat celuilalt. Prin urmare, este posibil să se definească termenul $\omega =_{def}(\delta \delta )$ ${\ displaystyle \ omega = _ {def} (\ delta \ delta)}$ $\ omega = _ {{def}} (\ delta \ delta)$ , și observați că se reduce la sine $\omega \rightarrow _{\beta }\omega \rightarrow _{\beta }\dots$ ${\ displaystyle \ omega \ rightarrow _ {\ beta} \ omega \ rightarrow _ {\ beta} \ dots}$ $\ omega \ rightarrow _ {{\ beta}} \ omega \ rightarrow _ {{\ beta}} \ dots$ .

Notă

^ Barendregt, Calculul Lambda

Bibliografie

( EN ) Henk P. Barendregt , The Lambda Calculus, its Syntax and Semantics - Studies in Logic Volume 40, College Publication, Londra, 2012. ISBN 978-1-84890-066-0 . Această carte este o sursă enciclopedică privind calculul lambda netipat. Conține o mulțime de definiții și demonstrații, dar foarte puține explicații cu privire la semnificația și interpretarea rezultatelor prezentate.
Maurizio Gabbrielli și Simone Martini, Limbaje de programare: principii și paradigme , ediția a II-a, Milano, McGraw-Hill , 2011. ISBN 978-88-386-6573-8 .
( EN ) Jean-Yves Girard, Dovezi și tipuri , Paul Taylor și Yves Lafont, Cambridge University Press, 2003 [1989] , ISBN 0-521-37181-3 . Adus 24/03/2014 . Carte pe calcul lambda tastat și ordinul doi.

Elemente conexe

linkuri externe

(EN) Calcul Lambda , al Enciclopediei Britannice , Encyclopædia Britannica, Inc.

Controlul autorității	LCCN (EN) sh85074174 · GND (DE) 4166495-4 · BNF (FR) cb119586908 (data)

Portalul de filosofie

Portal IT

Portalul de matematică

[1] Barendregt, Calculul Lambda

[1]