2016-08-31 1 views
0

Quel devrait être le type d'une fonction de réduction en une seule étape pour une machine abstraite? x -> Maybe x ou x -> x?Code Haskell pour le redex en une étape de la machine abstraite?

Étant donné une telle fonction de réduction en une seule étape, comment écrirait-on la fonction de réduction multi-pas qui donne la forme normale d'un terme d'entrée?

+0

Qu'est-ce 'x' ? Quelle machine abstraite? Que devrait faire une étape? Et probablement les deux types iraient bien, le 'Maybe 'juste mélange la terminaison de signalisation dans la valeur de retour. – Bergi

+0

En supposant que 'x' est le type de l'état, vous avez également besoin d'un argument de type' y', ce qui vous amène à un état différent. – chepner

+0

Cela réduira la fonction. Lorsqu'il est appliqué à un terme donne le terme obtenu après une étape d'exécution de la machine abstraite. Supposons que x est un type de données pour représenter les termes d'un langage d'expressions arithmétiques et booléennes. – user158083

Répondre

1

Normalement, vous voulez que la fonction de réduction à une seule étape soit de type T -> Maybe T. Ensuite, pour redexes, vous renvoyez un Just, et pour les formulaires normaux, vous renvoyez Nothing. Cela suit un principe général selon lequel les fonctions doivent renvoyer autant d'informations qu'elles calculent à l'appelant que possible, ce qui aide à réduire le recalcul de votre programme.

Si votre fonction de réduction en une seule étape est singleStepReduce :: T -> T, il a deux choix quand donné un argument qui est déjà en forme normale:

  • Retour l'argument. Cela nécessite que l'appelant fasse quelque chose comme x == singleStepReduce x ou isNF x pour déterminer si l'argument est dans NF; c'est l'information singleStepReduce est déjà déterminante, donc c'est un gaspillage de calcul; en outre, x == singleStepReduce x est très coûteux en calcul, tandis que isNF x duplique encore que la détermination et permet de réduire les règles de réduction et les règles de détermination des formes normales, ce qui viole les principes de base de l'ingénierie logicielle.
  • Retour undefined. C'est pire. cela signifie que l'appelant n'a aucun moyen de récupérer du formulaire normal, obligeant l'appelant à utiliser isNF x avant d'appeler singleStepReduce x, et de laisser le problème que les définitions de isNF x et singleStepReduce x implémentent une logique de chevauchement non résolue.

La mise en œuvre d'un réducteur à plusieurs étapes, à condition que vous êtes ok avec le réducteur d'entrer dans une boucle infinie à des conditions qui ne disposent pas d'une forme normale, est alors assez simple:

multiStepReduce :: (a -> Maybe a) -> a 
multiStepReduce r x = case r x of 
    Nothing -> x 
    Just y -> multiStepReduce r y 
+0

Encore pire, 'x == singleStepReduce x' n'est pas équivalent à' isNF x' quand 'x' a une transition en auto-bouclage. – chi