Teoria e computabilidade de tipos simplesmente tipados.

Question

Suponha que tipos atômicos de cálculo lambda simplesmente tipado ($\lambda\to$) são interpretados como conjuntos. Toda função computável (total) pode ser escrita como termo em tal cálculo?

Se não, dê um contra-exemplo. Se sim, por favor, dê um título de algum livro ao qual eu possa me referir. (Suspeito que seja algo como "tese de Kleene", mas não tenho certeza.)

ps existe referência "padrão" para algum livro (monografia?) sobre cálculo lambda digitado simples que contém tudo que cobre este tópico?

Answer 1

A resposta é não. Se por tipos atômicos queremos dizer constantes de tipo base sem nenhuma regra de introdução ou eliminação, então para qualquer tipo base$A$, o tipo$A \rightarrow A$tem apenas a função identidade$\lambda x. x$como morador fechado. Isto segue por indução em formas normais. Daí, se$A$é interpretado como qualquer conjunto com mais de um elemento, existem funções computáveis ​​que não são definíveis como termos lambda.

Há uma caracterização precisa das funções da teoria dos conjuntos que são definíveis como termos STLC: estas são as funções que preservam todos os predicados lógicos de Kripke em tipos básicos. Aqui está uma bela e moderna exposição com uma formalização Agda . A ideia AFAIK vem daqui , mas acho isso um pouco desatualizado na terminologia e na exposição. A frase-chave para pesquisar resultados como este é "definibilidade lambda".

E se tivermos tipos de base para números naturais,$\mathsf{Bool}$, etc., com as regras apropriadas de introdução e eliminação? Por exemplo, pode STLC+$\mathsf{Nat}$definir todos os computáveis$\mathbb{N} \rightarrow \mathbb{N}$funções? A resposta ainda é não. Não existe uma linguagem de programação total para todas as funções computáveis ​​totais, por razões Gödelianas. Em particular, nenhuma linguagem total implementa um autointerpretador, porque isso poderia ser usado para implementar a recursão geral, contrariando a totalidade. Este é um resultado folclórico, você pode encontrá-lo, por exemplo, como Teorema 3.2 aqui .

No caso de STLC+$\mathsf{Nat}$, temos informações um pouco mais específicas sobre funções definíveis: sabemos que o ordinal da teoria da prova desse sistema é$\epsilon_0$, uma vez que a) esta linguagem é o Sistema T de Gödel, e Gödel mostrou que as funções definíveis no Sistema T são precisamente as funções comprovadamente totais na Aritmética de Peano b) a força teórica de prova de PA é$\epsilon_0$. Portanto$f_{\epsilon_0}$na hierarquia de crescimento rápido é um exemplo para um computável$\mathbb{N} \rightarrow \mathbb{N}$função que não é definível em STLC+$\mathsf{Nat}$, e de fato cresce mais rápido do que qualquer STLC+$\mathsf{Nat}$-função definível.