Version imprimable
Bonjour à tous,
quelqu'un peut m'aider à programmer la réduction dans le système F?
par exemple, quand on veut calculer le successeur de 3 on doit avoir comme résultat 4, ça je sais le faire à la main mais je n'arrive pas à mettre en place l'algorithme calculant la réduction en général dans le système F.
Merci d'avance.
Quel est le problème ? Comment tu fais à la main ? A quoi ressemble ton algorithme qui ne marche pas ?
Bonjour,
merci pour votre réponse.
en fait, j'essaie de programmer la réduction dans le système F, j'ai fait pas mal d'exemples a la main pour voir comment ça marche, mais après pour programmer ça, j'ai des difficultés. Par exemple, si on veut faire la réduction dans le successeur d'un entier (exemple entier=2), d’après ce que j'ai compris, les étapes a suivre sont les suivantes:
d'abord faire une première réduction pour remplacer l'entier (le n dans le lambda terme en entrée par le lambda terme correspondant a l'entier 2)
puis on fait la réduction de type par rapport a cet entier
puis la réduction des termes par rapport a cet entier (tant qu'il y a des redex on fait la réduction, on peut avoir deux fonctions, une pour la réduction du petit lambda et l'autre concerne la réduction des grands lambda)
et a la fion on obtient un lambda terme qui correspond a succ(2)=3
mon problème est comment procéder pour programmer ça? comment va être la structure de l'expression en entrée? en général, comment on procède pour implémenter la réduction dans le système F?
En général, pour implémenter la réduction dans un lambda-calcul qui bénéficie de propriétés agréables (genre confluence), on :Citation:
Envoyé par samou_kh
- se fixe une stratégie de réduction (cf. call-by-value, call-by-name, call-by-need, etc.).
- applique "bêtement" les règles de réduction, en se laissant guider par la stratégie.
Comment programmer ça ? C'est une question bien vague. Il faut choisir un langage, définir un type de données pour représenter une expression. Ensuite l'algorithme est assez simple, généralement tu regardes la tête de ton expression, et selon la forme qu'elle a tu agis, récursivement, en conséquence.
Je suis moi même sur le travail d'un inféreur de type. En réalité, j'ai pas toutes les notions que peut avoir Ptival mais je peux te donner quelques pistes déjà.
Il faut bien que tu comprends qu'un type, c'est une structure semblable à un arbre. En effet, par exemple dans le cas d'une fonction let succ x = x + 1, le type est int -> int. Nous avons ici, un arbre composé d'un racine -> et de deux enfants int et int. C'est le cas simple, et dans ce genre de travail, il faut penser à tout ! Dans des fonctions plus complexes, les arguments peuvent être des fonctions et donc des sous arbres à la racine. J'ai opté pour une structure abre n-aire dans mon cas.
Ensuite, je serais pas dire si ce que j'ai fait est le système F (je connais pas tout ça) mais la politique d'évaluation que j'ai mené tout au long est la politique call-by-value (très utilisé apparament). Je cherchais à chaque fois les valeurs et sur le type courant, j'ajoutais des contraintes.
Par exemple, pour la fonction succ, pour la varible x, je rajouter la contrainte d'un entier. Ensuite, je passais à une étape d'unification qui factorisait toutes les contraintes d'un type en une constante (toujours pour, au lieu d'émettre l'hypothèse qu'il soit un entier, l'unification dit formellement que c'est un entier). À partir de là, on sait déduire le type d'une fonction en faisant une analyse récursive descendante. Dans le cas où il n'y aurait aucunes contraintes qui pourrait déduire une constante, on dit que le type est polymorphe.
Il en vient maintenant à l'aplication et à la spécialisation des fonctions. En effet, il faut là aussi voir le type de l'exécution et le type de la fonction à exécuter. Par exemple, succ 5, comme type d'exécution, on a int -> 'a. On sait que succ est du type int -> int, on compare les deux. On prendra soin de ne spécialiser que le type lié à succ (et pas le type résultant de l'exécution de succ). Ici, il n'y a pas de spécialisation à faire mais tu imagines bien que face à un type polymorphe, il faudra le remplacer par le type présent dans l'exécution.
Je pense pas être super clair, étant moi même débutant dans le domaine. Cependant, mon programme fonctionne, on peut dire que c'est une bonne chose :lol: ! Je peux te conseiller le dernier chapitre du livre Le Langage Caml qui offre une explication qui m'a bien aidé même si elle est limité. En tout cas, ce livre pose les bonnes bases.
Comme je l'ai dit en privé à Dinosaure, même si son message est intéressant, il ne répond en fait pas à ta question, puisqu'il concerne l'inférence de type dans un langage ML, alors que tu t'intéresses ici à la réduction. Cela dit, si un jour tu t'intéresses à l'inférence de type, tu peux toujours le lire.
Pour ce qui est de la réduction, normalement ça n'est pas trop difficile si tu as bien compris comment ça marchait. Évidemment, si tu appliques les règles que tu connais (bêta-réduction et tout ça), ça serait plus simple d'utiliser des indices de Bruijn, ce qui complique un peu la chose, et à mon avis tu peux faire plus simple en renvoyant une valeur pour les fonctions (la fonction et son environnement, par exemple), puis en ajoutant l'argument et sa valeur à l'environnement de la fonction. Mais comme tu veux.