Lambdakalkyyli

Lambdakalkyyli (engl. lambda calculus) on formaalin laskennan malli. Sen avulla voidaan käsitellä matemaattisia ja laskennallisia ongelmia.

Lambdakalkyyli on Turing-täydellinen, eli sillä voidaan ilmaista mitä tahansa matemaattisia laskennan ongelmia.

Lambdakalkyyliä voidaan myös itsessään pitää ohjelmointikielenä.

Historiaa

Alonzo Church kehitti lambdakalkyylin kollegoineen 1920 ja 30-luvulla.

Korjattuaan ensiversionsa ongelmia Church julkisti vuonna 1936 tietojenkäsittelyyn sopivan osion, tyypittömän lambdakalkyylin. Myöhemmin 1940-luvulla Church julkisti yksinkertaisesti tyypitetyn lambdakalkyylin.

Funktionaaliset ohjelmointikielet perustuvat pitkälti lambda-kalkyyliin.

Peruskäsitteet

Lambdakalkyylin ilmaisu koostuu termeistä. Termit ovat muuttujat, lambda-abstraktiot, ja sovellukset. Muuttujia määritellään abstraktioilla, ja niitä käytetään sovelluksilla.

Termit

• muuttuja, esim. i, x, v
• abstraktio, käyttää symboleita . ja λ, esim. lambda λx.i
• sovellus, esim. lambdojen y ja i sovellus: yi

Lambda

Lambda-abstraktiota symboloi kreikkalaisen aakkosten kirjain λ.

Churchin numeraalit

Numerot voidaan ilmaista monilla eri tavoin. Yksi tapa on Churchin numeraalit.

• 0 := λfx. x
• 1 := λfx. fx
• 2 := λfx. f( fx )
• 3 := λfx. f( f( fx ))
• jne.

Tyypitetty ja tyypittämätön

Tyypittämättömässä lambdakalkyylissä ei ole lainkaan valmiiksi määriteltyjä vakioita tai operaattoreita kuten numerot, aritmeettiset operaatiot tai ehtolauseet. Tarvittaessa ne määritellään, kuten esim. numerot Churchin numeraaleilla.

Tyypitetyssä lambdakalkyylissä jokaiselle termille tulee olla yksi tyyppi.

Katso myös

• Churchin-Turingin teesi
• Lisp -ohjelmointikieli.