A Bidirectional Krivine Machine ( Short Paper )

Bidirectional evaluation [Mayer et al., 2018] allows the output value of a λ-term to be modified and then back-propagated through the term, repairing leaf terms as necessary. To accompany their call-by-value formulation, we present two call-by-name systems. First, we recount the call-by-value approach proposed in [Mayer et al., 2018]; the key idea concerns back-propagating values through function application. Next, we formulate an analogous call-by-name system and establish corresponding correctness properties. Lastly, we define a backward Krivine-style evaluator that, while being functionally equivalent to the “direct” by-name backward evaluator, exhibits notable characteristics. 0 Introduction Recently, we proposed a technique called bidirectional evaluation [Mayer et al., 2018] that allows arbitrary expressions in a λ-calculus to be “run in reverse,” including those which produce function values. In this system, (1) an expression e is evaluated to a value v, (2) the user makes “small” changes to the value yielding v′, and (3) the new value v′ (structurally equivalent to v) is “pushed back” through the expression, generating repairs as necessary to ensure that the new expression e′ (structurally equivalent to e′) evaluates to v′. Show below is the syntax of a pure λ-calculus extended with constants c. Our presentation employs natural (big-step, environment-style) semantics [Kahn, 1987], where function values are closures. Call-by-value function closures 〈E;λx.e〉 refer to call-by-value environments E—which bind call-by-value values—and call-by-name function closures 〈D;λx.e〉 refer to call-by-name environments D—which bind expression closures 〈D; e〉 yet to be evaluated. A stack S is a list of call-by-name expression closures. Expressions e ::= c | λx.e | x | e1 e2 Call-By-Value Values v ::= c | 〈E;λx.e〉 Call-By-Value Environments E ::= − | E, x 7→ v Call-By-Name Values u ::= c | 〈D;λx.e〉 Call-By-Name Environments D ::= − | D, x 7→ 〈Dx; e〉 Krivine Argument Stacks S ::= [] | 〈D; e〉 :: S Definition 1 (Structural Equivalence). Structural equivalence of expressions (e1 ∼ e2), values (v1 ∼ v2 and u1∼ u2), environments (E1 ∼ E2 and D1 ∼ D2), and expression closures (〈E1; e1〉 ∼ 〈E2; e2〉 and 〈D1; e1〉 ∼ 〈D2; e2〉) is equality modulo constants c1 and c2, which may differ, at the leaves of terms. Copyright c © by the paper’s authors. Copying permitted for private and academic purposes. In: A. Editor, B. Coeditor (eds.): Proceedings of the XYZ Workshop, Location, Country, DD-MMM-YYYY, published at http://ceur-ws.org