Llògica combinatòria

La llògica combinatòria és la llògica última i com tal pot ser un model simplificat del còmput, usat en la teoria de la computabilidad (l'estudi de qué pot ser computat) i la teoria de la prova (l'estudi de qué es pot provar matemàticament).

Introducció

La teoria, a causa de la seua simplicitat, captura les característiques essencials de la naturalea del còmput. La llògica combinatòria (LC) és el fonament del càlcul lambda, en eliminar l'últim tipo de variable d'este: la variable lambda. En LC les expressions lambda (usades per a permetre l'abstracció funcional) són substituidas per un sistema llimitat de combinadores, les funcions primitives que no contenen cap variable lliure (ni lligada). És fàcil transformar expressions lambda en expressions combinatòries, i lloc que la reducció d'un combinador és més simple que la reducció lambda, LC s'ha utilisat com la base per a la posada en pràctica d'alguns llenguages de programació funcionals no-estrictes en software i hardware.

Sumari del càlcul lambda

El càlcul lambda es referix a objectes cridats lambda-térmens, que són cadenes de símbols d'una de les formes següents:

• v
• λv.E1
• (E1 E2)

a on v és un nom de variable pres d'un conjunt infinit predefinit de noms de variables, i E1 i E2 són lambda-térmens. Els térmens de la forma λv.E1 són cridades abstracció. La variable ν es diu el paràmetro formal de l'abstracció, i E1 és el cos de l'abstracció.

El terme λv.E1 representa la funció que, si és aplicada a un argument, lliga el paràmetro formal v a l'argument i llavors computa el valor resultant de E1--- açò és, retorna E1, en cada ocurrència de ν substituido per l'argument.

Els térmens de la forma (E1 E2) són cridats aplicacions. Les aplicacions modelen l'invocació o eixecució d'una funció: La funció representada per E1 és invocada, en E2 com el seu argument, i es computa el resultat. Si E1 (a voltes cridat l'aplicant) és una abstracció, el terme pot ser reduït: E2, l'argument, es pot substituir en el cos de E1 en lloc del paràmetro formal de E1, i el resultat és un nou terme lambda que és equivalent a l'antic. Si un terme lambda no conté cap subtérmino de la forma (λv.E1 E2) llavors no pot ser reduït, i es diu que està en forma normal.

L'expressió I[a/v] representa el resultat de prendre el terme I i substituyendo totes les ocurrències lliures de v pel a. Escrivim aixina

(λv.I a) ⇒ I[a/v] 

per convenció, prenem (b c d... z) com a abreviatura per a (... (((a b) c) d)... z). (Regla d'associació per esquerra).

La motivació per a esta definició de la reducció és que captura el comportament essencial de totes les funcions matemàtiques. Per eixemple, considere's la funció que computa el quadrat d'un número. Es pot escriure el quadrat de x és xx (usant "*" per a indicar la multiplicació.) x ací és el paràmetro formal de la funció. Per a evaluar el quadrat per a un argument particular, digam 3, ho insertem en la definició en lloc del paràmetro formal:

El quadrat de 3 és 3*3

per a evaluar l'expressió que resulta 3*3, tindríem que recórrer al nostre coneiximent de la multiplicació i del número 3. ya que qualsevol còmput és simplement una composició de l'evaluació de funcions adequades en arguments primitius adequats, este principi simple de substitució és suficient per a capturar el mecanisme essencial del còmput. Per una atra part, en el càlcul lambda, nocions tals com '3' i '*' pot ser representat sense cap necessitat d'operadors primitius externament definits o de constants. És possible identificar els térmens que en el càlcul lambda, quan estan interpretats convenientment, es comporten com el número 3 i l'operador de la multiplicació.

El càlcul lambda és computacionalment equivalent en poder a molts atres models plausibles per al còmput (màquines de Turing incloses); és dir, qualsevol càlcul que es puga conseguir en qualssevol d'estos atres models es pot expressar en el càlcul lambda, i viceversa. Segons la tesis de Church-Turing, abdós models poden expressar qualsevol còmput possible. Potser semble sorprenent que el càlcul lambda puga representar qualsevol còmput concebible usant solament les nocions simples d'abstracció funcional i aplicació basat en la substitució textual simple de térmens per variables. Pero encara més notable és que inclús l'abstracció no és requerible. La Llògica Combinatòria és un model del còmput equivalent al càlcul lambda, pero sense l'abstracció.

Vore també

• Haskell Curry

• Paradoxa de Curry