Evaluation and convergence in the computational calculus
Résumé
In Moggi's computational calculus, reduction is the contextual closure of the rules obtained by orienting three monadic laws. In the literature, evaluation is usually defined as the closure under weak contexts (no reduction under binders): E = | let x := E in M. We show that, when considering all the monadic rules, weak reduction is non-deterministic, non-confluent, and normal forms are not unique. However, when interested in returning a value (convergence), the only necessary monadic rule is β , whose evaluation is deterministic.
Domaines
Logique en informatique [cs.LO]Origine | Fichiers produits par l'(les) auteur(s) |
---|