Linear logic also provided another tool, dubbed geometry of interaction [
The Interaction Abstract Machine. This latter idea has been developed in many directions
in the ’90s [
Related Work. The literature on geometry of interaction and its applications is huge, and
goes from, e.g., Girard’s original papers [
Terms of the -calculus are defined as follows: -terms
, ::= ∈ ⃒⃒ . ⃒⃒ where is a countable set of variables. Free and bound variables are defined as usual: . binds in . A term is closed when there are no free occurrences of variables in it. Terms are considered modulo -equivalence, and capture-avoiding (meta-level) substitution of all the free occurrences of for in is noted { }. Contexts are just -terms containing exactly one occurrence of a special symbol, the hole ⟨·⟩ , intuitively standing for a removed subterm. Here we adopt levelled contexts, whose index, i.e. the level, stands for the number of -abstractions (i.e. the number of !-boxes in linear logic terminology, if one translates the -calculus according to the call-by-value translation) the hole lies in.
0 ::= ⟨·⟩ | 0 | 0
+1 ::= . | +1 | +1 We simply write (or ) for a context whenever the level is not relevant. The operation consisting of replacing the hole ⟨·⟩ with a term in a context is noted ⟨⟩ and called plugging. Please note that for every bound variable , if this is isolated by its binding context . , then is the number of s occurring in the syntax tree of the term between the occurrence of and its binder . In other words, is the de Bruijn index of . The operational semantics that we adopt here is weak head evaluation →ℎ, defined as follows: (. )1 . . . ℎ
→ℎ { }1 . . . ℎ.
We further restrict the setting by considering only closed terms, and refer to our framework as Closed Call-by-Name (shortened to Closed CbN). Basic well known facts are that in Closed CbN the normal forms are precisely the abstractions and that →ℎ is deterministic.
In this paper, an abstract machine M is a transition system →M over a set of states (we omit the subscript M when it is clear from the context). We use the standard notations →* and → to denote the transitive and reflexive closure, and the composition times of of →, respectively. The machines considered in this paper move over the code, i.e. the initially fed -term, without ever changing it. A position in a term is represented as a pair (, ) of a sub-term of and a context such that ⟨⟩ = . The shape of states depends on the specific machine, but they always include a position (, ) plus some other data structures. +1 ::= · ::= ⃒⃒ ·
Initial states (on ) are always positioned at the root of the term (, ⟨·⟩ ), where is a closed term. Their precise shape depends on the actual machine. A state is final if no transitions apply. A run is a possibly empty sequence of transitions. An initial run (from ) is a run from an initial state (on ). A state is reachable if it is the target state of an initial run. A complete run is an initial run ending on a final state. Given a machine M, we write M()⇓ if M reaches a M()⇓ if and only if →ℎ terminates on , for every closed term . ifnal state starting from , and M()⇑ otherwise. We say that M implements Closed CbN when
The Krivine abstract machine [
The KAM, defined in Fig. 1, records every -redex that it encounters using two data structures, the environment and the stack . The basic idea is that, by saving encountered -redexes in the environment , the machine can simply look up in for the argument of the binder whenever encountering a variable occurrence . This is found looking at the entry in the environment corresponding to the de Bruijn index of . The stack is used to collect encountered arguments that still have to be paired to abstractions to form -redexes, and then go into the environment .
Closures, Stacks, and Environments.
environments, plus the independent one for stacks are defined in Fig. 1, together with the definition of states. The idea is that every piece of code comes with an environment, forming a closure, which is why environments and closures are mutually defined. We denote by the set of KAM states.
Transitions, Initial and Final States. Initial states of the KAM are in the form := (, ⟨·⟩ , , ). The transitions of the KAM are in Fig. 1—their union is noted →KAM. The idea is that the →sub transition looks in the environment for the argument of the variable under evaluation. The KAM evaluates the term until the top abstraction of the weak head normal form of is found, that is a run either never stops or ends in a state of the shape = (., , , ). This is guaranteed by the fact that terms are closed and the standard (but omitted) invariant
Logged Positions ::= ◇ ⃒⃒ (. , +1)
Directions ::= ↓ ⃒⃒ ↑
Tapes ::= ⃒⃒ ∙ · ⃒⃒ ∘ · ⃒⃒ · 0 ::=
Logs +1 ::= ·
States ::= (, , , , ) Term . . ⟨⟩ . ⟨⟩ ensuring that on reachable states the level of the context equals the length of the environment, so that the KAM never gets stuck on a →sub transition.
Theorem 2.1 ([
In this section we define the Boring Interaction Abstract Machine (BIAM). We follow [
A Bird’s Eye View of the BIAM. Intuitively, the behavior of the BIAM can be seen as that of a token that travels around the syntax tree of the program under evaluation. Similarly to the KAM, it looks for the head variable of a term, but without storing the encountered -redexes in an environment. When it finds the head variable, the BIAM looks for the argument which should replace it, because having no environment it cannot simply look it up. These two search mechanisms are realized by two diferent phases and directions of exploration of the code, noted ↓ and ↑. The functioning is actually more involved because there is also a backtracking mechanism, requiring to save and manipulate code positions in the token. Last, the machine never duplicates the code, but it distinguishes diferent uses of a same code (position) using logs. Unfortunately, there are no easy intuitions about how logs handle the diferent uses. BIAM States. The BIAM travels on a -term carrying some data structures, defined in Fig. 2, which store information about the computation and determine the next transition to be applied. · ◇ · ∙ · ◇ · ∘ · →∙ 3 →∙ 4 →arg →bt1 .
⟨⟨·⟩⟩
A key point is that navigation is done locally, moving only between adjacent positions.1 The BIAM also has a direction of navigation that is either ↓ or ↑ (pronounced down and up). The token carries two stacks, called log and tape, whose main components are logged positions. Roughly, a log is a trace of the relevant positions in the history of a computation. A logged position is either an occurrence of a distinguished symbol ◇ (representing a dereliction in linear logic jargon), or a position plus a log, meant to trace the history that led to that position. Logs and logged positions are then defined by mutual induction, as it was the case for closures and environments in the KAM. We use · also to concatenate logs, writing, e.g., · , using for a log of unspecified length. The tape is a list of logged positions plus occurrences of the special symbols ∙ and ∘ , needed to record the crossing of abstractions and applications. A state of the machine is given by a position, a log and a tape , together with a direction. Initial states have the form := (, ⟨·⟩ , , ◇ ).2 Directions are often omitted and represented via colors and underlining: ↓ is represented by a red and underlined code term, ↑ by a blue and underlined code context. We denote by the set of BIAM states.
Transitions. Intuitively, the machine evaluates the term until the head abstraction of its head normal form is found. The transitions of the BIAM are split into two groups, ↓-transitions, which depend on the structure of the code term, in Fig. 2, and ↑-transitions, which depend on the structure of the code context, in Fig. 3. Their union is noted →BIAM. The idea is that ↓-states (, , , ) are queries about the head variable of (the head normal form of) and ↑-states (, , , ) are queries about the argument of an abstraction.
Simple Properties. The BIAM satisfies several nice properties which can be proved just by examining the transition rules. If we consider it as an automaton it is bi-deterministic, i.e. it is deterministic and reversible. Moreover, the tape satisfies a FIFO stack policy.
Proposition 3.1 (Reversibility and Pumping). If 1 →BIAM 2, then: 1. ⊥ →BIAM 1⊥, where ⊥ is with inverted direction.
2 2. 1 + →BIAM 2 + , where if has tape , then + ′ has tape · ′. 1Note that also the transition from the variable occurrence to the binder in →var and →bt2 are local if -terms are represented by implementing occurrences as pointers to their binders, as in the proof net representation of -terms, upon which some concrete implementation schemes are based, see [31]. 2Initial non-empty states could seem weird at first. However, they have a natural linear logical interpretation. In the call-by-value translation values are always !-boxed, and derelictions are needed to open such boxes. The symbol ◇ indeed represents a dereliction, i.e. a query to open a box, thus needed also in the initial state.
If we restrict ourselves to reachable states, we are able to establish some properties about them, by induction on the initial run that leads to them.
Proposition 3.2 (Invariants). If (, , , , ) is a reachable BIAM state, then: 1. satisfies the regular expression (· (∙ | ∘ ))* · . 2. || = .
These two invariants together guarantee that the BIAM is never blocked on the transition →var. A much stronger (and way more involved) invariant that we are going to present in the next section guarantees that the BIAM can only be blocked on states of the form (. , , , ), which therefore is the only possible shape of final states.
This section presents the main technical result of this paper, namely that adding jumps (in the
sense of Danos and Regnier [
Jumps. We have already stressed that each transition of the BIAM is local. This means that at each step the token moves to positions which are adjacent to the previous ones in the syntax tree of the -term under evaluation. This is not the case for the KAM. Indeed, the transition →sub moves the focus of the evaluation to an arbitrary position of the term. We call these non-local transitions jumps. Of course, jumps are possible because during the already carried out computation some positions have been saved. In particular, one could see a similar pattern between the BIAM transition →∙ 1 (or →∙ 2) and the KAM transition →sea (or → ). Ignoring the constant ∙ (which is not needed in the KAM, although it could be straightforwardly added), their diference lies in the fact that in transition →sea the dereliction constant ◇ (and in transition → a generic logged position ) have been substituted by a closure , that saves the encountered arguments (together with their respective environments). These closures are then used in the jump of transition →sub.
The Boring Jumping Abstract Machine. We formalize the intuition above by defining the Boring Jumping Abstract Machine (BJAM), in Fig. 4. One could already notice the (bi-)similarity with the KAM, this is why we have kept the same transition names. Consistently with the BIAM, initial BJAM states have the form (, ⟨·⟩ , , 0), where 0 is a dummy closure, and final states have the shape (., , , ). We denote by the set of BJAM states. This machine is obtained from the BIAM by making just two small adjustments. (i) Saving a closure in transition →∙ 1 instead of putting simply a ◇ ; and (ii) jumping in transition →var to the argument stored in the right closure (as in the KAM). With these two modifications, one immediately notices that ↑-transitions are no more needed. Indeed, since the initial states are of ↓-direction and without any ∘ , ↑-states are no more reachable (and the →bt2 transition is never fired). Please notice that closures here, and diferently from the KAM, can be surrounded by arbitrary logged contexts. Indeed closures can be pushed deep inside at arbitrary depth by the BJAM transition →sub. ::= ⃒⃒ ∙· ⃒⃒ · ::= ⟨·⟩ ⃒⃒ (. , · )
Env
Stack · ∙ ·
Logged Closures
::= ⟨⟩ T Ctx we briefly illustrate how the three machines compute with a small example.
Example 4.1. We consider the term := (. )(. ). The BJAM, the BIAM, and the KAM complete runs are as follows (where := (. )⟨·⟩ and := . ):
2 (, ⟨·⟩ , , 0) →BJAM (, (. ⟨·⟩ )(. ), (, , ), 0) →BJAM (, , , (. ⟨·⟩ , 0)) 2 2 (, ⟨·⟩ , , ◇ ) →BIAM (, (. ⟨·⟩ )(. ), ◇ , ◇ ) →BIAM (, , , (. ⟨·⟩ , ◇ ))
2 (, ⟨·⟩ , , ) →KAM (, (. ⟨·⟩ )(. ), (, , ), ) →KAM (, , , ) The reader can immediately notice that the BJAM somehow subsumes both the BIAM and the way, one obtains KAM states by removing all the logged contexts surrounding closures. KAM. From BJAM states one obtains BIAM states by turning all closures into ◇ , and, in a dual Improvements, Abstractly.
We formalize the intuition above through a bisimulation-like
argument. In particular, we need to prove that BJAM jumps can be simulated by (possibly many)
BIAM transitions. We use the abstract framework of improvements, already setup in [
′, ′′ℛ′ and ≤ + 1. → ′, ′ →
′′, ′ℛ′′ and ≥ + 1. 2. Transition left: if ∈ and → ′, then there exists ′′ ∈ and ′ ∈ such that 3. Transition right: if ∈ and → ′, then there exists ′ ∈ and ′′ ∈ such that What improves along an improvement is the number of transitions required to reach a final state, if any.
Proposition 4.3 ([
Relating the BIAM and the BJAM. The main dificulty in relating BIAM and BJAM runs lies in proving that BJAM jumps can be simulated by the BIAM. To do so, we first define a translation (· ) : → , from BJAM states to BIAM states (and extended to all of their components) as follows: (, , , ) := (, , , )
( · ) := · (. , · ) := (. , () · ) ( · ) := · (∙ · ) := ∙ · ⟨⟩ := ⟨◇⟩ ( ) := ⟨·⟩ := ⟨·⟩ Then, we define the relation ≻ ⊆
× that we want to prove being an improvement as: ≻ if and only if and are reachable and = It is immediate to show that initial states (on the same term) are related: indeed we have that (, ⟨·⟩ , , (, ⟨·⟩ , )) = (, ⟨·⟩ , , ◇ ). At this point, one has to prove that the relation ≻ satisfies Definition 4.2. One would like to proceed examining all the transitions of the BJAM, and while transitions →sea, and → are easy to reason about, there is no easy way to handle transition →sub. Indeed, while the BJAM performs a jump, the BIAM performs a (possibly very long) series of transitions. To solve this issue, we resort to proving a very strong invariant that somehow relates BJAM and BIAM states.
The Exhaustible Invariant. We lift the technique introduced by Accattoli et al. in [
Definition 4.4 (Stack tests). Let = (, , , ) be an BJAM state. Then, the BIAM state := (, , , ( ′) · ⟨◇⟩ · ∘ ) is a stack test for of focus for each decomposition = ′ · ⟨⟩ · ′′ · ′ of the stack.
Definition 4.5 (Environment tests). Let = (, ⟨. ⟩, · ⟨⟩· , ) be an BJAM state. Then, the BIAM state := (. ⟨⟩, , , ⟨◇⟩ · ∘ ) is an environment test for of focus .
Definition 4.6 (State induced by a closure). Given a closure := (, , ), the BJAM state induced by is defined as := (, , , ).
Then we are able to give a formal definition of exhaustible states, based on the previously defined notions.
Definition 4.7 (Exhaustible states). ℰ is the smallest set of those BJAM states such that for any stack or environment test of of focus , there exists a BIAM run : →+IAM () such that ∈ ℰ .
Now, by induction on the length of the run, we can prove that all reachable BJAM states are actually exhaustible.
Lemma 4.8. Let be a reachable BJAM state. Then is exhaustible.
Proof. We proceed by induction on the length of the run that leads to . If = 0, the statement is trivially true. We consider the diferent cases relative to the inductive step. • Application:
′ = (, , , ) →sea (, ⟨⟨·⟩ ⟩, , (, ⟨⟨·⟩⟩ , ) · ∙ · ) = – Environment tests: by i.h., since they are the same of those of ′. – Stack tests: the first stack test of is = (, ⟨⟨·⟩ ⟩, , ◇ · ∘ (, ⟨⟨·⟩⟩ , ). It is positive since ), where = (, ⟨⟨·⟩ ⟩, , ◇ · ∘
) →arg (, ⟨⟨·⟩⟩ , , ) = () does not have any stack test and its environment tests are the same as those of ′, hence positive by i.h.. For all the other stack tests ′ of of focus ′, we have ′ = (, ⟨⟨·⟩ ⟩, , ◇ · ∙ · ( ′) · ⟨◇⟩ · ∘ ) →∙ 3 (, , , ( ′) · ⟨◇⟩ · ∘ ) = ′′ where ′ · ⟨′⟩ is a proper prefix of . Please note that ′′ is a stack test of ′, and hence positive by i.h.. • Abstraction:
′ = (., , , · ∙ · ) → (, ⟨. ⟨·⟩⟩ , · , ) = – Environment tests: environment tests of are those of ′ plus (., , , · ∘ ), which is the first (from the left) stack test of ′, and hence positive by i.h.. – Stack tests: all stack tests of of focus rewrite in one step to stack tests of ′, positive by i.h.. In fact: (, ⟨. ⟨·⟩⟩ , · , ( ′) · ⟨◇⟩ · ∘ ) →∙ 4 (., , , · ∙ · ( ′) · ⟨◇⟩ · ∘ ) where ′ · ⟨⟩ is a proper prefix of . • Variable: ′ = (, ⟨. ⟩, · ⟨, ′, ′⟩ · , · ) →var (, ′, ′, (. , · ) · ) = – Environment tests: since ′ is exhaustible by i.h., we have that its environment test relative to := (, ′, ′) := (. ⟨⟩, , , ⟨◇⟩ · ∘
+ ) → IAM () := (, ′, ′, ) and is exhaustible. Please note that its environment tests are positive. Thus, also environment tests of are positive since they are the same of . – Stack tests: we have two cases. First we consider the stack test relative to the leftmost position (. , · ), i.e.:
(, ′, (′) , (. , · ) · ∘ ) From the point above, by reversibility and pumping (. , · ) · ∘ , we have: (, ′, (′) , (. , · )∘· ) →+IAM (. ⟨⟩, , , ⟨◇⟩·∘ (. , · )∘· ) Now,
(. , · )∘· ) →bt2 (, ⟨. ⟩, · ⟨◇⟩· , ·∘ ) and this last state is the leftmost stack test of ′, hence positive by i.h..
The same method can be used for all the other stack tests of the form
(, ′, (′) , (, . , · ) · ( ′) · (′) · ∘ ) where ′ · ′ is a proper prefix of (of course pumping (. , · ) · ( ′) · (′) · ∘ ). Example 4.9. Being the invariant and the related definitions hard to grasp, we provide an example of application. We consider the reachable BJAM state (, (. ⟨·⟩ )(. ), (., (. )⟨·⟩ , ), 0), seen in Example 4.1. It has one environment test, namely (., ⟨·⟩ (. ), , ◇ · ∘ ), of focus := (., (. )⟨·⟩ , ). The BJAM state induced by is := (., (. )⟨·⟩ , , ), and indeed we have that: (., ⟨·⟩ (. ), , ◇ · ∘
) →arg (. , (. )⟨·⟩ , , ) = ()
We use Lemma 4.8 to prove the following key proposition, that establishes the simulation of the BJAM by the BIAM.
Proposition 4.10. ≻ is an improvement.
Proof. We need to verify all points of Definition 4.2. Point 1 (final state right) is immediate. Indeed if ≻ and is final, i.e. in the form := (., , , ), then also := (. , , , ) is a final state.
We prove point 2 and 3 together. We proceed by analysing the shape of .
• Case →sea. The following diagram proves this case.
(, , , ) (, ⟨⟨·⟩ ⟩, , ·◇ ∙ · ) ≻ ≻ (, , , ) ↓
sea (, ⟨⟨·⟩ ⟩, , (, ⟨⟨·⟩⟩ , )· ∙ · ) • Case → . The following diagram proves this case.
(. , , , · ∙ · ) (, ⟨. ⟨·⟩⟩ , · , ) ≻ ≻ (., , , · ∙ · ) ↓
(, ⟨. ⟨·⟩⟩ , · , ) • Case →sub. We need to close the following diagram: (, ⟨. ⟩, () · ⟨◇⟩· , · )
≻ (, ⟨. ⟩, · ⟨, ′, ′⟩· , · ) ↓ var Since is reachable, and hence exhaustible by Lemma 4.8, we apply the definition of exhaustible state to the environment closure (, ′, ′). This means that we have the sequence of reductions: := (. ⟨⟩, , , ⟨◇⟩ · ∘
+ ) →BIAM (, ′, (′) , ) which, pumping (. , () ·
· ) , allows us to close the diagram.
Relating the BJAM and the KAM.
We have related the BIAM and the BJAM. What is left is then to relate the BJAM and the KAM. Intuitively, BJAM states are just KAM states decorated with logged contexts. Moreover, the two machines morally behave the same. Indeed, logged contexts are never used by the BJAM, because in transition →sub they are just thrown away from the environment. This is why the proof of improvement (actually a strong bisimulation) between the BJAM and the KAM is easy. As before, we first define a translation from BJAM states to KAM states (and extended to all of their components) that just ignores logged contexts, the rightmost dummy closure in the stack, and the ∙ symbol, as follows: (· ) : → , (, , , · ) := (, , , ) ( · ) := · ( · ) := · (∙ · ) :=
( ) := ⟨⟩ :=
≃ ⊆ × that we want to prove being an improvement as: ≃ if and only if and are reachable and = We immediately observe that ≃ is an improvement (actually a strong bisimulation). Proposition 4.11. The BJAM and the KAM are strongly bisimilar.
Then, we can state our main result, namely that the BIAM can simulate the KAM. Theorem 4.12. There is an improvement between the BIAM and the KAM.
Proof. Since the composition of two improvements is again an improvement, the desired improvement is ≻ ; ≃.
Corollary 4.13. The BIAM implements Closed Call-by-Name.
Proof. Since improvements preserve (non)termination (Lemma 2).
We have analyzed the relationship between the BIAM, the BJAM, and the KAM. We use this section to clarify some points that we have (intentionally) overlooked, and that we leave for further work.
Relationship with the IAM. The reader may wonder what is the relationship between the BIAM and the IAM obtained through the call-by-name translation of intuitionistic logic inside linear logic. A simple inspection of the transitions rules of the BIAM reveals that the two machines are likely to be strongly bisimilar. However, it is not clear whether and how it is possible to prove the correspondence directly, i.e. by exhibiting a concrete strong bisimulation between the states of the two machines, which are indeed very diferent. The length of the log is in fact equal to the depth of the code context, which is defined in a diferent way in the two translations. This question has to do with the intimate nature of the two translations, and is thus intriguing.
Call-by-Value Adequacy and Intersection Types. In [
With this paper we have clarified some obscure points in the relationship between Krivine’s
abstract machine, the call-by-value (or “boring”) Girard’s translation of intuitionistic logic inside
linear logic, and Girard’s geometry of interaction. The connection between these three concepts
was already considered by Danos and Regnier in [
We would like to thank Beniamino Accattoli with whom we have discussed this topic. The first author is funded by the ERC CoG “DIAPASoN” (GA 818616). The second author is supported by the ANR PPS Project ANR-19-CE48-0014 and the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 101034255”. in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, IEEE Computer Society, 2017, pp. 1–12. doi:10.1109/LICS.2017.8005112. [26] P. Curien, H. Herbelin, Computing with abstract böhm trees, in: M. Sato, Y. Toyama (Eds.), Third Fuji International Symposium on Functional and Logic Programming, FLOPS 1998, Kyoto, Japan, Apil 2-4, 1998, World Scientific, Singapore, 1998, pp. 20–39. [27] P. Curien, H. Herbelin, Abstract machines for dialogue games (2007). URL: http://arxiv.
org/abs/0706.2544. [28] U. Schöpp, On the relation of interaction semantics to continuations and defunctionalization, Logical Methods in Computer Science 10 (2014). doi:10.2168/LMCS-10(4: 10)2014. [29] U. Schöpp, From call-by-value to interaction by typed closure conversion, in: X. Feng, S. Park (Eds.), Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, volume 9458 of Lecture Notes in Computer Science, Springer, 2015, pp. 251–270. doi:10.1007/ 978-3-319-26529-2\_14. [30] B. Accattoli, U. Dal Lago, G. Vanoni, The space of interaction, in: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021, pp. 1–13. doi:10. 1109/LICS52264.2021.9470726. [31] B. Accattoli, B. Barras, Environments and the complexity of abstract machines, in: W. Vanhoof, B. Pientka (Eds.), Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017, ACM, 2017, pp. 4–16. doi:10.1145/3131851.3131855.