Lógica combinatoria

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

formalismo lógico usando combinadores en lugar de variables

Lógica combinatoria es una notación para eliminar la necesidad de variables cuantificadas en lógica matemática. Fue presentado 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 'prelógica' eso aclararía el papel de las variables cuantificadas en lógica, esencialmente eliminándolas. Otra forma de eliminar variables cuantificadas es la lógica de funtores predicados de Quine. Mientras que el poder expresivo de la lógica combinatoria típicamente excede al de la lógica de primer orden, el poder expresivo de la lógica de funtores predicados 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 profesor 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ó ser 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 fue de Haskell Curry y sus estudiantes, o de Robert Feys en Bélgica. Curry y Feys (1958), y Curry et al. (1972) analizan 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, vea 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 puede verse 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, la lógica combinatoria se ha utilizado para modelar algunos lenguajes de programación y hardware funcionales 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 se puede dar 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 unir 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 se pueden representar mediante las siguientes tres formas de cadenas:

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

Donde $v$ es un nombre variable dibujado de un conjunto infinito predefinido nombres variables, y $E_{1}$ y $E_{2}$ son lambda-terms.

Términos del formulario ${displaystyle lambda v.E_{1}}$ se llaman abstracciones. La variable v es llamado el parámetro formal de la abstracción, y $E_{1}$ es cuerpode la abstracción. El término ${displaystyle lambda v.E_{1}}$ representa la función que, aplicada a un argumento, une 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 ${displaystyle (E_{1}E_{2})}$ se llaman Aplicaciones. Modelo de aplicaciones función invocación o ejecución: la función representada por $E_{1}$ es estar invocado, con $E_{2}$ como su argumento, y el resultado es calculado. Si $E_{1}$ (A veces se llama el applicand) es una abstracción, el término puede ser Reducción: $E_{2}$ , el argumento, puede ser sustituido en el cuerpo de $E_{1}$ en lugar del parámetro formal $E_{1}$ , y el resultado es una nueva lambda término que es equivalente al viejo. Si un término de lambda no contiene subterms of the form ${displaystyle ((lambda v.E_{1})E_{2})}$ entonces no se puede reducir, y se dice estar en forma normal.

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

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

Por convención, tomamos ${displaystyle (abc)}$ como shorthand para ${displaystyle ((ab)c)}$ (es decir, la aplicación queda 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}

(Usando " $*$ "para indicar multiplicación.) x aquí está el parámetro formal de la función. Para evaluar el cuadrado para un particular argumento, decir 3, lo insertamos en la definición en lugar de la 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. Desde computación es simplemente una composición de la evaluación de adecuado funciones sobre argumentos primitivos adecuados, esta simple sustitución principio suficiente para captar el mecanismo esencial de la computación. Además, en el cálculo de la lambda, nociones como '3' y ' $*$ Puede ser representado sin necesidad de primitiva definida externamente operadores o constantes. Es posible identificar términos en el cálculo de lambda, que, cuando se interpreta adecuadamente, se comportan como número 3 y como el operador de multiplicación, q.v. iglesia codificación.

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

Quizás sea sorprendente que el cálculo lambda pueda representar cualquier cálculo concebible utilizando sólo las nociones simples de función abstracción y aplicación basada en la simple sustitución textual de términos para las variables. Pero aún más notable es que la abstracción es ni siquiera requerido. La lógica combinatoria es un modelo de computación equivalente al cálculo lambda, pero sin abstracción. La ventaja de esto es que evaluar expresiones en 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 la lógica combinatoria es mucho más simple, porque no hay 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 reemplazarlo en la combinatoria cálculo. En lugar de abstracción, el cálculo combinatorio proporciona una conjunto limitado de funciones primitivas a partir de las cuales otras funciones pueden ser construido.

Términos combinatorios

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

Sintaxis	Nombre	Descripción
x	Variable	Un personaje o una cadena que representa un término combinatorio.
P	Función primitiva	Uno de los símbolos de combinación I, K, S.
(M N)	Aplicación	Aplicar una función a un argumento. M y N son términos combinatorios.

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

Para acortar 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 (left-asociativity) que para aplicación múltiple en el cálculo de 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 ... x n) E

donde E es un término que menciona solo variables del conjunto ${x 1 ... 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, la identidad combinador, definido por

()I 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) Sí.) x

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

()K x Sí.) x

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

()S x y z) =x z ()Y z)

S 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.

Dados S y K, el propio I es innecesario, ya que puede construirse a partir de los otros dos:

()S K) x)

=S K x)

=K x ()K x)

= x

para cualquier término x. Tenga en cuenta que aunque ((S K K) x) = (I x) 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 la igualdad de funciones: que dos funciones son iguales si siempre producen los mismos resultados para el mismo argumentos Por el contrario, los propios términos, junto con los reducción de combinadores primitivos, capturan la noción de igualdad intencional de funciones: que dos funciones son iguales solo si tienen implementaciones idénticas hasta la expansión de primitivas combinadores. Hay muchas maneras de implementar una función de identidad; (S K K) y yo se encuentran entre estos caminos. (S K S) es otro más. Nosotros utilizará 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 el combinador Y, que se puede utilizar para implementar la recursividad.

Integridad de la base S-K

S y K se pueden componer para producir combinadores que son extensionalmente iguales a cualquier término lambda y, por lo tanto, por Church' s tesis, a cualquier función computable que sea. 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:

T[x= x
T[E1 E2)] = título ()T[E1] T[E2])
T[λx.E= ()K T[ESi x no ocurre libre en E)
T[λx.x= I
T[λx.λy.E= T[λx.T[λy.E]] (si x ocurre libre en E)
T[λx.(E1 E2)] = título ()S T[λx.E1] T[λx.E2Si x ocurre libre en E1 o 1 E2)

Tenga en cuenta que T[ ] tal como se indica no es una función matemática bien tipificada, sino más bien una reescritura de términos: aunque finalmente produce un combinador, la transformación puede generar expresiones intermedias que no son términos lambda ni combinadores, por 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 (ver Resumen del cálculo lambda 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 combinadora [x]E en la que la variable x no es libre, tal que [x]E x = E se cumple. Un algoritmo muy simple para la abstracción de paréntesis se define por inducción en la estructura de las expresiones de la siguiente manera:

[x]Sí.:= K Sí.
[x]x:= I
[x]E1 E2) S[x]E1[x]E2)

La abstracción de paréntesis induce una traducción de términos lambda a expresiones combinadoras, mediante la interpretación de abstracciones lambda mediante el algoritmo de abstracción de paréntesis.

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.(Sí. x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(y)K K xI x) y))

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

(y)I x))

= (y x)

La representación combinatoria, (S (K (S I)) (S (K K ) yo)) es mucho más largo que la representación como término lambda, λx.λy.(y x). Esto es típico. En general, la construcción T[ ] puede expandir una lambda término 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 abstracción. Dos casos especiales, 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 primeras dos reglas también son simples: las variables se convierten en sí mismas, y las aplicaciones, que están permitidas en términos combinatorios, son convertidos en combinadores simplemente convirtiendo el aplicante y el argumento a los 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 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, produciendo (E₁ E₂)[x: = a]. Pero sustituir a en (E₁ E₂) en lugar de x es lo mismo que sustituirlo en tanto E₁ como E₂, por lo que

()E1 E2)x:= a=E1[1]x:= a] E2[2]x:= a])

()λx.(E1 E2) a()λx.E1 a)λx.E2 a)

=S λx.E1 λx.E2 a)

=S λx.E1 λx.E2) a)

Por igualdad extensional,

λx.(E1 E2) =S λx.E1 λx.E2)

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

()S T[λx.E1] T[λx.E2])

evidentemente encaja a la perfección. E₁ y E₂ cada uno contiene estrictamente menos aplicaciones que (E₁ E₂), por lo que la recursividad debe terminar en una lambda término 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 menor si tenemos en cuenta la regla de la η-reducción:

T[λx.(E x) = T[ESi 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, es suficiente convertir E en forma combinatoria.

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

T[λx.λy.(Sí. x)

=...

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

=S ()K ()S I) K) (por pira-reducción)

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

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

=K ()S I) x ()K x) Sí.)

=S I ()K x) Sí.)

=I Sí. ()K x y)

=Sí. ()K x y)

=y x)

Del mismo modo, la versión original de la transformación T[ ] transformó la función identidad λf.λx.(f x) en (S (S (K S) (S (K K) I)) (K I)). Con la regla de reducción η, λf.λx.(f x) es transformado en yo.

Base de un punto

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

X ↑ λx(xS)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 usa X como su único combinador.

Otro ejemplo simple de una base de un punto es:

X ' ↑ λx.(x K S KCon

()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 llaman 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 usando solo S y K:

B =S ()K) K)

C =S ()S ()K ()S ()K) K) S)K)

Estos combinadores son extremadamente útiles al traducir 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. Usándolos, podemos extender las reglas para la transformación de la siguiente manera:

T[x⇒ x
T[E1 E2⇒ ()T[E1] T[E2])
T[λx.E⇒K T[ESi x no es libre en E)
T[λx.x⇒ I
T[λx.λy.E⇒ T[λx.T[λy.E]] (si x está libre en E)
T[λx.(E1 E2⇒ ()S T[λx.E1] T[λx.E2Si x es libre en ambos E1 y E2)
T[λx.(E1 E2⇒ ()C T[λx.E1] T[E2Si x está libre en E1 pero no E2)
T[λx.(E1 E2⇒ ()B T[E1] T[λx.E2Si x está libre en E2 pero no E1)

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

T[λx.λy.(Sí. x)

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

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

= T[λx.(C I x)

=C I.

{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 Sí.)

=I Sí. x)

=Sí. 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 CLK versus CLI

Se debe hacer una distinción entre el cálculo 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 λ_K, el cálculo λ_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 CL_I cálculo. 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 (igualdad de módulo). Cada término λ_I se puede convertir en un combinador igual CL_I de acuerdo con reglas similares a las presentadas anteriormente para la conversión de λ_K términos en CL_K combinadores. 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.(x z Sí.)

L[B= λx.λy.λz.(x ()Sí. z)

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

L[E1 E2) =L[E1] L[E2])

Tenga en cuenta, sin embargo, que esta transformación no es la inversa transformación de cualquiera 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, como sigue:

()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 ningún otro orden de reducción puede acortar la expresión.

Ahora, supongamos que N fuera un combinador para detectar formas normales, tal que

{displaystyle (mathbf {N} x)={begin{cases}mathbf {T}{text{ if }}x{text{ has a normal form}}\mathbf {F}{text{ otherwise.}}end{cases}}}

(Dónde)

T

F

representan las codificación de la Iglesia convencional del verdadero y falso, λx.λy.x y λx.λy.Sí., transformado en lógica combinatoria. Las versiones combinatorias tienen

T = K

F = K I)

Ahora deja

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

ahora considere el término (S I I Z). ¿(S I I Z) tiene un ¿forma? 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 lo hace tienen una forma normal, entonces lo anterior se reduce de la siguiente manera:

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

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

= Ω

pero Ω no tiene una forma normal, entonces tenemos una contradicción. Pero si (S I I Z) no tiene una forma normal, el anterior se reduce como sigue:

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

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

=I I)

= I

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

El análogo de 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, devuelve T o F. 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 NM tiene una forma normal para cada argumento M. El análogo del teorema de Rice dice que todo predicado completo es trivial. La demostración de este teorema es bastante sencilla.

Prueba

Por reductio ad absurdum. Supongamos que hay un predicado no trivial completo, digamos N. Porque... N se supone que no es trivial hay combinadores A y B tales que

()N A) T y

()N B) F.

Definir la NEGACIÓN λx(si)N xentonces B más A) λx.(N x) B A)

Definir ABSURDUMY NEGATION)

Teorema de punto fijo da: ABSURDUM = (NEGATION ABSURDUM), para

ABSURDUMY NEGATION) = (NEGATION (Y NEGATION) (NEGATION ABSURDUM).

Porque... N se supone que está completo:

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

Caso 1: F =N ABSURDUM = N (NEGATION ABSURDUM) = (N A) TUna contradicción.
Caso 2: T =N ABSURDUM = N (NEGATION ABSURDUM) = (N B) FOtra vez una contradicción.

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

De este teorema de indecidibilidad se sigue inmediatamente que no existe un 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 hay predicado completo, digamos IGUAL, tal que:

(EQUAL A B) T si A = B y

(EQUAL A B) F si A ل B.

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

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, programación en expresiones funcionales que no contienen variables, junto con poderosas 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.

Lógica

El isomorfismo de Curry-Howard implica una conexión entre la lógica y la programación: toda prueba 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 tipada 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),

ASÍ#A →B → C) → (A → B) →A → C)),

y la aplicación de funciones corresponde a la regla de separación (modus ponens)

MP: A y A → B inferente B.

El cálculo consistente en AK, ASÍ, y MP es completo para el fragmento implicacional de la lógica intuitionista, que se puede ver como sigue. Considere el conjunto W de todos los conjuntos de fórmulas deductivamente cerrados, ordenados por inclusión. Entonces... $langle W,subseteqrangle$ es un marco de Kripke intuitionista, y definimos un modelo $Vdash$ en este marco por

XVdash Aiff Ain X.

Esta definición obedece las condiciones de satisfacción de →: por un lado, si $XVdash Ato B$ , y $Yin W$ es tal que $Ysupseteq X$ y $YVdash A$ , entonces $YVdash B$ por modus ponens. Por otro lado, si $XnotVdash Ato B$ , entonces $X,Anotvdash B$ por el teorema de deducción, así el cierre deductivo $Xcup{A}$ es un elemento $Yin W$ tales que $Ysupseteq X$ , $YVdash A$ , y $YnotVdash B$ .

Vamos A sea cualquier fórmula que no sea provable en el cálculo. Entonces... A no pertenece al cierre deductivo X del conjunto vacío, así $XnotVdash A$ , y A no es intuitivamente válido.

Contenido relacionado

Más resultados...