Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 4 sur 4
  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 Substitution des termes dans le systeme F

    Bonjour à tous,

    je veux implémenter le système F et je trouve des difficultés au niveau de la substitution des termes. Pour les quatre premiers cas de substitution (constante, variable, application et abstraction), il n y a aucun problème, mais je trouve des difficultés au niveau de l'application de type et l'abstraction de type.

    Dans ces deux derniers cas, on doit faire la substitution des termes et la substitution des types:

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

    (M[α:=A] est une substitution sur les termes, T[α:=A] sur les types)
    Comment effectuer une telle substitution sachant que M[α:=A] consiste a remplacer une variable de terme par un terme et T[α:=A] consiste a remplacer une variable de type par un type?

    Est ce que c'est possible d'avoir des exemples de telle substitution?

    Le même problème avec l'abstraction de type?

    Merci d'avance.

  2. #2
    Membre actif Avatar de Ptival
    Homme Profil pro Valentin Robert
    Étudiant
    Inscrit en
    juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Nom : Homme Valentin Robert
    Âge : 25
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : juin 2004
    Messages : 70
    Points : 153
    Points
    153

    Par défaut

    Je ne suis pas sûr de comprendre ton problème. Disposes-tu d'un exemple de code ou pseudo-code dans un langage quelconque ?

    Pour la substitution de termes dans les termes, tu fais comme dans le lambda-calcul simplement typé.

    Pour la substitution de types dans les termes, tu dois remplacer les occurences du type à substituer dans (λx:α.t), et tu dois t'arrêter quand tu croises une abstraction de types (Λα.t) qui cache ton α.

    Pour la substitution de types dans les types, tu fais "comme" dans le lambda-calcul simplement typé, mais à un niveau supérieur. (?)

    En l'absence d'éclaircissements sur ce qui te pose problème, je ne vais pas tenter de détailler plus.

  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 votre réponse.

    Pour la substitution des types dans les types, il n y a aucun problème.

    Pour la substitution des termes dans les termes, j'ai un petit problème lors d'une application de type et lors d'une abstraction de type.

    Est ce qu'il suffit juste de faire la substitution des termes? sans prendre en considération les types?

    voici le code que j'ai en Prolog:
    Le cas d'une application de type:
    Code :
    1
    2
    3
    4
    5
    6
    7
    8
    9
    %le cas d'une application de type: 
    %on fait la substitution dans (N,pii(T,B)
    %le résultat est Term_final1. Le résultat final sera (appl_type((Term_final1,U),B)
    
    substitution_term((X,T),(Y,T),(appl_type((N,pii(T,B)),U),B),(Term_final,Type)):- 
                     substitution_term((X,T),(Y,T),(N,pii(T,B)),(Term_final1,Type1)),  
                     Term_final= appl_type((Term_final1,U),B),
                     Type=B.
    Le cas d'une abstraction de type:

    Code :
    1
    2
    3
    4
    5
    substitution_term((X,T),(Y,T),(lam_type(N,(B,A)),(pii(N,A))),(Term_final,Type)):-
                            substitution_term((X,T),(Y,T),(B,A), (Term1,Type1)),
                            Term_final=lam_type((N,(Term1,Type1)),pii(N,Type1)),
                            Type=(pii(N,Type1)).
    je voudrais savoir si ça est correct?

    Pour la substitution des types dans les termes, je pense qu'on fait appel a cette substitution lors de la bêta-réduction? Est ce que c'est possible d'avoir plus de détails sur cette substitution?

  4. #4
    Membre actif Avatar de Ptival
    Homme Profil pro Valentin Robert
    Étudiant
    Inscrit en
    juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Nom : Homme Valentin Robert
    Âge : 25
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : juin 2004
    Messages : 70
    Points : 153
    Points
    153

    Par défaut

    Citation Envoyé par samou_kh Voir le message
    Est ce qu'il suffit juste de faire la substitution des termes? sans prendre en considération les types?
    A priori oui. Lorsqu'on croise une abstraction de type, on continue à substituer dans son corps. Lorsqu'on croise un terme appliqué à un type, on continue à substituer dans le corps du terme.

    ---

    Je ne comprends pas bien le code Prolog, les notations me sont trop obscures (pii, N, ... ?)

    ---

    Citation Envoyé par samou_kh Voir le message
    Pour la substitution des types dans les termes, je pense qu'on fait appel a cette substitution lors de la bêta-réduction? Est ce que c'est possible d'avoir plus de détails sur cette substitution?
    On peut ou pas le faire à vrai dire. Les annotations de type dans les termes servent plutôt à guider l'algorithme de typage. Le contenu calculatoire du terme est finalement indépendant de celles-ci, si bien qu'on peut les effacer avant de procéder à la bêta-réduction.

    Si on souhaite quand même le faire, la substitution se fait simplement :

    Substituer le type β au type α :
    - (λx:α.t) devient (λx:β.t') où t' est la substitution dans t.
    - (λx:γ.t) devient (λx:γ.t') où t' est la substitution dans t.
    - (Λα.t) reste (Λα.t).
    - (Λγ.t) devient (Λγ.t') où t' est la substitution dans t.
    Et pour le reste on fait les substitutions récursives sans se poser de question.

    Je ne suis pas expert en la matière et je peux me tromper, mais c'est comme ça que je ferais naïvement.

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
  •