Lambda-kalkulo

En matematika logiko kaj komputoscienco, Lambda-kalkulo, ankaŭ skribata kiel λ-kalkulo, estas formalisma sistemo por esplori difinon de funkcio, ĝian aplikon kaj rikuron. Ĝin enkondukis Alonzo Church kaj Stephen Cole Kleene en 1930-aj jaroj dum esploro de bazoj de matematiko, sed oni trovis ke ĝi estas utila ilo por solvo de problemoj de teorio de rikuro kaj eĉ povas esti bazo de nova paradigmo de komputila programado, la funkcia programado.

Oni povas rigardi lambda-kalkulon kiel idealisma, minimumisma programa lingvo. Per ĝi oni povas esprimi iun ajn algoritmon, kaj ĝuste tiu fakto faras modelon de funkcia programado tiel grava. Funkciaj programoj estas senstataj kaj zorgas nur pri funkcioj, kiuj akceptas kaj redonas datumojn (inkluzive aliaj funkcioj), sed ne produktas iujn ajn kromefikojn en iu 'stato', kaj sekve ne ŝanĝas enirantan datumon. Modernaj funkciaj programlingvoj, kiuj realigas, plene aŭ parte, lambda-kalkulon estas Erlang, Haskell, Lisp, ML kaj Scheme, samkiel kelkaj pli novaj Agda, Clojure, Coq, F#, Idris, Nemerle kaj Scala.

Ĝis nun lambda-kalkulo ludas gravan rolon en bazoj de matematiko tra korespondo de Curry-Howard. Tamen, kiel naiva bazo de matematiko, netipigita lambda-kalkulo ne povas eviti aroteoriajn paradoksojn (vidu, ekzemple, paradokson de Kleene-Rosser).

La originala lambda-kalkulo, enkondukita fare de Church, estas "netipigita lambda-kalkulo". Pli modernaj aplikoj koncernas tipigitan lambda-kalkulon.

Neformala priskribo

En lambda-kalkulo ĉiu esprimo estas unuopa funkcio, t.e. funkcio kun nur unu enigo (argumento). Kiam la esprimo estas aplikita al alia esprimo ('vokita' kun alia esprimo kiel argumento), ĝi redonas unuopan valoron, kiu estas, do, ĝia rezulto.

Funkcio estas anonime difinita per lambda-esprimo, kiu esprimas agon de funkcio al ĝia argumento. Ekzemple, funkcio "aldoni du", en kiu  f(x) = x + 2  en lambda-kalkulo estus esprimita kiel  λ x. x + 2  (aŭ ekvivalente kiel  λ y. y + 2;  ĉar la nomo de formala parametro ne gravas (vidu $\alpha$-konverton)), kaj la apliko de sama funkcio al argumento f(3) estus skribata kiel  (λ x. x + 2) 3.  Notu, ke tia priskribo estas fakte neformala, ĉar esprimo x + 2 (aŭ eĉ numero 2) ne vere estas parto de lambda-kalkulo. Klarigo kiel numeroj kaj aritmetiko povas esti priskribata per vera lambda-kalkulo estos trovebla sube.

La funkcia apliko estas maldekstre asocia:  f x y = (f x) y.  Konsideru funkcion kiu uzas alian funkcion kiel argumenton kaj aplikas ĝin al numero 3 tiumaniere: λ f. f 3.  Tiu lasta funkcio povas esti aplikita al nia pli frua "aldonu du" funkcio tiel ĉi:  (λ f. f 3) (λ x. x + 2).  La tri esprimoj:

• (λ f. f 3) (λ x. x + 2)
• (λ x. x + 2) 3
• 3 + 2

estas ekvivalentaj.

Funkcio kun du variabloj estas esprimita en lambda-kalkulo kiel funkcio de unu argumento, kiu redonas funkcion de unu argumento (vidu kariigo). Ekzemple, funkcio  f(x, y) = x - y  estus skribata kiel  λ x. λ y. x - y. Laŭ komuna konsento, oni mallongigas kariigitajn funkciojn kiel, en tiu ĉi ekzemplo,  λ x y. x - y. Kvankam tio ne estas parto de formala difino de la lingvo,

λ x₁ x₂ … x_n. esprimo

estas kutime uzata mallongigo por

λ x₁. λ x₂. … λ x_n. esprimo

Ne ĉiun lambda-esprimon oni povas redukti tiamaniere ĝis iu difinita valoro. Konsideru, ekzemple

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

kaj provu imagi kio okazos se oni aplikos unuan funkcion al la argumento. Notu ke ĉar en λ-kalkulo ĉio estas funkcio, x en la ĉi-supra esprimo estas funkcio, kaj tio signifas ke x x estu komprenita kiel: funkcio x, kiu aplikiĝas al funkcio x.

Rezulte naskiĝas jeno:

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

Kiu produktas jenon:

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

.

.

.

Kaj tiel plu al nefinio.

Simila situacio aperas por:

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

 (λ x. x x)  estas ankaŭ konata kiel ω kombinatoro;  ((λ x. x x) (λ x. x x))  estas konata kiel Ω,  ((λ x. x x x) (λ x. x x x))  kiel Ω₂ ktp.

Lambda-kalkulaj esprimoj povas enhavi liberajn variablojn, t.e. variablojn ne ligitajn al iu λ. Ekzemple, variablo  y  estas libera en esprimo  (λ x. y) , ĉar la funkcio ĉiam produktus rezulton y. Iam tio bezonigas renomadon de formalaj argumentoj. Ekzemple, en la ĉi-suba formulo la litero y unue estas formala parametro, kaj poste libera variablo:

(λ x y. y x) (λ x. y).

Por redukti la esprimon, ni renomos unuan difinilon al z, kaj do redukto ne miksos la nomojn:

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

La redukto, do, estos:

λ z. z (λ x. y).

Necesas nur formaligi la esprimon kaj anstataŭigi lambda-esprimilojn per kombinatoroj por atingi kombinatoran logikon.

Formala difino

Difino

Lambda-esprimoj konsistas de

variabloj v₁, v₂, . . . v_n

abstraktadaj simboloj λ kaj .

parentezoj ( )

Aro de lambda-esprimoj, Λ, povas esti difinita rikure:

1. Se x estas variablo, do x ∈ Λ
2. Se x estas variablo kaj M ∈ Λ, do ( λ x . M ) ∈ Λ
3. Se M, N ∈ Λ, do ( M N ) ∈ Λ

Instancoj de 2 estas abstraktadoj kaj instancoj de 3 estas aplikoj.

Notacio

Por pli facile legebla notacio, aplikiĝas jenaj konsentoj:

Plej eksteraj parentezoj estas forlasataj: M N anstataŭ (M N).

Aplikoj estas defaŭlte maldekstre asociaj: M N P signifas (M N) P.

La abstraktado daŭriĝas kiom eblas plej dekstre: λ x . M N signifas λ x . (M N) kaj ne (λ x . M) N

Sekvenco de abstraktadoj estas mallongataj: λ x . λ y . λ z . N mallongiĝas kiel λ x y z . N

Liberaj kaj ligitaj variabloj

Abstraktada operatoro λ laŭdifine ligas ion ajn kio okazas en la abstraktado. Variabloj, kiuj okazas en diapazono de lambdo nomiĝas ligita. Ĉiuj aliaj variabloj estas liberaj. Ekzemple, en sekva esprimo y estas ligita variablo kaj x estas la libera:

λ y . x x y

Ankaŭ notu, ke variablo ligiĝas al "plej proksima lambdo. En sekva esprimo unu sola okuro de x ligiĝas al dua lambdo:

λ x . y (λ x . z x)

Aro de liberaj variabloj en lambda-esprimo, M, estas skribata kiel FV(M) kaj difinita per rikuro al la strukturo de terminoj, kiel:

1. FV( x ) = {x}, kie x estas variablo
2. FV ( λ x . M ) = FV ( M ) - {x}
3. FV ( M N ) = FV ( M ) $\cup$ FV ( N )

Esprimo kiu ne enhavas liberajn variablojn nomiĝas fermita. Fermitaj lambda-esprimoj estas ekvivalentaj al kombinatoroj de kombinatora logiko.

Redukto

α-konverto

Alfa-konverto ebligas ŝanĝon de nomoj de ligitaj variabloj. Ekzemple, alfa-konverto de  λx.x  estus  λy.y . Ofte en lambda-kalkulo esprimoj, kiuj diferencas nur je alfa-konverto estas konsiderataj ekvivalentaj.

Precizaj reguloj por alfa-konverto estas ne tute trivialaj. Unue, dum alfa-konvertado licas renomigi nur variabloj ligitaj al la sama abstraktado. Ekzemple, alfa-konverto de  λx.λx.x  povas rezulti en  λy.λx.x , sed ne en  λy.λx.y . La lasta havus malsaman signifon.

Due, alfa-konverto ne eblas se ĝi rezultus en ligiĝo de variablo al alia abstraktado. Ekzemple, se ni anstataŭigos x kun y en λx.λy.x, ni ricevus tute alian esprimon λy.λy.y.

Anstataŭigo

Anstataŭigo, skribata kiel E[V := E′], signifas anstataŭigon de variablo V per esprimo E′ ĉiam kiam ĝi estas libera ene de E. La preciza difino devas esti bone pripensita por evito de religiĝo de variabloj.Ekzemple, estas malĝuste transformigi (λ x.y)[y := x] en (λ x.x), ĉar la anstataŭigita x originale estis libera, sed iĝis ligita. Ĝusta anstataŭigo ĉi-okaze estus, ekzemple, (λ z.x), kio estus α-ekvivalenta al la originala esprimo.

Anstataŭigo de terminoj de λ-kalkulo estas difininta per rikuro al strukturo de terminoj jene:

x[x := N]        ≡ N

y[x := N]        ≡ y, se x ≠ y

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

(λ y. M)[x := N] ≡ λ y. (M[x := N]), se x ≠ y kaj y∉fv(N)

Notu, ke anstataŭigo estas difinita ĝis kiam rezulta esprimo estas α-ekvivalenta al la originala.

β-redukto

Beta-redukto esprimas ideon de apliko de la funkcio. La beta-redukto de  ((λ V. E) E′)  estas simple  E[V := E′] .

η-konverto

Eta-konverto esprimas ideon de ekstensionaleco, kio ĉi-kunteskte signifas, ke du funkcioj estas la sama s.n.s. ili donas saman rezulton por ĉiuj argumentoj. Eta-konverto konvertas  λ x. f x  kaj  f  kaj male, kiam x ne estas libera en f.

La konverto ne ĉiam estas ĝusta, kiam oni rigardas lambda-esprimojn kiel programojn. Kalkulo de  λ x. f x  povas finiĝi eĉ kiam esploro f ankoraŭ daŭras.

Bazoj de matematiko per lambda-kalkulo

Aritmetiko

Ekzistas kelkaj manieroj por difini naturalojn per lambda-kalkulo, sed la plej kutima estas maniero de numeraloj de Church. Per ĝi la difino estas jena:

0 := λ f x. x

1 := λ f x. f x

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

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

ktp. Numeralo de Church estas altnivela funkcio - ĝia argumento estas unuargumenta funkcio f kaj la rezulto alia unuargumenta funkcio. Church-numeralo n estas funkcio, kiu prenas funkcion f kiel argumenton kaj redonas la n-an kompozicion de f kun si mem. Tion oni skribas kiel f⁽ⁿ⁾ kaj fakte estas la n-a potenco de f (rigardata kiel operatoro); f⁽⁰⁾ estas difinita kiel identeca funkcio. Tiaj rikuraj kompozicioj obeas leĝojn de eksponentoj, kaj, do, tiaj numeraloj estas aritmetikaj. Notu ke 0 rezultas en x mem, t.e. ĝi estas esence la identeca funkcio, kaj 1 redonas la identecan funkcion. (Ankaŭ notu ke en originala lambda-kalkulo de Church, la formala parametro de la lambda-esprimo devis aperi almenaŭ unufoje ene de la funkcio, kio faris ĉi-supran difinon de 0 neebla.)

Ni povas difini funkcion de "sekva numero", kiu prenas numeron n kaj redonas n + 1 per aldono de unu apliko de f:

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

Ĉar la m-a kompozicio de f aplikata al n-a kompozicio de f donas m+n-an kompozicion de f, ni povas difini operacion de adicio:

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

Funkcion PLUS oni povas rigardi kiel funkcion de adicio de du naturaloj, kiu prenas du naturalojn kiel argumentojn kaj redonas unu naturalon kiel rezulton. Oni povas testi ke

PLUS 2 3    kaj    5

estas ekvivalentaj lambda-esprimoj. Ĉar aldono de m al n povas esti atingita per aldono de 1 m-foje, ekvivalenta difino estas:

PLUS := λ n m. m SUCC n

Simile, multiplikon eblas difini kiel

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

Alternative

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

ĉar multipliko de m kaj n estas sama kiel rikuro de funkcio de "adicio de n" m-foje al nulo. La funkcio de "antaŭa numero" estas difinita per  PRED n = n - 1  por a pozitiva entjero n kaj  PRED 0 = 0 . Tio estas noteble pli malfacile. La formulo

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

povas esti testita per montro, ke se T estas (λ g h. h (g f)), do T⁽ⁿ⁾(λ u. x) = (λ h. h(f^(n-1)(x)) ) por n > 0. Du aliaj difinoj de PRED estos donitaj sube, unu per kondiĉaj operatoroj kaj unu per paroj.

Kiam funkcio de "antaŭa numero" estas difinita, la subtraho estas facila:

SUB := λ m n. n PRED m,

do SUB m n donas m - n kiam m > n kaj 0 aliokaze.

Logiko kaj predikatoj

Laŭ konsento, la sekvaj du difinoj estas uzataj por logikaj tipoj TRUE (vero) kaj FALSE (malvero):

TRUE := λ x y. x

FALSE := λ x y. y

(Notu ke FALSE estas ekvivalenta al Church-numera nulo, difinita sube)

Poste, per tiuj du λ-terminoj, ni povas difini logikaj operatoroj. Ĉi-sube estas nur kelkaj el eblaj difinoj, ekzistas ankaŭ aliaj variantoj de samaj funkcioj:

AND := λ p q. p q p

OR := λ p q. p p q

NOT := λ p a b. p b a

IFTHENELSE := λ p a b. p a b

Nun ni povas komputi logikajn funkciojn, ekzemple:

AND TRUE FALSE

≡ (λ p q. p q p) TRUE FALSE →_β TRUE FALSE TRUE

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

kaj ni vidas ke AND TRUE FALSE estas ekvivalenta al FALSE.

Predicato estas tiu funkcia, kiu rezultas en logika valoro. La plej fundamenta predikato estas ISZERO kiu redonas TRUE se ĝia argumento estas Church-numera 0, kaj FALSE se ĝi estas io alia:

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

La sekva predikato testas ĉu la unua argumento estas ne pli granda ol la dua:

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

kaj ĉar m = n s.n.s. LEQ m n kaj LEQ n m, eblas facile konstrui predikaton po por numera egaleco.

La atingebleco de predikatoj kaj ĉi-subaj difinoj de TRUE kaj FALSE ebligas oportune skribi "se-do-alie"-esprimojn per labmda-kalkulo. Ekzemple, "retrotransforman funkcion" f(0)=0;f(n+1)=n oni povas difini kiel:

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

kiun oni povas indukte testi, montrante ke n (λ g k. ISZERO (g 1) k (PLUS (g k) 1) ) (λ v. 0) estas la "aldonu n - 1" funkcio por n > 0.

Paroj

Paron (duopon de valoroj) oni povas difini per supre-definitaj funkcioj TRUE kaj FALSE, uzante la Church-enkodon por paroj. Ekzemple, funkcio PAIR enkadrigas paron (x,y), dum FIRST redonas unuan elementon el ĝi kaj SECOND la duan.

PAIR := λ x y f. f x y

FIRST := λ p. p TRUE

SECOND := λ p. p FALSE

NIL := λ x. TRUE

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

Iu ajn ligita listo povas esti difinita kiel NIL por malplena listo aŭ kiel PAIR de unua elemento kaj listo de ĉiuj aliaj elementoj. Predikato NULL testas ĉu la valoro estas NIL.

Kiel ekzemplon de uzo de paroj oni povas konsideri la la funkcion de "movo laŭ la listo", kiu ŝanĝas paron (m, n) al (n, n+1). Ĝi difiniĝas kiel

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

kaj tio ebligas krei pli legeblan varianton de supre-menciita funkcio de "antaŭa elemento":

PRED := λ n. FIRST (n Φ (PAIR 0 0))

Rikuro

Rikuro estas maniero difini funkcion per la funkcio mem. Je unua rigardo ŝajnas, ke lambda-kalkulo ne ebligas tion. Sed vere oni ja povas fari rikuran difinon per lambda-kalkulo. Konsideru ekzemple, kiel oni rikure difinas funkcion de faktorialo f(n)

f(n) = 1, se n = 0; kaj n·f(n-1), se n>0.

En lambda-kalkulo ne eblas difini funkcion, kiu inkluzivus sin mem kiel argumenton. Por fari similan difinon oni devas krei median funkcion g, kiu prenas f kiel argumenton kaj redonas alian funkcion kun argumento n:

g := λ f n. (1, if n = 0; and n·f(n-1), if n>0).

La funkcio, kiun g redonas estas aŭ la konstanto 1, aŭ n-obla apliko de funkcio f al n-1. Per predikato ISZERO lkaj aliaj supre-difinitaj logikaj kaj algebraj funkcioj, oni povas difini g per lambda-kalkulo.

Tamen funkcio g ankoraŭ ne estas rikura. Por ke oni povu uzi g en rikura faktoriala funkcio, la funkcio f, kiun oni donas al g kiel argumenton devas havi specialajn ecojn. La funkcio f devas ekspandiĝi al funkcio g kun nur unu argumento, kaj tiu argumento devas ree esti f!

En aliaj vortoj, f devas ekspandiĝi al g(f). Per tio g povus ekspandiĝi al ĉi-supra faktoriala funkcio kaj kalkuli ĝin ĝis nivelo de rikuro. En tiu ekspando f reaperos kaj ree ekspandiĝos al g(f) por daŭrigo de rikuro. Tia speco de funkcio, kie f = g(f), estas nomata fiksita punkto de g, kaj aperas ke oni povas implementi ĝin per lambda-kalkulo per t.n. paradoksa operatoro aŭ operatoro de fiksita punkto, kutime skribata kiel Y -- la kombinatoro de fiksita punkto:

Y = λ g. (λ x. g (x x)) (λ x. g (x x))

En lambda-kalkulo Y g estas fiksita punkto de g, kaj ĝi ekspandiĝas al:

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)) (Komparu kun antaŭa ŝtupo)

g (Y g).

Nun, por kompletigi la rikuron de nia faktoriala funkcio ni simple vokos  g (Y g) n,  kie n estas numero, kies faktorialo ni kalkulas.

Se n = 5, tio ekspandiĝas al:

(λ n.(1, if n = 0; and n·((Y g)(n-1)), if n>0)) 5

1, if 5 = 0; and 5·(g(Y g)(5-1)), if 5>0

5·(g(Y g) 4)

5·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 4)

5·(1, if 4 = 0; and 4·(g(Y g)(4-1)), if 4>0)

5·(4·(g(Y g) 3))

5·(4·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 3))

5·(4·(1, if 3 = 0; and 3·(g(Y g)(3-1)), if 3>0))

5·(4·(3·(g(Y g) 2)))

...

Kaj tiel plu, rikure trapasante strukturon de algoritmo. Ĉiu rikure difinita funkcio povas esti rigardata kiel fiksita punkto de iu alia taŭga funkcio, kaj do per uzo de Y ĉiu rikure difinita funkcio povas esti esprimita kiel lambda-esprimo. Interalie, nun ni povas koncize difini subtrahon, multiplikon kaj komparon de naturaloj per rikuro.

Komputeblaj funkcioj

Funkcio F: N → N de naturaloj estas komputebla funkcio se kaj nur se ekzistas lambda-esprimo f en kiu por ĉiu paro (x, y) en N, F(x)=y se kaj nur se f x =_β y,  kie x kaj y estas Church-numeroj akordaj al x and y laŭorde kaj =_β signifas ekvivalentecon ĝis beta-redukto. Tio ĉi estas unu el multaj manieroj difini komputeblecon; aliaj variantoj kaj diskuto troveblas en tezo de Church-Turing.

Nedecidebleco de ekvivalenteco

Ne ekzistas algoritmo, kiu prenus du lambda-esprimojn kaj redonas TRUE aŭ FALSE depende de ĉu la esprimoj estas ekvivalentaj. Tio ĉi estis historie la unua problemo por kiu nedecidebleco povas esti rigore pruvita. Unue, la pruvo aperis, ke neniu komputebla funkcio povas decidi ekvivalenteco. Poste tezo de Church pruvis, ke nek povis iu ajn algoritmo.

La pruvo de Church unue reduktas la problemon ĝis la demando ĉu donita lambda-esprimo havas normalan formon. Normala formo estas ekvivalenta esprimo, kiun oni ne plu povas redukti. Poste li konjektis tiun esprimon komputebla kaj do esprimebla per lambda-kalkulo. Bazante sin je pli fruaj verkoj far Kleene kaj konstruktante Gödel-numeradon por lambda-esprimoj, li konstruis lambda-esprimon e, kiu rigore sekvas pruvon de unua nekompleteca teoremo de Gödel. Se oni aplikas e al ĝia propra Gödel-numero, aperas kontraŭdiro.

Lambda-kalkulo en programlingvoj

Kiel montris Peter Landin en sia klasika verko A Correspondence between ALGOL 60 and Church's Lambda-notation de jaro 1965, oni povas kompreni sekvencajn procedurajn programlingvojn en terminoj de lambda-kalkulo, kaj tio donas bazajn mekanismojn por procedura abstraktado kaj procedura apliko.

Uzo de lambda-kalkulo en programado bezonas rigardon de "funkcioj" kiel objektoj de unua klaso, kio envokas problemon pri implemento de stak-bazitaj programlingvoj, konatan kiel Funarg-problemo.

La plej uzata implemento de lambda-kalkulo en programado estas funkciaj programlingvoj, kiuj plejparte baziĝas je lambda-kalkulo kun konstantoj kaj datumtipoj. Lisp uzas varianton de lambda-notacio por difino de funkcioj, sed nur ĝia pure funkcia varianto Lispkit Lisp estas vere ekvivalenta al lambda-kalkulo.

Ekzemplo de lambda-funkcio en Lisp:

(lambda (x) (* x x))

Ĉi-supra Lisp-ekzemplo disvolviĝas al funkcio de unua klaso. La termino lambda enkondukas la funkcion, kaj sekvas listo de argumentoj. Ĉi-funkcio havas nur unu argumenton x. Poste sekvas la esprimoj, kiuj estas ekzekutitaj. Ĉi-tie estas nur unu esprimo (* x x) kiu multiplikas x je x.

Funkciaj lingvoj ne estas la solaj kiuj subtenas funkciojn kiel objektojn de unua klaso. Sennombraj imperativaj programlingvoj kiel Pascal, antaŭlonge subtenas transdonon de subprogramoj kiel argumentoj al aliaj subprogramoj. En C kaj C-similaj variantoj de C++ ekvivalenta rezulto estas atingata per transdono de montriloj al kodo de funkcioj aŭ subprogramoj. Tiaj mekanismoj estas limigitaj al funkcioj skribataj speciale en la kodo kaj ne ebligas rektan subtenon de funkcioj de pli alta nivelo. Kelkaj imperativaj objekt-orientitaj programlingvoj havas apartajn notaciojn por reprezenti funkciojn de iu ajn klaso. Tiaj mekanismoj ekzistas en C++, Smalltalk kaj pli moderne en Eiffel ("agentoj") kaj C# ("delegatoj"). Jen ekzemplo de realigo de tia funkcio per "inline agent"-esprimo de Eiffel

agent (x: REAL): REAL do Result := x * x end

Tiu ĉi objekto korespondas al lambda-esprimo λ x . x*x (kun voko per valoro). Oni povas rigardi ĝin kiel iun alian esprimon, t.e. transdoni ĝin al iu ajn funkcio aŭ rutino. La valoro de square estas esprimo de ĉi-supra "agento", kaj la rezulto de apliko de square al la valoro de (β-redukto) estas esprimata kiel square.item ([a]), kien la argumento estas transdonita kiel duopo.

En Python tia ekzemplo uzas la lambda Arkivigite je 2007-06-09 per la retarkivo Wayback Machine-formojn de funkcioj:

func = lambda x: x ** 2

Tio ĉi kreas novan anoniman funkcion kun nomo func, kiun oni povas transdoni al aliaj funkcioj, variabloj ktp. Python ankaŭ povas rigardi iun ajn funkcion kreitan per standarda def Arkivigite je 2007-06-08 per la retarkivo Wayback Machine-esprimo kiel objekto de unua klaso.

Simile funkcias la Smalltalk-esprimo

[ :x | x * x ]

Tio ĉi estas objekto de unua klaso (bloka fermo) kiun oni ankaŭ povas transdoni al variabloj, funkcioj ktp.

Simila ekzemplo de C++ (uzanta Boost.Lambda bibliotekon):

std::for_each(c.begin(), c.end(), std::cout << _1 * _1 << std::endl);

Tie ĉi standarda biblioteka funkcio for_each aplikiĝas al ĉiu membro de ujo 'c', kaj printas duan potencon de ĉiu elemento. La _1-notacio estas konsento de Boost.Lambda (originale devenanta de Boost.Bind) por reprezento de unua argumento x ie ajn aliloke.

Simpla C#-delegato, kiu prenas variablon kaj redonas duan potencon, pova poste transdoniĝi al aliaj funkcian aŭ delegatoj, aspektas jene:

//Declare a delegate signature
delegate double MathDelegate(double i);
//Create a delegate instance
MathDelegate f = delegate(double i) { return Math.Pow(i, 2); };

/* Passing 'f' function variable to another method, executing,
 and returning the result of the function
 */
double Execute(MathDelegate f)
{
 return f(100);
}

Ekde C# 3.0, la lingvo enhavas lambda-esprimojn similan al tiu de Python aŭ Lisp. La esprimo disvolviĝas al supremenciita delegato, sed povas esti skribata pli facile:

//Create a delegate instance
MathDelegate f = i => i * i;
Execute(f);
// or more simply put
Execute(i => i * i);

Strategioj de redukto

Ĉu eblas normaligi la terminon kaj kiom da laboro necesas por tio je grava parto dependas de uzata redukta strategio. La plej grava distingo inter reduktaj strategioj en funkciaj programlingvoj estas distingo inter rigora komputado kaj malloborema komputado.

Ĉi-sube ni uzos terminon 'redex', kio estas mallongigo de 'reduktebla esprimo'. Ekzemple, (λ x. M) N estas beta-redex, ĉar ĝi estas reduktebla per beta-transformo; λ x. M x estas eta-redex se x ne estas libera en M. La rezulto de redukto de redex estas ĝia reduktaĵo. En antaŭaj ekzemploj, iliaj reduktaĵoj estas, laŭvice, M[x:=N] kaj M.

Plenaj beta-reduktoj

Iu redex povas esti reduktita iam ajn. Tio signifas, ke aparta redukta strategio, ĉar ordo de redukto estas rigardata negrava.

Aplika ordo

La plej dekstra kaj plej ena redex estas ĉiam reduktita unuavice. Evidente, tio signifas, ke argumentoj de la funkcio estas reduktitaj antaŭ la funkcio mem. Aplika ordo ĉiam emas apliki funkciojn al normalaj formoj, eĉ kiam tio ne eblas.

Plimulto de programlingvoj (inkluzive Lisp, ML kaj imperativaj lingvoj kiel C kaj Java) priskribiĝis kiel "rigoraj", kio signifas ke la funkcioj estas aplikitaj al nenormaligaj argumentoj, restas nenoramligaj. Tion oni akiras per uzo de aplika ordo, kio nomiĝas "strikta komputado".

Normala ordo

La plej maldekstra kaj plej ekstera redex estas ĉiam reduktita unuavice. T.e. kiam eblas la strukturo de abstraktado estas anstataŭigita per la pli facila antaŭ ol dedukto de argumentoj.

Voko per nomo

Sama, kiel normala ordo, sed reduktoj ne okazas ene de abstraktadoj. Ekzemple λ x.(λ x.x)x laŭ tiu strategio estas rigardata kiel normala formo, kvankam ĝi enhavas redex (λ x.x)x.

Voko per valoro

Nur la plej eksteraj redex-oj estas reduktitaj. La redex estas reduktata nur se ĝia plej dekstra parto havas reduktitan valoron (variablon aŭ lambda-abstrakton).

Voko laŭ neceso

Kiel normala ordo, sed la argumentoj ne estas reduktataj ĝin oni vere tion bezonas - do, ĝis kiam necesas transdoni la rezulton. Tio ĉi en praktikaj kuntekstoj estas nomata "malloborema komputado". La argumentoj, kiuj ne estas reduktitaj, akiras "nomojn" en formo de montrilo, kaj la redex estas reprezentita en formo de tunko.

Aplika ordo ne estas normaliga strategio. La kutima kontraŭekzemplo estas jena: difinu Ω = ωω kie ω = λ x. xx. Ĉi-esprimo enhavas nur unu redex, la tutan esprimon mem. Ĝia reduktaĵo ree estas Ω. Ĉar tio ĉi estas nura ebla redukto, Ω ne havas normalan formon en iu ajn redukta strategio. Per aplika ordo redukto de esprimo KIΩ = (λ x y . x)(λ x.x)Ω komenciĝas je redukto de Ω, ĉar ĝi estas plej dekstra redex, sed ĉar Ω ne havas normalan formon, la redukto haltas tie ĉi, kaj normala formo de KIΩ ne estas trovita.

Kontraste, normala ordo ĉiam trovas normaligan redukton se tiu ekzistas. En ĉi-supra ekzemplo, KIΩ reduktiĝas ĝis sia normala formo, kio estas I. Maladvantaĝo de tiu strategio estas ke la argumentoj povas kopiiĝi, kaj tio malfaciligas la komputon. Ekzemple, (λ x.xx)((λ x.x)y) reduktiĝas al ((λx.x)y)((λx.x)y) per tiu strategio, pro kio aperas du pli redex-oj. Do, plena redukto bezonas pluajn du etapojn. Kaj se la unua argumento estus reduktita unuavice, tio ne estus bezonata.

Avantaĝo de aplika ordo estas ke ĝi ne kaŭzas nenecesajn komputaĵojn, ĉar ĝi ne anstataŭigas argumentojn kun redex-oj, kaj do ne bezonas kopii ilin, duobligante la laboron. En ĉi-supra ekzemplo, aplika ordo reduktas (λ x.xx)((λ x.x)y) unue al (λ x.xx)y kaj poste al normala ordo yy, do, bezonas du etapojn anstataŭ tri.

La plej puraj funkciaj programlingvoj, aparte Miranda kaj ĝiaj posteuloj inkluzive Haskell kaj pruvaj lingvoj de aŭtomata pruvo de teoremoj, uzas mallaboreman komputadon, kiu estas esence sama strategio kiel voko laŭ neceso. Tio ĉi similas al normala ordo, sed ĝi sukcesas eviti duobligon de laboro per kvotigo. En ĉi-supra ekzemplo, (λ x.xx)((λ x.x)y) reduktiĝas al ((λx.x)y)((λx.x)y), kiu havas du redex-ojn, sed ĉar ili estas samaj, voko laŭ neceso reprezentas ilin ambaŭ per unu sama objekto. Do, kiam unu estas reduktita, la alia estas ankaŭ.

Rimarko pri komplikeco

Kvankam ideo de beta-redukto ŝajnas sufiĉe simpla, ĝi ne estas atoma operacio kaj do havas netrivian koston je komputada komplikeco. Pli precize, oni devas aŭ trovi lokojn de ĉiuj aperoj de ligita variablo V en esprimo E, kiu bezonus malŝparon de tempo, aŭ konservi informon pri tiuj lokoj, kio malŝparus spacon. Naiva serĉo por lokoj de V en E estas O(n) en longo n de esprimo E. Tio uzeblas por stude de sistemoj kun eksplika anstataŭigo. Direktoroj de Sinot proponas manieron por trovi lokojn de liberaj variabloj en esprimoj.

Paraleleco kaj konkuro

La eco de teoremo de Church-Rosser en lambda-kalkulo signifas ke beta-reduktado povas esti religita en iu ajn ordo, eĉ paralele. Tio signifas, ke malsamaj nedetermenismaj strategioj de redukto funkcias kun tio. Tamen, lambda-kalkulo mem ne enhavas iujn ajn apartajn konstruojn por paralela komputado. Oni povas aldoni konstruojn kiel futuroj al lambda-kalkulo por atingi paralelecon. Aliaj procezkalkuloj estas kreitaj por priskribo de komunikado kaj konkuro.

Semantiko

La fakto ke terminoj de lambda-kalkulo agas kiel funkcio al aliaj lambda-kalkulaj terminoj kaj eĉ al si mem kondukis al demandoj pri semantiko de lambda-kalkulo. Ĉu oni povas aldoni senchavan signifon al terminoj de lambda-kalkulo? La natura semantiko estis trovi aron D izomorfa al funkcia spaco D → D de funkcioj al ĝi mem. Tamen, neniu netriviala tia D povas ekzisti pro limigoj de kardinaleco, ĉar aro de ĉiuj funkcioj de D al D havas pli grandan kardinalecon ol D.

En 1970-aj jaroj, Dana Scott montris ke se oni konsiderus nur kontinuajn funkciojn, aro aŭ domajno D kun necesa eco estas trovebla. Tio, do, donis modelon por lambda-kalkulo.

Tiu ĉi verko ankaŭ formis bazon por denotacia semantiko de programlingvoj.