Combinador de la lógica de los axiomas

Question

Estoy llevando a cabo algunos experimentos en los teoremas con combinador de la lógica, que es de aspecto prometedor, pero hay un obstáculo:se ha señalado que en el combinador lógica es cierto que, por ejemplo,I = SK, pero esto no es un teorema, se tiene que ser añadido como un axioma.¿Alguien sabe de una lista completa de los axiomas que deben agregarse?

Editar:Por supuesto, usted puede probar por la mano que I = SK, pero a menos que me falta algo, no es un teorema en el sistema de combinador de la lógica de la igualdad.Dicho esto, usted puede macro expandir me SKK...pero todavía estoy perdiendo algo importante.Tomando el conjunto de los puntos p(X) y ~p(X), que fácilmente resolver una contradicción en el ordinario de la lógica de primer orden, y la conversión de ellos a SK, la realización de la sustitución y la evaluación de todas las llamadas de S y K, mi programa genera los siguientes (donde yo estoy usando ' para Unlambda del acento grave):

"eq "s "s "s 'k s "s "s 'k s "s 'k k 'k eq "s "s k s k k k k "s 'k k 'k false 'k de verdad k verdadero

Parece que tal vez lo que necesito es un conjunto adecuado de reglas para el manejo de los parciales de las llamadas 'k y "s, es solo que no estoy viendo lo que dichas normas deben ser, y toda la literatura que se puede encontrar en esta zona fue escrito para un público objetivo de los matemáticos no programadores.Sospecho que la respuesta es, probablemente, bastante simple una vez que usted lo entienda.

Answer 1

Algunos libros de texto definir Yo como mera alias para ((S, K) K).En este caso son idénticas (como términos) per definitionem.Para demostrar su igualdad (como funciones), sólo tenemos que demostrar que la igualdad es el reflexivo, el cual puede ser alcanzado por una reflexividad axioma esquema:

• La proposición `E = E"es discutible (La reflexividad axioma esquema, crea una instancia para cada uno de los posibles términos señalados aquí por metavariable E)

Por lo tanto, supongo que en las siguientes, que Sus preguntas investiga otro enfoque:cuando el combinador Yo no está definido como un la mera alias por término compuesto ((S, K) K), pero introducida como un independiente básica combinator constante en su propio, cuya semántica operacional es declarado explícitamente por el axioma esquema de

• ``(Yo E) = E"es discutible (I-axioma esquema)

Supongo que Su pregunta

si podemos deducir formalmente (restante dentro del sistema), que un autónomo se define Yo se comporta exactamente como ((S, K) K), cuando se emplea como funciones en las reducciones?

Creo que podemos, sino que debemos recurrir a herramientas más fuerte.Suponemos que el habitual axioma esquemas no son suficientes, tenemos que declarar también la extensionality propiedad (igualdad de funciones), que es el punto principal.Si queremos formalizar extensionality como un axioma, tenemos que aumentar nuestro idioma con el objeto de variables libres.

Yo creo que tenemos que adoptar un enfoque para la construcción de la lógica combinatoria, que tenemos que permitir también el uso de variables en el objeto de idioma.Oof supuesto, me refiero a "sólo" gratis los objetos de valor.El uso de variables vinculadas sería hacer trampa, tenemos que permanecer dentro de la esfera de la lógica combinatoria.El uso libre de varaibles no es hacer trampa, es un honesto herramienta.Por lo tanto, podemos hacer la prueba formal de Que sea necesario.

Además de la simple igualdad de axiomas y reglas de inferencia (transitividad, la reflexividad, simetría, Leibniz reglas), debemos agregar un extensionality la regla de inferencia para la igualdad.Aquí es el punto donde la libertad de las variables de la materia.

En Csörnyei 2007:157 y 158, he encontrado el siguiente enfoque.Creo que de esta manera la prueba de que se puede hacer.

Algunas observaciones:

La mayoría de los axiomas son, de hecho, esquemas de axioma, que consta de un número infinito de axiomas de los casos.Las instancias deben crear instancias para cada posible E, F, G términos.Aquí, el uso de la cursiva para metavariables.

La superficial de la infinita naturaleza de los esquemas de axioma no elevar la computabilidad de problemas, ya que pueden ser realizadas en un tiempo finito:nuestro sistema de axiomas es recursiva.Esto significa que una inteligente parser puede decidir en un tiempo finito (por otra parte, de manera muy eficaz), si una determinada proposición es una instancia de un axioma esquema, o no.Así, el uso de esquemas de axioma no levanta ni teórico ni práctico problemas.

Ahora vamos a parecer nuestro marco:

Idioma

ALFABETO

Constantes:Los tres siguientes son llamados constantes: K, S, Yo.

He añadido la constante Yo sólo porque Tu pregunta presupone que no tenemos definido el combinador Yo como un mero alias/macro por término compuesto S K K, pero es una constante independiente en su propio.

He de indicar constantes negrita capiteles romanos.

Signo de solicitud:Un signo @ de `aplicación" es suficiente (prefijo de notación con arity 2).Como azúcar sintáctico, yo uso aquí parantheses en lugar de la explícita inicio de sesión de aplicación:Voy a usar el explícito tanto de apertura ( y cierre ) de los signos.

Variables:Aunque combinador de la lógica de no hacer uso de las variables vinculadas, alcance, etc, pero podemos introducir variables libres.Sospecho, que no sólo son de azúcar sintáctico, pueden fortalecer el sistema de deducción, demasiado.Me conjetura, que Su pregunta se requiere su uso.Cualquier conjunto infinito enumerable (distintos de los constantes signos y paréntesis) servirá como el alfabeto de las variables, voy a indicar aquí con formato romana en minúsculas letras x, y, z...

TÉRMINOS

Los términos están definidos de forma inductiva:

• Cualquier constante es un término
• Cualquier variable es un término
• Si E es un término, y F es un término demasiado, entonces también (E F) es un término

Yo a veces uso práctico de los convenios como azúcar sintáctico, por ejemplo,escribir

E F G H

en lugar de

(((E F) G) H).

Deducción

La conversión de esquemas de axioma:

• ``K E F = E"es discutible (K-axioma esquema)
• ``S F G H = F H (G H"es discutible (S-axioma esquema)
• ``Yo E = E"es discutible (I-axioma esquema)

He añadido el tercer conversión axioma (Yo la regla), solamente porque Su pregunta presupone que no hemos definido el combinador Yo como un alias/macro para S K K.

La igualdad axioma esquemas y reglas de inferencia

• ``E = E"es discutible (La reflexividad axioma)
• Si "E = F"es deducible, luego "F = E"también es discutible (La simetría la regla de inferencia)
• Si "E = F"es discutible, y "F = G"es discutible también, entonces también "E = G"es reducible (Transitividad la regla)
• Si "E = F"es deducible, luego "E G = F G"también es discutible (Leibniz regla me)
• Si "E = F"es deducible, luego "G E = G F"también es discutible (Leibniz regla II)

Pregunta

Ahora vamos a investigar Su pregunta.Suponemos que el sistema de deducción definido hasta ahora no es lo suficientemente fuerte como para demostrar Su pregunta.

Es la proposición "Yo = S K K"deducible?

El problema es que tenemos que demostrar la equivalencia de funciones.Consideramos dos funciones equivalentes si se comportan de la misma manera.Las funciones de la ley, de manera que se aplica a los argumentos.Debemos demostrar que ambas funciones a actuar de la misma manera, si se aplica a cada uno de los posibles argumentos.De nuevo, el problema con el infinito!Sospecho, esquemas de axiomas no puede ayudarnos aquí.Algo como

Si E F = G F es discutible, entonces también E = G es discutible

no serían capaces de hacer el trabajo:podemos ver que esto no producir lo que queremos.Utilizando, podemos demostrar que

``Yo E = S K K E"es discutible

para cada E plazo de instancia, pero estos resultados están separados sólo instancias de, y no puede ser utilizado como un conjunto de otras deducciones.Sólo tenemos resultados concretos (infinitamente muchos), no siendo capaz de resumir:

• que tiene de E := K
• tiene para E := S
• que tiene de E := K K
• .
• .
• .

...

no podemos resumir estos fragmentado resultado instancias en un solo gran resultado, indicando extensionality!No podemos verter estos de bajo valor fragmento en el embudo de una regla de inferencia que se funden en un único más valioso resultado.

Tenemos que aumentar la potencia de nuestro sistema de deducción.Tenemos que encontrar una herramienta formal que puede agarra el problema.Sus preguntas conduce a extensionality, y creo que, declarando extensionality necesidades que nos pueden plantear proposiciones que se sostenga por *****arbitrarias***** de los casos.Por eso creo que debe permitir la libre variables dentro de nuestro objeto de idioma.Suponemos que la siguiente regla de inferencia va a hacer el trabajo:

• Si la variable x no es parte de los términos ni E ni F, y declaración (E x) = (F x) es deducible, luego E = F también es discutible (Extensionality la regla de inferencia)

Lo difícil en este axioma, fácilmente conduce a confusión:x es un objeto variables, totalmente emancipado y respetado a partes de nuestro objeto de lenguaje, mientras que el E y G son metavariables, no las partes del objeto del lenguaje, sino que se utiliza sólo para una notación concisa de esquemas de axioma.

(Comentario:Más precisamente, el extensionality regla de inferencia debe ser formalizado en un más cuidadoso manera, la introducción de un metavariable x sobre todos los posibles objeto las variables x, y, z..., y también a otro tipo de metavariable E sobre todos los posibles plazo de instancias.Pero esta distinción entre los dos tipos de metavariables además de las variables de objeto no es tan didáctico aquí, no afecta a Su pregunta demasiado.)

Prueba

Vamos a demostrar ahora que la proposición de que `Yo = S K K''.

Pasos para el lado izquierdo:

• la proposición `Yo x = x" es una instancia de I-axioma esquema con instatiation [E := x]

Pasos para la mano derecha:

• La proposición "S K K x = K x (K x)" es una instancia de S-axioma esquema con las instancias [E := K, F := K, G := x], por lo tanto es discutible
• La proposición "K x (K x) = x" es una instancia de K-axioma esquema con las instancias [E := x, F := K x], por lo tanto es discutible

La transitividad de la igualdad:

• Declaración "S K K x = K x (K x)" coincide con la primera premisa de transitividad la regla de inferencia, y la declaración "K x (K x) = x" coincide con la segunda premisa de esta regla de inferencia.Los casos son [E := S K K x, F := K x (K x), G = x].La conclusión a la que tiene demasiado: E = G.La reescritura de la conclusión con los mismos casos, podemos obtener la declaración de "S K K x = x", por lo tanto, esta es discutible.

La simetría de la igualdad:

• El uso de "S K K x = x", podemos inferir "x = S K K x"

La transitividad de la igualdad:

• El uso de "Yo x = x" y "x = S K K x", podemos inferir "Yo x = S K K x"

Ahora hemos allanado el camino para el punto crucial:

• La proposición "Yo x = S K K x" coincide con la primera premisa de La extensión de la regla de inferencia:(E x) = (F x), con las instancias [E := Yo, F := S K K].La conclusión a la que también debe tener, es decir, "E = F"con los mismos casos ([E := Yo, F := S K K]), dando la proposición "Yo = S K K", quod brindamos demonstrandum.

---

Csörnyei, Zoltán (2007): Lambda-kalkulus.Un funkcionális programozás alapjai. Budapest:Typotex.ISBN-978-963-9664-46-3.

Answer 2

No es necesario definir I como un axioma. Comenzar con lo siguiente:

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

Desde SKanything = anything, entonces SKanything es una función de la identidad, al igual que I.

Así, I = SKK y I = SKS. No hay necesidad de definir I como un axioma, se puede definir como el azúcar de sintaxis, que alias SKK.

Las definiciones de S y K son Sólo axiomas.

Answer 3

Los axiomas son habituales completa para la igualdad beta, pero no dan la igualdad eta. Curry encontró un conjunto de una treintena de axiomas a los habituales para conseguir la igualdad de integridad de beta-eta. Que están enumerados en Hindley y Seldin de Introducción a los combinadores y cálculo lambda .

Roger Hindley, de Curry último problema , se enumeran algunos desiderata adicional que podría desear de asignaciones entre el cálculo lambda y notas que no tenemos las asignaciones que satisfagan todos ellos. Es probable que no importa mucho acerca de todos los criterios.