Existe um cálculo lambda digitado que seja consistente e Turing completo?

20

Existe um cálculo lambda digitado em que a lógica correspondente sob a correspondência de Curry-Howard é consistente e onde existem expressões lambda tipificáveis ​​para todas as funções computáveis?

Esta é, sem dúvida, uma pergunta imprecisa, sem uma definição precisa de "cálculo lambda digitado". Estou basicamente me perguntando se existem (a) exemplos conhecidos disso ou (b) provas conhecidas de impossibilidade para algo nessa área.

Edit: @cody fornece uma versão precisa dessa pergunta em sua resposta abaixo: existe um sistema lógico de tipo puro (LPTS) que seja consistente e Turing completo (em um sentido definido abaixo)?

Morgan Thomas
fonte
2
Não há cálculo recursivamente axiomatizable (lambda ou outro) cujas funções recursivas comprovadamente totais são todas funções recursivas; portanto, seu cálculo precisaria envolver termos não-terminativos.
Emil Jeřábek apoia Monica
2
Essa resposta tem um teorema que diz que você não pode ter nenhum tipo de cálculo que seja completo e total de Turing .
Andrej Bauer
1
Provavelmente, ele responderá à sua pergunta assim que você for suficientemente preciso. Eu acho que a prova de Andrej é desnecessariamente complicada (mas mostra mais): o ponto é simplesmente que, se houvesse um sistema efetivamente descrito em que todas as funções recursivas fossem representáveis ​​de tal maneira que você possa certificar sintaticamente que uma expressão é uma representação honesta de um função recursiva (por exemplo, verificando se foi digitada corretamente no sistema), você obteria uma função recursiva total universal, o que é impossível.
Emil Jeřábek apoia Monica
1
Obviamente, uma resposta clássica para esse tipo de pergunta poderia ser: digitada -calculus com tipos de interseção , pois ela digita todos (e somente aqueles) termos que estão fortemente normalizando. É mais uma questão filosófica perguntar se o cálculo admite ou não uma "interpretação de Curry-Howard". λ
Cody
2
É difícil ser mais preciso aqui, porque a pergunta não é precisa.
Andrej Bauer

Respostas:

21

Tudo bem, eu vou dar uma olhada nisso: em geral, para um determinado sistema de tipo , o seguinte é verdadeiro:T

Se todos os termos do tipo bem no cálculo estiverem normalizando, será consistente quando visto como uma lógica.TT

A prova geralmente prossegue assumindo que você tenha um termo do tipo , usando a redução de assunto para obter uma forma normal e, em seguida, prosseguindo por indução na estrutura desse termo para obter uma contradição.absurdFalse

É natural se perguntar se o inverso vale, ou seja,

Para qualquer sistema de tipos , se for logicamente consistente , todos os termos bem digitados em estão normalizando.TTT

O problema disso é que não existe uma noção mais geral real de "sistema de tipos" e ainda menos concordância sobre o significado de consistência lógica para esses sistemas. No entanto, podemos empiricamente verificar se

Para os sistemas de tipos mais conhecidos que têm uma interpretação lógica, o inverso é realmente válido.

Como isso se vincula à Completude de Turing? Bem, por um lado, se a verificação de tipo for decidível , o argumento de Andrej mostra que um dos seguintes itens deve ser válido:

  1. O conjunto de todos os programas bem digitados não é o Turing Complete.
  2. Existe um programa bem digitado e sem terminação.

Isso tende a sugerir que:

Os sistemas de tipos que têm uma interpretação lógica e são consistentes e são recursivamente enumeráveis não são Turing Complete.

Dar um teorema real, em vez de uma sugestão, exige que a noção de sistemas de tipos e interpretações lógicas seja matematicamente precisa.

Agora, dois comentários vêm à mente:

  1. Existe um sistema de tipos indecidíveis , o sistema de tipos de interseção que tem uma interpretação lógica e pode representar todos os normalização . Como você observa, isso não é o mesmo que ser Turing Complete, pois o tipo de uma função total pode precisar ser atualizado (refinado, de fato) antes de aplicá-lo ao argumento desejado. O cálculo é um cálculo "estilo curry" e é igual a STLC + Γ M : τλ e yH:τσ

    ΓM:τΓM:σΓM:τσ
    É claro que a "interpretação"=leva a uma interpretação lógica consistente.
    ΓM:τσΓM:τΓM:τσΓM:σ
    =
  2. Existe uma classe de sistemas de tipos, os Pure Type Systems , nos quais essa pergunta pode ser precisa. Nesse contexto, no entanto, a interpretação lógica é menos clara. Pode-se ficar tentado a dizer: "um PTS é consistente se tiver um tipo desabitado". Mas isso não funciona, pois os tipos podem viver em diferentes "universos", onde alguns podem ser consistentes e outros não. Coquand e Herbelin definem uma noção de Logical Pure Type Systems , na qual a questão faz sentido, e mostram

    Todo LPTS inconsistente e não dependente possui um combinador de loop (e Turing Complete)

    O que responde à pergunta em uma direção (inconsistente TC) neste caso. Até onde eu sei, a pergunta para o LPTS geral ainda é aberta e bastante difícil.


Edit: O inverso do resultado Coquand-Herbelin não é tão fácil quanto eu pensava! Aqui está o que eu vim até agora.

Um lógico puro tipo de sistema é um PTS com (pelo menos) do tipo e T y p e , (pelo menos) o axioma P r o p : T y p e e (pelo menos) a regra ( P r o p , P r o p , P r o p ) , com o requisito adicional de que não existem tipos de tipo P r o p .PropTypeProp:Type(Prop,Prop,Prop)Prop

Agora eu vou assumir uma declaração particular de Turing Integralidade: corrigir um LPTS e deixá Γ ser o contextoLΓ

Γ=nat:Prop, 0:nat, S:natnat

éTuring completasse para cada total de função calculável f : NN existe um termo T f tais que y t f : n um tn um T e para cada n N t f ( S n 0 ) * β S f ( n ) 0Lf:NNtf

Γtf:natnat
nN
tf (Sn 0)βSf(n) 0

Agora, o argumento de diagonalização de Andrej mostra que existem não termináveis do tipo n a t .tnat

Agora parece que estamos no meio do caminho! Dado um termo não terminação , queremos substituir ocorrências de n um t por algum tipo genérico A e se livrar de 0 e S em Γ , e teremos a nossa inconsistência ( A é habitada no contexto A : P r o p )!Γloop:natnatA0SΓAA:Prop

Infelizmente, é aqui que eu fico preso, pois é fácil substituir pela identidade, mas o 0 é muito mais difícil de se livrar. Idealmente, gostaríamos de usar algum teorema da recursão Kleene, mas ainda não o descobri.S0

cody
fonte
OK, então os dois primeiros esclarecimentos sobre sua observação (1). O que você quer dizer quando diz que esse sistema de tipos de interseção não é recursivamente enumerável? Certamente, o conjunto de teoremas do sistema é re, porque você o deu como um cálculo seqüencial direto. Além disso, o resultado que eu vejo comprovado no artigo que você vinculou é que os termos tipáveis ​​no sistema são exatamente os termos fortemente normalizadores; mas isso não é diferente de dizer que ele pode digitar exatamente o total de funções computáveis? Por exemplo, não é fortemente normalizado, mas não total? λx.xx
Morgan Thomas
Agora, uma pergunta sobre sua observação (2). Parece-me que o teorema que você cita não é o que nos interessa. Diz que para todo LPTS não dependente, se for inconsistente, é Turing completo. Mas gostaríamos de saber se, para cada LPTS, se o Turing está completo, é inconsistente. Estou entendendo algo errado aqui?
Morgan Thomas
@MorganThomas: Ah, você está correto sobre o primeiro ponto: o que eu quis dizer é que o sistema de tipos não pode ser decidido , ou seja, dada , a afirmação Γ t : A é indecidível. Eu vou corrigir isso no post. Γ,t,UMAΓt:A
Cody
O segundo ponto: você também está certo de que se pode ter uma função não total que seja bem digitada (embora não se possa necessariamente aplicá-la a um determinado argumento). Vou alterar a resposta.
Cody
1
Terceiro ponto. Você está correto de novo! No entanto, o inverso (no caso especial do LPTS) é bastante trivial. Vou descrever o argumento.
Cody
11

Aqui está uma resposta para uma variante da precisão da minha pergunta por @ cody. Existe um LPTS consistente que é Turing completo no sentido aproximadamente de cody, se permitirmos a introdução de axiomas adicionais e regras de redução de . Assim, estritamente falando, o sistema não é um LPTS; é apenas algo parecido com um.β

Considere o cálculo das construções (ou seu membro favorito do cubo ). Este é um LPTS, mas vamos adicionar coisas extras que o tornam não um LPTS. Escolha os símbolos constantes nat , 0 , S e adicione os axiomas:λnat,0,S

0 : nat S : nat nat

nat:
0:nat
S:natnat

Indexe os programas da máquina de Turing por números naturais e, para cada número natural , escolha um símbolo constante f e , adicione o axioma f e : nat nat e, para todos e , x N , adicione a regra de redução βefefe:natnate,xNβ

fe(x)βΦe(x),

em que, como de costume é a saída da e th programa máquina Turing sobre x . Se Φ e ( x ) diverge, esta regra não faz nada. Observe que, adicionando esses axiomas e regras, os teoremas do sistema permanecem recursivamente enumeráveis, embora seu conjunto de regras de redução β não seja mais decidível, mas apenas recursivamente enumerável. Acredito que poderíamos facilmente manter o conjunto de regras de redução β decidível, explicitando explicitamente os detalhes de um modelo de computação na sintaxe e nas regras do sistema.Φe(x)exΦe(x)ββ

Agora, essa teoria é claramente Turing completa no sentido de @cody, apenas pela força bruta; mas a alegação é que também é consistente. Vamos construir um modelo disso.

Vamos de três sets, de tal forma que:U1U2U3

  • (onde S é a função sucessora).,N,0,SU1S
  • Cada conjunto é transitivo; se , então a U i .abUiaUi
  • Cada conjunto é fechado sob a formação de espaços funcionais; ou seja, se , então B AU i .A,BUiBAUi
  • Cada conjunto é fechado sob a formação de produtos dependentes; ou seja, se e f : Um L i , em seguida, Π um Um F ( um ) L i .AUif:AUiaAf(a)Ui

A existência de tais conjuntos segue, por exemplo, o ZFC mais o axioma de que todo cardeal é delimitado por um cardeal inacessível; podemos considerar que cada conjunto é um universo de Grothendieck.Ui

Definimos uma "interpretação" como um mapeamento do conjunto de nomes de variáveis ​​para elementos de U 2 . Dada uma interpretação v , podemos definir uma interpretação I v dos termos do sistema da maneira evidente:vU2vIv

  • , para x um nome de variável.Iv(x)=v(x)x
  • .Iv()=U1,Iv()=U2
  • .Iv(nat)=N,Iv(0)=0,Iv(S)=S
  • , ou seja, a função NN definida pelo e th programa Turing.Iv(fe)=ΦeNNe
  • Iv(AB)=Iv(A)(Iv(B))Iv(A)Iv(B)Iv(AB)=0
  • Iv(λx:A.B)aIv(A)Iv[x:=a](B)
  • Iv(Πx:A.B)=aIv(A)Iv[x:=a](B)

AIv(A)U3vA:BvA:BIv(A)Iv(B)ΓA:Bvvx:C(x:C)ΓvA:B

ΓA:BΓA:Bx,yy:x:yy

β

Morgan Thomas
fonte
2
Afe(x)Φe(x)ιββfe(x)ιβ
Eu acho que você está certo. Este não é o meu campo, por isso sou um pouco desajeitado ao fazer as coisas. :-) Eu acho que sua prova funciona, e uma conseqüência interessante, se eu estiver certo, é que essa teoria não tem muita força de consistência. Parece uma teoria potencialmente muito poderosa, pois possui tipos e números naturais, o que deve permitir que você interprete a teoria dos conjuntos; mas aparentemente você não pode, porque pode provar que é consistente sem usar a poderosa teoria dos conjuntos!
Morgan Thomas