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^[1].

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.

1. ↑ Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.