Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 8 sur 8
  1. #1
    Membre confirmé Avatar de Ekinoks
    Profil pro
    Étudiant
    Inscrit en
    novembre 2003
    Messages
    670
    Détails du profil
    Informations personnelles :
    Âge : 27
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : novembre 2003
    Messages : 670
    Points : 266
    Points
    266

    Par défaut Lambda-calcul simplement typé : terminaison assurée ?

    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.

  2. #2
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 207
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 30
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 207
    Points : 16 756
    Points
    16 756

    Par défaut

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


    Strong Normalization of Substitutions je peux de l'envoyer par mail ,)
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  3. #3
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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).

  4. #4
    Membre confirmé Avatar de Ekinoks
    Profil pro
    Étudiant
    Inscrit en
    novembre 2003
    Messages
    670
    Détails du profil
    Informations personnelles :
    Âge : 27
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : novembre 2003
    Messages : 670
    Points : 266
    Points
    266

    Par défaut

    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.

  5. #5
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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.

  6. #6
    Membre chevronné
    Inscrit en
    mars 2010
    Messages
    308
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 308
    Points : 793
    Points
    793

    Par défaut

    Citation Envoyé par Ekinoks Voir le message
    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...

  7. #7
    Membre confirmé Avatar de Ekinoks
    Profil pro
    Étudiant
    Inscrit en
    novembre 2003
    Messages
    670
    Détails du profil
    Informations personnelles :
    Âge : 27
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : novembre 2003
    Messages : 670
    Points : 266
    Points
    266

    Par défaut

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

  8. #8
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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. »

+ Répondre à la discussion
Cette discussion est résolue.

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •