Eliminação de corte para cálculo com nats ou outro tipo de dados indutivo?

14

Alguém me leva a um artigo detalhando um teorema da eliminação de cortes para a lógica intuicionista proposicional, incluindo um tipo de dados indutivo, como os números naturais (listas ou árvores também ficariam bem)? Um exemplo do tipo de sistema no qual estou interessado é o T de Godel, que possui tipos dados pela gramática . Não estou muito interessado em quantificadores sobre números naturais ou predicados indexados por números naturais.UMA:: =N|UMAUMA

Eu sei como provar a normalização beta para a versão de dedução natural desses sistemas usando um argumento de relações lógicas (ou técnicas relacionadas, como NbE), mas gostaria de saber se existem referências padrão sobre como adaptar esses métodos aos cálculos sequenciais.

A razão pela qual pergunto é que estou estudando a adição de operadores de ponto fixo para recursão protegida em um idioma. A idéia denotacional é bastante antiga - interpretar tipos como espaços ultramétricos e pontos fixos através do teorema de Banach - mas as técnicas puramente sintáticas que conheço para provar a eliminação de cortes não parecem se adaptar tão bem.

Neel Krishnaswami
fonte

Respostas:

10

E o trabalho de Ulrich Berger? Por exemplo Normalização forte para cálculos lambda aplicados . A parte "constantes recursivamente definidas" fornece tipos indutivos, mais ou menos. E não se deixe levar pela palavra "não digitado", ele também obtém resultados para sistemas digitados.

Andrej Bauer
fonte
Esta é uma ideia muito interessante! Estou interessado em adicionar (por exemplo) constantes para pontos fixos que não são necessariamente regras da esquerda ou da direita, portanto, esse parece ser um bom lugar para procurar.
Neel Krishnaswami
10

Você pode dar uma olhada em McDowell e Miller's Cut-Elimination for a Logic with Definitions and Induction , que mostra como adotar o método de Tait em um cálculo seqüencial intuicionista de primeira ordem com um predicado de números naturais definido indutivamente.

Noam Zeilberger
fonte
Obrigado - li este artigo há algum tempo, mas esqueci. Vou dar outra olhada.
Neel Krishnaswami