Bidirectional evaluation [Mayer et al., 2018] allows the output value of a -term to be modi ed 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 de ne a backward Krivinestyle evaluator that, compared to the functionally equivalent \direct" by-name backward evaluator, is notable for its relative simplicity.
Introduction
v E u D S ::= ::= ::= ::= ::= ::= c j
x:e j x j e1 e2 c j hE; x:ei
j E; x 7! v c j hD; x:ei
j D; x 7! hDx; ei [] j hD; ei :: S De nition 1 (Structural Equivalence). Structural equivalence of expressions (e1 e2), values (v1 v2 and u1 u2), environments (E1 E2 and D1 D2), and expression closures (hE1; e1i hE2; e2i and hD1; e1i hD2; e2i) is equality modulo constants c1 and c2, which may di er, at the leaves of terms.
Bidirectional Call-By-Value Evaluation hE; x:ei ) hE; x:ei
hE; xi ) E(x) BV-E-App hE; e1i ) hEf ; x:ef i hE; e2i ) v2 hEf ; x 7! v2; ef i ) v hE; e1 e2i ) v hE; ci ( c0 hE; c0i
BV-U-Const hE; x:ei ( hE0; x:e0i
hE0; x:e0i hE; xi ( v0
hE[x 7! v0]; xi hE; e1i ) hEf ; x:ef i hE; e2i ) v2 hEf ; x 7! v2; ef i ( v0 hEf0 ; x 7! v20; e0f i hE; e1i ( hEf0 ; x:e0f i hE1; e01i hE; e2i ( v20 hE2; e02i hE; e1 e2i ( v0 hE1e1 e2 E2; e01 e02i
BV-U-Fun BV-U-Var
BV-U-App
Given an expression closure hE; ei (a \program") that evaluates to v, together with an updated value v0, evaluation update traverses the evaluation derivation and rewrites the program to hE0; e0i such that it evaluates to v0. The rst three update rules are simple. Given a new constant c0, the BV-U-Const rule retains the original environment and replaces the original constant. Given a new function closure hE0; x:e0i, the BV-U-Fun rule replaces both the environment and expression. Given a new value v0, the BV-U-Var rule replaces the environment binding corresponding to the variable x used; E[x 7! v0] denotes structure-preserving replacement.
The rule BV-U-App for function application is what enables values to be pushed back through all expression forms. The rst two premises evaluate the function and argument expressions using forward evaluation, and the third premise pushes the new value v0 back through the function body under the appropriate environment. Two key aspects of the remainder of the rule warrant consideration. The rst key is that update generates three new terms to grapple with: Ef0 , v20, and e0f . The rst and third are \pasted together" to form the new closure hEf0 ; x:e0f i that some new function expression e01 must evaluate to, and the second is the value that some new argument expression e02 must evaluate to; these obligations are handled recursively by update (the fourth and fth premises). The second key is that two new environments E1 and E2 are generated; these are reconciled by the following merge operator, which requires that all uses of a variable be updated consistently in the output.1 De nition 2 (BV Environment Merge E1e1 e2 E2). Theorem 1 (Structure Preservation of BV Update).
If hE; ei )BV v and v v0 and hE; ei (BV v0 hE0; e0i, then hE; ei hE0; e0i.
If hE; ei (BV v0 hE0; e0i, then hE0; e0i )BV v0. 8 v1 if v1 = v2 <
v1 if x 2= freeVars (e2) : v2 if x 2= freeVars (e1) 1In practice, it is often useful to allow the user to specify a single example of a change, to be propagated to other variable uses automatically. [Mayer et al., 2018] proposes an alternative merge operator which trades soundness for practicality.
Bidirectional Call-By-Name Evaluation Next, we de ne a bidirectional call-by-name system, which largely follows the call-by-value version.
hD; ei )BN u
hD; ei (BN u0 hD0; e0i
BN-E-Fun BN-E-Var
BN-E-Const
hD; ci ) c hD; x:ei ) hD; x:ei D(x) = hDx; ei
hDx; ei ) u hD; xi ) u BN-E-App
hD; e1i ) hDf ; x:ef i hDf ; x 7! hD; e2i; ef i ) u hD; e1 e2i ) u hD; ci ( c0 hD; c0i
BN-U-Const hD; x:ei ( hD0; x:e0i
hD0; x:e0i D(x) = hDx; ei hDx; ei ( u0
hDx0; e0i hD; xi ( u0 hD[x 7! hDx0; e0i]; xi
BN-U-Fun
BN-U-Var hD; e1i ) hDf ; x:ef i hDf ; x 7! hD; e2i; ef i ( u0 hDf0 ; x 7! hD2; e02i; e0f i
hD; e1i ( hDf0 ; x:e0f i hD1; e01i hD; e1 e2i ( u0 hD1e1 e2 D2; e01 e02i
BN-U-App
The BN-U-Const and BV-U-Fun rules are analogous to the call-by-value versions. The BN-U-Var rule for
variables must now evaluate the expression closure to a value, and recursively update that evaluation derivation.
Being call-by-name, rather than call-by-need, we do so every time the variable is used, without any memoization.
The BN-U-App for application is a bit simpler than BV-U-App, because the argument expression is not forced
to evaluate; thus, there is no updated argument expression to push back. Environment merge for call-by-name
environments
If hD; ei )BN u and u u0 and hD; ei (BN u0
If hD; ei (BN u0 hD0; e0i, then hD0; e0i )BN u0.
hD0; e0i, then hD; ei
In addition to being sound with respect to forward call-by-name evaluation, it is sound with respect to forward call-by-value evaluation. To formalize this proposition below, we refer to the lifting dEe and dve of by-value environments and values, respectively, to by-name versions, and to the evaluation JhD; eiK of a delayed expression closure to a by-value value|these de nitions can be found in [Mayer and Chugh, 2019]. Theorem 5 (Completeness of BN Evaluation).
If hE; ei )BV v, then hdEe; ei )BN dve.
Theorem 6 (Soundness of BN Update for BV Evaluation).
If hE; ei )BV v and hdEe; ei (BN dv0e hD0; e0i, then JhD0; e0iK = v0. 3
Bidirectional Krivine Evaluation Lastly, we de ne a bidirectional \Krivine evaluator" (Figure 3) in the style of the classic (forward) Krivine machine [Krivine, 1985], an abstract machine that implements call-by-name semantics for the lambda-calculus. While lower-level than the \direct" call-by-name formulation, the forward and backward Krivine evaluators are even more closely aligned than the prior versions.
Following the approach of the Krivine machine, the forward evaluator maintains a stack S of arguments (i.e. expression closures). When evaluating an application e1 e2, rather than evaluating the e1 to a function closure, the argument expression e2|along with the current environment D|is pushed onto the stack S of function arguments (the K-E-App rule); only when a function expression \meets" a (non-empty) stack of arguments is the function body evaluated (the K-E-Fun-App rule). The K-E-Const, K-E-Fun, and K-E-Var rules are similar to the call-by-name system, now taking stacks into account.
The backward evaluator closely mirrors the forward direction. Recall the two keys for updating applications (BV-U-App and BN-U-App): pasting together new function closures to be pushed back to the function
(hD; ei; S) V u
(hD; ei; S) W u0 K-E-Const (hD; ci; []) V c K-E-Fun (hD; x:ei; []) V hD; x:ei K-E-Var D(x) = hDx; ei (hDx; ei; S) V u
(hD; xi; S) V u K-E-Fun-App (hDf ; x 7! hD2; e2i; ef i; S) V u (hDf ; x:ef i; hD2; e2i :: S) V u
K-E-App (hD; e1i; hD; e2i :: S) V u (hD; e1 e2i; S) V u
K-U-Const (hD; ci; []) W c0
(hD; c0i; []) K-U-Fun (hD; x:ei; []) W hD0; x:e0i
(hD0; x:e0i; []) K-U-Var D(x) = hDx; ei (hDx; ei; S) W u0 (hD; xi; S) W u0 (hD[x 7! hDx0; e0i]; xi; S0)
(hDx0; e0i; S0) K-U-Fun-App (hDf ; x 7! hD2; e2i; ef i; S) W u0 (hDf ; x:ef i; hD2; e2i :: S) W u0
K-U-App (hD; e1i; hD; e2i :: S) W u0 (hD; e1 e2i; S) W u0 (hDf0 ; x 7! hD20; e02i; e0f i; S0) (hDf0 ; x:e0f i; hD20; e02i :: S0) (hD1e1 e2 D2; e01 e02i; S0)
(hD1; e01i; hD2; e02i :: S0) expression, and merging updated environments. Because the forward evaluation rule K-E-App does not syntactically manipulate a function closure, the update rule K-U-App does not construct a new closure to be pushed back. Indeed, only the environment merging aspect from the previous treatments is needed in K-U-App. The K-U-Fun-App rule for the new Krivine evaluation form|following the structure of the K-E-Fun-App rule|creates a new function closure and argument which will be reconciled by environment merge.2 Theorem 7 (Structure Preservation of Krivine Update).
If (hD; ei; S) V u and u u0 and (hD; ei; S) W u0 (hD0; e0i; S0), then hD; ei
The following connects the Krivine system to our (natural-semantics style) call-by-name system (and, hence,
our call-by-value system)|analogous to the connection between the Krivine machine and traditional
substitutionbased call-by-name systems
Theorem 9 (Equivalence of Krivine Evaluation and BN Evaluation).
(h ; ei; []) V u i h ; ei )BN u.
Corollary 1 (Soundess of Krivine Update for BN Evaluation).
If h ; ei )BN u and (h ; ei; []) W u0 (h ; e0i; []), then h ; e0i )BN u0.
Corollary 2 (Soundess of Krivine Update for BV Evaluation).
If h ; ei )BV v and (h ; ei; []) W dv0e (h ; e0i; []), then h ; e0i )BV v0.
We conclude with two observations about the backward Krivine evaluator. First, it never creates new values (function closures, in particular) to be pushed back (like BV-U-App and BN-U-App do). Therefore, if the user interface is con gured to disallow function values from being updated (that is, if the original program produces a rst-order value c), then the K-U-Fun rule for bare function expressions can be omitted from the system.
Second, unlike the call-by-value and call-by-name versions, the backward Krivine evaluator does not refer to forward evaluation at all! The backward rules are straightforward analogs to the forward rules, using environment merge to reconcile duplicated environments. We believe this simplicity may help when scaling the design and implementation of bidirectional evaluation to larger, more full-featured languages.
2Our backward evaluator is not a proper \machine": the K-U-Var and K-U-App rules manipulate environments produced by recursive calls. Although not our goal here, we expect that existing approaches for turning our natural semantics formulation into an abstract state-transition machine (including the use of, e.g., markers or continuations) ought to work for turning our natural semantics into one of the \next 700 Krivine machines" [Douence and Fradet, 2007]. This work was supported by Swiss National Science Foundation Early Postdoc.Mobility Fellowship No. 175041 and U.S. National Science Foundation Grant No. 1651794.