Discussion :

[samou_kh]

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.

[Ptival]

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.

[samou_kh]

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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?

[Ptival]

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

---

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.