Normalisation forte
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.
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.
Réponses
-
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 -
Ca tombe bien, j'ai le bouquin.
Merci infiniment et à bientôt peut-être pour de nouvelles aventures.
Pierrot.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.2K Toutes les catégories
- 9 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 64 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 314 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 773 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres