Classificação dos cálculos lambda digitados / não tipados

Alguém pode explicar brevemente (se isso for possível!) Ou me referir a uma referência, resumindo as diferenças entre o cálculo lambda não digitado e o cálculo lambda digitado mais comum?

Estou particularmente procurando declarações de seu poder expressivo, equivalências a sistemas lógicos / aritméticos ou métodos de computação e analogias com linguagens de programação, se aplicável.

Embora eu certamente pretenda ler, algo como uma tabela de referência descrevendo os cálculos e suas equivalências / diferenças / lugar na hierarquia seria uma enorme referência para me ajudar a resolvê-los.

Não dizendo que o abaixo está correto, apenas tentando esboçar algumas das impressões que tenho para ver se elas pelo menos servem como ponto de partida (ou algo para corrigir!)

Cálculo lambda não tipado - eq. à lógica de primeira ordem - não é possível fazer X

Cálculo lambda simplesmente digitado - eq para ... lógica, relacionada ao Lisp?

Lambda 'polimórfico' calc - etc.

Cálculo de Construções - lógica intucionista?

Lógica Combinatória - comparável a ??? cálculo lambda digitado, relacionado ao tipo de linguagem APL / J

Se isso se relacionar com o cubo lambda e seus três eixos, melhor.

Embora eu esteja familiarizado com o básico do cálculo lambda e da programação com linguagens funcionais, nunca estudei minha cabeça ou fiz conexões significativas com os sistemas de tipos envolvidos e os diferentes tipos de cálculos lambda (e talvez pi?).

Quando tento pesquisar isso, não posso deixar de me desviar, abrindo muitas abas do navegador e se ramificando em tantas direções que nunca entro em nenhuma delas com profundidade!

Não tenho certeza se o que estou pedindo é razoável, mas espero que pelo menos tenha pintado uma imagem suficiente para sugerir alguma leitura que possa explicar o que estou procurando?

Sua mesa está um pouco confusa; aqui está um melhor.

• Cálculo lambda sem tipo - sem interpretação lógica, como observa Andrej
• Cálculo lambda de tipo simples - lógica proposicional intuicionista
• Cálculo lambda polimórfico - lógica pura de segunda ordem (ou seja, sem quantificadores de primeira ordem)
• Tipos dependentes - generalização da lógica de primeira ordem
• Cálculo de construções - generalização da lógica de ordem superior

A dependência de tipo é mais geral que a quantificação de primeira ordem, pois transforma provas em objetos que você pode quantificar. Existem cálculos lambda correspondentes a FOL intuicionistas comuns, mas não são amplamente usados ​​o suficiente para ter um nome especial - as pessoas tendem a ir direto para os tipos dependentes.

Também é possível relacionar a forma sintática de um cálculo com sistemas lógicos.

• Cálculos do combinador (por exemplo, combinadores SKI) - sistemas no estilo Hilbert
• Forma A-normal - cálculo sequencial
• Cálculo lambda de tipo ordinário - dedução natural

$\lambda$$\lambda$$\lambda$nat$\lambda$$0$$T$

$\lambda$$\lambda$

$\lambda$$\lambda$

$\lambda$$\lambda$$\lambda$Ulambda : U -> (U -> U)gamma : (U -> U) -> U$\lambda$$\mathbb{U}$$\lambda$$\mathcal{C}$$\mathbb{U}$$\mathbb{U}$$[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$$\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$

Referências:

• Dana S. Scott: " Cálculo Lambda: Alguns Modelos, Alguma Filosofia ", Estudos em Lógica e os Fundamentos da Matemática, Volume 101, 1980, Páginas 223-265, Simpósio Kleene

• Hendrik Pieter Barendregt: " O cálculo lambda: sua sintaxe e semântica ", Elsevier, 1984.

Uma discussão bastante abrangente dessas coisas pode ser encontrada neste livro: Palestras sobre o isomorfismo Curry-Howard . Isso se baseia na versão antiga disponível gratuitamente: Palestras sobre o Isomorfismo Curry-Howard .