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:
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?(M{T})[α:=A] := M[α:=A]{T[α:=A]}
(M[α:=A] est une substitution sur les termes, T[α:=A] sur les types)
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.
Partager