Lógica combinatoria

La lógica combinatoria es una notación que elimina la necesidad de variables cuantificadas en la lógica matemática . Fue introducida por Moses Schönfinkel ^{[ 1 ]} y Haskell Curry ^{[ 2 ]} , y más recientemente se ha utilizado en informática como un 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 , 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 únicamente la aplicación de funciones y combinadores definidos previamente para definir un resultado a partir de sus argumentos.

En matemáticas

La lógica combinatoria se concibió 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 funtores de predicados de Quine . Si bien el poder expresivo de la lógica combinatoria suele superar al de la lógica de primer orden , el poder expresivo de la lógica de funtores de predicados es idéntico al de la lógica de primer orden ( Quine 1960, 1966, 1976 ).

El inventor 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 finales de 1927. ^{[ 3 ]} A finales 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 de la computación teórica comenzó a interesarse por 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, véase el libro de Barendregt , ^{[ 4 ]} que revisa los modelos que Dana Scott ideó para la lógica combinatoria en las décadas de 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 considerarse una variante del cálculo lambda , en la 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 combinatorias, y la reducción combinatoria es mucho más sencilla 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 , cuyas únicas primitivas son los combinadores S y K, complementados con entrada/salida de caracteres. Aunque no es un lenguaje de programación práctico, Unlambda tiene cierto interés teórico.

La lógica combinatoria admite diversas interpretaciones. Muchos de los primeros trabajos de Curry mostraron cómo traducir conjuntos de axiomas de la lógica convencional a ecuaciones de lógica combinatoria. ^{[ 5 ]} Dana Scott, en las décadas de 1960 y 1970, demostró 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:

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

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

Términos del formulario $\lambda v.E_{1}$ se denominan abstracciones . La variable $v$ se denomina parámetro formal de la abstracción, y $E_{1}$ es el cuerpo de la abstracción. El término $\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 $E_{1}$ — es decir, regresa $E_{1}$ , con cada ocurrencia de $v$ reemplazado por el argumento.

Términos del formulario $E_{1}E_{2}$ se denominan aplicaciones . Las aplicaciones modelan la invocación o ejecución de funciones: la función representada por $E_{1}$ debe ser invocado, con $E_{2}$ como su argumento, y se calcula el resultado. Si $E_{1}$ (a veces llamado el solicitante ) es una abstracción, el término puede reducirse : $E_{2}$ , el argumento, puede ser sustituido en el cuerpo de $E_{1}$ en lugar del parámetro formal de $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 se puede reducir y se dice que está en forma normal .

La expresión $E[v:=a]$ representa el resultado de tomar el término $E$ y reemplazando todas las ocurrencias libres de $v$ en él con $a$ Así escribimos.

((\lambda vE)a)\Rightarrow E[v:=a]

Por convención, tomamos $(abc)$ como abreviatura de $((ab)c)$ (es decir, la aplicación es asociativa por la izquierda ).

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

El cuadrado de

x

es

x*x

(Usando " $*$ " para indicar multiplicación.) $x$ Aquí está 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

3*3

Para evaluar la expresión resultante $3*3$ , tendríamos que recurrir a nuestro conocimiento de la multiplicación y el 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 sencillo principio de sustitución basta para capturar el mecanismo esencial del cálculo. Además, en el cálculo lambda, nociones como '3' y ' $*$ ' puede 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 computación posible.

Resulta sorprendente que el cálculo lambda pueda representar cualquier computación imaginable utilizando únicamente las nociones simples de abstracción de funciones y su 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 computación equivalente al cálculo lambda, pero sin abstracción. La ventaja de esto radica en que evaluar expresiones en el cálculo lambda es bastante complejo, ya que la semántica de la sustitución debe especificarse con sumo cuidado para evitar problemas de captura de variables. En contraste, evaluar expresiones en la lógica combinatoria es mucho más sencillo, puesto que no existe la noción de sustitución.

Cálculo combinatorio

Dado que la abstracción es la única forma de construir 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 construir otras funciones.

Términos combinatorios

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

Las funciones primitivas son combinadores , o funciones que, vistas 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 $(...((E_{1}E_{2})E_{3})...E_{n})$ . Esta es la misma convención general (asociatividad 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_{1}\dots x_{n})=E

dónde $E$ es un término que menciona solo variables del conjunto $\{x_{1}\dots 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 de identidad, definido por

(I\ x)=x

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

((K\ x)\ y)=x

para todos los términos $x$ y $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\ y\ z)=(x\ z\ (y\ z))

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

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

((S\,K\,K)\,x)

=(S\,K\,K)\,x

=K\,x\,(K\,x)

=x

para cualquier término $x$ . Tenga en cuenta que aunque $((S\,K\,K)\,x)=(Ix)$ para cualquier $x$ , $(S\,K\,K)$ 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 igualdad de funciones: que dos funciones se consideran 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 se consideran iguales solo si tienen implementaciones idénticas hasta la expansión de combinadores primitivos. Hay muchas maneras de implementar una función identidad ; $(S\,K\,K)$ y $I$ están entre estas formas. $(S\,K\,S)$ es otro ejemplo. Usaremos la palabra equivalente para referirnos a la igualdad extensional.

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

Integridad de la base SK

S y K pueden combinarse para producir combinadores que son extensionalmente iguales a cualquier término lambda y, por lo tanto, según la tesis de Church, a cualquier función computable . La demostración 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:

T [ x ] ⇒ x
T [( E ₁E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
T [ λx . E ] ⇒ ( K T [ E ]) (si x no aparece libre en E )
T [ λx . x ] ⇒ I
T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (si x aparece libre en E )
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 ni términos lambda ni combinadores, según 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 (véase el 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 aplicación y produce una expresión combinadora [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 las expresiones de la siguiente manera: ^{[ 6 ]}

[ x ] y := K y
[ x ] x := yo
[ x ]( mi ₁mi ₂ ) := S ([ x ] mi ₁ )([ x ] mi ₂ )

La abstracción mediante corchetes induce una traducción de términos lambda a expresiones combinatorias, interpretando las abstracciones lambda mediante el algoritmo de abstracción mediante corchetes.

Conversión de un término lambda a un término combinatorio equivalente.

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

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

= 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 el combinador de forma similar a una cola, "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)

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

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

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

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

= (y ( I x))

= (yx)

La representación combinatoria, ( S ( K ( SI )) ( S ( KK ) I )) es mucho más larga que la representación como un 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 la transformación T [ ]

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 sencillas: 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 aplicadondo y el argumento en combinadores.

Las reglas 5 y 6 son las que nos interesan. La regla 5 simplemente establece 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 cambio, 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 , lo que produce ( 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 .( mi ₁mi ₂ ) a ) = (( λx . mi ₁a ) ( λx . mi ₂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

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

evidentemente cumple con los requisitos. 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 en absoluto, 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 [ ] pueden hacerse 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 ; esto es extensionalmente igual a la función E misma. Por lo tanto, basta con convertir E a forma combinatoria.

Teniendo en cuenta esta simplificación, el ejemplo anterior queda así:

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

= ...

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

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

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

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

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

= ( SI ( K x ) y )

= ( I y ( K x y ))

= ( y ( K x y ))

= ( yx )

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 cualquier combinador extensionalmente igual a cualquier término lambda. Un ejemplo sencillo de dicha base 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 lo es. 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

La base de un punto más simple conocida es una ligera modificación de S :

S' ≡ λxλyλz . (xz) (y (λw. z))) con

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

S' ( S' ( S' S ' ( S' S' ( S' S' ))( S' ( S' ( S' S' ( S' S' )))))) S' S' = ^β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 únicamente S y K :

B = ( S ( KS ) K )

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

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

T [ x ] ⇒ x
T [( E ₁E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
T [ λx . E ] ⇒ ( K T [ E ]) (si x no es libre en E )
T [ λx . x ] ⇒ I
T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (si x es libre en E )
T [ λx .( E ₁E ₂ )] ⇒ ( S T [ λx . E ₁ ] T [ λx . E ₂ ]) (si x es libre tanto en E ₁ como en E ₂ )
T [ λx .( E ₁E ₂ )] ⇒ ( C T [ λx . E ₁ ] T [ E ₂ ]) (si x es libre en E ₁ pero no en E ₂ )
T [ λx .( E ₁E ₂ )] ⇒ ( B T [ E ₁ ] T [ λx . E ₂ ]) (si x es libre en E ₂ pero no en E ₁ )

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

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

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

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

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

= ( C I ) (reducción η)

={\mathsf {C}}_{*}

(notación canónica tradicional:

{\mathsf {X}}_{*}={\mathsf {XI}}

)

={\mathsf {I}}'

(notación canónica tradicional:

{\mathsf {X}}'={\mathsf {CX}}

)

Y, en efecto, ( C I x y ) se reduce a ( y x ):

( C I x y )

= ( I y x )

= ( y x )

La motivación aquí es que B y C son versiones limitadas de S , con B x y = S ( K x ) y y C x y = S x ( K y ). Mientras que S x yz = ( xz ) ( yz ) toma un valor ( z ) y lo sustituye tanto en el aplicadondo ( x ) como en su argumento ( y ) antes de realizar la aplicación, C realiza la sustitución solo en el aplicadondo (( xz ) y ), y B solo en el argumento ( x ( yz )).

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 denominaban 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) .

Cálculo CL _K versus CL _I

Es necesario distinguir entre el cálculo CL _K, tal como se describe en este artículo, y el cálculo CL _I. Esta distinción corresponde a la que existe 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 aparición libre en E .

En consecuencia, el combinador K no está presente ni 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 de CL _{I (módulo igualdad). Cada término λ}_I se puede convertir en un combinador CL _I extensionalmente igual según reglas similares a las presentadas anteriormente para la conversión de términos λ _K en combinadores CL _K. Véase el capítulo 9 de Barendregt (1984).

Church (1941) (§12) define dos combinadores mínimos para el cálculo λ _I : I = λ a . a y J = λ abcd . ab ( adc ). También propone conjuntos primitivos alternativos de combinadores, B , C , W , I (donde W = λ ab . abb es el mismo que se usa hoy en día), o B , T , U , I (donde T = JII = λ ab . ba = CI , y U = λ a . aa = WI que él llama D ).

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 .( x z y )

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

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

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

Sin embargo, tenga en cuenta 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 simplificarse. Es indecidible 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 como se hace con 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 de Church ). También se puede considerar un modelo de computación trivial de juguete donde "calculamos" propiedades de los 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 de 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 simplificado afirma que todo predicado completo es trivial. La demostración de este teorema es bastante sencilla. ^{[ 9 ]}

Prueba

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

( N A ) = T y

( N B ) = F.

Definir NEGACIÓN ≡ λx .(si ( N x ) entonces B sino A ) ≡ λx .(( N x ) B A )

Definir ABSURDO ≡ ( Y NEGACIÓN)

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

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

Porque se supone que N debe ser completo:

( N ABSURDUM) = F o
( N ABSURDO) = T

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

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

De este teorema de indefinibilidad se deduce inmediatamente que no existe ningún predicado completo que pueda discriminar entre términos que tienen forma normal y términos que no la tienen. También se deduce 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 EQUAL, entonces para todo A , λx. (EQUAL x A ) tendría que ser un predicado completo no trivial.

Sin embargo, cabe señalar que de este teorema de indefinibilidad se deduce inmediatamente que muchas propiedades de los términos que son obviamente decidibles tampoco pueden definirse mediante predicados completos: por ejemplo, no existe ningún predicado que pueda determinar si la primera letra de función primitiva que aparece en un término es una K. Esto demuestra que la definibilidad mediante predicados no es un modelo razonable de decidibilidad.

Aplicaciones

Compilació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 denominó programación tácita , es decir, programar en expresiones funcionales sin variables, junto con potentes herramientas 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 lógica y programación: toda demostración de un teorema de lógica intuicionista corresponde a una reducción de un término lambda tipado, y viceversa. Además, los teoremas pueden identificarse con signaturas de tipo de función . En concreto, una lógica combinatoria tipada corresponde a un sistema de Hilbert en teoría de la demostración .

Los combinadores K y S corresponden a los axiomas

AK : A → ( B → A ),

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

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

MP : de A y A → B inferir B .

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

X\Vdash A\iff A\in X.

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

Sea A una fórmula cualquiera que no se puede demostrar en el cálculo. Entonces A no pertenece a la clausura deductiva X del conjunto vacío , por lo tanto $X\not \Vdash A$ y A no es intuicionistamente válido.

Véase también

Sistemas informáticos de aplicación
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 de combinadores SKI
Supercombinador
Para imitar a un ruiseñor

Referencias

↑ Schönfinkel 1924 , El artículo que fundó la lógica combinatoria. Traducción al inglés: Schönfinkel (1967) .
↑ Curry 1930 .
↑ Seldin 2008 .
↑ Barendregt 1984 .
↑ Hindley y Meredith 1990 .
↑ Turner 1979 .
↑ Lachowski 2018 .
↑ Goldberg 2004 .
↑ Engeler 1995 .
↑ Cherlin 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. North Holland . ISBN 0-444-87508-5.
Bimbó, Katalin (2012). Lógica combinatoria: pura, aplicada y tipificada . ISBN 978-1-4398-0000-3.
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. S2CID 25802202 .
Church, Alonzo (1941). Los cálculos de conversión lambda. Anales de estudios matemáticos número 6. Princeton University Press .
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). Lógica combinatoria . Vol. I. Ámsterdam: North Holland. ISBN 0-7204-2208-6.{{cite book}}: Incompatibilidad de ISBN/Fecha ( ayuda )
Curry, Haskell Brooks ; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Lógica combinatoria . Vol. II. Ámsterdam: North Holland. 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). " Esquemas de tipos principales 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 . Recuperado el 9 de septiembre de 2018 .
Paulson, Lawrence C. (1995). Fundamentos de la programación funcional . Universidad de Cambridge.
Quine, Willard Van Orman (1960). «Variables explicadas». Actas de la Sociedad Filosófica Americana . 104 (3): 343–347 . JSTOR 985250. Reimpreso como capítulo 23 de Quine (1996) .
Quine, Willard Van Orman (1996) [1960]. "Variables explicadas". Artículos selectos de lógica (ed. ampliada, 2.ª ed. impresa). Cambridge, Mass.: Harvard University Press . págs. 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-0674324497OCLC 503886453
Seldin, Jonathan P. (3 de marzo de 2008). "La lógica de Curry y Church" (PDF) . Recuperado el 17 de septiembre de 2023 .
Smullyan, Raymond (1985). Para imitar a un ruiseñor y otros acertijos lógicos, incluyendo una asombrosa aventura en lógica combinatoria . Knopf. ISBN 0-394-53491-3Una introducción amena a la lógica combinatoria, presentada como una serie de acertijos recreativos que utilizan metáforas de la 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 constituyen una introducción más formal a la lógica combinatoria, con especial énfasis en los resultados de punto fijo.
Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. Lecciones sobre el isomorfismo de Curry-Howard (PDF) . Estudios en lógica y fundamentos de las matemáticas. Vol. 149 (1.ª ed.). Elsevier . pág. 442. ISBN 978-0444520777Archivado del 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 del 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: Computaciones con objetos a través de ejemplos y ejercicios (2.ª ed.). Moscú: "Center JurInfoR" Ltd. ISBN 5-89158-101-9.
Wolfram, Stephen (2021). Combinadores: Una perspectiva centenaria . Wolfram Media . ISBN 978-1-57955-043-1Una celebración del desarrollo de los combinadores, cien años después de su introducción por Schönfinkel (1924) .(Libro electrónico: ISBN) 978-1-57955-044-8)

Enlaces externos

Enciclopedia de Filosofía de Stanford : " Lógica combinatoria " por Katalin Bimbó .
Notas en bloque de Curry, 1920-1931.
Keenan, David C. (2001) " Para diseccionar un ruiseñor: 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 de lógica combinatoria
Wolfram, Stephen (29 de abril de 2020). Combinadores: Celebración del centenario . Proyecto de Física de Wolfram en YouTube . Recuperado el 26 de septiembre de 2023 .

[FOOTNOTESchönfinkel1924The_article_that_founded_combinatory_logic._English_translation:_[[#CITEREFSchönfinkel1967|Schönfinkel_(1967)]]-1] Schönfinkel 1924 , El artículo que fundó la lógica combinatoria. Traducción al inglés: Schönfinkel (1967) .

[FOOTNOTECurry1930-2] Curry 1930 .

[FOOTNOTESeldin2008-3] Seldin 2008 .

[FOOTNOTEBarendregt1984-4] Barendregt 1984 .

[FOOTNOTEHindleyMeredith1990-5] Hindley y Meredith 1990 .

[FOOTNOTETurner1979-6] Turner 1979 .

[FOOTNOTELachowski2018-7] Lachowski 2018 .

[FOOTNOTEGoldberg2004-8] Goldberg 2004 .

[FOOTNOTEEngeler1995-9] Engeler 1995 .

[FOOTNOTECherlin1991-10] Cherlin 1991 .

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

En matemáticas

En informática

Resumen del cálculo lambda

Cálculo combinatorio

Términos combinatorios

Reducción en lógica combinatoria

Ejemplos de combinadores

Integridad de la base SK

Conversión de un término lambda a un término combinatorio equivalente.

Explicación de la transformación T [ ]

Simplificaciones de la transformación

reducción η

Base de un punto

Combinadores B, C

Cálculo CL K versus CL I

Conversión inversa

Indecidibilidad del cálculo combinatorio

Indefinibilidad por predicados

Aplicaciones

Compilación de lenguajes funcionales

Lógica

Véase también

Referencias

Literatura

Enlaces externos

Cálculo CL _K versus CL _I