Lógica combinatoria

Formalismo lógico que utiliza combinadores en lugar de variables

La lógica combinatoria es una notación para eliminar la necesidad de variables cuantificadas en la lógica matemática . Fue introducida por Moses Schönfinkel ^[1] y Haskell Curry ^[2] y se ha utilizado más recientemente en informática como modelo teórico de computación y también como base para el diseño de lenguajes de programación funcional . Se basa en combinadores , que fueron introducidos por Schönfinkel en 1920 con la idea de proporcionar una forma análoga de construir funciones (y eliminar cualquier mención de variables), particularmente en la lógica de predicados . Un combinador es una función de orden superior que utiliza solo la aplicación de la función y combinadores definidos anteriormente para definir un resultado a partir de sus argumentos.

En matemáticas

La lógica combinatoria fue concebida originalmente como una "prelógica" que aclararía el papel de las variables cuantificadas en la lógica, esencialmente eliminándolas. Otra forma de eliminar las variables cuantificadas es la lógica de predicados functores de Quine . Si bien el poder expresivo de la lógica combinatoria normalmente excede al de la lógica de primer orden , el poder expresivo de la lógica de predicados functores es idéntico al de la lógica de primer orden (Quine 1960, 1966, 1976).

El inventor original de la lógica combinatoria, Moses Schönfinkel , no publicó nada sobre lógica combinatoria después de su artículo original de 1924. Haskell Curry redescubrió los combinadores mientras trabajaba como instructor en la Universidad de Princeton a fines de 1927. ^[3] A fines de la década de 1930, Alonzo Church y sus estudiantes en Princeton inventaron un formalismo rival para la abstracción funcional, el cálculo lambda , que resultó más popular que la lógica combinatoria. El resultado de estas contingencias históricas fue que hasta que la ciencia informática teórica comenzó a interesarse en la lógica combinatoria en las décadas de 1960 y 1970, casi todo el trabajo sobre el tema fue realizado por Haskell Curry y sus estudiantes, o por Robert Feys en Bélgica . Curry y Feys (1958) y Curry et al. (1972) examinan la historia temprana de la lógica combinatoria. Para un tratamiento más moderno de la lógica combinatoria y el cálculo lambda en conjunto, consulte el libro de Barendregt , ^[4] que revisa los modelos que Dana Scott ideó para la lógica combinatoria en los años 1960 y 1970.

En informática

En informática , la lógica combinatoria se utiliza como un modelo simplificado de computación , empleado en la teoría de la computabilidad y la teoría de la demostración . A pesar de su simplicidad, la lógica combinatoria captura muchas características esenciales de la computación.

La lógica combinatoria puede ser vista como una variante del cálculo lambda , en el que las expresiones lambda (que representan la abstracción funcional) se reemplazan por un conjunto limitado de combinadores , funciones primitivas sin variables libres . Es fácil transformar expresiones lambda en expresiones de combinadores, y la reducción de combinadores es mucho más simple que la reducción lambda. Por lo tanto, la lógica combinatoria se ha utilizado para modelar algunos lenguajes de programación funcional no estrictos y hardware . La forma más pura de esta visión es el lenguaje de programación Unlambda , cuyos únicos primitivos son los combinadores S y K aumentados con entrada/salida de caracteres. Aunque no es un lenguaje de programación práctico, Unlambda es de cierto interés teórico.

La lógica combinatoria puede recibir diversas interpretaciones. Muchos de los primeros artículos de Curry mostraban cómo traducir los conjuntos de axiomas de la lógica convencional en ecuaciones de lógica combinatoria. ^[5] Dana Scott, en los años 1960 y 1970, mostró cómo combinar la teoría de modelos con la lógica combinatoria.

Resumen del cálculo lambda

El cálculo lambda se ocupa de objetos llamados términos lambda , que pueden representarse mediante las siguientes tres formas de cadenas:

• ⁠ ⁠ ${\displaystyle v}$
• ⁠ ⁠ ${\displaystyle \lambda v.E_{1}}$
• ⁠ ⁠ ${\displaystyle (E_{1}E_{2})}$

donde ⁠ ⁠ ${\displaystyle v}$ es un nombre de variable extraído de un conjunto infinito predefinido de nombres de variables, y ⁠ ⁠ ${\displaystyle E_{1}}$ y ⁠ ⁠ ${\displaystyle E_{2}}$ son términos lambda.

Los términos de la forma ⁠ ⁠ ${\displaystyle \lambda v.E_{1}}$ se denominan abstracciones . La variable v se denomina parámetro formal de la abstracción y ⁠ ⁠ ${\displaystyle E_{1}}$ es el cuerpo de la abstracción. El término ⁠ ⁠ ${\displaystyle \lambda v.E_{1}}$ representa la función que, aplicada a un argumento, vincula el parámetro formal v al argumento y luego calcula el valor resultante de ⁠ ⁠ ${\displaystyle E_{1}}$ —es decir, devuelve ⁠ ⁠ ${\displaystyle E_{1}}$ , con cada ocurrencia de v reemplazada por el argumento.

Los términos de la forma ⁠ ⁠ ${\displaystyle (E_{1}E_{2})}$ se denominan aplicaciones . Las aplicaciones modelan la invocación o ejecución de funciones: se debe invocar la función representada por ⁠ ⁠ , con ${\displaystyle E_{1}}$⁠ ⁠ ${\displaystyle E_{2}}$ como argumento, y se calcula el resultado. Si ⁠ ⁠ ${\displaystyle E_{1}}$ (a veces llamado el aplicando ) es una abstracción, el término puede reducirse : ⁠ ⁠ ${\displaystyle E_{2}}$ , el argumento, puede sustituirse en el cuerpo de ⁠ ⁠ ${\displaystyle E_{1}}$ en lugar del parámetro formal de ⁠ ⁠ ${\displaystyle E_{1}}$ , y el resultado es un nuevo término lambda que es equivalente al anterior. Si un término lambda no contiene subtérminos de la forma ⁠ ⁠ , ${\displaystyle ((\lambda v.E_{1})E_{2})}$ entonces no puede reducirse y se dice que está en forma normal .

La expresión ⁠ ⁠ ${\displaystyle E[v:=a]}$ representa el resultado de tomar el término E y reemplazar todas las ocurrencias libres de v en él con a . Por lo tanto, escribimos

⁠ ⁠ ${\displaystyle ((\lambda v.E)a)\Rightarrow E[v:=a]}$

Por convención, tomamos ⁠ ⁠ ${\displaystyle (abc)}$ como abreviatura de ⁠ ⁠ ${\displaystyle ((ab)c)}$ (es decir, la aplicación se deja asociativa ).

La motivación de esta definición de reducción es que captura el comportamiento esencial de todas las funciones matemáticas. Por ejemplo, considere la función que calcula el cuadrado de un número. Podríamos escribir

El cuadrado de x es ⁠ ⁠ ${\displaystyle x*x}$

(Utilizando " " para ${\displaystyle *}$ indicar multiplicación.) x aquí es el parámetro formal de la función. Para evaluar el cuadrado de un argumento particular, digamos 3, lo insertamos en la definición en lugar del parámetro formal:

El cuadrado de 3 es ⁠ ⁠ ${\displaystyle 3*3}$

Para evaluar la expresión resultante ⁠ ⁠ ${\displaystyle 3*3}$ , tendríamos que recurrir a nuestro conocimiento de la multiplicación y del número 3. Dado que cualquier cálculo es simplemente una composición de la evaluación de funciones adecuadas sobre argumentos primitivos adecuados, este simple principio de sustitución es suficiente para capturar el mecanismo esencial del cálculo. Además, en el cálculo lambda, nociones como '3' y ' ⁠ ⁠ ' ${\displaystyle *}$ pueden representarse sin necesidad de operadores primitivos o constantes definidos externamente. Es posible identificar términos en el cálculo lambda que, cuando se interpretan adecuadamente, se comportan como el número 3 y como el operador de multiplicación, qv codificación de Church .

Se sabe que el cálculo lambda es computacionalmente equivalente en potencia a muchos otros modelos plausibles de computación (incluidas las máquinas de Turing ); es decir, cualquier cálculo que pueda realizarse en cualquiera de estos otros modelos puede expresarse en cálculo lambda, y viceversa. Según la tesis de Church-Turing , ambos modelos pueden expresar cualquier cálculo posible.

Tal vez sea sorprendente que el cálculo lambda pueda representar cualquier cálculo concebible utilizando únicamente las nociones simples de abstracción de funciones y aplicación basada en la simple sustitución textual de términos por variables. Pero aún más notable es que ni siquiera se requiere abstracción. La lógica combinatoria es un modelo de cálculo equivalente al cálculo lambda, pero sin abstracción. La ventaja de esto es que evaluar expresiones en el cálculo lambda es bastante complicado porque la semántica de la sustitución debe especificarse con gran cuidado para evitar problemas de captura de variables. En contraste, evaluar expresiones en lógica combinatoria es mucho más simple, porque no existe la noción de sustitución.

Cálculos combinatorios

Dado que la abstracción es la única forma de crear funciones en el cálculo lambda, algo debe reemplazarla en el cálculo combinatorio. En lugar de la abstracción, el cálculo combinatorio proporciona un conjunto limitado de funciones primitivas a partir de las cuales se pueden crear otras funciones.

Términos combinatorios

Un término combinatorio tiene una de las siguientes formas:

Las funciones primitivas son combinadores , o funciones que, cuando se ven como términos lambda, no contienen variables libres .

Para abreviar las notaciones, una convención general es que ⁠ ⁠ ${\displaystyle (E_{1}E_{2}E_{3}...E_{n})}$ , o incluso ⁠ ⁠ ${\displaystyle E_{1}E_{2}E_{3}...E_{n}}$ , denota el término ⁠ ⁠ ${\displaystyle (...((E_{1}E_{2})E_{3})...E_{n})}$ . Esta es la misma convención general (asociatividad por la izquierda) que para la aplicación múltiple en el cálculo lambda.

Reducción en lógica combinatoria

En lógica combinatoria, cada combinador primitivo viene con una regla de reducción de la forma

( P x ₁ ... x _n ) = E

donde E es un término que menciona únicamente variables del conjunto { x ₁ ... x _n } . Es de esta manera que los combinadores primitivos se comportan como funciones.

Ejemplos de combinadores

El ejemplo más simple de un combinador es I , el combinador identidad, definido por

( yo x ) = x

para todos los términos x . Otro combinador simple es K , que fabrica funciones constantes: ( K x ) es la función que, para cualquier argumento, devuelve x , por lo que decimos

(( Kx ) y ) = x

para todos los términos x e y . O, siguiendo la convención para aplicaciones múltiples,

( K x y ) = x

Un tercer combinador es S , que es una versión generalizada de la aplicación:

( S x yz ) = ( xz ( yz ))

S aplica x a y después de sustituir z en cada uno de ellos. O dicho de otra manera, x se aplica a y dentro del entorno z .

Dados S y K , I en sí mismo es innecesario, ya que puede construirse a partir de los otros dos:

(( SKK ) x )

= ( SKK x )

= ( K x ( K x ))

= x

para cualquier término x . Nótese que aunque (( SKK ) x ) = ( I x ) para cualquier x , ( SKK ) en sí mismo no es igual a I . Decimos que los términos son extensionalmente iguales . La igualdad extensional captura la noción matemática de la igualdad de funciones: que dos funciones son iguales si siempre producen los mismos resultados para los mismos argumentos. En contraste, los términos mismos, junto con la reducción de combinadores primitivos, capturan la noción de igualdad intensional de funciones: que dos funciones son iguales solo si tienen implementaciones idénticas hasta la expansión de combinadores primitivos. Hay muchas formas de implementar una función identidad; ( SKK ) e I están entre estas formas. ( SKS ) es otra más. Usaremos la palabra equivalente para indicar igualdad extensional, reservando igual para términos combinatorios idénticos.

Un combinador más interesante es el combinador de punto fijo o combinador Y , que puede utilizarse para implementar la recursión .

Integridad de la base SK

S y K pueden ser compuestos para producir combinadores que sean extensionalmente iguales a cualquier término lambda y, por lo tanto, según la tesis de Church, a cualquier función computable. La prueba consiste en presentar una transformación, T [ ] , que convierte un término lambda arbitrario en un combinador equivalente.

T [ ] puede definirse de la siguiente manera:

1. T [ x ] ⇒x
2. T [( E₁E₂ ) ] ⇒ ( T [ E₁ ] T [ E₂ ] )
3. T [ λx . E ] ⇒ ( K T [ E ]) (si x no aparece libre en E )
4. T [ λx.x ] ⇒ I​
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (si x aparece libre en E )
6. T [ λx .( E ₁ E ₂)] ⇒ ( S T [ λx . E ₁] T [ λx . E₂ ]) (si x aparece libre en E ₁ o E ₂)

Nótese que T [ ] tal como se da no es una función matemática bien tipificada, sino más bien un reescritor de términos: aunque eventualmente produce un combinador, la transformación puede generar expresiones intermedias que no son términos lambda ni combinadores, a través de la regla (5).

Este proceso también se conoce como eliminación de abstracción . Esta definición es exhaustiva: cualquier expresión lambda estará sujeta a exactamente una de estas reglas (ver Resumen del cálculo lambda más arriba).

Está relacionado con el proceso de abstracción de corchetes , que toma una expresión E construida a partir de variables y aplicaciones y produce una expresión de combinador [x]E en la que la variable x no es libre, de modo que [ x ] E x = E se cumple. Un algoritmo muy simple para la abstracción de corchetes se define por inducción sobre la estructura de expresiones de la siguiente manera: ^[6]

1. [ x ] y  := K y
2. [ x ] x  := yo
3. [ x ]( E₁ E₂ ) := S ([ x ] E₁ )([ x ] E₂ )

La abstracción entre corchetes induce una traducción de términos lambda a expresiones combinadoras, interpretando abstracciones lambda utilizando el algoritmo de abstracción entre corchetes.

Conversión de un término lambda en un término combinatorio equivalente

Por ejemplo, convertiremos el término lambda λx . λy .( y x ) en un término combinatorio:

T [ λx.λy. ( yx ) ] ​​

= T [ λx . T [ λy .( y x )]] (por 5)

= T [ λx .( S T [ λy . y ] T [ λy . x ])] (por 6)

= T [ λx .( SI T [ λy . x ])] (por 4)

= T [ λx .( SI ( K T [ x ]))] (por 3)

= T [ λx .( SI ( K x ))] (por 1)

= ( S T [ λx .( SI )] T [ λx .( K x )]) (por 6)

= ( S ( K ( SI )) T [ λx .( K x )]) (por 3)

= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . x ])) (por 6)

= ( S ( K ( SI )) ( S ( KK ) T [ λx . x ])) (por 3)

= ( S ( K ( SI )) ( S ( KK ) I )) (por 4)

Si aplicamos este término combinatorio a cualesquiera dos términos x e y (introduciéndolos en forma de cola en el combinador 'desde la derecha'), se reduce de la siguiente manera:

( S ( K ( S I ) ) ( S ( K K ) I ) xy)

= ( K ( S I ) x ( S ( K K ) I x) y)

= ( S I ( S ( K K ) I x) y)

= ( yo y ( S ( K K ) yo xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (y( Ix ))

= (yx)

La representación combinatoria, ( S ( K ( SI )) ( S ( KK ) I )) es mucho más larga que la representación como término lambda, λx . λy .(yx). Esto es típico. En general, la construcción T [ ] puede expandir un término lambda de longitud n a un término combinatorio de longitud Θ ( n ³ ). ^[7]

Explicación de layo[ ] transformación

La transformación T [ ] está motivada por el deseo de eliminar la abstracción. Dos casos especiales, las reglas 3 y 4, son triviales: λx . x es claramente equivalente a I , y λx . E es claramente equivalente a ( K T [ E ]) si x no aparece libre en E .

Las dos primeras reglas también son simples: las variables se convierten en sí mismas, y las aplicaciones, que están permitidas en términos combinatorios, se convierten en combinadores simplemente convirtiendo el aplicando y el argumento en combinadores.

Las reglas 5 y 6 son las que nos interesan. La regla 5 simplemente dice que para convertir una abstracción compleja en un combinador, primero debemos convertir su cuerpo en un combinador y luego eliminar la abstracción. La regla 6 en realidad elimina la abstracción.

λx .( E ₁ E ₂) es una función que toma un argumento, digamos a , y lo sustituye en el término lambda ( E ₁ E ₂) en lugar de x , dando como resultado ( E ₁ E ₂)[ x  : = a ]. Pero sustituir a en ( E ₁ E ₂) en lugar de x es lo mismo que sustituirlo tanto en E ₁ como en E ₂, por lo que

( mi ₁ mi ₂)[ x  := a ] = ( mi ₁[ x  := a ] mi ₂[ x  := a ])

( λx .( E ₁ E ₂) a ) = (( λx . E ₁ a ) ( λx . E ₂ a ))

= ( S λx . E ₁ λx . E ₂ a )

= (( S λx . E₁ λx . E ₂) a )

Por igualdad extensional,

λx .( mi ₁ mi ₂) = ( S λx . mi ₁ λx . mi ₂)

Por lo tanto, para encontrar un combinador equivalente a λx .( E ₁ E ₂), es suficiente encontrar un combinador equivalente a ( S λx . E ₁ λx . E ₂), y

( ST [ λx . E ₁] T [ λx . E ₂] )

Evidentemente, se ajusta al proyecto. E ₁ y E ₂ contienen cada uno estrictamente menos aplicaciones que ( E ₁ E ₂), por lo que la recursión debe terminar en un término lambda sin ninguna aplicación, ya sea una variable o un término de la forma λx . E .

Simplificaciones de la transformación

η-reducción

Los combinadores generados por la transformación T [ ] se pueden hacer más pequeños si tenemos en cuenta la regla de η-reducción :

T [ λx .( E x )] = T [ E ] (si x no es libre en E )

λx .( E x ) es la función que toma un argumento, x , y le aplica la función E ; esta es extensionalmente igual a la función E misma. Por lo tanto, es suficiente convertir E a forma combinatoria.

Teniendo en cuenta esta simplificación, el ejemplo anterior se convierte en:

  T [ λx.λy. ( yx ) ]​​

= ...

= ( S ( K ( SI )) T [ λx .( K x )])

= ( S ( K ( SI )) K ) (por η-reducción)

Este combinador es equivalente al anterior, más largo:

  ( S ( K ( SI )) K x y )

= ( K ( SI ) x ( K x ) y )

= ( SI ( K x ) y )

= ( yo y ( k x y ))

= ( y ( K x y ))

= ( y x )

De manera similar, la versión original de la transformación T [ ] transformó la función identidad λf . λx .( f x ) en ( S ( S ( KS ) ( S ( KK ) I )) ( KI )). Con la regla de η-reducción, λf . λx .( f x ) se transforma en I .

Base de un punto

Existen bases de un punto a partir de las cuales se puede componer todo combinador de manera extensional igual a cualquier término lambda. El ejemplo más simple de una base de este tipo es { X } donde:

X ≡ λx .((x S ) K )

No es difícil comprobar que:

X ( X ( X X )) = ^β K y

X ( X ( X ( X X ))) = ^β S .

Dado que { K , S } es una base, se deduce que { X } también es una base. El lenguaje de programación Iota utiliza X como su único combinador.

Otro ejemplo sencillo de una base de un punto es:

X' ≡ λx .(x K S K ) con

( X' X' ) X' = ^β K y

X' ( X' X' ) = ^β S

De hecho, existen infinitas bases de este tipo. ^[8]

Combinadores B, C

Además de S y K , Schönfinkel (1924) incluyó dos combinadores que ahora se denominan B y C , con las siguientes reducciones:

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

También explica cómo a su vez pueden expresarse utilizando sólo S y K :

B = ( S ( KS ) K )

C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

Estos combinadores son extremadamente útiles cuando se traduce la lógica de predicados o el cálculo lambda en expresiones de combinadores. También fueron utilizados por Curry y mucho más tarde por David Turner , cuyo nombre se ha asociado con su uso computacional. Al utilizarlos, podemos extender las reglas para la transformación de la siguiente manera:

1. T [ x ] ⇒x
2. T [( E₁E₂ )] ⇒ ( T [ E₁ ] T [ E₂ ] )
3. T [ λx . E ] ⇒ ( K T [ E ]) (si x no es libre en E )
4. T [ λx.x ] ⇒ I​
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (si x es libre en E )
6. T [ λx .( E₁ E₂ )] ⇒ ( S T [ λx . E₁ ] T [ λx . E₂ ]) (si x es libre tanto en E₁ como en E₂ )
7. T [ λx .( E₁ E₂ )] ⇒ ( C T [ λx . E₁ ] T [ E₂ ]) (si x es libre en E₁ pero no en E₂ )
8. T [ λx .( E₁ E₂ )] ⇒ ( B T [ E₁ ] T [ λx . E₂ ]) (si x es libre en E₂ pero no en E₁ )

Usando los combinadores B y C , la transformación de λx . λy .( y x ) se ve así:

  T [ λx.λy. ( yx ) ]​​

= T [ λx.T [ λy . ( yx ) ] ]

= T [ λx .( C T [ λy . y ] x )] (por la regla 7)

= T [ λx .( C I x )]

= ( C I ) (η-reducción)

${\displaystyle =\mathbf {C} _{*}}$(notación canónica tradicional: ) ${\displaystyle \mathbf {X} _{*}=\mathbf {XI} }$

${\displaystyle =\mathbf {I} '}$(notación canónica tradicional: ) ${\displaystyle \mathbf {X} '=\mathbf {CX} }$

Y, de hecho, ( C I x y ) se reduce a ( y x ):

  ( C I x y )

= ( yo y x )

= ( y x )

La motivación aquí es que B y C son versiones limitadas de S. Mientras que S toma un valor y lo sustituye tanto en el aplicando como en su argumento antes de realizar la aplicación, C realiza la sustitución solo en el aplicando y B solo en el argumento.

Los nombres modernos de los combinadores provienen de la tesis doctoral de Haskell Curry de 1930 (véase Sistema B, C, K, W ). En el artículo original de Schönfinkel , lo que ahora llamamos S , K , I , B y C se llamaban S , C , I , Z y T respectivamente.

La reducción en el tamaño del combinador que resulta de las nuevas reglas de transformación también se puede lograr sin introducir B y C , como se demuestra en la Sección 3.2 de Tromp (2008).

CL_Kcontra CL_Icálculo

Se debe hacer una distinción entre el cálculo CL _K descrito en este artículo y el cálculo CL _I. La distinción corresponde a la que se hace entre el cálculo λ _K y el cálculo λ _I. A diferencia del cálculo λ _K , el cálculo λ _I restringe las abstracciones a:

λx . E donde x tiene al menos una ocurrencia libre en E .

En consecuencia, el combinador K no está presente en el cálculo λ _I ni en el cálculo CL _{I. Las constantes de} CL _I son: I , B , C y S , que forman una base a partir de la cual se pueden componer todos los términos CL _{I (módulo igualdad). Cada término λ I} se puede convertir en un combinador CL _I igual de acuerdo con reglas similares a las presentadas anteriormente para la conversión de términos λ _K en combinadores CL _{K. Véase el capítulo 9 en Barendregt (1984).}

Conversión inversa

La conversión L [ ] de términos combinatorios a términos lambda es trivial:

L [ I ] = λx.x​

L [ K ] = λx.λy.x​​​

L [ C ] = λx.λy.λz. ( xzy )​​​​ ​

L [ B ] = λx . λy . λz .( x ( y z ))

L [ S ] = λx . λy . λz .( x z ( y z ))

L [( E₁ E₂ )] = ( L [ E₁ ] L [ E₂ ])

Tenga en cuenta, sin embargo, que esta transformación no es la transformación inversa de ninguna de las versiones de T [ ] que hemos visto.

Indecidibilidad del cálculo combinatorio

Una forma normal es cualquier término combinatorio en el que los combinadores primitivos que aparecen, si los hay, no se aplican a suficientes argumentos como para simplificarlos. No se puede decidir si un término combinatorio general tiene una forma normal; si dos términos combinatorios son equivalentes, etc. Esto se puede demostrar de forma similar a los problemas correspondientes para los términos lambda.

Indefinibilidad por predicados

Los problemas indecidibles anteriores (equivalencia, existencia de forma normal, etc.) toman como entrada representaciones sintácticas de términos bajo una codificación adecuada (por ejemplo, codificación Church). También se puede considerar un modelo de cálculo trivial de juguete donde "calculamos" propiedades de términos por medio de combinadores aplicados directamente a los términos mismos como argumentos, en lugar de a sus representaciones sintácticas. Más precisamente, sea un predicado un combinador que, cuando se aplica, devuelve T o F (donde T y F representan las codificaciones Church convencionales de verdadero y falso, λx . λy . x y λx . λy . y , transformadas en lógica combinatoria; las versiones combinatorias tienen T = K y F = ( K I ) ). Un predicado N es no trivial si hay dos argumentos A y B tales que N A = T y N B = F . Un combinador N es completo si N M tiene una forma normal para cada argumento M . Un análogo del teorema de Rice para este modelo de juguete dice entonces que todo predicado completo es trivial. La prueba de este teorema es bastante simple. ^[9]

Prueba

Por reducción al absurdo. Supongamos que hay un predicado completo no trivial, digamos N. Como se supone que N no es trivial, existen combinadores A y B tales que

( N A ) = T y

( NB ) = F.​

Defina NEGACIÓN ≡ λx .(si ( N x ) entonces B de lo contrario A ) ≡ λx .(( N x ) B A )

Definir ABSURDO ≡ ( Y NEGACIÓN)

El teorema del punto fijo da: ABSURDO = (NEGACIÓN ABSURDO), para

ABSURDO ≡ ( Y NEGACIÓN) = (NEGACIÓN ( Y NEGACIÓN)) ≡ (NEGACIÓN ABSURDO).

Porque se supone que N está completo:

1. ( N ABSURDO) = Para
2. ( N ABSURDO) = T

• Caso 1: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T , una contradicción.
• Caso 2: T = ( N ABSURDO) = N (NEGACIÓN ABSURDO) = ( N B ) = F , nuevamente una contradicción.

Por lo tanto ( N ABSURDUM) no es ni V ni F , lo que contradice la presuposición de que N sería un predicado completo no trivial. QED

De este teorema de indefinibilidad se sigue inmediatamente que no existe ningún predicado completo que pueda discriminar entre términos que tienen una forma normal y términos que no la tienen. También se sigue que no existe ningún predicado completo, digamos IGUAL, tal que:

(IGUAL AB ) = T si A = B y

(IGUAL AB ) = F si A ≠ B .

Si existiera IGUAL, entonces para todo A , λx. (IGUAL x A ) tendría que ser un predicado completo no trivial.

Sin embargo, tenga en cuenta que también se sigue inmediatamente de este teorema de indefinibilidad que muchas propiedades de términos que son obviamente decidibles tampoco son definibles por predicados completos: por ejemplo, no hay ningún predicado que pueda decir si la primera letra de función primitiva que aparece en un término es una K. Esto muestra que la definibilidad por predicados no es un modelo razonable de decidibilidad.

Aplicaciones

Recopilación de lenguajes funcionales

David Turner utilizó sus combinadores para implementar el lenguaje de programación SASL .

Kenneth E. Iverson utilizó primitivas basadas en los combinadores de Curry en su lenguaje de programación J , sucesor de APL . Esto permitió lo que Iverson llamó programación tácita , es decir, programación en expresiones funcionales que no contienen variables, junto con herramientas poderosas para trabajar con dichos programas. Resulta que la programación tácita es posible en cualquier lenguaje similar a APL con operadores definidos por el usuario. ^[10]

Lógica

El isomorfismo de Curry-Howard implica una conexión entre la lógica y la programación: cada demostración de un teorema de lógica intuicionista corresponde a una reducción de un término lambda tipificado, y viceversa. Además, los teoremas pueden identificarse con firmas de tipo de función. En concreto, una lógica combinatoria tipificada corresponde a un sistema de Hilbert en teoría de demostraciones .

Los combinadores K y S corresponden a los axiomas

AK : A → ( B → A ),

COMO : ( A → ( B → C )) → (( A → B ) → ( A → C )),

y la aplicación de la función corresponde a la regla del desapego (modus ponens)

MP : de A y A → B se infiere B.

El cálculo que consta de AK , AS y MP está completo para el fragmento implicacional de la lógica intuicionista, que puede verse de la siguiente manera. Considérese el conjunto W de todos los conjuntos de fórmulas deductivamente cerrados, ordenados por inclusión . Entonces es un marco de Kripke intuicionista , y definimos un modelo en este marco por ${\displaystyle \langle W,\subseteq \rangle }$ ${\displaystyle \Vdash }$

${\displaystyle X\Vdash A\iff A\in X.}$

Esta definición obedece a las condiciones de satisfacción de →: por un lado, si , y es tal que y , entonces por modus ponens. Por otro lado, si , entonces por el teorema de deducción , por lo tanto la clausura deductiva de es un elemento tal que , , y . ${\displaystyle X\Vdash A\to B}$ ${\displaystyle Y\in W}$ ${\displaystyle Y\supseteq X}$ ${\displaystyle Y\Vdash A}$ ${\displaystyle Y\Vdash B}$ ${\displaystyle X\not \Vdash A\to B}$ ${\displaystyle X,A\not \vdash B}$ ${\displaystyle X\cup \{A\}}$ ${\displaystyle Y\in W}$ ${\displaystyle Y\supseteq X}$ ${\displaystyle Y\Vdash A}$ ${\displaystyle Y\not \Vdash B}$

Sea A cualquier fórmula que no sea demostrable en el cálculo. Entonces A no pertenece a la clausura deductiva X del conjunto vacío, por lo tanto , y A no es válida desde el punto de vista intuicionista. ${\displaystyle X\not \Vdash A}$

Véase también

• Sistemas de computación aplicativos
• Sistema B, C, K, W
• Máquina abstracta categórica
• Gramática categorial combinatoria
• Sustitución explícita
• Combinador de punto fijo
• Máquina de reducción de gráficos
• Cálculo lambda y álgebra cilíndrica , otros enfoques para modelar la cuantificación y eliminar variables
• Cálculo combinador SKI
• Supercombinador
• Burlarse de un ruiseñor

Referencias

1. Schönfinkel 1924, El artículo que fundó la lógica combinatoria. Traducción al español: Schönfinkel (1967).
2. Curry 1930.
3. Seldin 2008.
4. Barendregt 1984.
5. Hindley y Meredith 1990.
6. Turner 1979.
7. Lachowski 2018.
8. Goldberg 2004.
9. Engeler 1995.
10. Cherlín 1991.

Literatura

• Barendregt, Hendrik Pieter (1984). El cálculo lambda, su sintaxis y semántica. Estudios de lógica y fundamentos de las matemáticas . Vol. 103. Holanda del Norte . ISBN 0-444-87508-5.
• Cherlin, Edward (1991). "Funciones puras en APL y J". Actas de la conferencia internacional sobre APL '91 - APL '91 . págs. 88–93. doi :10.1145/114054.114065. ISBN 0897914414. Número de identificación del sujeto  25802202.
• Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [Fundamentos de la lógica combinatoria]. American Journal of Mathematics (en alemán). 52 (3). The Johns Hopkins University Press: 509–536. doi :10.2307/2370619. JSTOR  2370619.
• Curry, Haskell Brooks ; Feys, Robert (1958). Combinatory Logic . Vol. I. Ámsterdam: Holanda Septentrional. ISBN 0-7204-2208-6.
• Curry, Haskell Brooks ; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Combinatory Logic . Vol. II. Ámsterdam: Holanda Septentrional. ISBN. 0-7204-2208-6.
• Engeler, E. (1995). El programa combinatorio (PDF) . Birkhäuser. págs. 5–6.
• Field, Anthony J.; Harrison, Peter G. (1998). Programación funcional . Addison-Wesley. ISBN 0-201-19249-7.
• Goldberg, Mayer (2004). "Una construcción de bases de un punto en cálculos lambda extendidos". Information Processing Letters . 89 (6): 281–286. doi :10.1016/j.ipl.2003.12.005.
• Hindley, J. Roger ; Meredith, David (1990). "Principales esquemas de tipos y desprendimiento condensado". Journal of Symbolic Logic . 55 (1): 90–105. doi :10.2307/2274956. JSTOR  2274956. MR  1043546. S2CID  6930576.
• Hindley, J. Roger ; Seldin, Jonathan P. (2008) [1986]. Cálculo lambda y combinadores: una introducción (2.ª ed.). Cambridge University Press . ISBN 9780521898850.
• Lachowski, Łukasz (2018). "Sobre la complejidad de la traducción estándar del cálculo lambda a la lógica combinatoria". Reports on Mathematical Logic . 2018 (53): 19–42. doi : 10.4467/20842589RM.18.002.8835 . Consultado el 9 de septiembre de 2018 .
• Paulson, Lawrence C. (1995). Fundamentos de programación funcional. Universidad de Cambridge.
• Quine, Willard Van Orman (1960). "Variables explained away". Actas de la American Philosophical Society . 104 (3): 343–347. JSTOR  985250. Reimpreso como Capítulo 23 de Quine (1996)
• Quine, Willard Van Orman (1996) [1960]. "Variables explicadas". Selected Logic Papers (edición inicial, segunda edición impresa). Cambridge, Mass.: Harvard University Press . pp. 227–235. ISBN 9780674798373.
• Schönfinkel, Moisés (1924). "Über die Bausteine ​​der mathematischen Logik" (PDF) . Mathematische Annalen (en alemán). 92 (3–4): 305–316. doi :10.1007/bf01448013. S2CID  118507515. El artículo que fundó la lógica combinatoria. Traducción al inglés: Schönfinkel (1967)
• Schönfinkel, Moisés (1967) [1924]. Van Heijenoort, Jean (ed.). Über die Bausteine ​​der mathematischen Logik [ Sobre los componentes básicos de la lógica matemática ]. De Frege a Gödel: un libro de consulta sobre lógica matemática, 1879-1931. Traducido por Bauer-Mengelberg, Stefan. Cambridge, MA, EE.UU.: Harvard University Press . págs. 355–366. ISBN 978-0674324497.OCLC 503886453  .
• Seldin, Jonathan P. (3 de marzo de 2008). "La lógica de Curry y la Iglesia" (PDF) . Consultado el 17 de septiembre de 2023 .
• Smullyan, Raymond (1985). Burlarse de un ruiseñor y otros acertijos lógicos, incluida una asombrosa aventura en lógica combinatoria . Knopf. ISBN 0-394-53491-3Una introducción suave a la lógica combinatoria, presentada como una serie de rompecabezas recreativos que utilizan metáforas de observación de aves .
• Smullyan, Raymond (1994). Diagonalización y autorreferencia . Guías de lógica de Oxford. Vol. 27. Oxford y Nueva York: Oxford University Press . ISBN 978-0198534501Los capítulos 17 a 20 son una introducción más formal a la lógica combinatoria, con un énfasis especial en los resultados de punto fijo.
• Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. Lecciones sobre el isomorfismo de Curry-Howard (PDF) . Estudios de lógica y fundamentos de las matemáticas. Vol. 149 (1.ª ed.). Elsevier . pág. 442. ISBN 978-0444520777Archivado desde el original (PDF) el 16 de octubre de 2005. Consultado el 22 de abril de 2017 .
• Tromp, John (2008). "Cálculo lambda binario y lógica combinatoria" (PDF) . En Calude, Cristian S. (ed.). Aleatoriedad y complejidad, de Leibniz a Chaitin . World Scientific Publishing Company. Archivado desde el original (PDF) el 4 de marzo de 2016.
• Turner, David A. (1979). "Otro algoritmo para la abstracción de corchetes". The Journal of Symbolic Logic . 44 (2): 267–270. doi :10.2307/2273733. JSTOR  2273733. S2CID  35835482.
• Wolfengagen, VE (2003). Lógica combinatoria en programación: cálculos con objetos mediante ejemplos y ejercicios (2.ª ed.). Moscú: "Center JurInfoR" Ltd. ISBN 5-89158-101-9.
• Wolfram, Stephen (2021). Combinadores: una visión centenaria. Wolfram Media . ISBN 978-1-57955-043-1Una celebración del desarrollo de los combinadores, cien años después de que fueran introducidos por Schönfinkel (1924 )(Libro electrónico: ISBN 978-1-57955-044-8 ) 

Enlaces externos

• Enciclopedia de Filosofía de Stanford : "Lógica combinatoria" de Katalin Bimbó .
• Notas en bloque de Curry, 1920-1931.
• Keenan, David C. (2001) "Para diseccionar un sinsonte: una notación gráfica para el cálculo lambda con reducción animada".
• Rathman, Chris, "Combinator Birds". Una tabla que destila gran parte de la esencia de Smullyan (1985).
• Combinadores de arrastrar y soltar (Applet de Java)
• Cálculo Lambda Binario y Lógica Combinatoria.
• Servidor web de reducción lógica combinatoria
• Wolfram, Stephen (29 de abril de 2020). Combinators: celebración del centenario. Wolfram Physics Project en YouTube . Consultado el 26 de septiembre de 2023 .