Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 18 sur 18
  1. #1
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut Lambda-calcul typé (système F) : algorithme de substitution

    Bonjour à tous,

    quelqu'un peut me donner en détails l'algorithme de substitution qu'on applique dans le système F?

    Merci d'avance.

  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 217
    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 217
    Points : 17 566
    Points
    17 566

    Par défaut

    tu devrais lire ceci :
    https://who.rocq.inria.fr/Gilles.Dow...es_types.ps.gz

    en particulier le chapitre 9
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  3. #3
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Bonjour,

    Merci pour le document, mais je trouve toujours un petit soucis concernant le cas d'une abstraction, quelqu'un peut me l'expliquer?

    Merci d'avance.

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

    Par défaut

    Je connais Système F mais je ne comprends pas ta question. Qu'est-ce qui te pose problème et qu'est-ce que tu attends de nous ?

    gorgonite > ce cours est intéressant mais je ne pense pas que ce soit une bonne source pour Système F, qui y est essentiellement décrit comme un cas particulier de Pure Type System. C'est puissant et abstrait, mais pas le plus intuitif ou clair quand on débute...

  5. #5
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 217
    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 217
    Points : 17 566
    Points
    17 566

    Par défaut

    Citation Envoyé par gasche Voir le message
    gorgonite > ce cours est intéressant mais je ne pense pas que ce soit une bonne source pour Système F, qui y est essentiellement décrit comme un cas particulier de Pure Type System. C'est puissant et abstrait, mais pas le plus intuitif ou clair quand on débute...
    si je ne devais en lire qu'un seul (disponible en français), ce serait celui-là...
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

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

    Par défaut

    Ton message m'y fait penser: j'ai écris des notes sur les lambda-calculs typés pour un exposé à une groupe de travail de logique, qui présentent le lambda-calcul, Système F et Système Fomega de façon relativement vulgarisée -- mais plutôt pour des logiciens que pour des informaticiens.
    Si ça intéresse quelqu'un, c'est ici :
    http://gdt.ludics.eu/images/5/58/Type_theory_course.pdf

    Bien sûr c'est un document de présentation/vulgarisation, en une dizaine de pages, pas du tout un cours ayant vocation d'être complet sur le sujet. Ça ne peut certainement pas remplacer un document comme le cours de Dowek, mais à mon avis c'est plus accessible pour une première approche.

  7. #7
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Merci à tous pour ces explications.

    Je trouve que ce document est très intéressant.

    Ma question est:

    est ce qu'il y a une différence entre l'algorithme de substitution dans le lambda calcul pure et l'algorithme de substitution dans le système F?

    je sais que dans le système F on doit gérer deux types de substitutions:

    la substitution des termes
    la substitution des types

    Je voudrais savoir est ce que c'est le même algorithme qu'on doit appliquer dans les deux substitutions ou pas?


    Je vous remercie tous.

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

    Par défaut

    Je pense que tu peux répondre toi-même à ta question en définissant ces deux algorithmes de substitution pour les comparer. L'idée d'un algorithme de substitution est assez simple: on remplace les variables, et on substitue récursivement les sous-termes d'une expression un peu compliquée, en faisant attention à gérer les conflits de variables au niveau des lieurs (lambda, let, etc.) qui définissent de nouvelles variables (ayant peut-être le même nom que la variable substituée).

    Comment définis-tu ces deux substitutions ?

  9. #9
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Pour la substitution des termes, je pense qu'il faut appliquer l'algorithme classique, càd:

    -si t est une variable, alors t[x/u]=u si x=t et t sinon

    -si t est une application (vw)alors t[x/u]=v[x/u]w[x/u]

    -si t est une abstraction (lambda y.v) alors t[x/u]=lambda y.(v[x/u]) si x est différent de y sinon t.

    Mais la question se complique au niveau des types.

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

    Par défaut

    Ça c'est l'algorithme classique sur le lambda-calcul non typé. Quelle définition de System F utilises-tu ? Je suppose que c'est une définition explicitement typé, et alors tu as des cas supplémentaires à gérer (l'abstraction et l'application de types) dans ta définition de la substitution des termes.

    (Quand je demande "quelle définition", je me demande quelles sont les grammaires que tu utilises pour décrire les termes et les types valides de ton système. Les règles de typage sont aussi importantes mais on peut les deviner à partir des grammaires en général.)

  11. #11
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Bonjour,

    Vous avez raison, l'algorithme que je viens de citer concerne le lambda calcul simple et pas le système F.

    1)Pour la définition des types dans le système F, on a ceci:

    Les types de base: t, v , les variables et les constantes.


    Les variables de types: si α est une variable de type, alors α est un type.


    Si A et B sont des types alors A ->B est un type.


    Si α est une variable de type, B est un type alors ΠαB est un type.


    En résumé: A,B:= α| A ->B | ΠαB


    2)Les termes du système F sont définis comme suit:

    Les termes de base: variables et constantes.


    Application: si M et N sont des termes alors MN est un terme.


    Abstraction: si x est une variable de terme, A est un type et M est un terme, alors λx:A.M est un terme.


    Application de type: si M est un terme, A un type alors M{A} est un terme.


    Abstraction de type: si α est une variable de type, M un terme, alors Λα.M est un terme.

    Maintenant pour les algorithmes de substitution, on a:

    1)Algorithme de substitution des types:

    T[α:=A]

    a)T est une constante: rien a faire.

    b)T est une variable de type:
    -T=α alors T[α:=A]=A
    -T=B alors T[α:=A]=B

    c)T est une application: T est U->V

    T[α:=A]= U[α:=A]->V[α:=A]

    d)T est une abstraction:ΠB.T[α:=A]

    1)α est différent de B:
    -pas de B dans A alors:

    ΠB.(T[α:=A])


    -B dans A alors il faut renommer B en G avec G n'appartient pas a T[B]A

    2)α=B alors T.

    j'aurais besoin de votre aide pour l'algorithme de substitution des termes.

    Merci d'avance.

  12. #12
    Invité de passage
    Profil pro oussama ferhi
    Inscrit en
    mars 2010
    Messages
    1
    Détails du profil
    Informations personnelles :
    Nom : oussama ferhi

    Informations forums :
    Inscription : mars 2010
    Messages : 1
    Points : 1
    Points
    1

    Par défaut

    svp Gasche, est ce que c est possible d avoir un exemple de grammaire contenant la définition des types et des termes du système F
    merci d'avance

  13. #13
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Bonjour,

    je ne sais pas si je peux vous aider, mais voici ce que je propose en prolog:

    Pour les termes, mais sans l'application de types et sans l'abstraction de types:

    Code :
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    is_Term(X):-
          var(X);
          atomic(X).
    
    is_Term(app(M,N)):-
                 is_Term(M),
                 is_Term(N).
    
    is_Term(lam(X-A,M)):-
                 var(X),
                 is_Term(M),
                 is_Type(A).


    ce je propose pour les types est comme suit:

    Code :
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    cst_type(e).
    var_type(t).
    
    is_Type(X):-
           cst_type(X);
           var_type(X).
           
    is_Type(X->Y):-
              is_Type(X),
              is_Type(Y).
              
    is_type(pi(A,T)):-
                  is_type(T),
                  var_type(A).

    Est ce que cette définition peut être considérée comme une grammaire à utiliser pour l'algorithme de substitution?

  14. #14
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 217
    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 217
    Points : 17 566
    Points
    17 566

    Par défaut

    inutile de faire doublon, mets juste le lien vers ton proto en prolog
    http://www.developpez.net/forums/d12...g/#post6624637
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

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

    Par défaut

    Citation Envoyé par samou_kh Voir le message
    a)T est une constante: rien a faire.

    b)T est une variable de type:
    -T=α alors T[α:=A]=A
    -T=B alors T[α:=A]=B

    c)T est une application: T est U->V

    T[α:=A]= U[α:=A]->V[α:=A]

    d)T est une abstraction:ΠB.T[α:=A]

    1)α est différent de B:
    -pas de B dans A alors:

    ΠB.(T[α:=A])


    -B dans A alors il faut renommer B en G avec G n'appartient pas a T[B]A

    2)α=B alors T.

    j'aurais besoin de votre aide pour l'algorithme de substitution des termes.
    En gros, l'idée est d'explorer récursivement les sous-termes, jusqu'à rencontrer un type, et là tu appliques l'algorithme de substitution sur les types.

    Donc tu auras par exemple

    (M{T})[α:=A] := M[α:=A]{T[α:=A]}

    (M[α:=A] est une substitution sur les termes, T[α:=A] sur les types)

    Le reste marche à peu près comme ça. La seule subtilité est
    l'abstraction de type (Λβ.M)[α:=A] où il faut raisonner selon qu'il
    y a un conflit de variables (α=β) ou non.

    (Il y a aussi un risque de capture des variables dans A, mais ce
    risque est déjà présent dans la substitution de termes et vous n'en
    avez pas parlé pour l'instant donc j'imagine qu'on raisonne
    avec assez de noms frais, ou modulo α-conversion.)

  16. #16
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 707
    Points
    2 707

    Par défaut

    Il existe des Prolog étendus spécialement pour la substitution de variables.
    Sur l'instant je pense à Alpha-Prolog mais je sais qu'il y en a d'autres (Qu-Prolog, Lambda Prolog) .
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  17. #17
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Bonjour,

    merci pour vos réponses.

    Pour l'algorithme de substitution pour les termes, d’après ce que j'ai compris, il n y a pas une grande différence avec les types, donc on peut l’écrire de cette façon:

    a)T est une constante: rien a faire.

    b)T est une variable de type:
    -T=α alors T[α:=A]=A
    -T=B alors T[α:=A]=B

    c)T est une application: T est UV

    T[α:=A]= U[α:=A]V[α:=A]

    d)T est une abstraction:lambda X:C.T[α:=A] (avec C le type de X

    1)α est différent de X:
    -pas de X dans A alors:

    lambda X:C.T[α:=A]


    -X dans A alors il faut renommer X en Y avec Y n'appartient pas a T[X]A

    2)α=X alors T.

    e)T est une application de type

    f)T est une abstraction de type


    et dans le cas e et f qu'il faut gérer plusieurs cas.

    Est ce que c'est bien ça l'algorithme de substitution des termes dans le système F?

    Merci d'avance.

  18. #18
    Invité de passage
    Inscrit en
    avril 2007
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 12
    Points : 0
    Points
    0

    Par défaut

    Bonjour,

    je pense que j'ai dit quelques bêtises sur l'algorithme de substitution des termes, je corrige ça:

    on veut gérer l'alpha conversion M[alpha:=A]
    1)M est une constante, alors rien a faire

    2)M est une variable de terme alors on a deux cas:

    a) M=alpha alors M[alpha:=A]=A
    b) M est différente de alpha et M=B alors M[alpha:=A]=B

    3)M est une application: M=UV

    M[alpha:=A]= U[alpha:=A] V[alpha:=A]

    4)M est une abstraction: M=lambda x:B.N

    a)alpha=x, alors M[alpha:=A]=M=lambda x:B.N

    b)alpha est différente de x:

    1)x n'appartient pas a N:
    M[alpha:=A]:=lambda x:B.(N[alpha:=A])

    2)x appartient a N:
    a)x ne figure pas dans A alors
    M[alpha:=A]:=lambda x:B.(N[alpha:=A])

    b)x figure dans A alors on renomme x par y dans M (avec y ne figure pas ni dans N ni dans A) et après on fait la substitution.
    M[alpha:=A]:=lambda y:B.(N[alpha:=A]).


    pour les deux derniers cas, l'application de type et l'abstraction de type, d’après la réponse de Mr gasche:

    application de type:
    (M{T})[α:=A] := M[α:=A]{T[α:=A]}

    mais est ce que je peux avoir plus d'explication sur comment on fait réellement cette substitution et aussi celle de l'abstraction de type( des exemples si c'est possible)


    Merci a tous.

    J'attends vos remarques.

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
  •