mirror of
https://github.com/digital-asset/daml.git
synced 2024-09-20 01:07:18 +03:00
e4717654a5
* LF: Small-step semantics for expression evaluation This PR factors expression evaluation into two parts: - a set of evaluation contexts that determine *where to reduce next* - a set of small-step reduction rules The PR then redefines the big-step semantics relation as the iteration of that small-step relation. The main motivation for this change is to simplify & shorten the semantics a lot by using evaluation contexts. These contexts not only determine the evaluation order, they also handle the propagation of errors from subterms. This means the small-step reduction rules really only have to deal with redexes, so there's a lot fewer rules. Incidentally, this change introduces semantics for infinitely looping terms. Big-step relations generally can't handle infinitely looping terms, but small-step relations handle them automatically. I'm not sure if a similar simplification is possible for update interpretation, but this seems worthwhile for expressions at least. changelog_begin changelog_end * call-by-value, separate app e.c. lines * split redex evaluation from small-step evaluation * use kᵪ for erasable kind |
||
|---|---|---|
| .. | ||
| contract-id.rst | ||
| daml-lf-1.rst | ||
| experimental.rst | ||
| transaction.rst | ||
| value.rst | ||