Lambda-kalkulo: Malsamoj inter versioj

278 bitokojn forigis ,  antaŭ 3 jaroj
e
sen resumo de redaktoj
e
e
[[Dosiero:Lambda lc.svg|thumbeta|rightdekstra|180px]]
En [[matematika logiko]] kaj [[komputoscienco]], '''Lambda-kalkulo''', ankaŭ skribata kiel '''λ-kalkulo''', estas [[formalismo|formalisma sistemo]] por esplori difinon de [[funkcio (matematiko)|funkcio]], ĝian aplikon kaj [[rikuro]]n. Ĝ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]]<ref>Henk Barendregt, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.7908 ''The Impact of the Lambda Calculus in Logic and Computer Science.''] ''The Bulletin of Symbolic Logic'', Volume '''3''', Number 2, June 1997.</ref>.
 
 
== 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 <tt>&nbsp;''f''(''x'') = ''x'' + 2&nbsp;</tt> en lambda-kalkulo estus esprimita kiel <tt>&nbsp;λ ''x''. ''x'' + 2&nbsp;</tt> (aŭ ekvivalente kiel <tt>&nbsp;λ ''y''. ''y'' + 2</tt>;&nbsp; ĉar la nomo de formala parametro ne gravas (vidu <math>\alpha</math>-konverton)), kaj la apliko de sama funkcio al argumento <tt>''f''(3)</tt> estus skribata kiel <tt>&nbsp;(λ ''x''. ''x'' + 2) 3</tt>.&nbsp; Notu, ke tia priskribo estas fakte neformala, ĉar esprimo <tt>''x'' + 2</tt> (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.
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 <tt>&nbsp;''f''(''x'', ''y'') = ''x'' - ''y''&nbsp;</tt> estus skribata kiel <tt>&nbsp;λ ''x''. λ ''y''. ''x'' - ''y''</tt>. Laŭ komuna konsento, oni mallongigas kariigitajn funkciojn kiel, en tiu ĉi ekzemplo, <tt>&nbsp;λ ''x'' ''y''. ''x'' - ''y''</tt>. Kvankam tio ne estas parto de formala difino de la lingvo,
: <tt>λ ''x''<sub>1</sub> ''x''<sub>2</sub> … ''x''<sub>n</sub>. esprimo</tt>
estas kutime uzata mallongigo por
:.
:.
Kaj tiel plu al nefinio.
 
Simila situacio aperas por:
# Se M, N ∈ Λ, do ( M N ) ∈ Λ
Instancoj de 2 estas ''abstraktadoj'' kaj instancoj de 3 estas ''aplikoj''.<ref>{{Citaĵo de libro
| familinomo = Barendregt
| personnomo = Hendrik Pieter
| author-link =
| last2 =
| first2 =
| author2-link =
| titolo = The Lambda Calculus: Its Syntax and Semantics
| place =
| eldoninto = North Holland, Amsterdam. [ftp://ftp.cs.ru.nl/pub/CompMath.Found/ErrataLCalculus.pdf Corrections]
| jaro = 1984
| volumo = 103
| serio = Studies in Logic and the Foundations of Mathematics
| eldono = Revised edition
| url = http://www.elsevier.com/wps/find/bookdescription.cws_home/501727/description
| doi =
| id =
| isbn = 0-444-87508-5}}
</ref>
 
: Sekvenco de abstraktadoj estas mallongataj: λ x . λ y . λ z . N mallongiĝas kiel λ x y z . N<ref name="Selinger">
{{Citaĵo de libro
| personnomo = Peter
| familinomo = Selinger
| author-link =
| first2 =
| last2 =
| author2-link =
| editor-last =
| editor-first =
| editor2-last =
| editor2-first =
| contribution =
| contribution-url =
| titolo = Lecture Notes on the Lambda Calculus
| year =
| paĝoj = 9
| place =
| eldoninto = Department of Mathematics and Statistics, University of Ottawa
| url = http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
| doi =
| id = }}</ref>
=== 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:
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:
# FV( x ) = {x}, kie x estas variablo
# FV ( λ x . M ) = FV ( M ) - {x}
# FV ( M N ) = FV ( M ) <math>\cup</math> FV ( N )<ref name="BarendregtBarendsen">{{Citaĵo de libro
| familinomo = Barendregt
| personnomo = Henk
| author-link =
| familinomo2 = Barendsen
| personnomo2 = Erik
| author2-link =
| titolo = Introduction to Lambda Calculus
| place =
| publisher =
| jaro = March 2000
| volume =
| edition =
| url = ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf
| doi =
| id =
| isbn = }}</ref>
 
Esprimo kiu ne enhavas liberajn variablojn nomiĝas ''fermita''. Fermitaj lambda-esprimoj estas ekvivalentaj al ''kombinatoroj'' de [[kombinatora logiko]].
 
=== Anstataŭigo ===
Anstataŭigo, skribata kiel <tt>E[V := E′]</tt>, signifas anstataŭigon de variablo <tt>V</tt> per esprimo <tt>E′</tt> ĉiam kiam ĝi estas libera ene de <tt>E</tt>. La preciza difino devas esti bone pripensita por evito de religiĝo de variabloj.Ekzemple, estas malĝuste transformigi na <tt>(λ x.y)[y := x]</tt> en <tt>(λ x.x)</tt>, ĉar la anstataŭigita <tt>x</tt> originale estis libera, sed iĝis ligita. Ĝusta anstataŭigo ĉi-okaze estus, ekzemple, <tt>(λ z.x)</tt>, kio estus α-ekvivalenta al la originala esprimo.
 
Anstataŭigo de terminoj de λ-kalkulo estas difininta per rikuro al strukturo de terminoj jene:
ktp. Numeralo de Church estas [[altnivela funkcio]] - ĝia argumento estas unuargumenta funkcio <tt>''f''</tt> kaj la rezulto alia unuargumenta funkcio. Church-numeralo <tt>''n''</tt> estas funkcio, kiu prenas funkcion <tt>''f''</tt> kiel argumenton kaj redonas la <tt>''n''</tt>-an kompozicion de <tt>''f''</tt> kun si mem. Tion oni skribas kiel <tt>''f''<sup>(''n'')</sup></tt> kaj fakte estas la <tt>''n''</tt>-a potenco de <tt>''f''</tt> (rigardata estiel operatoro); <tt>''f''<sup>(0)</sup></tt> estas difinita kiel identeca funkcio. Tiaj rikuraj kompozicioj obeas leĝojn de eksponentoj, kaj, do, tiaj numeraloj estas aritmetikaj. Notu ke <tt>0</tt> rezultas en <tt>''x''</tt> mem, t.e. ĝi estas esence la identeca funkcio, kaj <tt>1</tt> ''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 <tt>0</tt> neebla.)
 
Ni povas difini funkcion de "sekva numero", kiu prenas numeron <tt>''n''</tt> kaj redonas na <tt>''n'' + 1</tt> per aldono de unu apliko de <tt>''f''</tt>:
: <tt>SUCC := λ ''n'' ''f'' ''x''. ''f'' (''n'' ''f'' ''x'')</tt>
Ĉar la <tt>''m''</tt>-a kompozicio de <tt>''f''</tt> aplikata al <tt>''n''</tt>-a kompozicio de <tt>''f''</tt> donas <tt>''m+n''</tt>-an kompozicion de <tt>''f''</tt>, ni povas difini operacion de [[adicio]]:
estas ekvivalentaj lambda-esprimoj. Ĉar aldono de <tt>''m''</tt> al <tt>''n''</tt> povas esti atingita per aldono de 1 <tt>''m''</tt>-foje, ekvivalenta difino estas:
: <tt>PLUS := λ ''n'' ''m''. ''m'' SUCC ''n''</tt><ref>{{cite book
| last = Felleisen
| first = Matthias
| authorlink =
| coauthors = Matthew Flatt
| title = Programming Languages and Lambda Calculi
| publisher =
| date = 2006
| location =
| pages = 26
| url = http://www.cs.utah.edu/plt/publications/pllc.pdf
| doi =
| id =
| isbn = }}</ref>
Simile, [[multipliko]]n eblas difini kiel
: <tt>MULT := λ ''m'' ''n'' ''f'' . ''m'' (''n'' ''f'')</tt><ref>
{{Citaĵo de libro
| personnomo = Peter
| familinomo = Selinger
| author-link =
| first2 =
| last2 =
| author2-link =
| editor-last =
| editor-first =
| editor2-last =
| editor2-first =
| contribution =
| contribution-url =
| titolo = Lecture Notes on the Lambda Calculus
| year =
| paĝoj = 16
| place =
| eldoninto = Department of Mathematics and Statistics, University of Ottawa
| url = http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
| doi =
| id = }}</ref>
Alternative
: <tt>MULT := λ ''m'' ''n''. ''m'' (PLUS ''n'') 0</tt>,
La funkcio de "antaŭa numero" estas definita per <tt>&nbsp;PRED ''n'' = ''n'' - 1&nbsp;</tt> por a pozitiva [[entjero]] <tt>''n''</tt> kaj <tt>&nbsp;PRED 0 = 0&nbsp;</tt>. Tio estas noteble pli malfacile. La formulo
: <tt>PRED := λ ''n'' ''f'' ''x''. ''n'' (λ ''g'' ''h''. ''h'' (''g'' ''f'')) (λ ''u''. ''x'') (λ ''u''. ''u'')&nbsp;</tt>
povas esti testita per montro, ke se <tt>T</tt> estas <tt>(λ ''g'' ''h''. ''h'' (''g'' ''f''))</tt>, do <tt>T<sup>(''n'')</sup>(λ ''u''. ''x'') = (λ ''h''. ''h''(''f''<sup>(''n''-1)</sup>(''x'')) )</tt> por <tt>''n'' > 0</tt>. Du aliaj difinoj de <tt>PRED</tt> estos donitaj sube, unu per kondiĉaj operatoroj kaj unu per paroj.
 
Kiam funkcio de "antaŭa numero" estas difinita, la [[subtraho]] estas facila:
: <tt>SUB := λ ''m'' ''n''. ''n'' PRED ''m''</tt>,
do <tt>SUB ''m'' ''n''</tt> donas na <tt>''m'' - ''n''</tt> kiam <tt>''m'' > ''n''</tt> kaj na <tt>0</tt> aliokaze.
=== Logiko kaj predikatoj ===
Laŭ konsento, la sekvaj du difinoj estas uzataj por logikaj tipoj <tt>TRUE</tt> ([[vero]]) kaj <tt>FALSE</tt> ([[malvero]]):
La atingebleco de predikatoj kaj ĉi-subaj difinoj de <tt>TRUE</tt> kaj <tt>FALSE</tt> ebligas oportune skribi "se-do-alie"-esprimojn per labmda-kalkulo. Ekzemple, "retrotransforman funkcion" <tt>''f''(0)=0;''f''(n+1)=n</tt> oni povas defini kiel:
: <tt>PRED := λ ''n''. ''n'' (λ ''g k''. ISZERO (''g'' 1) k (PLUS (''g k'') 1) ) (λ ''v''. 0) 0 </tt>
kiun oni povas indukte testi, montrante ke <tt>''n'' (λ ''g k''. ISZERO (''g'' 1) k (PLUS (''g k'') 1) ) (λ ''v''. 0)</tt> estas la "aldonu na <tt>''n''</tt> - 1" funkcio por <tt>''n''</tt> > 0.
 
=== Paroj ===
:<tt>''f''(''n'') = 1, se ''n'' = 0; kaj ''n''·''f''(''n''-1), se ''n''>0</tt>.
 
En lambda-kalkulo ne eblas difini funkcion, kiu inkluzivus sin mem kiel argumenton. Por fari similan difinon oni devas krei median funkcion <tt>''g''</tt>, kiu prenas na <tt>''f''</tt> kiel argumenton kaj redonas alian funkcion kun argumento <tt>''n''</tt>:
 
:<tt>''g'' := λ ''f'' ''n''. (1, if ''n'' = 0; and ''n''·''f''(''n''-1), if ''n''>0)</tt>.
 
La funkcio, kiun <tt>''g''</tt> redonas estas aŭ la konstanto <tt>1</tt>, aŭ ''n''-obla apliko de funkcio <tt>''f''</tt> al <tt>''n''-1</tt>. Per predikato <tt>ISZERO</tt> lkaj aliaj supre-difinitaj logikaj kaj algebraj funkcioj, oni povas difini na <tt>''g''</tt> per lambda-kalkulo.
 
Tamen funkcio <tt>''g''</tt> ankoraŭ ne estas rikura. Por ke oni povu uzi na <tt>''g''</tt> en rikura faktoriala funkcio, la funkcio <tt>''f''</tt>, kiun oni donas al <tt>''g''</tt> kiel argumenton devas havi specialajn ecojn. La funkcio <tt>''f''</tt> devas ekspandiĝi al funkcio <tt>''g''</tt> kun nur unu argumento, kaj tiu argumento devas ree esti <tt>''f''</tt>!
 
En aliaj vortoj, <tt>''f''</tt> devas ekspandiĝi al <tt>''g''(''f'')</tt>. Per tio <tt>''g''</tt> povus ekspandiĝi al ĉi-supra faktoriala funkcio kaj kalkuli ĝin ĝis nivelo de rikuro. En tiu ekspando <tt>''f''</tt> reaperos kaj ree ekspandiĝos al <tt>''g''(''f'')</tt> por daŭrigo de rikuro. Tia speco de funkcio, kie <tt>''f'' = ''g''(''f'')</tt>, estas nomata ''fiksita punkto'' de <tt>''g''</tt>, kaj aperas ke oni povas implementi ĝin per lambda-kalkulo per t.n. ''paradoksa operatoro'' aŭ ''operatoro de fiksita punkto'', kutime skribata kiel <tt>''Y''</tt> -- la [[kombinatoro de fiksita punkto]]:
:<tt>(λ ''x''. ''g'' (''x'' ''x'')) (λ ''x''. ''g'' (''x'' ''x''))</tt>
:<tt>''g'' ((λ ''x''. ''g'' (''x'' ''x'')) (λ ''x''. ''g'' (''x'' ''x''))</tt> (Komparu kun antaŭa ŝtupo)
:<tt>''g'' (''Y'' ''g'')</tt>.
 
Nun, por kompletigi la rikuron de nia faktoriala funkcio ni simple vokos na <tt>&nbsp;''g'' (''Y'' ''g'') ''n''</tt>,&nbsp; kie ''n'' estas numero, kies faktorialo ni kalkulas.
 
Se ''n'' = 5, tio ekspandiĝas al:
 
=== Nedecidebleco de ekvivalenteco ===
Ne ekzistas algoritmo, kiu prenus du lambda-esprimojn kaj redonas na <tt>TRUE</tt> aŭ <tt>FALSE</tt> 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 [[Numero de Gödel|Gödel-numeradon]] por lambda-esprimoj, li konstruis lambda-esprimon <tt>''e''</tt>, kiu rigore sekvas pruvon de [[Teoremoj de nekompleteco|unua nekompleteca teoremo de Gödel]]. Se oni aplikas na <tt>''e''</tt> al ĝia propra [[Gödel-numero]], aperas kontraŭdiro.
== Lambda-kalkulo en programlingvoj ==
Kiel montris [[Peter Landin]] en sia klasika verko <cite>[http://portal.acm.org/citation.cfm?id=363749&coll=portal&dl=ACM A Correspondence between ALGOL 60 and Church's Lambda-notation]</cite> de jaro [[1965]], oni povas kompreni sekvencajn [[procedura programado|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 [[objekto de unua klaso|objektoj de unua klaso]], kio envokas problemon pri implemento de [[stako|stak]]-bazitaj programlingvoj, konatan kiel [[Funarg-problemo]].
<source lang="csharp">
/* Passing 'f' function variable to another method, executing,
and returning the result of the function
*/
double Execute(MathDelegate f)
{
return f(100);
}
</source>
 
=== 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, <tt>(λ x. M) N</tt> estas ''beta-redex'', ĉar ĝi estas reduktebla per beta-transformo; <tt>λ x. M x</tt> estas ''eta-redex'' se <tt>x</tt> ne estas libera en <tt>M</tt>. La rezulto de redukto de ''redex'' estas ĝia reduktaĵo. En antaŭaj ekzemploj, iliaj reduktaĵoj estas, laŭvice, <tt>M[x:=N]</tt> kaj <tt>M</tt>.
:Plimulto de programlingvoj (inkluzive [[Lisp]], [[ML (programlingvo)|ML]] kaj imperativaj lingvoj kiel [[C (programlingvo)|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 maldeksta kaj plej ekstera ''redex'' estas ĉiam reduktita unuavice. T.e. kiam eblas la struktoro 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 <tt>λ x.(λ x.x)x</tt> laŭ tiu strategio estas rigardata kiel normala formo, kvankam ĝi enhavas na ''redex'' <tt>(λ x.x)x</tt>.
;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 <tt>Ω = ωω</tt> kie <tt>ω = λ x. xx</tt>. Ĉi-esprimo enhavas na nur unu ''redex'', la tutan esprimon mem. Ĝia reduktaĵo ree estas <tt>Ω</tt>. Ĉar tio ĉi estas nura ebla redukto, <tt>Ω</tt> ne havas normalan formon en iu ajn redukta strategio. Per aplika ordo redukto de esprimo <tt>KIΩ = (λ x y . x)(λ x.x)Ω</tt> komenciĝas je redukto de <tt>Ω</tt>, ĉar ĝi estas plej dekstra ''redex'', sed ĉar <tt>Ω</tt> ne havas normalan formon, la redukto haltas tie ĉi, kaj normala formo de <tt>KIΩ</tt> ne estas trovita.
 
Kontraste, normala ordo ĉiam trovas normaligan redukton se tiu ekzistas. En ĉi-supra ekzemplo, <tt>KIΩ</tt> reduktiĝas ĝis sia normala formo, kio estas <tt>I</tt>. Maladvantaĝo de tiu strategio estas ke la argumentoj povas kopiiĝi, kaj tio malfaciligas la komputon. Ekzemple, <tt>(λ x.xx)((λ x.x)y)</tt> reduktiĝas al <tt>((λx.x)y)((λx.x)y)</tt> 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 na <tt>(λ x.xx)((λ x.x)y)</tt> unue al <tt>(λ x.xx)y</tt> kaj poste al normala ordo <tt>yy</tt>, do, bezonas du etapojn anstataŭ tri.
 
La plej ''puraj'' funkciaj programlingvoj, aparte [[Miranda (programlingvo)|Miranda]] kaj ĝiaj posteuloj inkluzive [[Haskell]] kaj pruvaj lingvoj de [[aŭtomata pruvo de teoremoj]], uzas ''[[mallaborema komputado|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, <tt>(λ x.xx)((λ x.x)y)</tt> reduktiĝas al <tt>((λx.x)y)((λx.x)y)</tt>, 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ŭ.
Tiu ĉi verko ankaŭ formis bazon por [[denotacia semantiko]] de programlingvoj.
 
== Notoj kaj referencojReferencoj ==
{{Referencoj}}
<references /> <!-- Helpo : http://eo.wikipedia.org/wiki/Helpo:Referencoj kaj piednotoj -->
 
[[Kategorio:Lambda-kalkulo|*]]