Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 6 sur 6
  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 Réduction dans le système F

    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.

  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 : 168
    Points
    168

    Par défaut

    Quel est le problème ? Comment tu fais à la main ? A quoi ressemble ton algorithme qui ne marche pas ?

  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.

    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?

  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 : 168
    Points
    168

    Par défaut

    Citation Envoyé par samou_kh Voir le message
    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 :

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

  5. #5
    Candidat au titre de Membre du Club
    Homme Profil pro Romain Calascibetta
    Inscrit en
    février 2012
    Messages
    11
    Détails du profil
    Informations personnelles :
    Nom : Homme Romain Calascibetta
    Localisation : France

    Informations forums :
    Inscription : février 2012
    Messages : 11
    Points : 14
    Points
    14

    Par défaut

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

  6. #6
    Invité de passage
    Inscrit en
    décembre 2009
    Messages
    3
    Détails du profil
    Informations forums :
    Inscription : décembre 2009
    Messages : 3
    Points : 2
    Points
    2

    Par défaut

    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.

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
  •