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

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

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.$T$$T$

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.$\mathrm{absurd}$$\mathrm{False}$

É 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.$T$$T$$T$

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 : $\lambda$ e y⊢H:τ∩

   $$\frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma}$$ É claro que a "interpretação"∩=∧leva a uma interpretação lógica consistente. $$\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$$ $\cap=\wedge$

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.$\Rightarrow$

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 .$\mathrm{Prop}$$\mathrm{Type}$$\mathrm{Prop}:\mathrm{Type}$$(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$$\mathrm{Prop}$

Agora eu vou assumir uma declaração particular de Turing Integralidade: corrigir um LPTS e deixá Γ ser o contexto$L$$\Gamma$

éTuring completasse para cada total de função calculável f : N → N existe um termo T f tais que y ⊢ t f : n um t → n um T e para cada n ∈ N t f ( S n 0 ) → * β S f ( n )$L$$f:\mathbb{N}\rightarrow\mathbb{N}$$t_f$

Agora, o argumento de diagonalização de Andrej mostra que existem não termináveis do tipo n a t .$t$$\mathrm{nat}$

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 )!$\Gamma \vdash \mathrm{loop}:\mathrm{nat}$$\mathrm{nat}$$A$$0$$S$$\Gamma$$A$$A:\mathrm{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.$S$$0$

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.$\beta$

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:$\lambda$$\text{nat}, 0, S$

⊢ 0 : nat ⊢ S : nat →

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 $e$$f_e$$f_e : \text{nat} \to \text{nat}$$e,x \in \mathbb{N}$$\beta$

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.$\Phi_e(x)$$e$$x$$\Phi_e(x)$$\beta$$\beta$

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:$U_1 \in U_2 \in U_3$

• (onde S é a função sucessora).$\emptyset, \mathbb{N}, 0, S \in U_1$$S$
• Cada conjunto é transitivo; se , então a ∈ U i .$a \in b \in U_i$$a \in U_i$
• Cada conjunto é fechado sob a formação de espaços funcionais; ou seja, se , então B A ∈ U i .$A, B \in U_i$$B^A \in U_i$
• 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 .$A \in U_i$$f : A \to U_i$$\prod_{a \in A} f(a) \in U_i$

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.$U_i$

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:$v$$U_2$$v$$I_v$

• , para x um nome de variável.$I_v(x) = v(x)$$x$
• .$I_v(\ast) = U_1, I_v(\Box) = U_2$
• .$I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$
• , ou seja, a função N → N definida pelo e th programa Turing.$I_v(f_e) = \Phi_e$$\mathbb{N} \to \mathbb{N}$$e$
• $I_v(AB) = I_v(A)(I_v(B))$$I_v(A)$$I_v(B)$$I_v(AB) = 0$
• $I_v(\lambda x : A. B)$$a \in I_v(A)$$I_{v[x:=a]}(B)$
• $I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$

$A$$I_v(A) \in U_3$$v$$A : B$$v \models A : B$$I_v(A) \in I_v(B)$$\Gamma \models A : B$$v$$v \models x : C$$(x : C) \in \Gamma$$v \models A : B$

$\Gamma \vdash A : B$$\Gamma \models A : B$$x,y$$y : \ast \models x : y$$y$$\emptyset$

$\beta$