Lógica combinatoria - Combinatory logic

La lógica combinatoria es una notación para eliminar la necesidad de variables cuantificadas en lógica matemática . Fue introducido por Moses Schönfinkel y Haskell Curry , y más recientemente se ha utilizado en informática como modelo teórico de computación y también como base para el diseño de lenguajes de programación funcionales . 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 usa solo la aplicación de función y combinadores definidos anteriormente para definir un resultado a partir de sus argumentos.

En matemáticas

La lógica combinatoria se pensó originalmente como una "pre-ló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 del functor de predicados de Quine . Mientras que el poder expresivo de la lógica combinatoria excede típicamente al de la lógica de primer orden , el poder expresivo de la lógica del functor de predicado 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 la 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. 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 informática 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 era de Haskell Curry y sus estudiantes, o de 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 juntos, consulte el libro de Barendregt , 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 cálculo , utilizado en la teoría de la computabilidad y la teoría de la prueba . A pesar de su simplicidad, la lógica combinatoria captura muchas características esenciales de la computación.

La lógica combinatoria se puede ver 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 combinador, y la reducción de combinador es mucho más simple que la reducción de lambda. Por lo tanto, se ha utilizado la lógica combinatoria para modelar algunos lenguajes de programación funcional y hardware no estrictos . La forma más pura de esta vista es el lenguaje de programación Unlambda , cuyas únicas primitivas son los combinadores S y K aumentados 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 puede recibir una variedad de interpretaciones. Muchos de los primeros artículos de Curry mostraron cómo traducir conjuntos de axiomas para la lógica convencional en ecuaciones de lógica combinatoria (Hindley y Meredith 1990). Dana Scott en las décadas de 1960 y 1970 mostró cómo casar la teoría de modelos y 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 es un nombre de variable extraído de un conjunto infinito predefinido de nombres de variables, y y son términos lambda. ${\ Displaystyle v}$${\ Displaystyle E_ {1}}$${\ Displaystyle E_ {2}}$

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

Los términos del formulario se denominan aplicaciones . Invocación o ejecución de la función del modelo de aplicaciones: se invoca la función representada por , con su argumento, y se calcula el resultado. Si (a veces llamado aplicando ) es una abstracción, el término puede reducirse :, el argumento, puede sustituirse en el cuerpo de en lugar del parámetro formal de , y el resultado es un nuevo término lambda que es equivalente al antiguo uno. Si un término lambda no contiene subterráneos de la forma , no se puede reducir y se dice que está en forma normal . ${\ Displaystyle (E_ {1} E_ {2})}$${\ Displaystyle E_ {1}}$${\ Displaystyle E_ {2}}$${\ Displaystyle E_ {1}}$${\ Displaystyle E_ {2}}$${\ Displaystyle E_ {1}}$${\ Displaystyle E_ {1}}$${\ Displaystyle ((\ lambda v.E_ {1}) E_ {2})}$

La expresión representa el resultado de tomar el término E y reemplazar todas las apariciones libres de v en él con a . Así escribimos ${\ Displaystyle E [v: = a]}$

${\ Displaystyle ((\ lambda vE) a) \ Flecha derecha E [v: = a]}$

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

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}$

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

El cuadrado de 3 es ${\ Displaystyle 3 * 3}$

Para evaluar la expresión resultante , 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 principio de sustitución simple es suficiente para capturar el mecanismo esencial de cálculo. Además, en el cálculo lambda, nociones como '3' y ' ' se pueden representar sin necesidad de constantes o operadores primitivos 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, codificación qv Church . ${\ Displaystyle 3 * 3}$${\ Displaystyle *}$

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 se pueda realizar en cualquiera de estos otros modelos se puede expresar en cálculo lambda y viceversa. Según la tesis de Church-Turing , ambos modelos pueden expresar cualquier cálculo posible.

Quizás sea sorprendente que el cálculo lambda pueda representar cualquier cálculo concebible utilizando solo las nociones simples de abstracción y aplicación de funciones basadas en la sustitución textual simple 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 sustitución debe especificarse con mucho cuidado para evitar problemas de captura de variables. Por el contrario, 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 fabricar funciones en el cálculo lambda, algo debe reemplazarla en el cálculo combinatorio. En lugar de 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:

Sintaxis	Nombre	Descripción
X	Variable	Carácter o cadena que representa un término combinatorio.
PAG	Función primitiva	Uno de los símbolos de combinadores I , K , S .
(MINNESOTA)	Solicitud	Aplicar una función a un argumento. M y N son términos combinatorios.

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 , o incluso , denota el término . Esta es la misma convención general (asociatividad por la izquierda) que para la aplicación múltiple en cálculo lambda. ${\ Displaystyle (E_ {1} E_ {2} E_ {3} ... E_ {n})}$${\ Displaystyle E_ {1} E_ {2} E_ {3} ... E_ {n}}$${\ Displaystyle (... ((E_ {1} E_ {2}) E_ {3}) ... E_ {n})}$

Reducción de la lógica combinatoria

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

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

donde E es un término que menciona solo variables del conjunto { x ₁ ... x _n } . Es así como 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

( 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

(( K x ) 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 se aplica x a y después de la primera sustitución z en cada uno de ellos. O dicho de otra manera, x se aplica ay dentro del entorno z .

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

(( SKK ) x )

= ( SKK x )

= ( K x ( K x ))

= x

para cualquier término x . Tenga en cuenta que aunque (( SKK ) x ) = ( I x ) para cualquier x , ( SKK ) en sí 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 de identidad; ( SKK ) y yo estamos entre estos caminos. ( SKS ) es otro 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 se puede utilizar para implementar la recursividad .

Completitud de la base SK

S y K se pueden componer 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 prueba es 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 ] => yo
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 ₂)

Tenga en cuenta que T [] como se indica 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 exactamente a una de estas reglas (consulte Resumen del cálculo lambda más arriba).

Está relacionado con el proceso de abstracción de paréntesis , que toma una expresión E construida a partir de variables y aplicación y produce una expresión combinatoria [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 en la estructura de expresiones de la siguiente manera:

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

La abstracción de corchetes induce una traducción de términos lambda a expresiones combinatorias, mediante la interpretación de abstracciones lambda utilizando el algoritmo de abstracción de 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 ) a 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 de dos términos x e y (alimentándolos en una cola similar a la moda en el combinador 'desde la derecha'), que reduce la siguiente manera:

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

= ( K ( S yo ) x ( S ( K K ) yo x) y)

= ( S yo ( S ( K K ) yo 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 ( yo x))

= (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 ³ ).

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 simples: las variables se convierten a 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.

Son las reglas 5 y 6 las que son de interés. 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 realmente 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 , produciendo ( 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 ₂, entonces

( E ₁ E ₂) [ x  : = a ] = ( E ₁ [ x  : = a ] E ₂ [ 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 . ( E ₁ E ₂) = ( S λx . E ₁ λx . E ₂)

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 encaja a la perfección. E ₁ y E ₂ contienen cada uno estrictamente menos aplicaciones que ( E ₁ E ₂), por lo que la recursividad 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 está 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, es suficiente convertir E a forma combinatoria.

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

  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, 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 ))

= ( yx )

De manera similar, la versión original de la transformación T [] transformó la función de 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

Hay bases de un punto a partir de las cuales cada combinador puede componerse extensivamente igual a cualquier término lambda. El ejemplo más simple de tal base es { X } donde:

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

No es difícil verificar 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 usa X como su único combinador.

Otro ejemplo simple 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.

Combinadores B, C

Además de S y K , el artículo de Schönfinkel incluía 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 se pueden expresar a su vez utilizando solo 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 en expresiones de combinador. También fueron utilizados por Curry , y mucho más tarde por David Turner , cuyo nombre se ha asociado con su uso computacional. Utilizándolos, 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 está libre en E )
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (si x está 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 E₂ )
8. T [ λx . ( E₁ E₂ )] ⇒ ( B T [ E₁ ] T [ λx . E₂ ]) (si x es libre en E₂ pero no E₁ )

Usando 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 )] (según la regla 7)

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

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

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

= (Notación canónica tradicional: )${\ Displaystyle \ mathbf {I} '}$${\ 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 solicitante como en su argumento antes de realizar la aplicación, C realiza la sustitución solo en el solicitante y B solo en el argumento.

Los nombres modernos de los combinadores provienen de la tesis doctoral de Haskell Curry de 1930 (ver 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.

Cálculo CL _K versus CL _I

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

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

Como 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 de CL _I (módulo de 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 de 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 . ( x z y )

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

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

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

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 para simplificarlos. Es indecidible si un término combinatorio general tiene una forma normal; si dos términos combinatorios son equivalentes, etc. Esto es equivalente a la indecidibilidad de los problemas correspondientes para términos lambda. Sin embargo, una prueba directa es la siguiente:

Primero, el término

Ω = ( S I I ( S I I ))

no tiene forma normal, porque se reduce a sí mismo después de tres pasos, de la siguiente manera:

   ( S I I ( S I I ))

= ( I ( S I I ) ( I ( S I I )))

= ( S I I ( I ( S I I )))

= ( S I I ( S I I ))

y claramente ninguna otra orden de reducción puede acortar la expresión.

Ahora, suponga que N fuera un combinador para detectar formas normales, de modo que

${\ displaystyle (\ mathbf {N} \ x) = {\ begin {cases} \ mathbf {T}, {\ text {if}} x {\ text {tiene una forma normal}} \\\ mathbf {F} , {\ text {de lo contrario.}} \ end {cases}}}$

(Donde T y F representan las codificaciones convencionales de Church 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 )) .

Ahora deja

Z = ( C ( C ( B N ( S I I )) Ω ) I )

ahora considere el término ( S I I Z ). ¿Tiene ( S I I Z ) una forma normal? Lo hace si y solo si lo siguiente también lo hace:

  ( S I I Z )

= ( I Z ( I Z ))

= ( Z ( I Z ))

= ( Z Z )

= ( C ( C ( B N ( S I I )) Ω ) I Z ) (definición de Z )

= ( C ( B N ( S I I )) Ω Z I )

= ( B N ( S I I ) Z Ω I )

= ( N ( S I I Z ) Ω I )

Ahora necesitamos aplicar N a ( S I I Z ). O ( S I I Z ) tiene una forma normal o no. Si no tiene una forma normal, a continuación de lo anterior reduce como sigue:

  ( N ( S I I Z ) Ω I )

= ( K Ω I ) (definición de N )

= Ω

pero Ω no no tienen una forma normal, por lo que tenemos una contradicción. Pero si ( S I I Z ) no tiene una forma normal, lo anterior se reduce de la siguiente manera:

  ( N ( S I I Z ) Ω I )

= ( K I Ω I ) (definición de N )

= ( Yo yo )

= Yo

lo que significa que la forma normal de ( S I I Z ) es simplemente I , otra contradicción. Por lo tanto, el combinador hipotético de forma normal N no puede existir.

El análogo de la lógica combinatoria del teorema de Rice dice que no existe un predicado no trivial completo. Un predicado es un combinador que, cuando se aplica, los rendimientos o bien T o F . Un predicado N es no trivial si hay dos argumentos A y B de tal manera que N A = T y N B = F . Un combinador N es completa si y sólo si N M tiene una forma normal para cada argumento M . El análogo del teorema de Rice dice entonces que todo predicado completo es trivial. La demostración de este teorema es bastante simple.

Prueba: Por reductio ad absurdum. Supongamos que hay un predicado completa no trivial, por ejemplo N . Debido a que se supone que N no es trivial, existen combinadores A y B tales que

( N A ) = T y

( N B ) = F .

Defina NEGACIÓN ≡ λx . (Si ( N x ) entonces B más A ) ≡ λx . (( N x ) B A )

Definir ABSURDUM ≡ ( Y NEGATION)

El teorema del punto fijo da: ABSURDUM = (NEGATION ABSURDUM), para

ABSURDUM ≡ ( Y NEGATION) = (NEGATION ( Y NEGATION)) ≡ (NEGATION ABSURDUM).

Porque se supone que N debe estar completo:

1. ( N ABSURDUM) = F o
2. ( N ABSURDO) = T

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

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

De este teorema de indecidibilidad se deduce inmediatamente que no existe un predicado completo que pueda discriminar entre términos que tienen una forma normal y términos que no tienen una forma normal. También se deduce que no hay un predicado completo, digamos EQUAL, tal que:

(IGUAL AB ) = T si A = B y

(EQUAL AB ) = F si A ≠ B .

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

Aplicaciones

Compilación de lenguajes funcionales

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

Kenneth E. Iverson usó primitivas basadas en los combinadores de Curry en su lenguaje de programación J , un sucesor de APL . Esto permitió lo que Iverson llamó programación tácita , es decir, programar 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.

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 tipificado, y viceversa. Además, los teoremas se pueden identificar con firmas de tipo de función. Específicamente, una lógica combinatoria tipificada corresponde a un sistema de Hilbert en la teoría de la prueba .

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 de desprendimiento (modus ponens)

MP : de A y A → B inferir B .

El cálculo que consta de AK , AS y MP está completo para el fragmento implicacional de la lógica intuicionista, que se puede ver de la siguiente manera. Considere el conjunto W de todos los conjuntos de fórmulas deductivamente cerrados, ordenados por inclusión . Entonces es un marco intuicionista de Kripke , 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 , luego por modus ponens. Por otro lado, si , a continuación, por el teorema de la deducción , por lo tanto el cierre deductiva de que 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 pueda demostrarse en el cálculo. Entonces A no pertenece al cierre deductivo X del conjunto vacío, por lo tanto , y A no es intuicionistamente válido. ${\ Displaystyle X \ not \ Vdash A}$

Ver también

• Sistemas informáticos 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 del combinador de SKI
• Supercombinador
• Para burlarse de un ruiseñor

Referencias

Otras lecturas

• Barendregt, Hendrik Pieter (1984). El cálculo lambda, su sintaxis y semántica. Estudios de Lógica y Fundamentos de las Matemáticas . Volumen 103. Holanda Septentrional . ISBN 0-444-87508-5. |volume=tiene texto extra ( ayuda )
• Curry, Haskell B .; Feys, Robert (1958). Lógica combinatoria . Vol. I. Amsterdam: Holanda Septentrional. ISBN 0-7204-2208-6. |volume=tiene texto extra ( ayuda )
• Curry, Haskell B .; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Lógica combinatoria . Vol. II. Amsterdam: Holanda Septentrional. ISBN 0-7204-2208-6. |volume=tiene texto extra ( ayuda )
• Field, Anthony J .; Harrison, Peter G. (1998). Programación funcional . Addison-Wesley. ISBN 0-201-19249-7.
• 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
• Hindley, JR ; Seldin, JP (2008). λ-cálculo y combinadores: una introducción . Prensa de la Universidad de Cambridge .
• Paulson, Lawrence C. (1995). Fundamentos de la programación funcional . Universidad de Cambridge.
• Quine, WV (1960). "Variables explicadas". Actas de la American Philosophical Society . 104 (3): 343–347. JSTOR  985250 .Reimpreso como Capítulo 23 de Selected Logic Papers de Quine (1966), págs. 227-235
• Schönfinkel, Moses , 1924, " Über die Bausteine ​​der mathischen Logik ", traducido como "Sobre los bloques de construcción de la lógica matemática" en From Frege to Gödel: un libro de consulta en lógica matemática, 1879-1931 , Jean van Heijenoort , ed. Harvard University Press , 1967. ISBN  0-674-32449-8 . El artículo que fundó la lógica combinatoria.
• Smullyan, Raymond , 1985. Para burlarse de un ruiseñor . Knopf. ISBN  0-394-53491-3 . Una suave introducción a la lógica combinatoria, presentada como una serie de acertijos recreativos utilizando metáforas de observación de aves.
• ______, 1994. Diagonalización y autorreferencia . Prensa de la Universidad de Oxford . Los capítulos 17-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. y Paweł Urzyczyn, 1999. Conferencias sobre el isomorfismo Curry-Howard . Universidad de Copenhague y Universidad de Varsovia , 1999.
• Wolfengagen, VE (2003). Lógica combinatoria en programación: Cálculos con objetos a través de ejemplos y ejercicios (2ª ed.). Moscú: "Centre JurInfoR" Ltd. ISBN 5-89158-101-9.
• Wolfram, Stephen (2021). Combinadores: una vista centenaria . Wolfram Media . ISBN 978-1-57955-043-1.e ISBN  978-1-57955-044-8 . Una celebración del desarrollo de los combinadores, cien años después de que fueran introducidos por Moses Schönfinkel en 1920.

enlaces externos

• Enciclopedia de Filosofía de Stanford : " Lógica combinatoria " por Katalin Bimbó .
• 1920-1931 Bloques de notas de Curry.
• Keenan, David C. (2001) " 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 lógica combinatoria