Galois connecting call-by-value and call-by-name
| Autor: | McDermott, Dylan, Mycroft, Alan |
|---|---|
| Rok vydání: | 2022 |
| Předmět: |
evaluation order
FOS: Computer and information sciences Theory of computation → Categorical semantics Computer Science - Programming Languages call-by-push-value categorical semantics computational effect Theory of computation → Semantics and reasoning Theory of computation → Denotational semantics Programming Languages (cs.PL) |
| DOI: | 10.48550/arxiv.2202.08246 |
| Popis: | We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with side-effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving these properties. The key ingredient is Levy’s call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example side-effects including divergence and nondeterminism. LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 32:1-32:19 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|