Combinator lógica axiomas

Question

Eu sou a realização de alguns experimentos no teorema provar com combinator lógica, que é olhar promissor, mas há uma pedra de tropeço:tem sido apontado que em combinator lógica é verdade que, por exemplo,I = SKK, mas este não é um teorema, tem de ser adicionado como um axioma.Alguém sabe de uma lista completa dos axiomas que precisa ser adicionado?

Editar:É claro que você pode provar por a mão que I = SKK, mas a menos que eu estou faltando alguma coisa, não é um teorema do sistema de combinator lógica com a igualdade.Dito isso, você pode apenas macro expanda eu SKK...mas ainda me falta algo importante.Tomando o conjunto de cláusulas de p(X) e ~p(X), o que facilmente resolver uma contradição em comum a lógica de primeira ordem, e convertê-los para SK, realizando a substituição e a avaliação de todas as chamadas de S e K, o meu programa gera a seguinte (onde eu estou usando ' for baseada num é backtick):

"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 true 'k verdadeiro

Parece que talvez o que eu preciso é de um conjunto apropriado de regras para a manipulação parcial chama de " k "s, só não estou vendo o que essas regras deveriam ser, e toda a literatura que se pode encontrar nesta área foi escrito para um público-alvo de matemáticos não programadores.Eu suspeito que a resposta é, provavelmente, bastante simples uma vez que você entenda isso.

Answer 1

Alguns livros definir Eu como mera alias para ((S K) K).Neste caso, eles são idênticos (como termos) per definitionem.Para provar sua igualdade (como funções), precisamos apenas provar que a igualdade é reflexiva, que pode ser alcançada através de uma reflexividade axioma esquema:

• A proposição `E = E"é dedutível (A reflexividade axioma esquema, instanciado para cada possível termos denotado aqui por metavariable E)

Assim, suponho que na seguidores, que Suas perguntas investiga outra abordagem:quando combinator Eu não está definido como um mera alias para o termo composto ((S K) K), mas apresentado como um autônomo básico combinator constante em sua própria, cuja semântica operacional é declarada explicitamente pelo axioma regime de

• ``(Eu E) = E"é dedutível (I-axioma o esquema)

Suponho que a questão pergunta

se podemos deduzir formalmente (dentro do sistema), que tal um autônomo-definido Eu comporta-se exatamente como ((S K) K), quando usado como funções em reduções?

Eu acho que nós podemos, mas temos de recorrer a mais forte ferramentas.Eu conjectura de que o de costume axioma esquemas não são suficientes, temos que declarar também o extensionality propriedade (igualdade de funções), que é o ponto principal.Se queremos formalizar extensionality como um axioma, temos que aumentar o nosso objeto de idioma com variáveis livres.

Eu acho que, temos que adotar tal abordagem para a construção de combinatória lógica, que nós temos para permitir também o uso de variáveis no objeto de linguagem.Ausência temporária do curso, eu quero dizer "basta" livre objetos de valor.Usando variī aveis estaria traindo, temos que permanecer dentro do reino da lógica combinatória.Usando o livre varaibles não é engano, é um honesto ferramenta.Assim, podemos fazer a prova formal de que Você necessário.

Além da simples igualdade de axiomas e regras de inferência (transitividade, reflexividade, simetria, Leibniz regras), deve-se adicionar um extensionality regra de inferência para a igualdade.Aqui é o ponto onde as variáveis livres importa.

Em Csörnyei 2007:157-158, eu encontrei a seguinte abordagem.Eu acho que desta forma, a prova pode ser feito.

Algumas observações:

A maioria dos axiomas são, na verdade, axioma esquemas de, que consiste de um número infinito de axioma instâncias.As instâncias deve ser instanciado para cada possível E, F, G termos.Aqui, eu uso o itálico para metavariables.

O superficial natureza infinita do axioma regimes de não levantar computability problemas, porque eles podem ser enfrentados em um tempo finito:o nosso axioma do sistema é recursiva.Isso significa que um inteligente analisador pode decidir em um tempo finito (além disso, de forma muito eficaz), se uma dada proposição é uma instância de um esquema de axioma, ou não.Assim, o uso do axioma regimes de não levantar nem teórico nem prático problemas.

Agora vamos parecem nosso quadro:

Idioma

ALFABETO

Constantes:Os três seguintes são chamados de constantes: K, S, Eu.

Eu adicionei o constante Eu só porque a Sua pergunta pressupõe que não temos definido o combinator Eu como um mero alias/macro para o termo composto S K K, mas ele é um autônomo constante no seu próprio.

Eu denotam constantes por negrito capitais romanas.

Sinal de aplicação:Um sinal @ de `aplicação" é suficiente (prefixo de notação de aridade 2).Como um açúcar sintático, eu uso aqui parantheses em vez de a aplicação explícita sinal:Eu uso o explícito abrir ( e fechar ) de sinais.

Variáveis:Embora combinator lógica não fazer uso de variī aveis, escopo, etc., mas podemos introduzir variáveis livres.Eu suspeito que eles não são apenas açúcar sintático, eles podem fortalecer o sistema de dedução, também.Eu conjectura, que a Sua pergunta vai exigir o seu uso.Qualquer conjunto infinito enumerável (separado das constantes e parênteses, sinais) vai servir como o alfabeto de variáveis, vou indicar aqui com formatado romanas minúsculas letras x, y, z...

TERMOS

Os termos são definidos indutivamente:

• Qualquer constante é um termo
• A variável é um termo
• Se E é um termo, e F é um termo muito, então também (E F é um termo

Eu às vezes uso prático convenções como um açúcar sintático, por exemplo,escrever

E F G H

em vez de

(((E F) G) H).

Dedução

Conversão axioma regimes:

• ``K E F = E"é dedutível (K-axioma o esquema)
• ``S F G H = F H (G H"é dedutível (S-axioma o esquema)
• ``Eu E = E"é dedutível (I-axioma o esquema)

Eu adicionei o terceiro conversão axioma (Eu regra geral) só porque a Sua pergunta pressupõe que nós não definido o combinator Eu como um alias/macro para S K K.

Igualdade axioma esquemas e regras de inferência

• ``E = E"é dedutível (A reflexividade axioma)
• Se "E = F"é dedutível, em seguida,"F = E"também é dedutível (Simetria regra de inferência)
• Se "E = F"é dedutível, e "F = G"é dedutível também, então também "E = G"é redutível (A transitividade regra geral)
• Se "E = F"é dedutível, em seguida,"E G = F G"também é dedutível (Regra de Leibniz eu)
• Se "E = F"é dedutível, em seguida,"G E = G F"também é dedutível (Leibniz regra II)

Pergunta

Agora vamos investigar a Sua pergunta.Eu conjectura de que o sistema de dedução definido até agora não é forte o suficiente para provar a Sua pergunta.

É proposta "Eu = S K K"dedutível?

O problema é que temos de provar a equivalência de funções.Podemos considerar duas funções equivalentes se eles se comportam da mesma maneira.Funções de agir, de modo que eles são aplicados aos argumentos.Devemos provar que ambas as funções funcionam da mesma forma, se aplicada a cada argumentos possíveis.Novamente, o problema com o infinito!Eu suspeito que, esquemas de axiomas não pode nos ajudar aqui.Algo como

Se E F = G F é dedutível, em seguida, também E = G é dedutível

não seria suficiente para fazer o trabalho:podemos ver que este não produzir o que queremos.Usando-o, podemos provar que

``Eu E = S K K E"é dedutível

para cada E prazo instância, mas estes resultados são apenas separados instâncias, e não pode ser usado como um todo, para outros descontos.Só temos resultados concretos (infinitos), não sendo capaz de resumi-los:

• isso vale para E := K
• vale para E := S
• isso vale para E := K K
• .
• .
• .

...

podemos resumir esses fragmentada resultado de instâncias em uma única grande resultado, indicando extensionality!Nós não pode derramar essas de baixo valor fragmento para o funil de uma regra de inferência que iria derreter-los juntos em um único e mais valioso do resultado.

Temos de aumentar o poder do nosso sistema de dedução.Temos de encontrar um instrumento formal que pode agarra o problema.Suas perguntas, leva a extensionality, e eu acho que, declarando extensionality necessidades que podem representar proposições que segure para * * * ****arbitrária***** instâncias.É por isso que eu acho que deve permitir a livre variáveis dentro de nosso objeto de linguagem.Eu conjectura de que o adicional seguinte regra de inferência irá fazer o trabalho:

• Se a variável x não é parte dos termos nem E nem F, e a declaração (E x) = (F x) é dedutível, em seguida, E = F também é dedutível (Extensionality regra de inferência)

O difícil neste axioma, facilmente, levando a confusão:x é um objeto variáveis, totalmente emancipada e respeitado partes de nosso objeto de linguagem, enquanto E e G são metavariáveis, e não as partes do objeto língua, mas usado apenas para uma notação concisa do axioma de esquemas.

(Comentário:Mais precisamente, o extensionality regra de inferência deve ser formalizada de forma mais cuidada, a introdução de uma metavariável x sobre todas as possíveis objeto as variáveis x, y, z..., e também um outro tipo de metavariável E sobre todas as possíveis prazo instâncias.Mas esta distinção entre os dois tipos de metavariables mais o objeto de variáveis não é tão didático que, aqui, ele não afeta a Sua pergunta demais.)

Prova

Vamos provar agora a proposição de que `Eu = S K K''.

Passos para o lado esquerdo:

• a proposição `Eu x = x" é uma instância de I-axioma esquema com instatiation [E := x]

Passos para o lado direito:

• A proposição "S K K x = K x (K x)" é uma instância de S-axioma esquema com instanciações [E := K, F := K, G := x], assim, é dedutível
• A proposição "K x (K x) = x" é uma instância de K-axioma esquema com instanciações [E := x, F := K x], assim, é dedutível

A transitividade da igualdade:

• Instrução "S K K x = K x (K x)" corresponde a primeira premissa do a transitividade regra de inferência, e a declaração "K x (K x) = x" corresponde a segunda premissa da regra de inferência.As instanciações são [E := S K K x, F := K x (K x), G = x].Assim, a conclusão a que detém também: E = G.Reescrever a conclusão com as mesmas instâncias, nós instrução get "S K K x = x", portanto, este é dedutível.

A simetria da igualdade:

• Usando o "S K K x = x", pode-se inferir "x = S K K x"

A transitividade da igualdade:

• Usando o "Eu x = x" e "x = S K K x", pode-se inferir "Eu x = S K K x"

Agora temos que abriu o caminho para o ponto crucial:

• A proposição "Eu x = S K K x" corresponde com a primeira premissa do Extensão regra de inferência:(E x) = (F x), com instanciações [E := Eu, F := S K K].Assim, a conclusão deve também conter, ou seja, "E = F"com o mesmo instanciações ([E := Eu, F := S K K]), resultando na proposição "Eu = S K K", quod erat demonstrandum.

---

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

Answer 2

Você não precisa definir i como um axioma. Comece com o seguinte:

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

Desde SKnada = nada, então SKnada é uma função de identidade, assim como I.

Então, I = SKK e I = SKS. Não há necessidade de definir I como um axioma, você pode defini -lo como açúcar de sintaxe que aliases SKK.

As definições de S e K são apenas axiomas.

Answer 3

Os axiomas usuais são completos para a igualdade beta, mas não dão igualdade de ETA. Curry encontrou um conjunto de cerca de trinta axiomas para os usuais para obter integridade para a igualdade beta-eta. Eles estão listados em Hindley e Seldin's Introdução aos combinadores e lambda-cálculo.

Roger Hindley, Último Problema de Curry, lista alguns desideratos adicionais que podemos querer dos mapeamentos entre o cálculo Lambda e as notas de que não temos mapeamentos que satisfazem todos eles. Você provavelmente não vai se importar muito com todos os critérios.