Normalisation forte

Le barbu rasé

Je peine à montrer la normalisation forte d'un système de types.

J'ai lu (sans d'ailleurs beaucoup comprendre) plusieurs preuves de normalisation forte de diverses extension du lambda-calcul, et cela m'a réellement donné l'impression que la seule méthode est de s'y prendre "au cas par cas", sans qu'il y ait de stratégie générale.

En même temps, j'ai du mal à y croire. Quelqu'un (Ambrym?) pourrait-il infirmer en me proposant une telle stratégie ?

Merci d'avance,
Pierrot.

Ambrym0

Salut !
Mon stage de recherche consiste justement à démontrer un certains nombres de propriétés (notamment SN) sur des systèmes de types en utilisant principalement des propriétés sémantiques, ce qui permet de justifier en partie la syntaxe utilisée pour un grand nombre de systèmes.

On peut en fait faire mieux qu'une solution au cas par cas.
Une solution assez puissante consiste à utiliser les candidats de réductibilités (c'est d'ailleurs la seule démo connues pour certains systèmes de types dépendants). Le problème c'est qu'il semble qu'il y ait plusieurs définitions possibles (non équivalentes d'ailleurs). La plus répandue utilise 3 conditions de cloture que l'on trouve dans n'importe quel bouquin.

La stratégie est très bien expliquée dans le livre de Girard "PROOFS AND TYPES", qui te donneras également pleins d'intuitions sympas qu'il serait fastidieux de développer ici.

Ambrym

Le barbu rasé

Ca tombe bien, j'ai le bouquin.

Merci infiniment et à bientôt peut-être pour de nouvelles aventures.

Pierrot.