Idi na sadržaj

Lambda račun

S Wikipedije, slobodne enciklopedije

U matematičkoj logici i računarstvu, lambda račun, odnosno λ-račun, je formalni sistem dizajniran za ispitivanje definicije funkcije, aplikaciju funkcije, te rekurziju. Lambda račun se može koristiti za precizno definiranje izračunljive funkcije. Pitanje jesu li dva lambda izraza istovjetna ne može biti riješeno općenitim algoritmom. Ovo je bilo prvo pitanje, čak i prije problema zaustavljanja, za kojeg je mogla biti dokazana neodlučivost. Lambda račun je jako utjecao na funkcionalno programske jezike, kao što su Lisp, ML i Haskell.

Lambda račun se slobodno može nazvati najmanjim univerzalnim programskim jezikom. Sastoji se od jednog transformacijskog pravila (supstitucija varijable) i jednog načina definicije funkcije. Lambda račun je univerzalan na način da bilo koja izračunljiva funkcija može biti izražena i evaluirana koristeći njegov formalizam. Ovo je stoga istovjetno formalizmu Turingove mašine. Medutim, lambda račun naglašava transformacijska pravila i ne zamara se stvarnom mašinom koja ih ostvaruje i u tom smislu predstavlja pristup srodniji programskoj podršci nego hardveru.

Ovaj se članak bavi "netipovanim lambda računom" za razliku od u međuvremenu razvijenih tipovanih lambda računa.

Historija

[uredi | uredi izvor]

Lambda račun je uveo Alonzo Church 1930-ih u sklopu istrage o temeljima matematike.[1][2] Za izvorni sistem je se pokazalo da je logički nedosljedan 1935-e kad su Stephen Kleene i J. B. Rosser razvili Kleene–Rosserov paradoks. Zatim, u 1936-oj, Church je izolovao i publicirao samo dio ovoga što je bilo relevantno za izračunavanje. Ovo sada predstavlja netipovani lambda račun.[3] 1940-e godine, Church je također uveo sistem koji je bio računalno slabiji ali logički dosljedan što je sada poznat kao jednostavno tipovani lambda račun.[4]

Neformalni opis

[uredi | uredi izvor]

Formalna definicija

[uredi | uredi izvor]

Također pogledajte

[uredi | uredi izvor]

Literatura

[uredi | uredi izvor]

Monografije/udžbenici za postdiplomce:

  • Morten Heine Sørensen, Pawel Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006, ISBN 0-444-52077-5.
  • Pierce, Benjamin (2002), Types and Programming Languages, MIT Press, ISBN 0-262-16209-1.

Vanjski linkovi

[uredi | uredi izvor]

Reference

[uredi | uredi izvor]
  1. ^ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Druga serija, 33:346–366 (1932).
  2. ^ Za čitavu historiju pogledajte Cardoneov i Hindley-ov "History of Lambda-calculus and Combinatory Logic" (2006).
  3. ^ A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), str. 345-363.
  4. ^ A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).