English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We study the equivalence of eval-readback and eval-apply big-step evaluatorsin the general setting of the pure lambda calculus. The equivalence extends toevaluators in other lambda calculi (applied and typed) if the evaluation orderof redexes (i.e. the evaluation strategy) is realisable. We present a proofthat one-step equivalence holds when (1) the `readback' stage satisfiesstraightforward well-formedness provisos, (2) the `eval' stage implements a`uniform' strategy, and (3) the eval-apply evaluator implements a `balancedhybrid' strategy that has `eval' as a subsidiary strategy. The proof proceedsby application of the `lightweight fusion by fixed-point promotion' programtransformation on evaluator implementations to fuse readback and eval into thebalanced hybrid. The proof can be followed with no previous knowledge of thetransformation. We use Haskell 2010 as the implementation language, with allevaluators written in monadic style to guarantee semantics (strategy)preservation, but the choice of implementation language is immaterial.  To determine the scope of the equivalence, we provide an extensive survey ofthe strategy space using canonical eval-apply evaluators. We discuss thestrategies' properties and some of their uses and abstract machines. We improvethe formal definition of uniform and hybrid strategy, and use it to structurethe strategy space and to obtain the generic higher-order evaluators used inthe proof that deliver all plain evaluators as fixed-points by instantiation.We introduce a systematic notation for both evaluator styles and use it tosummarise strategy and evaluator equivalences, including (non-)equivalenceswithin a style and (non-)equivalences between styles not proven by thetransformation.

Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space