Normalisation forte du lambda-calcul simplement typé.

Je suis pas sur que ça intéressera quelqu'un, mais voici un problème que je me pose depuis hier. Au pire, ça me fera des notes pour plus tard.

Je reste persuadé, depuis hier après-midi, qu'il doit être possible de prouver que le lambda-calcul fortement typé normalise fortement à l'aide d'un bon ordre sur les termes typable. Plus précisément, je pense que l'ordre des multi-ensemble doit pouvoir être utilisable. Quand on fait une bêta-réduction (lambda x. t)v->t[x:=v] alors l'élément "lambda x" disparait, et v apparait plusieurs fois. C'est typiquement un cas où si v est un élément plus petit que "lambda x" alors on pourrait se retrouver avec un multi-ensemble inférieur.

Pour simplifier, on peut supposer qu'il n'y a pas de variable libre dans le terme typé et qu'on ne considère que les bêtas-réductions.

Sauf que bien sur, je n'arrive pas à trouver ce bon ordre de base, ni quel multi-ensemble prendre. Si on choisit de faire un multi-ensemble des variables, alors l'ordre des variables et loin d'être évident, et même si on suppose que chaque abstraction possède un paramètre formel x différent, après une réduction, ce paramètre est recopié. Alors on peut renommer les paramètres afin que chaque variable soit différente, mais dans ce cas il y a des fortes chance qu'on perde le bon ordre, puisque le nombre de variable qu'on peut écrire n'est à priori pas borné.

De toute façon, ça ne pouvait pas marcher, puisque ça ne tenait pas compte des types, et qu'il est connu que le lambda-calcul non typé ne normalise pas.

Un multi-ensemble des types des sous-termes pourrait être très bien, ou l'ordre de base est F=>G >F et F=>G >G. Sauf que si on a (lambda x.t):F=>G, v:F et donc (lambda x.t)v:G alors on retire un F=>G du multi-ensemble et on rajoute potentiellement plein de fois les types des sous-termes de v. Ça tombe bien, c'est là la force de l'ordre d'un multi-ensemble. Seul bémol, mais j'ai mis du temps à m'en rendre compte, rien n'empêche que v ait un sous-terme de type F=>G.

J'ai essayé d'autre truc, mais pour le moment rien de bien...

En gros, depuis mon réveil à 3 heure du matin, et maintenant 8 heure, j'ai passé une bonne parti de mon temps à réfléchir à ça, et la nuit n'avait pas porté de bon conseils...

Si par le plus grand des hasard, quelqu'un sait pourquoi cette méthode ne pourrait pas marcher (et de préférence, autre que: si ça marchait, quelqu'un y aurait déjà pensé), je suis tout à fait preneur. En tout cas, je trouve la question rigolote.

Commentaires

1. Le samedi 16 mai 2009, 15:07 par Le Créateur fou

"il est connu que le lambda-calcul non typé ne normalise pas"
Pas grave, il reste Polytechnique!

Pour le reste, essaye Gabuzomeu.

2. Le samedi 16 mai 2009, 17:47 par Arthur RAINBOW

Je ne comprends pas ton commentaire, créateur fou.
Pourquoi tu m'insultes?

Tu me cites comme si je disais une annerie.
Tu vois bien que j'ai écris "NON" typé. (Si c'était typé, ça normalise, ça je suis d'accord)

Mais l'exemple classique (lambda x.x x)(lambda x. x x) est clairement un terme qui ne normalise pas.

3. Le mardi 19 mai 2009, 23:30 par Arthur RAINBOW

Honte à moi. Tu ne m'accusais pas de dire une bétise, mais opposait "normalisé"="normal sup" à l'X.

Toutes mes excuses.

Ajouter un commentaire

Le code HTML est affiché comme du texte et les adresses web sont automatiquement transformées.

La discussion continue ailleurs

URL de rétrolien : http://www.milchior.fr/blog/index.php?trackback/54

Fil des commentaires de ce billet