Càlcul lambda

De Viquipèdia

El càlcul lambda és un sistema formal dissenyat per investigar la definició de funció, la noció d'aplicacions de funcions i la recursió. Fou introduït per Alonzo Church i Stephen Kleene a la dècada de 1930; Church va usar el càlcul lambda al 1936 per resoldre el Entscheidungsproblem. Pot ser usat per definir de manera neta i precisa què és una “funció computable”.

Church va resoldre negativament el Entscheidungsproblem: va provar que no hi ha algorisme que pugui ser considerat com una "solució" al Entscheidungsproblem.

El càlcul lambda ha influït enormement en el disseny de llenguatges de programació funcionals, especialment LISP.

Es pot considerar al càlcul lambda com el més petit llenguatge universal de programació. Consisteix en una regla de transformació simple (substitució de variables) i un esquema simple per definir funcions.

El càlcul lambda és universal perquè qualsevol funció computable pot ser expressada i avaluada mitjançant ell. Per tant, és equivalent a les màquines de Turing. Tot i això, el càlcul lambda no fa èmfasi en l'ús de regles de transformació i no considera les màquines reals que puguin implementar-lo. Es tracta doncs d'una proposta més propera al software que al hardware.