Discussion :

[samou_kh]

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.

[gasche]

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

[gasche]

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.

[samou_kh]

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.

[gasche]

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 ?

[samou_kh]

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.