Skip to Main content Skip to Navigation
Conference papers

Evaluation and convergence in the computational calculus

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271490
Contributor : Isabelle Gouat Connect in order to contact the contributor
Submitted on : Friday, June 25, 2021 - 6:16:36 PM
Last modification on : Tuesday, September 28, 2021 - 5:16:00 PM
Long-term archiving on: : Sunday, September 26, 2021 - 10:33:53 PM

File

TLLA_2021_paper_6.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271490, version 1

Collections

Citation

Claudia Faggian, Giulio Guerrieri, Riccardo Treglia. Evaluation and convergence in the computational calculus. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271490⟩

Share

Metrics

Record views

59

Files downloads

38