Intuition derrière une positivité stricte?

Je me demande si quelqu'un peut me donner l'intuition derrière pourquoi la positivité stricte des types de données inductifs garantit une forte normalisation.

Pour être clair, je vois comment avoir des occurrences négatives conduit à la divergence, c'est-à-dire en définissant:

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

nous pouvons écrire une fonction divergente.

Mais je me demande, comment pouvons-nous prouver que les types inductifs strictement positifs ne permettent pas la divergence? Existe-t-il une mesure d'induction qui nous permet de construire une preuve de forte normalisation (en utilisant des relations logiques ou similaires)? Et où une telle preuve se décompose-t-elle pour les événements négatifs? Y a-t-il de bonnes références qui montrent une forte normalisation pour une langue avec des types inductifs?

Il semble que vous souhaitiez un aperçu des arguments de normalisation pour les systèmes de types avec des types de données positifs. Je recommanderais la thèse de doctorat de Nax Mendler: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

$\lambda$

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

Nous obtiendrions:

où s'étend sur des termes aux formes normales. La mise en garde est que cette interprétation n'est définie que dans le 3ème cas lorsque a également une forme normale, ce qui nécessite un certain soin dans les définitions.$n$$f\ n$

On peut alors définir des fonctions récursives par induction sur cet ordinal.

Notez que ces types de données peuvent déjà être définis dans la théorie des ensembles classiques, comme indiqué dans l'excellent article sur les familles inductives de Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ). Cependant, comme les espaces de fonction sont si énormes, des types comme Ordnécessitent des ordinaux vraiment grands pour interpréter.

Une autre bonne source pour aller au-delà des types strictement positifs est la thèse de doctorat de Ralph Matthes: http://d-nb.info/956895891

Il discute des extensions du système F avec des types (strictement) positifs dans le chapitre 3 et prouve de nombreux résultats de normalisation solides dans le chapitre 9. Il y a quelques idées intéressantes discutées dans le chapitre 3.

1. Nous pouvons ajouter des points les moins fixes pour tout type avec variable libre , tant que nous pouvons fournir un témoin de monotonie . Cette idée est déjà présente dans le travail de Mendler que cody a mentionné. De tels témoins existent canoniquement pour tout type positif car ils sont syntaxiquement monotones.$\rho$$\alpha$$\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$

2. Lorsque nous passons de types strictement positifs à des types positifs, les types inductifs ne peuvent plus être considérés comme des arbres (l'encodage de type W). Au lieu de cela, ils introduisent une certaine forme d'imprédicativité parce que la construction d'un type inductif positif quantifie déjà sur le type lui-même. Notez qu'il s'agit d'une forme d'imprédicativité quelque peu légère, car la sémantique de ces types peut encore être expliquée en termes d'itération ordinale des fonctions monotones.

3. Matthes fournit également quelques exemples de types inductifs positifs. Particulièrement intéressants sont

   • le type de continuations , où ne se produit pas dans .$\mu.\, 1 + ((\alpha \to \rho) \to \rho)$$\alpha$$\rho$
   • le type qui fonctionne pour tout type en le transformant en un type positif. Notez que cela utilise très fortement l'imprédicativité du système F.$\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$$\rho$

Matthes utilise également des types inductifs positifs pour analyser la double négation, par exemple, dans cet article: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Il introduit une extension du de Parigot et prouve une forte normalisation.$\lambda\mu$

J'espère que cela répond à votre question.