Intuição por trás da estrita positividade?

Eu estou querendo saber se alguém pode me dar a intuição por que a estrita positividade de tipos de dados indutivos garante forte normalização.

Para ser claro, vejo como ter ocorrências negativas leva à divergência, ou seja, definindo:

data X where Intro : (X->X) -> X

podemos escrever uma função divergente.

Mas estou me perguntando, como podemos provar que tipos indutivos estritamente positivos não permitem divergências? ou seja, existe alguma medida de indução que nos permita construir uma prova de forte normalização (usando relações lógicas ou similar)? E onde essa prova se decompõe para ocorrências negativas? Existem boas referências que mostram forte normalização para uma linguagem com tipos indutivos?

Parece que você deseja uma visão geral dos argumentos de normalização para sistemas de tipos com tipos de dados positivos. Eu recomendaria a tese de doutorado de Nax Mendler: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

Como a data sugere, este é um trabalho bastante clássico. A intuição básica é que um ordinal pode ser associado a qualquer elemento de um tipo indutivo positivo, por exemplo, para o tipo de dados$\lambda$

Inductive Ord = Zero : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

Nós teríamos:

onde varia sobre termos com formas normais. A ressalva é que essa interpretação só é definida no terceiro caso quando tem uma forma normal, o que requer algum cuidado nas definições.$n$$f\ n$

Pode-se então definir funções recursivas por indução sobre este ordinal.

Observe que esses tipos de dados já podem ser definidos na teoria clássica dos conjuntos, conforme indicado no excelente artigo sobre famílias indutivas de Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ). No entanto, como os espaços de função são muito grandes, tipos como Ordrequerem ordinais realmente grandes para serem interpretados.

Outra boa fonte para ir além dos tipos estritamente positivos é a tese de doutorado de Ralph Matthes: http://d-nb.info/956895891

Ele discute extensões do Sistema F com tipos (estritamente) positivos no capítulo 3 e comprova muitos fortes resultados de normalização no capítulo 9. Existem algumas idéias interessantes discutidas no capítulo 3.

1. Podemos adicionar menos pontos fixos para qualquer tipo com variável livre , desde que possamos fornecer uma testemunha de monotonicidade . Essa idéia já está presente no trabalho de Mendler que eles mencionaram. Tais testemunhas existem canonicamente para qualquer tipo positivo, porque são sintaticamente monótonas.$\rho$$\alpha$$\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$

2. Quando passamos de tipos estritamente positivos para positivos, os tipos indutivos não podem mais ser vistos como árvores (a codificação do tipo W). Em vez disso, eles introduzem alguma forma de impredicatividade, porque a construção de um tipo indutivo positivo já quantifica sobre o próprio tipo. Observe que essa é uma forma um tanto moderada de impredicatividade, pois a semântica de tais tipos ainda pode ser explicada em termos de iteração ordinal de funções monótonas.

3. Matthes também fornece alguns exemplos de tipos indutivos positivos. Particularmente interessantes são

   • o tipo de continuação , em que não ocorre em .$\mu.\, 1 + ((\alpha \to \rho) \to \rho)$$\alpha$$\rho$
   • o tipo que funciona para qualquer tipo , transformando-o em um tipo positivo. Observe que isso usa muito a impredicatividade do sistema F.$\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$$\rho$

Matthes também usa tipos indutivos positivos para analisar a dupla negação, por exemplo, neste artigo: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Ele introduz uma extensão do de Parigot e prova forte normalização.$\lambda\mu$

Espero que isso ajude com sua pergunta.