Lambda-calcul simplement typé : terminaison assurée ? [Résolu]

[Ekinoks]

Bonjour,

Ça fait un petit moment que je m'intéresse au langage fonctionnel et plus précisément au lambda-calcul.
Un grand avantage du lambda-calcul simplement typé (souvent mis en avant) est la terminaison obligatoire des algorithmes.

Cette propriété m'intrigue et je cherche a comprendre comment cette propriété peut être assuré. Malheureusement, je n'arrive pas à trouver d'explication simple sur Internet (je connais très peu les langages fonctionnels).

Quelqu'un serait comment cette propriété peut être assuré ?

Merci pour votre aide.

[gorgonite]

te donnera plein de liens... mais souvent chez springer (accessible après abonnement)


Strong Normalization of Substitutions je peux de l'envoyer par mail ,)

[gasche]

Pour le lambda-calcul simplement typé, la preuve est simple, il s'agit d'un simple argument de bonne fondation : on trouve la bonne mesure sur les termes, et on montre qu'une réduction réduit strictement cette mesure, donc qu'il ne peut y avoir qu'un nombre fini de réductions.

L'idée de base c'est qu'on regarde dans un terme les parties qui ont un type "compliqué", avec beaucoup de flèches imbriquées. Quand tu fais des réductions, tu transformes un "redex" de la forme ((λx b) a) en b[x := a], donc tu passes d'une fonction (λx b) à une simple valeur b[x := a] : si tu regardes la "complication" des types, elle a diminué, puisque tu passes de (A→B) à B.
Quand tu regardes un terme dans l'ensemble, sa "complexité totale" est finie. Comme elle diminue quand tu réduis, et que tu peux choisir les bonnes réductions qui font qu'elle réduit *strictement*, tu sais que tu ne pourras avoir qu'un nombre fini de pas de réduction : ça termine forcément.

Plus précisément, on définit :
- le degré d'un type : d(type constant) = 0, d(A→B) = 1 + max(d(A), d(B))
- le degré d'un redexe : d((λx b) a) = d(A→B) où A→B est le type de (λx b)
- le degré d'un terme : le degré maximal de ses redexes

Ensuite, tu prends comme mesure d'un terme le couple (degré du terme, nombre de redexes de degré maximal). À chaque étape, tu choisis un redex ((λx b) a) de degré maximal tel que tous les rédexes qu'il contient sont de degré inférieur, et tu le réduis. Cela réduit strictement le nombre de redexes de degré maximal, car les redexes restants sont :
- les redexes dans la partie du terme restée inchangée
- les redexes présents dans a (donc de degré inférieur) qui ont été potentiellement dupliqués
- les redexes créés par le remplacement de x par a : si a est un λ-terme, les termes de la forme "x c" deviennent des redexes, du degré du type A de a, qui est par définition inférieur au degré du redex réduit ((λx b) a, de type A → B), donc inférieur au degré maximal

Si le nombre de redexes de degré maximal devient nul, on prend le degré inférieur maximal, on compte ses redexes et on recommence. À chacune de ces étapes, le nombre de redexes est fini (puisque le terme est fini), et le degré maximal décroit strictement, donc forcément on fini par s'arrêter (puisqu'il ne peut pas devenir négatif), et il n'y a plus de redexes à réduire : on a trouvé une forme normale.


Plus le système de type est puissant, plus la preuve de terminaison est difficile. Le lambda calcul simplement-typé n'est pas très puissant, donc la preuve de terminaison n'est ni très difficile, ni très intéressante. Par contre, dès que tu passes à System F, c'est beaucoup plus dur (cf. "Proofs and Types", disponible en ligne).

Il faut noter qu'on a juste montré qu'il était possible, en choisissant bien ses séquences de réduction, de réduire le terme en un nombre fini d'étape. Ça ne donne pas directement la preuve de normalisation forte (qui est que toute séquence de réduction convient).

[Ekinoks]

Merci beaucoup pour ces explications bluestorm, j'ai enfin compris l'idée de pourquoi la terminaison est assurée avec le lambda calcule simplement typé

Je comprends également mieux pourquoi le lambda calcule simplement typé a un pouvoir expressif si faible avec des contraintes sur ma "complexité" des types et le nombre de redexes de degré maximal qui doivent être strictement décroissants.

Je vais pouvoir m'attaquer aux System F :p

Encore merci pour vos réponses.

[gasche]

Si tu t'intéresses à System F et à ses extensions avec typage d'ordre supérieur (System Fω en particulier), je viens de découvrir un très bon document disponible en ligne : Programming in Higher-order Typed Lambda-Calculi. C'est un ouvrage auquel Benjamin Pierce (l'auteur du TAPL, ouvrage de référence sur les systèmes de types) a participé, et ça se sent, c'est clair et bien expliqué.

Il ne parle quasiment pas, par contre, de la question de terminaison. C'est plutôt une approche pratique : « est-ce que ces systèmes sont vraiment utiles pour programmer ? » Si tu cherches une vision surtout théorique, "Proofs and Types" (basé sur un cours de Girard) est une meilleure référence.

[TropMDR]

Envoyé par Ekinoks

Je vais pouvoir m'attaquer aux System F :p

La preuve de normalisation forte de F, faut déjà plus s'accrocher à son slip hein...

[Ekinoks]

Une approche pratique des System F peut être sympa et plus simple dans un premier temps, merci pour le lien

[gasche]

Oui enfin quand je dis "pratique", il ne faut pas s'attendre non plus à trouver un parseur XML hein... C'est plutôt pratique comme dans « c'est pratique pour définir un type de donné riche pour le lambda-calcul simplement typé, dans le style Higher Order Abstract Syntax. »