Computing with Abstract Böhm Trees

Pierre-Louis Curien (CNRS-ENS)  Hugo Herbelin (LITP)

Abstract

We focus on purely operational aspects of game semantics. We present abstract Böhm trees, which capture the computational core of λ-calculi for various proof systems and languages, including Scott’s Pcf. We introduce a computing device over abstract Böhm trees, called Strategic Abstract Machine, Pulling this device back to the syntax gives Krivine’s style abstract machines handling reduction in Pcf or in untyped λ-calculus without stack nor dump. Our device is step to step related to the interaction mechanism in Coquand’s or Hyland-Ong’s game semantics, and to an abstract form of Danos-Regnier’s pointer machine.

1 Introduction

In the recent years, game semantics has brought new insights on computation in typed programming languages [2, 13] and proof theory [3, 14, 4, 10], following older works by Gentzen and Lorenzen’s school – see Felscher [9]. For these semantics, terms and proofs are interpreted by strategies in some game and reduction to normal form is interaction between the strategies.

In [10], the second author has explored the relation between interaction in the semantics and reduction in the syntax: he observed that interaction between strategies in Coquand’s model of sequent calculus [4] follows step by step the process of weakhead cut-elimination. Then, observing the analogy between Hyland-Ong’s style of games [13] and Danos-Regnier’s variant [8] of Krivine’s abstract machine [5], the step by step correspondence between call-by-name abstract machines and interaction in games has become more precise [7] ^{1}. (In our setting, Coquand’s and Danos-Regnier’s machines are called View Abstract Machine (or VAM) and Pointer Abstract Machine (or PAM), respectively.)

In the present paper, we make the correspondence even more precise, between syntax and game semantics, and between call-by-name abstract machines for λ-calculi and interaction. Our treatment is based on a notion of abstract Böhm tree, which arises as a natural abstraction of λ-calculus’ (η-long) Böhm trees. Abstract Böhm trees have to be compared with Coquand’s strategies [4], with the innocent functions underlying Hyland-Ong’s innocent strategies [13], and with the strategies for E-dialogues in the sense of Felscher [9]. Abstract Böhm trees capture the computational core of pure simply-typed λ-calculus but also of simply-typed λ-calculi with constants and case statements (like Pcf [15]). They can be extended to capture untyped λ-calculus too.

In the first two sections, we exemplify the relation between concrete and abstract computing device. Two related machines are described. The first one, called KAM, is a simple variant of Krivine’s abstract machine specially devised for computing over simplytyped η-long normal λ-terms: it has no stack and only one rule. The second machine, called Strategic Abstract Machine (SAM), is the abstract counterpart of the KAM. It works on abstract Böhm trees. In section 4, we present a handy geometric notation for the execution in the SAM.

In section 5, we show that the SAM can handle computation over Pcf Böhm trees (which, roughly, are with respect to Pcf what Böhm trees are with respect to λ-calculus), without any need to add instructions to handle the case statements. However, a slight extension is necessary to handle arbitrary untyped λ-terms (section 6). Pulling back in the original concrete syntax the work carried out in sections 5 and 6, we get simple stack-free and dump-free callby-name enviromnent machines for computing over Pcf Böhm trees and over arbitrary untyped λ-terms, respectively (section 7).

1In [7], a relation between Abramsky-Jagadeesan’s style of game and the Geometry of Interaction is also exhibited.

Finally, in section 8, we show how the SAM relates to the VAM and the PAM discussed above.

2 Stack-free machine (KAM)

We introduce an abstract machine with two components – the code and the environment – to implement the reduction of η-long λ-terms. In such terms, each occurrence of a variable must appear in a context where it is applied to all its arguments, and in each sequence of abstractions λx⃗.M the number of parameters x_{1}, …, x_{n} is exactly the number of arguments N_{1}, …, N_{n} which the term λx⃗.M can accept according to its type. Moreover, we suppose that M, N_{1}, …, N_{n} are normal forms The two assumptions (η-long and normal) make the game-theoretic interpretation easier to grasp. The η-long restriction allows us to dispense of the stack component, which (in call-by-name) only serves to store arguments. Without the stack, we can discover a symmetry between the two remaining components. Indeed, the second restriction enables us to observe a strict alternation between the code and the environment. (The restrictions will be relaxed in section 6.)

To further smooth the way towards a reading of terms as strategies, we write a (head) normal form M = λx⃗.yN⃗ as: M = (λx⃗.W), where W = yN⃗. We split M in this way even if x⃗ is empty: in this case we write M = (W) and W = yN⃗. We call W a body, or code. The Stack-Free Krivine Abstract Machine (or KAM) has only one rule, given in figure 1. The states of the KAM are closures, i.e., pairs of the form W [e], where W is a code, and where e is an environment, i.e. a list of environment items B each consisting of a list of closures:

\begin{matrix}M ::= (λx⃗.W) & e ::= nil B^{•}e \\ W ::= yM⃗ & B ::= ⟨z⃗ ← M⃗⟩[e]. \end{matrix}

Thus environments are lists of lists of closures, not just lists of closures as in usual environment machines. This two-level structure corresponds to the representation of normal forms: each environment item is to be matched with a vector of λ’s, not just one. We usually do not write nil, e.g. B^{•}nil is written B, or (z⃗ ← M⃗)[nil] is written (z⃗ ← M⃗)[ ]. The notation ⟨z⃗ ← M⃗⟩[e] should be read as a vector M_{1}[e], …, M_{n}[e] of closures bound to z_{1}, …, z_{n}.

Each machine step can be decomposed in two phases. Given (xM⃗)[e], the machine first looks for the value of x in e. We assume that all bound variables have distinct names. Thus, there exists at most one pair (i, j) such that x = x_{ij}: i is the environment item in which the binding of x lies, and j is the posi-

(K) (xM⃗)[e] → W [⟨z⃗ ← M⃗⟩[e]^{•}e_{i}]

where

\begin{matrix}e = B_{0}^{•} ⋯^{•}B_{n} & B_{i} = ⟨x⃗_{i} ← N⃗_{i}⟩[e_{i}] \\ x = x_{ij} & N_{ij} = (λz⃗.W) \end{matrix}

Figure 1: The Stack-Free Krivine Abstract Machine

tion of x in this environment item. If (λz⃗.W) is the value of x, then the second phase consists in extending the environment with an anvironment item that binds M⃗ to z⃗. Figure 2 shows the execution of

u(λx.u(λy.x)) [u ← (λr.r(r(z)))].

We take u(λx.u(λy.x))[⟨u ← (λr.r(r(z)))⟩[ ]] as initial state. Notice the addition of [ ] to turn (λr.r(r(z))) into a closure. The code part and the environment part of the state are displayed in the second and the third column, respectively. In this execution, we have numbered the machine steps 2′, 3′, 4′, . . .. Notice the strict alternation between (subterms of) (u(λx.u(λy.x))) and (subterms of) (λr.r(r(z))) We have placed superscripts 2, 3, 4, … on the bindings of the environments which are used “between” the steps. More precisely, we can identify successive “moves” 2′, 2, 3′, 3, 4′, 4, … n′, n, (n + 1)′, …, which correspond to (copies of) subterms of (u(λx.u(λy.x))) and (λr.r(r(z))):

2′ points to u(λx.u(λy.x)) (code)
2 points to (λr.r(r(z)))  (term)
3′ points to r(r(z))  (code)

⋯

The following invariants hold, for each n: (i) the subterm associated with n is the value (in the environment) of the head variable of the code associated with n′; (ii) if the subterm associated with n is (λy⃗.W), then the code associated with (n + 1)′ is W.

3 Strategic machine (SAM)

In this section, we lift the machine presented in section 2 to a more abstract level, where terms are replaced by more general and more ”semantic” objects, called abstract Böhm trees, or strategies. We suppose given an alphabet A of moves, containing a special symbol •, which is to serve as initial move. Positions are sequences of moves with backward pointers from moves occurring at even places in the position to moves occurring at odd places. We choose to represent pointers by numbers that count the number of opponent’s moves between the pointing player’s move

\begin{matrix}2′ & u(λx.u(λy.x)) & ⟨u ←^{2} (λr.r(r(z)))⟩[ ] = ρ_{0} \\ 3′ & r(r(z)) & ⟨r ←^{3} (λx.u(λy.x))⟩[ρ_{0}] = ρ_{1} \\ 4′ & u(λy.x) & ⟨x ← (r(z))⟩[ρ_{1}]^{•}(ρ_{0} = ⟨u ←^{4} (λr.r(r(z)))⟩[ ]) = ρ_{2} \\ 5′ & r(r(z)) & ⟨r ←^{5} (λy.x)⟩[ρ_{2}] = ρ_{3} \\ 6′ & x & ⟨y ← (r(z))⟩[ρ_{3}]^{•}(ρ_{2} = ⟨x ←^{6} (r(z))⟩[ρ_{1}]^{•}ρ_{0}) = ρ_{4} \\ 7′ & r(z) & ⟨⟩[ρ_{4}]^{•}(ρ_{1} = ⟨r ←^{7} (λx.u(λy.x))⟩[ρ_{0}]) = ρ_{5} \\ 8′ & u(λy.x) & ⟨x ← (z)⟩[ρ_{5}]^{•}(ρ_{0} = ⟨u ←^{8} (λr.r(r(z)))⟩[ ]) = ρ_{6} \\ 9′ & r(r(z)) & ⟨r ←^{9} (λy.x)⟩[ρ_{6}] = ρ_{7} \\ 10′ & x & ⟨y ← (r(z))⟩[ρ_{7}]^{•}(ρ_{6} = ⟨x ←^{10} (z)⟩[ρ_{5}]^{•}ρ_{0}) = ρ_{8} \\ 11′ & z & ⟨⟩[ρ_{8}]^{•}ρ_{5} \end{matrix}

Figure 2: The execution of u(λx.u(λy.x)) [u ← (λr.r(r(z)))] (KAM)

and the pointed opponent’s move. (This is an abstraction of De Bruijn’s notation for the λ-calculus, cf. e.g. [1].) Thus an even position, i.e. a position of even length, is a non-empty sequence r of the form:

a_{1}[a_{2}, ↩^{κ_{1}}] ⋯ a_{2n−1}[a_{2n}, ↩^{κ_{n}}]

(a_{j} ∈ A for all j ≤ 2n and κ_{l} ∈ {0, 1, …, l−1}∪{ } for

all l ≤ n); a_{1}, a_{3}, … and [a_{2}, ↩^{κ_{1}}], [a_{4}, ↩^{κ_{2}}], … are called

opponent’s moves and player’s moves, respectively. If κ_{l} = , we say that [a_{2l}, ↩^{κ_{l}}] occurs free. Otherwise, we say that [a_{2l}, ↩^{κ_{l}}] is bound to a_{2(l−κ_{l})−1}. We use i to range over κ’s different from . An odd position q = a_{1}[a_{2}, ↩^{κ_{1}}] ⋯ a_{2n−1} is defined in the same way. We use p to denote a position which is either even or odd.

An abstract Böhm tree, or strategy, is a tree consisting of a set ϕ of even positions of the form •p, where • does not occur in p, closed under even nonempty prefixes and such that q[a_{1}, ↩^{κ_{1}}], q[a_{2}, ↩^{κ_{2}}] ∈ ϕ implies [a_{1}, ↩^{κ_{1}}] = [a_{2}, ↩^{κ_{2}}]. The last condition says that, in a strategy, a “query”, (that is, an odd position), if answered, is uniquely so. Therefore, any strategy can be unambiguously presented as a partial function, also written ϕ, from odd positions (in which the player’s moves are actually irrelevant) to pointing player’s moves [a, ↩^{κ}].

We also need the related notion of multistrategy. First we define a renaming operation: [a ← ϕ] = {ar | •r ∈ ϕ}. Hence [a ← ϕ]’s root is labelled by a. A multistrategy ψ is a union of renamed strategies [a_{1} ← ϕ_{1}], …, [a_{n} ← ϕ_{n}] (with all the a_{i}’s distinct and ≠ •). We write ψ more suggestively as:

ψ = [a_{1} ← ϕ_{1}, …, a_{n} ← ϕ_{n}].

As an illustration, we define a compilation of (η-long) λ normal forms. We take as alphabet A = {•} ∪ ω ∪ Var, where ω is the set of natural numbers, and where the variables x ∈ Var are only used as player’s moves of the form [x, ↩]. We perform the following transformation on the tree representation

\overbrace{M_{1} ⋯ M_{n}}^{λx⃗.y}

of a normal form M. The node “λx⃗.y” is split into two moves: “λx⃗” is associated to the opponent’s move • and “y” to a player’s move \underline{y}. One may think that two players are exploring M: the opponent asks for head variable and the player provides it. When y is free, \underline{y} is [y, ↩]. Otherwise, \underline{y} is [n, ↩^{i}] such that the binder is found 2i + 1 moves above and n denotes the position of y in the multiple abstraction λy_{1} ⋯ y_{m} which binds it, i.e. y = y_{n}. In the terminology of Danos and Regnier, n is called the rank and i is called the lift. The pairs (n, i), which we call Böhm indices, also appear in [12]. Finally, if ϕ_{i} is the translation of M_{i}, for all i, then the head opponent’s move • of ϕ_{i} is replaced by i. Summarising, the translation of M = (λx⃗.yM_{1} ⋯ M_{n}) is the following tree:

\overbrace{[1 ← ϕ_{1}] ⋯ [n ← ϕ_{n}]}^{•\underline{y}}

Here is a formal translation involving a function which takes a list σ of vectors of variables and a term M, and returns a strategy M^{σ}:

(λx⃗.yM⃗)^{σ} = {•y^{x⃗^{•}σ}} ⋃_{i=1···n}{•y^{x⃗^{•}σ}ir | •r ∈ (M_{i})^{x⃗^{•}σ}}

where

\begin{matrix}\overline{x^{nil} = [x, ↩]} & \frac{x = x_{i} x⃗ = x_{1} ⋯ x_{k}}{x^{x⃗^{•}σ} = [i, ↩^{0}]} \\ \frac{x^{σ} = [i, ↩^{j}]}{x^{y⃗^{•}σ} = [i, ↩^{j+1}]} & \frac{x^{σ} = [x, ↩]}{x^{y⃗^{•}σ} = [x, ↩]} \end{matrix}

The compilation of a term M is defined as M^{nil}. This is more than a compilation. It is injective (under our η-long assumption). We can even turn it into a bijection (whence the terminology of abstract Böhm trees), by imposing explicitly some additional conditions in the definition of a strategy ϕ.

Below, we display the compilation of the example of the previous section. The boxed comments give the correspondence with the source terms.

- Strategy for (u(λx.u(λy.x))):

•^{(} [u, ↩] { 1^{(λx} [u, ↩] { 1^{(λy} [1, ↩^{1}]^{x}

- Multistrategy for [u ← (λr.r(r(z)))]:

u^{(λr} [1, ↩^{0}]^{r} { 1^{(} [1, ↩^{1}]^{r} { 1^{(} [z, ↩]

We now express an abstract version of the KAM, called Strategic Abstract Machine (or SAM). The goal of a SAM execution is to compute (the “head normal form” of) a composition ϕ ∘ ψ of a strategy ϕ whose free player’s moves are [a_{1}, ↩], …, [a_{n}, ↩] with a multistrategy ψ = [a_{1} ← ϕ_{1}, …, a_{n} ← ϕ_{n}]. (Think of a substitution M[x⃗ ← N⃗].). The states of the SAM are abstract versions of closures: they are pairs p[e] of a position and an environment. The syntax for environments is as follows (where r stands for an even position)::

e ::= nil B^{•}e B ::= r[e] .

The rules of the SAM are given in figure 3. In rule (n)_{b}, π_{i+1}(e) denotes the (i + 1)-th element of e, i.e. π_{i+1}(B_{0}^{•} ⋯^{•}B_{i}^{•}e′) = B_{i}. For all the machines presented in the paper, we consider it implicit that there is a counter recording the current machine step number. The successive steps are numbered 1, 2′, 2, 3′, 3, 4′, …, with the following player/opponent and ϕ/ψ alternance:

1 initial opponent’s move in ϕ
2′ player’s move in ϕ
2 opponent’s move in ψ
3′ player’s move in ψ
3 opponent’s move in ϕ
4′ player’s move in ϕ

⋯

The following invariant holds: at each state p[e], the length of e is the number of opponent’s moves in p, including • (2n, (2n + 1)′) or not (2n − 1, 2n′).

The execution of the example of section 2 by the SAM is shown on figure 4. The empty environment in step 2′ reflects a minor difference in the treatment of the initial substitution [u ← (λr.r(r(z)))]. In section 2, we had turned this substitution into an initial

\begin{matrix}(1) & \overline{⟶ •[ ]} \\ (2n′) & \frac{ϕ(q) = [a, ↩^{κ}]}{q[e] ⟶ (q[a, ↩^{κ}])[e]} \\ ((2n + 1)′) & \frac{ψ(q) = [a, ↩^{κ}]}{q[e] ⟶ (q[a, ↩^{κ}])[e]} \\ (n)_{b} & \frac{r = q[a, ↩^{i}] and π_{i+1}(e) = r′[e′]}{r[e] ⟶ (r′a)[r[e]^{•}e′]} \\ (2n)_{f} & \frac{r = q[a, ↩]}{r[e] ⟶ a[r[e]]} \end{matrix}

Figure 3: The Strategic Abstract Machine

environment ⟨u ← (λr.r(r(z)))⟩[ ]. Here we treat it as a multistrategy stored outside, and the rule (2n)_{f} is used for fetching the value bound to u.

Below, we formalize our claim that the KAM can be viewed as an instance of the SAM. Let M = (λx⃗.W) be a term and N⃗ a vector of η-long and normal terms. Let ϕ = M^{nil} and ψ = [x_{1} ← N_{1}^{nil}, …, x_{n} ← N_{n}^{nil}] be their respective compilations. To each odd position q = •p in ϕ or q = x_{k}p in ψ, we associate a subterm M_{|p} of M or (N_{k})_{|p} of N_{k}:

(λy⃗.zP⃗)_{|ϵ} = (λy⃗.zP⃗) (λy⃗.zP⃗)_{|[a,↩^{κ}]kp} = (P_{k})_{|p}

If (λy⃗.zP⃗) is associated to q, we set vars(q) = y⃗, code(q) = zP⃗, and args(q) = P⃗. We can now define the translation from SAM states (at steps n′) to KAM states: ⌈(q[a, ↩^{κ}][e])⌉^{SK} = code(q)[⌈e⌉_{q}^{SK} ], where environments are translated as follows:

\overline{⌈nil⌉_{•}^{SK} = ⟨x⃗ ← N⃗⟩[ ]} ⌈nil⌉_{a}^{SK} = nil

\frac{q = q_{1}[a, ↩^{κ}]b r = q′[a′, ↩^{κ′}]}{⌈(r[e]^{•}e′)⌉_{q}^{SK} = ⟨vars(q) ← args(q′)⟩[⌈e⌉_{q′}^{SK} ]^{•}⌈e′⌉_{q_{1}}^{SK}}

Proposition 3.1 If r[e] is the state at step n′ of the SAM execution of (the compilation of) (λx⃗.W)N⃗, then ⌈r[e]⌉^{SK} is the state at step n′ of the KAM run started with W [⟨x⃗ ← N⃗⟩[ ]].

Thus each application of the unique rule of the KAM corresponds to a step n followed by a step n′ of the SAM.

4 Geometric machine (GAM)

In this section, we introduce a notation and a variation of the SAM which we call Geometric Abstract Machine, or GAM. In the GAM, execution consists in a travel in the strategy ϕ and the multistrategy ψ. Any step n or n′ of the SAM corresponds to an odd

\begin{matrix}2′ & •[u, ↩] & [ ] \\ 3′ & u[1, ↩^{0}] & (•[u, ↩])[ ] = e_{1} \\ 4′ & •[u, ↩]1[u, ↩] & (u[1, ↩^{0}])[e_{1}] = e_{2} \\ 5′ & u[1, ↩^{0}] & (•[u, ↩]1[u, ↩])[e_{2}] = e_{3} \\ 6′ & •[u, ↩]1[u, ↩]1[1, ↩^{1}] & (u[1, ↩^{0}])[e_{3}]^{•}e_{2} = e_{4} \\ 7′ & u[1, ↩^{0}]1[1, ↩^{1}] & (•[u, ↩]1[u, ↩]1[1, ↩^{1}])[e_{4}]^{•}e_{1} = e_{5} \\ 8′ & •[u, ↩]1[u, ↩] & (u[1, ↩^{0}]1[1, ↩^{1}])[e_{5}] = e_{6} \\ 9′ & u[1, ↩^{0}] & (•[u, ↩]1[u, ↩])[e_{6}] = e_{7} \\ 10′ & •[u, ↩]1[u, ↩]1[1, ↩^{1}] & (u[1, ↩^{0}])[e_{7}]^{•}e_{6} = e_{8} \\ 11′ & u[1, ↩^{0}]1[1, ↩^{1}]1[z, ↩] & (•[u, ↩]1[u, ↩]1[1, ↩^{1}])[e_{8}]^{•}e_{5} = e_{9} \end{matrix}

Figure 4: The execution of (u(λx.u(λy.x)))^{nil} ∘ [u ← (λr.r(r(z)))^{nil}] (SAM)

or even position of ϕ or ψ, respectively. The GAM execution tags opponent’s moves with step numbers, opening new copies when reaching a position that has already been visited. The GAM proceeds by constructing such tagged positions, which we call dynamic positions.

Formally, given the same alphabet of moves as in section 3, an even dynamic position is a sequence

R of the form ⟨a_{1}, j1⟩[a_{2}, ↩^{κ_{1}}] ⋯ ⟨a_{2n−1}, jn⟩[a_{2n}, ↩^{κ_{n}}],

where the a’s and the κ’s are as for positions, and where j_{1}, …, j_{n} ∈ ω are distinct natural numbers. A move ⟨a, j⟩ is called a dynamic opponent’s move, or a copy of opponent’s move. An odd dynamic position

Q = ⟨a_{1}, j1⟩[a_{2}, ↩^{κ_{1}}] ⋯ ⟨a_{2n−1}, jn⟩ is defined in the

same way. Any dynamic position P can be mapped to a position erase(P) obtained by erasing the tags. We write π_{l+1}(⟨a_{1}, j1⟩ ⋯ ⟨a_{2n−1}, jn⟩) = j_{n−l}. (for l ≤ n). In other words, π_{l+1}(P) is the (l + 1)-th tag of P (starting from the right).

A state of the GAM is a pair (Φ, Ψ), where Φ and Ψ are sets of dynamic positions. More precisely, each of the even positions of Φ has the form R = R_{1}⟨a, 2j − 1⟩[b, ↩^{κ}], and the function which maps R to 2j−1 is injective. We write R = Φ(2j′) and R_{1}⟨a, 2j − 1⟩ = Φ(2j − 1). The same property holds for Ψ (with even numbers), and we define Ψ(2j′ + 1) and Ψ(2j) similarly. Moreover, if ⟨a, j⟩ appears in a dynamic position r of Φ or Ψ, then all the opponent’s moves ⟨a′, j′⟩ occurring before ⟨a, j⟩ in r are such that j′ < j. Hence the successice tags determine a traversal of Φ ∪ Ψ. Moreover, a node cannot be visited before his descendants have been visited.

Figure 5 presents the rules of the GAM. At each step ν (ν = n or n′), the GAM extends a dynamic position of Φ ∪ Ψ with a player’s move or a dynamic opponent’s move, and adds the extended position P to Φ ∪ Ψ; P and ν are called the current position and the current step number, respectively.

(1)^{g} \overline{⟶ (\{⟨•, 1⟩\}, ∅)}

(2n′)^{g} \frac{Φ(2n − 1) = Q ϕ(erase(Q)) = [a, ↩^{κ}]}{(Φ, Ψ) ⟶ (Φ ⋃\{Q[a, ↩^{κ}]\}, Ψ)}

((2n + 1)′)^{g} \frac{Ψ(2n) = Q ψ(erase(Q)) = [a, ↩^{κ}]}{(Φ, Ψ) ⟶ (Φ, Ψ ⋃\{Q[a, ↩^{κ}]\})}

(2n)_{b}^{g} \frac{\begin{matrix}Φ(2n′) = Q[a, ↩^{i}] \\ π_{i+1}(Q) = 2m − 1 Ψ((2m − 1)′) = R′ \end{matrix}}{(Φ, Ψ) ⟶ (Φ, Ψ ⋃\{R′⟨a, 2n⟩\})}

(2n)_{f}^{g} \frac{Φ(2n′) = Q[a, ↩]}{(Φ, Ψ) ⟶ (Φ, Ψ ⋃\{⟨a, 2n⟩\})}

(2n + 1)^{g} \frac{\begin{matrix}Ψ((2n + 1)′) = Q[a, ↩^{i}] \\ π_{i+1}(Q) = 2m Φ(2m′) = R′ \end{matrix}}{(Φ, Ψ) ⟶ (Φ ⋃\{R′⟨a, 2n + 1⟩\}, Ψ)}

Figure 5: The Geometric Abstract Machine

The computation engine is concentrated in the rules (2n)_{b}^{g} or (2n + 1)^{g}. The “static” information

[a, ↩^{i}] is used to retrieve the tag 2m − 1 or 2m of

the copy of the opponent’s move to which [a, ↩^{i}] is bound. This index is paired with (or points to) the current position R′ of the machine at step (2m − 1)′ or 2m′, and R′, extended with a copy of a, becomes the current position. The two informations a and i in the move [a, ↩^{i}] give rise to two combined sorts of interaction, which we call tree interaction and pointer interaction, respectively. The information a allows to choose opponent’s move a: the determinism of ϕ at odd positions allows us to resolve the nondeterminism of ψ at even positions, and conversely. The information i allows us to determine which odd dynamic position the next opponent’s move should extend (in ψ or ϕ). The example given in section 3 illustrates pointer interaction only (the strategy and the multistrategy are each reduced to a single position). See section 5 for an example of tree interaction. Here is the final state of the execution of (u(λx.u(λy.x))[u ← (λr.r(r(z)))] on the GAM.

\begin{matrix}Φ & ⟨•, 1⟩^{(} [u, ↩] \{ \begin{matrix}⟨1, 3⟩^{(λx} [u, ↩] \{ ⟨1, 5⟩^{(λy}[1, ↩^{1}]^{x} \\ ⟨1, 7⟩^{(λx} [u, ↩] \{ ⟨1, 9⟩^{(λy}[1, ↩^{1}]^{x} \end{matrix} \\ Ψ & \{ \begin{matrix}⟨u, 2⟩^{(λr} [1, ↩^{0}] \{ ⟨1, 6⟩^{(} [1, ↩^{1}] \{ ⟨1, 10⟩^{(} [z, ↩] \\ ⟨u, 4⟩^{(λr} [1, ↩^{0}] \\ ⟨u, 8⟩^{(λr} [1, ↩^{0}] \end{matrix} \end{matrix}

Note the importance of the copying information contained in the tags: for example, the move 10′ (right after ⟨1, 9⟩) points to 7, not to 3, and this is precisely what gets us out of a loop.

The information contained in the tags allows to reconstruct the SAM environments. As an illustration, we show how to obtain the environment e_{8} of figure 4 starting from Φ(9) in the above example. The environment items of e_{8} are reconstructed using the pointer information contained in the non-initial dynamic opponent’s moves of Φ(9) = ⟨•, 1⟩[u, ↩ ]⟨1, 7⟩[u, ↩]. The first element is a closure r[e] where

r = erase(Ψ(9′)) = u[1, ↩^{0}] and where e = e_{7} is the environment reconstructed from Ψ(8). The second element is constructed similarly from Φ(7).

5 Pcf trees

In this section, we adapt the syntax of section 2 in order to cope with constants of base type and case statements, and we show how to encode this extension into abstract Böhm trees, without any need to extend the target language (except for the alphabet of moves). The syntax is given by:

\begin{matrix}M ::= (λx⃗.W) v ::= tt ff \underline{n} (n ∈ ω) \\ W ::= v case yM⃗ [v_{1} → (W_{1}), …, v_{k} → (W_{k})] \end{matrix}

The terms M are called finite Pcf Böhm trees, or simply Pcf trees, because they arise as the compact elements in a term model of the language Pcf [13, 2]. We compile Pcf trees much like λ normal forms. The alphabet isA = \{•\} ∪ ω ∪ Var ∪ \{\underline{n} | n ∈ ω\} ∪ \{tt, ff\}. We adopt the following tree representation for a Pcf term M:

\overbrace{M_{1} ⋯ M_{n} v_{1} → (W_{1}) ⋯ v_{k} → (W_{k})}^{λx⃗. case y}

We call M_{1}, …, M_{n} the argument branches, and v_{1} → (W_{1}), …, v_{k} → (W_{k}) the case branches. The node “λx⃗. case y” is split into the opponent’s move • followed by a player’s move \underline{y} as in section 3. An

occurrence of a basic constant v is compiled as [v, ↩^{i}], where i counts the number of case branches above it before the first argument branch is met. Finally, we replace the head opponent’s moves • in the translations ϕ_{i},ϕ′_{j} of M_{i},(W_{j}) by i,v_{j}, respectively:

\overbrace{[1 ← ϕ_{1}] ⋯ [n ← ϕ_{n}] [v_{1} ← ϕ′_{1}] ⋯ [v_{k} ← ϕ′_{k}]}^{•\underline{y}}

The formal translation is as follows:

(λx⃗.W)^{m;σ} = {•r | r ∈ W^{m;x⃗^{•}σ}}

v^{m;σ} = [v, ↩^{m}]

(case yM⃗ [v_{1} → (W_{1}) ⋯ v_{k} → (W_{k})])^{m;σ} =

\{ \begin{matrix}\{y^{σ}\} \\ ⋃_{i=1···n}\{y^{σ}ir | •r ∈ M_{i}^{0;σ}\} \\ ⋃_{j=1···k}\{y^{σ}v_{j}r | r ∈ (W_{j})^{(m+1);σ}\} \end{matrix}

where y^{σ} is as in section 3. The compilation of a term M is defined as M^{0;nil}. As an illustration, we compile the following example, and we exhibit the final state of its GAM execution:

(case f(tt) [ff ⇒ tt])[f ← (λx.case x [tt ⇒ ff, ff ⇒ tt])].

Strategy  Dynamic strategy
•^{(} [f, ↩]^{case} \{ \begin{matrix}1^{(} [tt, ↩^{0}] \\ ff[tt, ↩^{1}] \end{matrix}  ⟨•, 1⟩^{(}[f, ↩]^{case} \{ \begin{matrix}⟨1, 3⟩^{(} [tt, ↩^{0}] \\ ⟨ff, 5⟩[tt, ↩^{1}] \end{matrix}

Multistrategy  Dynamic multistrategy
f^{(λx} [1, ↩^{0}]^{case x} \{ \begin{matrix}tt[ff, ↩^{1}] \\ ff[tt, ↩^{1}] \end{matrix} ⟨f, 2⟩^{(λx} [1, ↩^{0}]^{case x} \{ ⟨tt, 4⟩[ff, ↩^{1}]

6 Executing arbitrary λ-terms

In this section, we successively remove the normal form restriction and the η-long restriction. We first describe how to compile an arbitrary η-long λ-term, and how to compute it. The basic idea, which is folklore, is to replace any redex (λx.M)N by a term (∗ N)[∗ ← (λx.M)], where ∗ is a special variable name. The alphabet is now {•, ∗} ∪ ω ∪ Var. To compile non-normal forms, we proceed in two phases, as in section 2. The first phase is unchanged. In the second phase, there are two cases. If M = (λx⃗.yM_{1} ⋯ M_{n}), then we proceed as in section 2. If M = (λx⃗.(λy.M_{0})M_{1} ⋯ M_{n}), let ϕ_{0}, ϕ_{1}, … ϕ_{n} be the translations of (λy.M_{0}), M_{1}, … M_{n}, respectively. Then M is translated to:

\overbrace{[1 ← ϕ_{1}] ⋯ [n ← ϕ_{n}] [∗ ← ϕ_{0}]}^{•[∗, ↩]}

How should we adjust the GAM or the SAM in order to execute a tree χ obtained as the target of this compilation? Here, there is no alternation between a strategy and a multistrategy. Instead, χ is a “strategy” in which the ∗’s signal (possibly nested) compositions of strategies. We therefore need to replace the rule (2n)_{f} by a new rule, which we shall call the ∗ rule. In the framework of the GAM, the ∗ rule can be described as follows: when the current position ends with [∗, ↩], the machine moves to (a copy) of the opponent’s move ∗ occurring immediately below. We illustrate this in figure 6.

We now address the second restriction. The basic idea is that the machine can cope with situations where a head variable has not enough arguments by making (or rather mimicking) an η-expansion dynamically, as the need arises. We illustrate this with (z(λxy.y)vw)[z ← (λu.u)] (we should actually write (z(λxy.y)vw)[z ← (λu.u), v ← v, w ← w], according to our conventions):

Strategy  Multistrategy

•^{(} [z, ↩] \{ \begin{matrix}1^{(λxy} & [2, ↩^{0}]^{y} \\ 2^{(} [v, ↩] \\ 2^{(} [w, ↩] \end{matrix}  •^{(λu} [1, ↩^{0}]^{u}

The SAM is blocked after step 4, because u has no argument, and a fortiori no second argument. If we had performed the η-expansion transforming (λu.u) into (λuu_{2}u_{3}.u(u_{2})(u_{3})), then we would have had no difficulty. The variables u_{2} and u_{3}, which we call expansion variables, are compiled to moves of the form [i, ↩^{1}]. We have i = 2 for u_{2} and i = 3 for u_{3}. We can let the machine think that u has a second argument by stating that if ψ(ra) is undefined (with r ∈ ψ),

then the run continues, and a move [i, ↩^{1}] (for an appropriate i) is played. Here is the full execution of the example.

\begin{matrix}(1)^{∗} & \overline{⟶ •[ ]} \\ (n′)^{∗} & \frac{χ(q) = [a, ↩^{κ}]^{m,n}}{q[e] ⟶ (q[a, ↩^{κ}]^{m,n})[e]} \\ (n′)_{η}^{∗} & \frac{q = q_{1}[a_{1}, ↩^{κ_{1}}]^{m_{1},n_{1}}a n_{1} < a}{q[e] ⟶ (q[a − n_{1} + m_{1}, ↩^{1}]^{0,0})[e]} \\ (n)_{b}^{∗} & \frac{r = q[a, ↩^{i}]^{m,n} and π_{i+1}(e) = r′[e′]}{r[e] ⟶ (r′a)[(r[e])^{•}e′]} \\ (n)_{∗}^{∗} & \frac{r = q[∗, ↩]^{m,n}}{r[e] ⟶ (r∗)[r[e]^{•}e]} \end{matrix}

Figure 7: The SAM^{∗}

\begin{matrix}(2′) & •[z, ↩] & [ ] \\ (2) & z & (•[z, ↩])[ ] = e_{1} \\ (3′) & z[1, ↩^{0}] & e_{1} \\ (3) & •[z, ↩]1 & (z[1, ↩^{0}])[e_{1}] = e_{2} \\ (4′) & •[z, ↩]1[2, ↩^{0}] & e_{2} \\ (4) & z[1, ↩^{0}]2 & (•[z, ↩]1[2, ↩^{0}])[e_{2}]^{•}e_{1} = e_{3} \end{matrix}

\begin{matrix}(5′) & z[1, ↩^{0}]2[3, ↩^{1}] & e_{3} \\ (5) & •[z, ↩]3 & (z[1, ↩^{0}]2[3, ↩^{1}])[e_{3}] = e_{4} \\ (6′) & •[z, ↩]3[w, ↩] & e_{4} \end{matrix}

In order to compute the appropriate i in general, we reformulate the compilation of λ-terms. We tag every player’s move corresponding to the head variable of a subterm (λx⃗.yM⃗) with a pair (m, n) of two natural numbers, which count the length of the two vectors x⃗ and M⃗. The modified compilation is as follows:

(λx_{1} ⋯ x_{m}.yM_{1} ⋯ M_{n})^{σ} =

{•(y^{x⃗^{•}σ})^{m,n}} ⋃_{i=1···n}{•(y^{x⃗^{•}σ})^{m,n}ir | •r ∈ (M_{i})^{x⃗^{•}σ}}

(λx_{1} ⋯ x_{m}.(λy.P)M_{1} ⋯ M_{n})^{σ} =

\{ \begin{matrix}\{•[∗, ↩]^{m,n}\} \\ ⋃\{•[∗, ↩]^{m,n} ∗ r | •r ∈ (λy.P)^{x⃗^{•}σ}\} \\ ⋃_{i=1···n}\{•[∗, ↩]^{m,n}ir | •r ∈ (M_{i})^{x⃗^{•}σ}\} \end{matrix}

Cumulating the two adjustments for non-normal forms and for non η-long terms (and hence for arbitrary untyped λ-terms), we arrive at an abstract machine which we call the SAM^{∗} (figure 7). The rule (n′)^{∗} is just an obvious reformulation of the rules ((2n + 2)′) and ((2n + 1)′) of the SAM. The rule (n′)_{η}^{∗} implements the dynamic η-expansions, and the last rule is the ∗ rule dealing with non-normal forms.

7 Back to the KAM

We can walk the reverse way from the game-theoretic machines to the KAM and express some of the implementation ideas developed in the earlier sections in

⟨•, 1⟩^{(} [∗, ↩] \{ \begin{matrix}⟨1, 6⟩^{(λz} & [1, ↩^{0}]^{z} \\ ⟨∗, 2⟩^{(λx} [∗, ↩] \{ \begin{matrix}⟨1, 5⟩^{(λy} & [1, ↩^{1}]^{x} & \{ ⟨1, 7⟩^{(}[1, ↩^{1}]^{y} \\ ⟨∗, 3⟩^{(λf} [∗, ↩] \{ \begin{matrix}1^{(λz} [u, ↩] \\ ⟨∗, 4⟩^{(λx} & [1, ↩^{1}]^{f} & \{ ⟨1, 8⟩^{(} [t, ↩] \end{matrix} \end{matrix} \end{matrix}

Figure 6: Final state of the execution of ((λx.(λf.(λx.f(t))(λz.u))(λy.x(y)))(λz.z))

(K)Pcf (case xM⃗ [v⃗ → V⃗])[e]

→ W [⟨z⃗ ← M⃗; v⃗ → V⃗ ⟩[e]^{•}e_{i}]

where \{ \begin{matrix}e = B_{0}^{•} ⋯^{•}B_{n} \\ B_{i} = ⟨x⃗_{i} ← N⃗_{i}; v⃗_{i} → V⃗_{i}⟩[e_{i}] \\ x = x_{ij} \\ N_{ij} = (λz⃗.W) \end{matrix}

(K)Pcf_{v} v[e] → V_{0j}[e_{0}]

where \{ \begin{matrix}e = B_{0}^{•}e′ \\ B_{0} = ⟨x⃗_{0} ← N⃗_{0}; v⃗_{0} → V⃗_{0}⟩[e_{0}] \\ v = v_{0j} \end{matrix}

Figure 8: The Stack-Free KAM for Pcf

the language of the λ-calculus or of Pcf trees. In this section, we present a Stack-Free KAM (or KAMPcf) for Pcf trees, and a full Stack-Free KAM (or KAM^{∗}) for the untyped λ-calculus.

We address Pcf trees first. We adopt a mild change of syntax with respect to section 5 (reflecting a small optimisation described below), and write case yM⃗ [v⃗ → W⃗] instead of case yM⃗ [v⃗ → (W⃗)]. We define a syntax of Pcf environments as follows:

e ::= nil B^{•}e B ::= ⟨x⃗ ← M⃗; v⃗ → V⃗ ⟩[e].

The rules of the KAMPcf are given in figure 8. There is no counterpart for the encoding of v as v^{i} given in section 5. This corresponds to an optimisation consisting in changing r ∈ (W_{j})^{(m+1);σ} into r ∈ W_{j}^{σ} in the compilation of section 5 and in removing the m’s altogether — this allows not to “cons” the empty closure in rule (K)Pcf_{v}.

We now adapt the encodings of section 6, using a syntax of terms rather than a syntax of positions. We

(K)^{∗}  ([j, ↩^{i}]M⃗)[e] → W [⟨M⃗⟩^{n}[e]^{•}e_{i}]

where  \{ \begin{matrix}e = B_{0}^{•} ⋯^{•}B_{n} \\ B_{i} = ⟨N⃗_{i}⟩^{n_{i}}[e_{i}] \\ j ≤ |N⃗_{i}| \\ N_{ij} = (λ^{n}.W) \end{matrix}

(K)_{η}^{∗} ([j, ↩^{i}]M⃗)[e] → [j − |N⃗_{i}| + n_{i0}, ↩^{1}][⟨M⃗⟩^{0}[e]^{•}e_{i}]

where  \{ \begin{matrix}e = B_{0}^{•} ⋯^{•}B_{n} \\ B_{i} = ⟨N⃗_{i}⟩^{n_{i}}[e_{i}] \\ j > |N⃗_{i}| \\ e_{i} = B_{i0}^{•} ⋯^{•}B_{in_{i}} \\ B_{i0} = ⟨M⃗_{i0}⟩^{n_{i0}}[e_{i0}] \end{matrix}

(K)_{∗}^{∗}  ((λ^{n}.W)M⃗)[e] → W [⟨M⃗⟩^{n}[e]^{•}e]

Figure 9: The full Stack-Free KAM

recall that in the notation of section 6, when we write m,n to decorate a head variable, m records the number of simultaneously abstracted λ’s, while n records the number of arguments. In a term-based syntax, the second information is visible, therefore we care only for the first information, which we now record on λ abstractions and then on environment components. This leads to the following syntax:

\begin{matrix}M ::= (λ^{n}.W) & e ::= nil B^{•}e \\ W ::= [j, ↩^{i}]M⃗ & B ::= ⟨M⃗⟩^{n}[e] \end{matrix}

Transposing the rules of the SAM^{∗}, we arrive at the KAM^{∗} (figure 9). In a binding ⟨N⃗⟩^{n}, n stands for the number of variables actually bound and is not necessarily the size of N⃗. When n < |N⃗|, the remaining N’s may be considered as an implicit stack. The converse situation happens in rule (K)_{η}^{∗}, where necessarily n_{i} > |N⃗_{i}|. In order to determine where a variable of rank j > |N⃗_{i}| is bound, we investigate ⟨M⃗_{i0}⟩^{n_{i0}}[e_{i0}]. If j − |N⃗_{i}| + n_{i0} > |M⃗_{i_{0}}|, then the exploration will continue in e_{i0}, and so on.

8 Computation as interaction

In this section, we relate the SAM to (an abstract versions of) Danos-Regnier’s Pointer Abstract Machine (PAM) where the environment is implicit [8], and to a machine called View Abstract Machine which formalises directly the notion of interaction between two persons playing moves (not positions) in turn (as in [4]). The two machines are derived from an analysis of the information redundancy in the SAM.

We observe that the environment component of the SAM states can be retrieved from the previous states of the execution: in rule (n)′, the environment e is just a copy of the environment component of the state at step n − 1; in rules (n)_{b} or (2n)_{f}, the environment becomes r[e]^{•}e′ or r[e]. Its head component r[e] is just a copy of the state of the machine at step n′; the tail component e′ is not directly accessible from the SAM state at step n′, since it comes from π_{i+1}(e) = r′[e′], but by construction of the environments along the execution, e′ was the environment component of the SAM state at some previous step. Thus, we can turn the SAM – a “history-free” machine, i.e. where any computation step depends on the previous state only – into a machine dealing only with positions, but history dependent.

In the PAM, the environments are implicit. The states of the PAM are • (at step 1), even positions (at steps n′), or tagged odd positions of the form ⟨q, m′⟩, called pointing positions (at steps n, n ≥ 2). There are no tags on positions of length 1. A history Γ is a sequence of states:

Γ ::= • Γa Γ(q[a, ↩^{κ}]) Γ⟨ra, m′⟩

We denote the successive elements of Γ by Γ^{•}1, Γ^{•}2′, Γ^{•}2, …, Γ^{•}ν (where ν = n or n′). If Γ^{•}n = ⟨q, m′⟩, we set jump_{Γ}(n) = m − 1. The rules of the PAM (figure 10) follow those of the SAM, forgetting the environment component of each SAM state, but recording the history. The main difference is in rule (n)_{b}^{p}: the pointer m′, which is precisely (jump_{Γ}(n) + 1)′, is recursively computed by using jump on smaller values.

We next define a compilation that maps a PAM history Γ to a SAM state ⌈Γ⌉^{PS} = p_{Γ^{•}ν}[e_{Γ}(ν)], where:

p_{•} = • p_{a} = a p_{q[a,↩^{κ}]} = q[a, ↩^{κ}] p_{⟨ra,m′⟩} = ra

(1)^{p}  \overline{⟶ •}
(2n′)^{p}  \frac{π(Γ^{•}(2n − 1)) = q ϕ(q) = [a, ↩^{κ}]}{Γ ⟶ Γ(q[a, ↩^{κ}])}
((2n + 1)′)^{p}  \frac{π(Γ^{•}2n) = q ψ(q) = [a, ↩^{κ}]}{Γ ⟶ Γ(q[a, ↩^{κ}])}

(n)_{b}^{p} \begin{matrix}Γ^{•}n′ = q[a, ↩^{i}] \\ jump_{Γ}^{i}(n − 1) = m Γ^{•}m′ = r′ \end{matrix}

Γ ⟶ Γ⟨r′a, m′⟩
(2n)_{f}^{p}  \frac{Γ^{•}2n′ = q[a, ↩]}{Γ ⟶ Γ a}

Figure 10: The Pointer Abstract Machine

e_{Γ}(n′) = e_{Γ}(n − 1) e_{Γ}(n) = (Γ^{•}n′)[e_{Γ}(n′)]^{•}e_{Γ}(jump_{Γ}(n))

Proposition 8.1 The SAM simulates the PAM: if Γ ⟶ Γ_{1}, then ⌈Γ⌉^{PS} ⟶ ⌈Γ_{1}⌉^{PS}.

Proof hint. We consider only rule (n)_{b}^{p}. We have

Γ^{•}n′ = q[a, ↩^{i}], jump_{Γ}^{i}(n − 1) = m, Γ^{•}m′ = r′, and Γ_{1} = Γ⟨r′a, m′⟩. The compilations of Γ and Γ_{1} are as

follows: ⌈Γ⌉^{PS} = (q[a, ↩^{i}])[e_{Γ}(n′)], and

⌈Γ_{1}⌉^{PS} = (r′a)[e_{Γ_{1}}(n)]
= (r′a)[(q[a, ↩^{i}])[e_{Γ_{1}}(n′)]^{•}e_{Γ_{1}}(jump_{Γ_{1}}(n))]
= (r′a)[⌈Γ⌉^{PS}^{•}e_{Γ_{1}}(jump_{Γ_{1}}(n))]
= (r′a)[⌈Γ⌉^{PS}^{•}e_{Γ}(m′)]

since by definition of jump_{Γ} we have

e_{Γ_{1}}(jump_{Γ_{1}}(n)) = e_{Γ_{1}}(m − 1) = e_{Γ_{1}}(m′) = e_{Γ}(m′)

To perform the SAM step n on ⌈Γ⌉^{PS}, we unfold the definition of e_{Γ}(n − 1):

π_{i+1}(e_{Γ}(n′)) = π_{i+1}(e_{Γ}(n − 1)) = (Γ^{•}jump_{Γ}^{i}(n − 1)′)[e_{Γ}(jump_{Γ}^{i}(n − 1)′)] = (Γ^{•}m′)[e_{Γ}(m′)]

hence ⌈Γ⌉^{PS} ⟶ ⌈Γ_{1}⌉^{PS}. □

Note that the complexity of the machine is the same for the SAM and for the PAM (jump^{i} and π_{i+1} are both in time proportional to i). However, the PAM handles a linear sequence of “positions”. This suggests to implement weak head reduction for Böhm trees by pushing pointing positions (in practice: physical pointers on terms) on a stack rather than by allocating environments in the heap as usual.

Next, we derive the VAM from an analysis of information redundancy in the PAM. Observing the rules of the PAM, we remark that the prefixes q at steps

(1)^{v}  \overline{⟶ •}
(2n′)^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{κ}]}{Γ ⟶ Γ[a, ↩^{κ}]}
((2n + 1)′)^{v}  \frac{ψ(view_{Γ}(2n)) = [a, ↩^{κ}]}{Γ ⟶ Γ[a, ↩^{κ}]}

(n)_{b}^{v}

Γ^{•}n′ = [a, ↩^{i}]

jump_{Γ}^{i}(n − 1) = m Γ ⟶ Γ⟨a, m′⟩

(2n)_{f}^{v}  \frac{Γ^{•}2n′ = [a, ↩]}{Γ ⟶ Γ a}

Figure 11: The View Abstract Machine

n′ and r′ at steps n can be retrieved from the positions in previous steps: in rule (n)_{b}^{p}, the information ⟨a, m′⟩ is enough, because r′ is known from the history at step m′; similarly, in rule (n′)^{p}, q is known from the history at step n − 1 and the information [a, ↩^{κ}] is enough. This leads to a simplified syntax of histories:

Γ ::= • Γa Γ[a, ↩^{κ}] Γ⟨a, m′⟩

But now, the information q in rule (n′)^{p} is no longer computable in one step. The move Γ^{•}(n − 1) only carries the last move of q = r′a. The rest r′ is the position implicit at step (n−1)′, which can be computed recursively via a function view defined as follows:

\overline{view_{Γ}(1) = •}  \frac{Γ^{•}(2n) = a}{view_{Γ}(2n) = a}

\frac{Γ^{•}n = ⟨a, m′⟩}{view_{Γ}(n) = view_{Γ}(m − 1) (Γ^{•}m′) a}

This leads to the machine described in figure 11. Finally, we define a compilation from VAM histories to PAM histories:

⌈•⌉^{VP} = • ⌈Γa⌉^{VP} = ⌈Γ⌉^{VP}a

⌈Γ[a, ↩^{κ}]⌉^{VP} = ⌈Γ⌉^{VP}((view_{Γ})[a, ↩^{κ}])

⌈Γ⟨a, m′⟩⌉^{VP} = ⌈Γ⌉^{VP}⟨(view_{Γ⟨a,m′⟩}), m′⟩

where view_{Γ^{•}1···Γ^{•}n} = view_{Γ}(n).

Proposition 8.2 The PAM simulates the VAM: if Γ ⟶ Γ_{1}, then ⌈Γ⌉^{VP} ⟶ ⌈Γ_{1}⌉^{VP}.

At each step, the VAM induces an additional computational cost proportional to the view’s length, hence the VAM is slower than the PAM and the SAM.

9 Conclusion

The SAM and the PAM are the analogues of machines that have been formulated in the framework of the λ-calculus, while the GAM and the VAM seem more specific of the language of games. Our framework allows us to express all these machines in a uniform notation and to relate them by mutual encodings, and hence enables us to transfer properties established in game semantics. For example, the VAM terminates [4, 6], hence the PAM, the GAM, and the stack-free machines SAM, KAM, and KAMPcf terminate. Types are not involved in the proof of termination. They only play a role in guaranteeing that the final states correspond to (an abstract form of) head normal forms, as shown in [6].

The SAM or the PAM are not merely paraphrasing abstract machines for the λ-calculus. They can serve to execute other kinds of code. Here we have dealt with Pcf trees. Other examples are λμ-calculus [11, 6] and cut elimination in Novikoff’s logic [4, 6].

References

[1] M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit substitutions, JFP 1(4), 375-416 (1991).

[2] S. Abramsky, R. Jagadeesan, and P. Malacaria, Full abstraction for Pcf, available by ftp at theory.doc.ic.ac.uk/papers (1995).

[3] A. Blass, Degrees of indeterminacy for games, Fundamenta Mathematicae 77, 151-166 (1972).

[4] T. Coquand, A semantics of evidence for classical arithmetic, J. of Symb. Logic 60, 325–337 (1995).

[5] P.-L. Curien, An abstract framework for environment machines, TCS 82, 389–402 (1991).

[6] P.-L. Curien, Abstract Böhm trees,to appear in Math. Structures in Computer Science.

[7] V. Danos, H. Herbelin, L. Regnier, Game semantics and abstract machines, in proceedings of LICS 96.

[8] V. Danos, L. Regnier, Machina ex deo, ou encore quelque chose à dire sur la machine de Krivine, unpublished (1990).

[9] W. Felscher, Dialogues as a foundation of intuitionistic logic, Handbook of Phil. Logic 3, 341-372 (1986).

[10] H. Herbelin, Séquents qu’on calcule, Thèse de Doctorat, Université Paris VII (1995).

[11] H. Herbelin, ***his paper on classical Böhm trees, in proceedings of TLCA97.

[12] G. Huet, An analysis of Böhm’s theorem, TCS 121, 145-167 (1993).

[13] M. Hyland, L. Ong, On full abstraction for Pcf, available by ftp at ftp.comlab.ox.ac.uk/pub/ Documents/techpapers/Luke.Ong, 1994.

[14] F. Lamarche, ***his paper on games and linear logic in proceedings of LICS 95??.

[15] D. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, TCS 121, 411-440 (1993).