Math. Struct. in Comp. Science (1993), vol. 11, pp. 1–000 Copyright \begin{matrix}c \\ ◯ \end{matrix} Cambridge University Press

Abstract Böhm Trees

Pierre-Louis Curien (CNRS-ENS)

Received 2 October 1997

We present a formalism of trees with pointers, called abstract Böhm trees, that provide a suitable abstract framework in which various cut-free proofs or normal terms of several λ-calculus based languages (including Pcf and Parigot’s λμ-calculus) can be faithfully encoded. A simple abstract machine called View Abstract Machine (VAM) allows us to compute over abstract Böhm trees. The VAM is closely related to Coquand’s interaction sequences and debates. The VAM execution over finite abstract Böhm trees always terminates. We next introduce an abstract notion of type that fits the purpose of guaranteeing that the VAM cannot go into deadlock, i.e., that it always reaches a satisfactory final state. Typed abstract Böhm trees can be turned into a category – more naturally a “multi-category” where the domains of arrows are sets of named objects, or records. We then go from the abstract to the concrete by giving examples. Our sets of abstract (typed) Böhm trees are relative to an alphabet and a set of types. By instantiating these two parameter sets appropriately, we recover successively: (η-long) typed Böhm trees, Pcf trees as considered in the game models of Hyland-Ong or of Abramsky-Jagadeesan-Malacaria, a notion of classical Böhm tree due to Herbelin that provides a classical version of Pcf trees in the style of λμ-calculus, and finally cut-free proofs in Novikov’s infinitary propositional logic as investigated by Coquand. In a companion paper, we investigate the operational aspects of (untyped) Böhm trees in more depth.

1. Introduction

The origin of this work lies in a convergence between two lines of research:

— one originating from Lorenz-Lorenzen’s game-theoretic interpretations of logical provability (Felscher 86; Coquand 95; Herbelin 95),

— the other from the more recent game models of Pcf (Hyland and Ong 94; Abramsky and Jagadeesan and Malacaria 95; Nickau 96), providing syntax-free accounts of an interesting infinite term model for Scott’s language Pcf (Milner 77; Plotkin 77).

It turns out that cut-free proofs of various sequent calculi on one hand, and Hyland and Ong’s innocent strategies on the other hand, can all be expressed as trees with pointers, just as λ-terms (or more precisely Böhm trees). In section 2, we develop a framework of abstract Böhm trees which can be instantiated to different calculi and languages, including those just mentioned. We introduce an abstract machine, called View Abstract Machine, or VAM, that performs computations over abstract Böhm trees. It is an adaptation to our general framework of Coquand’s debates (Coquand 95). Coquand has proved a “no infinite chatting” property which in our framework is a termination property: when executed on finite abstract Böhm trees, the VAM terminates. But the machine may stop without reaching a satisfactory final state. A typical example is provided by the execution of the (abstract Böhm tree version of) ΔΔ (where Δ = λx.xx).

In section 3, we define a notion of abstract type, and we show that correctly typed abstract Böhm trees are executed without deadlock, in other words that for such trees the VAM stops in a satisfactory final state that abstracts the λ-calculus notion of “having reached a head normal form”. We define a strong reduction machine, by which we mean, in the terminology of the λ-calculus, reduction to full normal form, as opposed to reduction to head normal form. In the terminology of games, we mean computing the composition of two strategies, as opposed to computing the first player’s move of the composition only.

In section 4, we illustrate the wide coverage of abstract Böhm trees. We treat successively Böhm trees, Pcf trees, classical Böhm trees, and proofs in Novikov’s infinitary propositional logic.

2. Untyped abstract Böhm trees

Throughout the paper, we suppose given a fixed set X whose elements are called abstract variable names. We want to define an abstract notion of tree with pointers, described as a set of branches, or positions.

Definition 2.1. (position) We suppose given an alphabet A, and a special symbol •. We assume that A, {•}, and X are disjoint. We define opponent’s moves, player’s moves and positions as follows:

— An initial opponent’s move is an element of {•} ∪ X (see definitions 2.2 and 2.3, respectively). An opponent’s move is an element of A ∪ {•} ∪ X. We let a range over A ∪ {•} ∪ X; if a ∈ A, then a is called a non-initial opponent’s move.

— A player’s move is either a pair [a, ↩^{i}] where a ∈ A and i ∈ ω (the set of natural numbers), or an element of X, written [x, ↩]. We let α range over A ∪ X and κ range over ω ∪ { }.

— An even position is a non-empty alternating sequence r of opponent’s moves and player’s moves, of the form:

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

where a_{1} ∈ {•} ∪ X and a_{2l−1} ∈ A for all l > 1 (whence the terminology of initial and non-inital opponent’s moves). If κ_{l} = , we say that [α_{2l}, ↩^{κ_{l}}] occurs free. For every l such that 1 ≤ l ≤ n and κ_{l} ≠ , we make the following assumption:

κ_{l} < l.  (1)

We say that [α_{2l}, ↩^{κ_{l}}] is bound to a_{2(l−κ_{l})−1}. An odd position q = a_{1}[a_{2}, ↩^{κ_{1}}] ⋯ a_{2n−1} is defined in the same way. We use p to denote an even position, and odd position, or a suffix of a position.

Thus, like in de Bruijn’s notation for λ-terms (Abadi and Cardelli and Curien and Lévy 91), pointers are represented by numbers which count the number of opponent’s moves between the pointing player’s move and the pointed opponent’s move.

Definition 2.1 presents the kit out of which actual data can be constructed, much like cliques can be constructed out of coherence spaces, configurations out of event structures, etc (Amadio and Curien 97). Here the datas are called strategies, or abstract Böhm trees.

Definition 2.2. (strategy) A strategy, or abstract Böhm tree, is a tree consisting of a non-empty set ϕ of even positions of the form •p satisfying the following properties:

(a) ϕ is closed under even non-empty prefixes, and

(b) q[α_{1}, ↩^{κ_{1}}], q[α_{2}, ↩^{κ_{2}}] ∈ ϕ implies [α_{1}, ↩^{κ_{1}}] = [α_{2}, ↩^{κ_{2}}].

Since ϕ is non-empty, it contains a unique position of the form •[α, ↩^{κ}], and [α, ↩^{κ}] is called the abstract head variable of ϕ. If we do not insist on having condition 2.1 (1), then we say that ϕ is a pseudo-strategy. A (pseudo-) strategy is called name-free if it contains no occurrence of a player’s move of the form [x, ↩].

Condition (b) says that, in a strategy, a “query”, (that is, a position of odd length), if answered, is uniquely so. Another way to put it is to say that ϕ is a tree of positions such that branching is only allowed under player’s moves. By condition (b), any strategy can be unambiguously presented as a partial function, also written ϕ, from odd positions to player’s moves [α, ↩^{κ}]. We also need the related notion of multi-strategy.

Definition 2.3. (multi-strategy) We define a renaming operation on strategies as follows:

[x ← ϕ] = {xr | •r ∈ ϕ}

where x ∈ X. A multi-strategy ψ is a union [x_{1} ← ϕ_{1}] ∪ ⋯ ∪ [x_{n} ← ϕ_{n}] of renamed strategies (with all the x_{i}’s distinct). We write ψ more suggestively as

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

We also write ϕ_{i} = ψ_{x_{i}}, for all i.

Remark 1. In the presentation of a strategy ϕ as a partial function q ↦ ϕ(q), the player’s moves of q are actually irrelevant. The same remark applies to multi-strategies. We call views sequences of opponent’s moves (starting with •, or with x). † Hence a strategy or a multi-strategy can be presented as a partial function from views to player’s moves. We shall use this presentation below in the definition of the View Abstract Machine.

In section 4 we shall see examples showing that abstract Böhm trees allow to represent terms or proofs of various concrete calculi. This suggests that abstract Böhm trees in general are computational objects. We next show how to compute with abstract Böhm trees, or how to compose them. In section 3, we shall present abstract typed Böhm trees as morphisms in a suitable (multi-) category. But just as the dynamics of λ-calculus is best understood in a type-free setting, our computation engine, called View Abstract Machine,

† This terminology will become clear later in this section (see in particular definition 2.5).

or VAM ‡, is best presented in an untyped setting. The VAM is the reformulation in our framework of Coquand’s debate machinery (Coquand 95).

The goal of a VAM execution is to compute the abstract head variable of a composition ϕ ∘ ψ of

— a strategy ϕ whose free player’s moves are [x_{1}, ↩], …, [x_{n}, ↩] with

— a multi-strategy ψ = [x_{1} ← ψ_{x_{1}}, …, x_{n} ← ψ_{x_{n}}]. (Think of a substitution M[x⃗ ← N⃗] in the λ-calculus.) The VAM execution consists in playing opponent’s moves in ϕ and ψ alternatively, keeping pointers that serve to reconstruct the positions in ϕ and ψ under which these moves actually take place. Formally, each machine step consists in rewriting such a sequence Γ of (pointing) moves, called a history, to a history which extends Γ by one move. Definition 2.4. (history) A pointing opponent’s move is a pair ⟨a, m⟩, where a ∈ A and m ≥ 1 is a natural number. Initial opponent’s moves do not carry pointers, but we call them pointing moves as well for uniformity. A non-terminated history is a sequence of pointing opponent’s moves. More precisely, non-terminated histories are defined by the following syntax:

Γ ::= • Γ x Γ ⟨a, m⟩ .

Terminated histories are sequences of the form Γ[x, ↩] or Γ[a, ↩^{0}], where Γ is a nonterminated history. In the sequel, we let Γ range over histories, i.e., over non-terminated and terminated histories. We denote the successive elements of a history Γ by Γ^{•}1, Γ^{•}2, …, Γ^{•}n. In a VAM execution, a terminated history corresponds to a final state of execution. The analysis of final states will be carried out in section 3 (see definition 3.5).

We next define two useful functions on histories. Definition 2.5. (jump,view) Let Γ be a non-terminated history. 1 We define a partial function jump_{Γ} from numbers to numbers by setting:

jump_{Γ}(n) = m − 1 iff Γ^{•}n = ⟨a, m⟩.

2 The related function view_{Γ} takes a number n as argument and returns a sequence of opponent’s moves:

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

We recall (cf. remark 1) that we have called sequences of opponent’s moves views, and that a strategy can be defined as a partial function from views to player’s moves. Definition 2.5 offers a dynamic account of views: the function view_{Γ} allows to reconstruct views in ϕ and ψ from a history. Consider ϕ and ψ as strategies for two players, call them

‡ In a companion paper (Curien and Herbelin 97), we present different variations of the VAM, including the Strategic Abstract Machine, or SAM, which is a stack-free and abstract version of Krivine’s abstract machine (Curien 91).

(1)^{v}  \overline{⟶ •}

(2n)_{b}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}] jump_{Γ}^{i}(2n − 1) = 2m − 1 > 1}{Γ ⟶ Γ⟨a, 2m − 1⟩}

(2n + 1)_{b}^{v}  \frac{ψ(view_{Γ}(2n)) = [a, ↩^{i}] jump_{Γ}^{i}(2n) = 2m}{Γ ⟶ Γ⟨a, 2m⟩}

(2n)_{f}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [x, ↩]}{Γ ⟶ Γ x}

(2n + 1)_{!}^{v}  \frac{ψ(view_{Γ}(2n)) = [x, ↩]}{Γ ⟶ Γ [x, ↩]}

(2n)_{!}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}] jump_{Γ}^{i}(2n − 1) = 1}{Γ ⟶ Γ[a, ↩^{0}]}

Fig. 1. The View Abstract Machine

Player and Opponent, respectively. Opponent plays opponent’s moves in ψ while Player plays opponent’s moves in ϕ. Each player in turn uses his view view_{Γ}(n) (where n is the length of the current history) to determine his next move, in a way which is explained below in detail. The notion of view was first defined in (Hyland and Ong 94). Hyland and Ong emphasise the idea of view by building it into the definition of strategy itself. In our words, they define strategies as functions from histories to player’s moves, that are neither history-free nor completely history-sensitive, by which is meant that Player (or Opponent) is allowed to use only part of the history – his view, whence the terminology – to determine his next move. We refer to (Hyland and Ong 94) for more intuition on the notion of view.

The rules of the VAM are given in figure 1. We consider it implicit that

— the execution is relative to a fixed pair of a strategy ϕ and of a multi-strategy ψ, and — there is a counter recording the current machine step number n. The succession of

the steps is: 1, 2, 3, 4, …, corresponding to alternating opponent’s moves in ϕ and ψ:

1 initial opponent’s move in ϕ
2 opponent’s move in ψ
3 opponent’s move in ϕ
⋯

Here is an informal explanation of the rules of the VAM. Rule (1)^{v} initiates the computation: the top move of ϕ may be considered as an initial query. Suppose that the machine has just performed 2n − 1 steps, for some n, the last step consisting of a move in ϕ. Then the next move will be played in ψ. The machine computes the view at step 2n − 1, and then reads the value [α, ↩^{κ}] of ϕ for this view. At this stage, we already know that α is the move played at step 2n. There are two cases: 1 If α = x (and thus κ = ), then the computation proceeds by playing the initial move

x of ψ. This can be considered as the communication of ϕ and ψ along the channel x. 2 If α = a and κ = i, the iteration of the function jump_{Γ} allows us to transform the

static information i into the dynamic information 2m − 1. There are again two cases.

(a) If 2m − 1 = 1, then a points to the initial move of the history, which constitutes an answer to the initial query, and terminates the execution.

(b) If 2m − 1 > 1, then the dialogue is not terminated: at step 2m − 2, a (pointing) move had been played in ψ, and the move a should be played in ψ right under that move: this is what the pointing information ⟨a, 2m − 1⟩ in the conclusion of rule (2n)_{b}^{v} is taking care of §.

Consider now the situation after an even number of steps. One similarly computes a view and the value [α, ↩^{κ}] of ψ for this view. We revisit the above cases as follows: 1 If α = x (and thus κ = ), then a “free variable” of ψ has been reached, and this

provides an answer to the initial query. 2 If α = a and κ = i, then the computation proceeds as in subcase 2(b) above. There is

no counterpart for the subcase 2(a), because if a is dynamically bound to the (copy of the) initial move x of ψ visited at step 2m, then the dialogue should be continued, because this step 2m had been performed in reaction to a step 2m − 1 played in ϕ.

Notice that the VAM stops after a step (n)_{!}^{v}: since we have not defined the view of a terminated history, there is no way to match the assumption of any rule labelled with n + 1 (see section 3 for a stronger framework where the machine can proceed further). Remark 2. The following two kinds of interaction, corresponding to the two parts a and i in the player’s move [a, ↩^{i}] present in the assumption of the rules (n)_{v}^{b}, respectively, are combined in the VAM.

— Tree interaction: the determinism of the strategy and of the multi-strategy allows to resolve the non-determinism of the choice of the next opponent’s move in the multi-strategy.

— Pointer interaction: the pointer structure allows us to determine the location of the nex move to play.

Hence the two interactions correspond to the respective questions: “which is the next move to play”, and “where is this move to be played”. They form the heart of the computational engine of the VAM.

§ The move a in ψ can be understood as “fetching the value of the bound variable” [a, ↩^{i}]. We refer to (Curien and Herbelin 97) for precise connections between the VAM and environment abstract machines.

Coquand has proved, in his terminology, that all debates between finite strategies terminate. In the present framework, his result implies that the VAM execution relative to finite ϕ and ψ terminates. For completeness, we include a proof of Coquand’s result (theorem 2.15), directly adapted from (a preliminary version of) (Coquand 95). The present proof is classical, while the proof published in (Coquand 95) is constructive. The proof is purely combinatorial, and uses only the pointer structure of the growing history (forgetting about the alphabet A) and the boundedness of views.

The following definition is taken from (Coquand 95), up to some change of notation. Definition 2.6. (interaction sequence) Let N be a natural number ≥ 2, or infinite. An interaction sequence over the interval [1, N] of ω is a pair (V, f) where

— f is a partial function from [1, N] to itself, and where

— V is a function from [1, N] to P (ω), satisfying:

V (n) = \{ \begin{matrix}\{n\} ∪ V (f(n) − 1) & if f(n) is defined \\ \{n\} & otherwise \end{matrix}

\{ \begin{matrix}f(1) is undefined \\ (f(n + 1) defined ⇒ f(n + 1) ∈ V (n)) . \end{matrix}

Lemma 2.7. If (V, f) is an interaction sequence, then, for all n: 1 (f(n) defined ⇒ f(n) < n), 2 V (n) ⊆ {1, …, n}. Proof. We write 1(n) to mean that property 1 holds for n, and similarly for 2. We prove successively:

— 2(1): This is obvious since V (1) = {1}.

— 2(n) ⇒ 1(n + 1): Since f(n + 1) ∈ V (n), we have f(n + 1) ∈ {1, …, n}, hence f(n + 1) < n + 1.

— 1(n) ⇒ 2(n): If V (n) = {n}, then a fortiori V (n) ⊆ {1, …, n}. If V (n) = {n} ∪ V (f(n)−1), then we conclude by induction since f(n) < n implies a fortiori f(n)−1 < n. □ In an interaction sequence (V, f), V is entirely determined by f, as the following lemma

shows. Lemma 2.8. Let V and f be of the types indicated in definition 2.6. Let g be defined by:

g(n) = \{ \begin{matrix}f(n) − 1 & if f(n) is defined \\ undefined & otherwise . \end{matrix}

Then (V, f) forms an interaction sequence if and only if, for all n ≥ 1:

V (n) = {g^{i}(n) | i ≥ 0 and g^{i}(n) defined}
(f(n + 1) defined ⇒ f(n + 1) = g^{i}(n) for some i ≥ 0) .

Proof. Let (V, f) be an interaction sequence. By lemma 2.7, we have g(n) < n for any n. Hence, given n, there exists an i such that g^{i}(n) is defined and g^{(i+1)} is not defined.

By unfolding we get

\begin{aligned}V (n) & = & \{n\} ∪ V (g(n)) & = & \{n, g(n)\} ∪ V (g^{2}(n)) & = & ⋯ \\ & = & \{n, g(n), …, g^{i−1}(n)\} ∪ V (g^{i}(n)) & = & \{n, g(n), …, g^{i}(n)\} & & . \end{aligned}

The converse direction is straightforward. □

Definition 2.9. (combinatorial view) Let Γ be a non-terminated history. We define two functions f_{Γ} and V_{Γ} as follows:

f_{Γ}(n) = m ⇔ Γ^{•}n = ⟨a, m⟩
\overline{V_{Γ}(1) = \{1\}}  \frac{Γ^{•}(2n) = x}{V_{Γ}(2n) = \{2n\}}  \frac{Γ^{•}n = ⟨a, m⟩}{V_{Γ}(n) = \{n\} ∪ V_{Γ}(m − 1)}

We call the V_{Γ}(n)’s the combinatorial views associated with Γ. (Clearly, for all n, the length of view_{Γ}(n) is the cardinal of V_{Γ}(n).)

Lemma 2.10. The pair (V_{Γ} , f_{Γ} ) of definition 2.9 forms an interaction sequence.

Proof. The two rules of the VAM adding a pointing move ⟨a, m⟩ to the history are (2n)_{v}^{b} and (2n + 1)_{v}^{b}. By considering the assumptions of these rules, we obtain, for all k ≥ 1 (even or odd):

f_{Γ}(k) = jump_{Γ}^{i}(k − 1) for some i ≥ 0.

Hence the condition of lemma 2.8 is satisfied. □

Coquand’s argument by contradiction consists in proving that if an execution does not terminate, then there must exist an infinitely growing (combinatorial) view.

Definition 2.11. We write m ≺ n if n < m and n − 1 ∈ V (m − 1).

By lemmas 2.8 and 2.7, an alternative definition of ≺ is:

m ≺ n ⇔ n − 1 ∈ g(V (m − 1)) ⇔ n ∈ f(V (m − 1)) .  (2)

Lemma 2.12. If f(f(n)) is defined, then n ≺ f(f(n)). Proof. We use the alternative definition (2) of ≺: we have f(n) ∈ V (n − 1), hence f(f(n)) ∈ f(V (n − 1)). □

For the next lemma, we adjust the definition of interaction sequence in order to be able to manipulate extracted interaction sequences. Replacing [1, N] by a sequence n_{1}, …, n_{k} such that n_{1} < n_{2} < ⋯ < n_{k}, we define now

g(n_{p}) = n_{q−1} if f(n_{p}) = n_{q}

V (n_{p}) = \{ \begin{matrix}\{n_{p}\} ∪ V (g(n_{p})) & if f(n_{p}) is defined \\ \{n_{p}\} & otherwise \end{matrix}

and the condition to satisfy is now

(f(n_{p+1}) defined ⇒ f(n_{p+1}) ∈ V (n_{p})).

If this condition is satisfied, we say that (V, f) is an interaction sequence on n_{1}, …, n_{k}. We define likewise an infinite interaction sequence on a sequence (n_{p})_{p≥0}. A sensible point here is that now V depends both on f and on (n_{p})_{p≥0}. We call V the combinatorial view function associated with f and (n_{p})_{p≥0}.

Definition 2.13. Suppose that (V, f) is an infinite interaction sequence on (n_{p})_{p≥0}, and let (n′_{p})_{p≥0} be an infinite subsequence of (n_{p})_{p≥0}. We say that (V, f) induces an interaction subsequence on (n′_{p})_{p≥0} if the following conditions hold: 1 (n′_{p})_{p≥0} is stable under f, i.e.,

∀ p (f(n′_{p}) defined ⇒ ∃ q (f(n′_{p}) = n′_{q})).

2 For all p, V′(n_{p}) ⊆ V (n_{p}), where V′ is the combinatorial view function associated

with f and (n′_{p})_{p≥0}. Remark 3. Condition 2 of definition 2.13 has the following consequence: if we have m ≺ n relatively to V′, then we also have m ≺ n relatively to V.

We can now state the key lemma. Lemma 2.14. Let (V, f) be an infinite interaction sequence on (n_{p})_{p≥0}. One of the following properties hold: 1 either for all q there exists r > q such that n_{q} = f(n_{r}), 2 or there exists a subsequence (n′_{p})_{p≥0} of the form

n_{1}, n_{2}, … n_{p−1}, m_{p}, m_{p+1}, …

such that m_{p} ≺ n_{p} and on which (V, f) induces an interaction subsequence. Proof. Suppose that property 1 does not hold, and let q be such that n_{q} ∉ f((n_{p})_{p≥0}). Let n_{p} = f(n_{q}) (the case where f(n_{q}) is undefined is treated similarly), and consider the sequence

(n′_{p})_{p≥0} = n_{1}, n_{2}, … n_{p−1}, n_{q+1}, n_{q+2}, ….

We first show n_{q+1} ≺ n_{p}, i.e., n_{p} ∈ f(V (n_{q})). This follows obviously from n_{p} = f(n_{q}) and n_{q} ∈ V (n_{q}). We next show that the subsequence (n′_{p})_{p≥0} is stable under f, i.e., that f(n_{r}) ∉ {n_{p}, n_{p+1}, …, n_{q}}, for all r > q. We call this property P (r) and prove it together with the following related property, for any r ≥ q, which we call Q(r):

V (n_{r}) ∩ {n_{p}, n_{p+1}, …, n_{q−1}} = ∅ .

We prove successively:

— Q(q): This is obvious by lemma 2.7 since V (n_{q}) = {n_{q}} ∪ V (n_{p−1}).

— Q(r − 1) ⇒ P (r): Since f(n_{r}) ∈ V (n_{r−1}), we have f(n_{r}) ∉ {n_{p}, n_{p+1}, …, n_{q−1}} by Q(r − 1). We also have f(n_{r}) ≠ n_{q} by assumption, hence P (r) holds.

— (P (r), Q(q), … Q(r − 1)) ⇒ Q(r) (r > q): We have V (n_{r}) = {n_{r}} ∪ V (n_{s−1}), where n_{s} = f(n_{r}). Clearly, n_{r} ∉ {n_{p}, n_{p+1}, …, n_{q−1}}. We know by P (r) that n_{s} ∉ {n_{p}, n_{p+1}, …, n_{q}}. There are two cases: if s < p, then a fortiori s − 1 < p, which ensures V (n_{s−1}) ∩ {n_{p}, n_{p+1}, …, n_{q−1}} = ∅; if s > q, then s − 1 ≥ q, hence we can conclude using Q(s − 1).

Finally, we have to check condition 2 of definition 2.13. Let g′ be the function defined by g′(n′_{p}) = n′_{q−1} if f(n′_{p}) = n′_{q}. The only possibilty to have g′(n_{r}) ≠ g(n_{r}) is that f(n_{r}) = n_{q+1}. Then g(n_{r}) = n_{q} while g′(n_{r}) = n_{p−1} = g(n_{p}) = g(g(n_{r})). Condition 2 then follows from lemma 2.8. □

Theorem 2.15. Let (V, f) be an infinite interaction sequence. The following properties hold:

1 The relation ≺ is not well-founded. 2 The set {♯(V (n)) | n ≥ 1} (where ♯(V (n)) denotes the cardinal of V (n)) has no upper

bound.

Proof. Suppose that ≺ is well-founded. We can construct a sequence (m_{p})_{p≥0} as follows. For each p, we choose m_{p+1} ≺-minimal among the set of all m’s for which f induces an interaction on an infinite subsequence starting with m_{1}, m_{2} …, m_{p}, m. (This set is maintained non-empty by the induction.) By construction and by lemma 2.14, we can extract from (m_{p})_{p≥0} an infinite sequence (n_{p})_{p≥0} such that n_{p} = f(n_{p+1}) for all p. This implies n_{2p} = f(f(n_{2(p+1)})), hence n_{2(p+1)} ≺ n_{2p} by lemma 2.12, and contradicts the wellfoundedness assumption. Notice the implicit use of remark 3 in the above argument: as the construction proceeds, successive subsequences are extracted, and the ≺-minimality is meant relative to each of the successive subsequences; condition 2 of definition 2.13 allows us to inherit the well-foundedness of ≺ along the construction.

We next prove that views are unbounded. Since ≺ is not well-founded, there exists a subsequence (l_{n})_{n≥0} such that l_{n+1} ≺ l_{n}, for all n. If we set k_{n} = l_{n} − 1, this rephrases as (k_{n} < k_{n+1} and k_{n} ∈ V (k_{n+1})). In particular, all the k_{n}’s are distinct. We observe, as an immediate consequence of the characterisation of V given in lemma 2.8, that, say,

(k_{n−1} ∈ V (k_{n}) and k_{n} ∈ V (k_{n+1})) ⇒ k_{n−1} ∈ V (k_{n+1}).

It follows that {k_{1}, …, k_{n}} ⊆ V (k_{n+1}), and the conclusion follows. □

Proposition 2.16. If ϕ and ψ are a finite strategy and a finite multi-strategy, respectively, then the VAM execution relative to ϕ and ψ terminates.

Proof. Suppose that the VAM does not terminate, and let Δ be the infinite history whose finite prefixes are the histories Γ such that ⟶^{⋆} Γ. Let (V_{Δ}, f_{Δ}) be the associated infinite interaction sequence (cf. lemma 2.10). We observe that

— the combinatorial views have an unbounded length, by theorem 2.15, while

— the views have a bounded length, being in the domain of definition of ϕ or ψ.

This yields a contradiction, since the lengths of the views are the cardinals of their underlying combinatorial views. □

In order to illustrate the VAM, we anticipate subsection 4.1 and describe a compilation of (untyped) λ normal forms, or finite Böhm trees, as defined by the following syntax:

M ::= λx⃗.W W ::= yM_{1} ⋯ M_{n} (n ≥ 0) .

(λx⃗.yM_{1} ⋯ M_{n})^{L} = {•y^{L,x⃗}} ⋃_{i=1···n}{•y^{L,x⃗}ir | •r ∈ (M_{i})^{L,x⃗}}

where

\overline{x^{nil} = [x, ↩]}  \frac{x = x_{i} x⃗ = x_{1} ⋯ x_{k}}{x^{L,x⃗} = [i, ↩^{0}]}  \frac{x^{L} = [i, ↩^{j}]}{x^{L,y⃗} = [i, ↩^{j+1}]}  \frac{x^{L} = [x, ↩]}{x^{L,y⃗} = [x, ↩]}

Fig. 2. Compilation of untyped λ normal forms

We take as alphabet A = ω. We perform the following transformation on the tree representation of a normal form M:

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

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}. 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 (Huet 93). Finally, if ϕ_{i} is the translation of M_{i}, for all i, then the head opponent’s move • of ϕ_{i} is replaced by i. In this way, we record that M_{i} is the i-th argument of y. To summarise, the translation of M = (λx⃗.yM_{1} ⋯ M_{n}) is the following tree:

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

Formally, we define in figure 2 a translation function involving a function which takes a list L of vectors of variables and a term M, and returns a strategy M^{L}. The compilation of a term M is defined as M^{nil}. We shall adapt this compilation to a typed setting in section 3, and shall show that it defines a bijective transformation to a suitable set of typed strategies.

Example 2.17. We display the computation of (u(λx.u(λy.x)))^{nil} ∘[u ← (λr.r(r(z)))^{nil}]. 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}

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

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

The execution of this example by the VAM is as follows (the step numbers are placed below the successive moves, as a help to the reader) :

\begin{matrix}• & u & ⟨1, 2⟩ & u & ⟨1, 4⟩ & ⟨1, 3⟩ & ⟨1, 2⟩ & u & ⟨1, 8⟩ & ⟨1, 7⟩ & [z, ↩] \\ 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 11 \end{matrix}

The successive views are as follows:

view_{Γ}(1) = •  view_{Γ}(2) = u view_{Γ}(3) = •1
view_{Γ}(4) = u  view_{Γ}(5) = •11 view_{Γ}(6) = u1
view_{Γ}(7) = •1  view_{Γ}(8) = u view_{Γ}(9) = •11
view_{Γ}(10) = u11

3. Typed abstract Böhm trees

We introduce a set of abstract types and revisit the definitions of section 2, imposing type constraints. Definition 3.1. (typed position) In addition to the alphabet A, we suppose given a set T of abstract types, or types for short, together with a partial function ( ) from T × A to T, written (σ, a) ↦ σ_{a}. A typed position is a position all of whose moves are decorated with a type superscript as follows:

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

We say that a_{1}[α_{2}, ↩^{κ_{1}}] ⋯ a_{2n−1}[α_{2n}, ↩^{κ_{n}}] is the underlying (untyped) position. Definition 3.2. (typed strategy) A typed strategy, or typed abstract Böhm tree, is a set ϕ of typed positions whose underlying set of positions forms a strategy, and satisfying the following two properties:

(1) If q[α, ↩^{κ}]^{σ} ∈ ϕ, then, for any τ ∈ T and b ∈ A:

(q[α, ↩^{κ}]^{σ}b^{τ} is answered in ϕ) ⇔ (σ_{b} is defined and σ_{b} = τ).

(2) If q[a, ↩^{i}]^{σ} ∈ ϕ, and if [a, ↩^{i}] is bound to b^{τ} in q, then σ = τ_{a}. Moreover, we require that all occurrences of a free player’s move [x, ↩] bear the same type. The type decorating • is called the type of ϕ.

In order to spare on notations, we shall freely omit the type decorations on moves when they are not relevant to the discussion. But the reader should keep in mind that they are implicitly carried through the constructions in the obvious way.

We now give a typed version of pseudo-strategies, relative to a list Σ of types.

Definition 3.3. Let ϕ be a set of typed positions whose underlying set of positions forms a pseudo-strategy, and let Σ be a list of types. Let r = q[a, ↩^{i}]^{σ} ∈ ϕ of length 2l such that [a, ↩^{i}] is not bound in ϕ. We write r^{Σ} for the (i − l + 1)-th type in the sequence Σ. We therefore assume that Σ has length at least i − l + 1 for all r = q[a, ↩^{i}]^{σ} ∈ ϕ such that [a, ↩^{i}] violates condition 2.1 (1). We call ϕ a typed pseudo-strategy relative to Σ if it satisfies the conditions listed in definition 3.2 plus the following one:

(3) If r = q[a, ↩^{i}]^{σ} ∈ ϕ, and if [a, ↩^{i}] is not bound in ϕ, then σ = (r^{Σ})_{a}. As for strategies, the type decorating • is called the type of ϕ.

In order to establish precise correspondences between concrete syntaxes of terms or proofs and abstract Böhm trees relative to appropriate A, T, and ( ), we shall rely on the following simple decomposition property for typed pseudo-strategies. Lemma 3.4. Let ϕ and Σ be such that ϕ is a typed pseudo-strategy relative to Σ. We can uniquely write:

ϕ = {•^{τ} [α, ↩^{κ}]^{σ}} ⋃ ( ⋃_{{a|σ_{a} is defined}}{•[α, ↩^{κ}]ap | •p ∈ ϕ_{a}}).

Moreover, all ϕ_{a}’s are pseudo-strategies relative to Σ, τ. We use the following synthetic notation for the decomposition:

ϕ ⇝ •^{τ} [α, ↩^{κ}]^{σ}, {ϕ_{a} | σ_{a} is defined}.

or, if {a | σ_{a} is defined} = {a_{1}, …, a_{n}}:

ϕ ⇝ •^{τ} [α, ↩^{κ}]^{σ}, ϕ_{a_{1}}, …, ϕ_{a_{n}}.

Proof. The underlying untyped positions of ϕ_{a} inherit the closure properties of the corresponding underlying untyped positions of ϕ, hence form a pseudo-strategy. Condition (1), which is entirely local, is also clearly inherited from condition (1) for ϕ. For conditions (2) and (3), there are three cases. Let r = •q[b, ↩^{i}]^{σ} ∈ ϕ_{a}.

— If [b, ↩^{i}] is bound in r, then it is a fortiori bound in •[α, ↩^{κ}]aq[b, ↩^{i}], and condition (2) follows from condition (2) for ϕ.

— By contraposing this implication, if [b, ↩^{i}] is not bound in •[α, ↩^{κ}]aq[b, ↩^{i}], then condition (3) follows from condition (3) for ϕ.

— If [b, ↩^{i}] is bound in •^{τ} [α, ↩^{κ}]aq[b, ↩^{i}] but not in r, then it is bound to •^{τ} in ϕ, so that condition (3) relative to Σ, τ follows from condition (2) for ϕ. □ We now show that typed strategies and pseudo-strategies are deadlock-free. We first

define the legal final states of the VAM. Definition 3.5. (legal final state) We say that the VAM is in a final (F) state when it has reached a step (2n + 1)_{!}^{v}, and that it is in a final (B) state when it has reached a step (2n)_{!}^{v}. (F and B stand for “free” and “bound”, respectively.) A state is called legal if it is either (F) final or (B) final.

At an (F) final state, the computation terminates because a free variable of ψ has been met. This is what happens in example 2.17. We can interpret this as a demand to

(1)^{v}  \frac{ϕ has type σ}{⟶ •^{σ}}

(2n)_{b}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}]^{σ} jump_{Γ}^{i}(2n − 1) = 2m − 1 > 1}{Γ ⟶ Γ⟨a, 2m − 1⟩^{σ}}

(2n + 1)_{b}^{v}  \frac{ψ(view_{Γ}(2n)) = [a, ↩^{i}]^{σ} jump_{Γ}^{i}(2n) = 2m}{Γ ⟶ Γ⟨a, 2m⟩^{σ}}

(2n)_{f}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [x, ↩]^{σ}}{Γ ⟶ Γ x^{σ}}

(2n + 1)_{!}^{v}  \frac{ψ(view_{Γ}(2n)) = [x, ↩]^{σ}}{Γ ⟶ Γ [x, ↩]^{σ}}

(2n)_{!}^{v}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}]^{σ} jump_{Γ}^{i}(2n − 1) = 1}{Γ ⟶ Γ[a, ↩^{0}]^{σ}}

Fig. 3. The typed VAM

the input multi-strategy. A simple example of (B) final state is obtained by composing •[1, ↩^{0}] (corresponding to (λx.x)) with an arbitrary multi-strategy: the execution results in the terminated history •[1, ↩^{0}]. See section 4.2 for another flavour of (B) final state.

In both cases (F) and (B), the machine stops because a “head normal form” has been reached. More precisely, for λ normal forms, the two cases of termination correspond to the following partition of head normal forms:

(λx⃗.yM⃗) (y free)  (F)
(λx⃗.xM⃗) (x bound) (B) .

In figure 3, we present a typed version of the VAM. The rules are those of the VAM, and in addition the type decorations indicated by ϕ and ψ are faithfully recorded. The typed VAM executes the composition of

— a strategy ϕ whose free player’s moves are [x_{1}, ↩]^{σ_{1}}, …, [x_{n}, ↩]^{σ_{n}} with

— a multi-strategy ψ = [x_{1} ← ψ_{x_{1}}, …, x_{n} ← ψ_{x_{n}}] whose initial moves x_{i} are decorated with the respective types σ_{i}. In other words, x_{i} and ψ_{x_{i}} (bound to x_{i}) must have the same type.

Proposition 3.6. The execution of a typed strategy composed with a typed multistrategy by the typed VAM can only terminate in a legal final state. Proof. The proposition is proved by induction on the length of the execution. Let Γ be a non-terminated history resulting of the n first steps of execution. We have to show that nothing prevents the next step to be executed. We claim that χ(view_{Γ}(n)) is defined, where χ is ϕ or ψ depending on the parity of n. We first show how to conclude from the claim. The statement follows immediately from the claim for rules (2n)_{f}^{v} and (2n + 1)_{!}^{v}.

For all the other rules, we have to show that if χ(view_{Γ}(n)) = [a, ↩^{i}], then jump_{Γ}^{i}(n) is defined. By condition 2.1 (1), view_{Γ} is long enough to have a suffix a_{i} ⋯ a_{0}. Unfolding the recursive definition of view_{Γ}, we have:

view_{Γ}(n) = view_{Γ}(jump_{Γ}(n))a_{0} = view_{Γ}(jump_{Γ}^{i}(n))a_{i−1} ⋯ a_{0} .  (3)

Hence jump_{Γ}^{i}(n) is defined, and the next step can be performed.

We are left with the proof of the claim. If Γ^{•}n = •, then the claim follows from the non-emptyness of ϕ. If Γ^{•}n = x, the claim follows similarly from the non-emptyness of ψ. If Γ^{•}n = ⟨a, m⟩, then the last rule applied is (n)_{b}^{v}. Suppose, say, that n is even. Reading the assumptions, and using (3) above as well as condition (2) of definition 3.2, we get that m = jump_{Γ}^{i}(n) for some i and that σ = τ_{a}. where τ is the type decoration of Γ^{•}m. By the definition of the typed VAM, τ is also the type decoration of ψ(view_{Γ}(m − 1)). Since view_{Γ}(n) = view_{Γ}(m − 1) a, we conclude using condition (1) of definition 3.2. □

In order to appreciate the previous proposition, we should see how it fails for non typable strategies. We show how the VAM executes ΔΔ = (λx.xx)(λx.xx), or in compiled form:

{•[x, ↩], •[x, ↩]1[x, ↩]}[x ← {x[1, ↩^{0}], x[1, ↩^{0}]1[1, ↩^{1}]}].

The execution by the VAM results in the following history:

\begin{matrix}• & x & ⟨1, 2⟩ & x & ⟨1, 4⟩ \\ 1 & 2 & 3 & 4 & 5 \end{matrix}

with the following associated views:

view_{Γ}(1) = • view_{Γ}(2) = x view_{Γ}(3) = •1 view_{Γ}(4) = x view_{Γ}(5) = •11 .

The VAM stops after step (5)_{b}^{v} without having reached a legal final state. Remark 4. The VAM could have computed a bit further if the strategy had been “ηexpanded”: the compilation of λx.x(λy.xy) answers the view •11 with the compilation of y. In the companion paper (Curien and Herbelin 97), we show how the VAM can be adapted to mimick η-expansions dynamically, yielding a non terminating computation (involving unbounded views, cf. proposition 2.16).

We now formulate a strong version of the VAM, called Strong VAM, which can compute full normal forms. The machine works on demand. Given a strategy ϕ and a multi-strategy ψ, it builds any position of the composition ϕ∘ψ, provided it is asked by an external agent, called the user, to progressively do so. We signal the user’s demands and the answers to the user by underlining. The user raises an initial query, call it \underline{•} in first approximation. The VAM is started, and runs until it reaches a legal final state that produces a player’s move \underline{[α, ↩^{κ}]} answering the initial query. We then know that •[α, ↩^{κ}] ∈ ϕ ∘ ψ, The user may raise a new query •[α, ↩^{κ}]b. A new run of the VAM is started, until a new “final” state is reached. If the final player’s move is bound, should we bind it to • or to b? To keep a proper scoping, we use a mechanism of names. This leads to the following notion of strong history and the following extension of the function view. We do not include type decorations to avoid overloading of notation.

Definition 3.7. (strong history) The syntax of strong histories is as follows:

Γ ::= \underline{•_{ν}} Γ\underline{a_{ν}} Γx Γ⟨a, m⟩ Γ\underline{[a, ↩^{ν}]} Γ\underline{[x, ↩]}

where ν ranges over an infinite set N of names. The underlined moves correspond to the progressive formation of the positions of the composition (see definition 3.9 and proposition 3.11).

Definition 3.8. (strong view) The strong views associated with a strong history are defined by the rules of definition 2.5 plus the following one:

\frac{Γ^{•}n = \underline{a_{ν}}}{view_{Γ}(n) = view_{Γ}(n − 2) a}

The rules of the Strong VAM are displayed in figure 4. The rules are

— those of the VAM (up to some change of notation), plus

— two new rules that formalise the user’s new demands.

The execution proceeds by progressively extending a strong history, which is flagged with a sign ? or !, where

? indicates that the machine is engaged in an internal dialogue whose goal is to answer

a user’s query, ! indicates that the last user’s query has just been answered.

Hence the flag ! stays exactly during one step.

Remark 5. While the VAM is deterministic, the transition relation of the Strong VAM is non-deterministic: at steps n_{?}^{s}, the choice of the move a is free, as long as the extended view is in the domain of ϕ or ψ. If the user knows which view he wants to explore, then the evaluation is deterministic with respect to that goal. We say that the execution is guided by the user.

Finally, we need to read back the positions of the composition, i.e. to strip off the moves that correspond to the internal dialogue of the machine. This is formalised in the following definition, which also takes care of installing the nameless notation for bindings.

Definition 3.9. (readback) The following function readback takes as argument a suffix of a strong history and an auxiliary list L of names, and returns a position.

Abstract Böhm Trees 17

(1)_{?}^{s}  \frac{ν new}{⟶ (\underline{•_{ν}} ?)}

(2n)_{b}^{s}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}] jump_{Γ}^{i}(2n − 1) = 2m − 1 Γ^{•}(2m − 1) ≠ \underline{b_{ν}}}{(Γ ?) ⟶ (Γ⟨a, 2m − 1⟩ ?)}

(2n + 1)_{b}^{s}  \frac{ψ(view_{Γ}(2n)) = [a, ↩^{i}] jump_{Γ}^{i}(2n) = 2m Γ^{•}2m ≠ \underline{b_{ν}}}{(Γ ?) ⟶ (Γ⟨a, 2m⟩ ?)}

(2n)_{f}^{s}  \frac{ϕ(view_{Γ}(2n − 1)) = [x, ↩]}{(Γ ?) ⟶ (Γx ?)}

(2n)_{!}^{s}  \frac{ϕ(view_{Γ}(2n − 1)) = [a, ↩^{i}] jump_{Γ}^{i}(2n − 1) = 2m − 1 Γ^{•}(2m − 1) = \underline{b_{ν}}}{(Γ ?) ⟶ (Γ\underline{[a, ↩^{ν}]} !)}

(2n + 1)_{!}^{s}  \frac{ψ(view_{Γ}(2n)) = [a, ↩^{i}] jump_{Γ}^{i}(2n) = 2m Γ^{•}2m = \underline{b_{ν}}}{(Γ ?) ⟶ (Γ\underline{[a, ↩^{ν}]} !)}

(2n)_{?}^{s}  \frac{ψ(view_{Γ}(2n − 1)a) defined ν new}{(Γ !) ⟶ (Γ\underline{a_{ν}} ?)}

(2n + 1)_{?}^{s}  \frac{ϕ(view_{Γ}(2n)a) defined ν new}{(Γ !) ⟶ (Γ\underline{a_{ν}} ?)}

Fig. 4. The Strong VAM

readback^{nil}(\underline{•_{ν}}Γ)  = • readback^{ν}(Γ)
readback^{L}(\underline{a_{ν}}Γ)  = a readback^{ν^{•}L}(Γ)
readback^{L}(xΓ)  = readback^{L}(Γ)
readback^{L}(⟨a, m⟩Γ)) = readback^{L}(Γ)
readback^{L}(\underline{[a, ↩^{ν}]}Γ) = [a, ↩^{ν_{L}}] readback^{L}(Γ)
readback^{L}(\underline{[x, ↩]}Γ) = [x, ↩] readback^{L}(Γ)

where

ν_{μ^{•}L} = \{ \begin{matrix}0 & if μ = ν \\ ν_{L} + 1 & if μ ≠ ν \end{matrix}

For a strong history we set readback(Γ) = readback^{nil}(Γ).

We now have all the material to define a “category” of typed abstract Böhm trees. We first define a notion of named multi-category that is well adapted to our purposes.

Definition 3.10. (named multi-category) A named multi-category consists of a collection of objects and a collection of morphisms; each morphism f has a target object B, and has a source consisting of a context of objects, i.e. a list Γ = x_{1} : A_{1}, …, x_{n} : A_{n} of named objects, with x_{1}, …, x_{n} all distinct. One writes f : Γ → B. For each context Γ = x_{1} : A_{1}, …, x_{n} : A_{n} and each i ≤ n, there exists a projection arrow π_{i} from Γ to A_{i}. Moreover there exists a composition operation: If Γ = x_{1} : A_{1}, …, x_{n} : A_{n} and Δ are contexts, if g_{1} : Δ → A_{1}, …, g_{n} : Δ → A_{n}, f : Γ → B are morphisms, then there is a composition written f ∘ [x_{1} ← g_{1}, …, x_{n} ← g_{n}] from Δ to B. The usual monoid laws are required:

(f ∘ [x_{1} ← g_{1}, …, x_{n} ← g_{n}]) ∘ [y⃗ ← h⃗] = f ∘ [x_{1} ← g_{1} ∘ [y⃗ ← h⃗], …, x_{n} ← g_{n} ∘ [y⃗ ← h⃗]] f ∘ [x_{1} ← π_{1}, …, x_{n} ← π_{n}] = f π_{i} ∘ [x_{1} ← g_{1}, …, x_{n} ← g_{n}] = g_{i}

Proposition 3.11. Let A, T, and be fixed. Typed abstract Böhm trees form a named multi-category. The objects are the elements of T, and a morphism from Γ to σ is a typed abstract Böhm tree ϕ such that all the occurrences of moves of the form [x, ↩]^{σ} in ϕ are such that x : σ is in Γ. The projection morphisms are π_{i} = •[x_{i}, ↩] and the composition is given by:

ϕ ∘ ψ = {readback(Γ) | ⟶^{⋆} (Γ !)}.

The right hand side of this definition does not mention ϕ, ψ explicitly, but one should keep in mind that the transition relation ⟶ is parametrised by ϕ and ψ.

Proof. We first check that ϕ ∘ ψ is a strategy. It is non-empty by proposition 2.16 and by proposition 3. If readback(Γ) ∈ ϕ ∘ ψ, then for each even prefix r of readback(Γ), there exists a prefix Δ of Γ such that

⟶^{⋆} (Δ !) ⟶^{⋆} (Γ !).

Hence ϕ ∘ ψ is closed under prefixes. The last condition (no branching at opponent’s moves) follows from the observations made in remark 5. The proof of associativity is tedious, but conceptually easy. Both sides (ϕ ∘ [x_{1} ← ψ_{x_{1}}, …, x_{n} ← ψ_{x_{n}}]) ∘ χ and ϕ ∘ [x_{1} ← ψ_{x_{1}} ∘ χ, …, x_{n} ← ψ_{x_{n}} ∘ χ] of the associativity equation are equal to the result of the three-ary composition ϕ ∘ [x_{1} ← ψ_{x_{1}}, …, x_{n} ← ψ_{x_{n}}] ∘ χ which can be computed by a strong VAM parametrised by ϕ, ψ, and χ. □

4. Some examples of abstract Böhm trees

4.1. η-long Böhm trees

We revisit the translation of finite Böhm trees given in section 2 in a typed setting. We restrict our attention to η-long normal forms, as defined by the following typing system. We suppose given a collection of basic types C, C_{1}, C′, . . .. The simple types are then

M ::= λx⃗ : σ⃗.W W ::= yM_{1} ⋯ M_{n} (n ≥ 0) .

\frac{Γ^{•}y = σ_{1} → ⋯ → σ_{n} → C Γ ⊢ M_{1} : σ_{1} ⋯ Γ ⊢ M_{n} : σ_{n}}{Γ ⊢ yM_{1} ⋯ M_{n} : C}

\frac{Γ, x⃗ : σ⃗ ⊢ W : C}{Γ ⊢ λx⃗ : σ⃗.W : σ⃗ → C}

Fig. 5. Typing rules for finite Böhm trees

generated by the following syntax:

σ ::= C σ → τ.

The η−long normal forms, or finite η−long typed Böhm trees, or finite typed Böhm trees for short, are defined via typing judgements Γ ⊢ M : σ, where Γ is a context consisting of a list of non-empty vectors x⃗ : σ⃗ of typed variables. In each of these vectors x⃗ = x_{1} ⋯ x_{n}, the variables x_{1}, …, x_{n} are supposed distinct. The following auxiliary function allows us to retrieve the type Γ^{•}y of a free variable y from the context Γ:

(Γ, x⃗ : σ⃗)^{•}y = \{ \begin{matrix}Γ^{•}y & if y does not appear in x⃗ \\ σ_{i} & if y = x_{i} \end{matrix}

If σ⃗ = σ_{1}, …, σ_{n}, we adopt the abbreviation σ⃗ → κ for σ_{1} → ⋯ → σ_{n} → κ. If n = 0, we then just mean κ. The typing rules are given in figure 5. Notice that the bodies W are forced to have a basic type, i.e. variables must be fully applied and terms of function types must be fully abstracted according to their type. The η-long format is essential to guarantee the completeness of the VAM execution (cf. remark 4).

On the other end, as anticipated in section 2, we take A = ω as alphabet, and the above set of simple types as set T of abstract types. We shall define the translation of closed finite typed Böhm trees. Similarly to the untyped case, the translation function involves a function that takes a context Γ and a term M, and returns a strategy M^{Γ}. This function uses itself an auxiliary function which takes a context Γ and a variable x and returns a player’s move decorated with a type. These functions are defined in figure 6. The compilation of a closed finite typed Böhm tree M is defined as M^{nil}. A type decoration σ in M^{nil} should be read as follows:

(player’s move)  σ = type of the corresponding variable
(opponent’s move) σ = type of the corresponding subterm .

Remark 6. We briefly indicate how the compilation can be extended to open typed Böhm trees. Suppose we want to compile M such that Γ ⊢ M : σ. As a first try, we might define the compilation by M^{Γ}, but then the free variable occurrences x are not transformed into [x, ↩], but in those “hybrid” player’s moves [i, ↩^{j}] that are bound in a companion list (cf. definition 3.3). In order to produce moves of the form [x, ↩], which

\frac{y^{Γ,x⃗:σ⃗} = [i, ↩^{j}]^{τ_{1}→···τ_{n}→C}}{(λx⃗ : σ⃗.yM⃗)^{Γ} = \{•^{σ⃗→C}y^{Γ,x⃗:σ⃗}\} ⋃_{k=1···n}\{•^{σ⃗→C}y^{Γ,x⃗:σ⃗}k^{τ_{k}}r | •^{τ_{k}}r ∈ (M_{k})^{Γ,x⃗:σ⃗}\}}

where

\frac{x = x_{i} x⃗ = x_{1} ⋯ x_{k}}{x^{Γ,x⃗:σ⃗} = [i, ↩^{0}]^{σ_{i}}}  \frac{x^{Γ} = [i, ↩^{j}]^{τ} and x does not appear in y⃗}{x^{Γ,y⃗:σ⃗} = [i, ↩^{j+1}]^{τ}}

Fig. 6. Compilation of typed Böhm trees

serve in hooking up strategies for composition, one may adapt the compilation of figure 6 as follows: we should compile M as M_{Γ}^{nil}, where Γ is carried out everywhere in a dummy way except when x_{Γ}^{nil} is met, which has to be compiled to [x, ↩]^{Γ^{•}x}.

The set of finite typed Böhm trees is in bijection with a subset of finite typed strategies for A, T, and a suitable function ( ). In order to characterise this subset, we have to impose furthermore a discipline for basic types. Definition 4.1. Let A = ω and let T be the set of types built as terms over the signature consisting of basic type symbols C, C_{1}, … and of → of arity 2. If σ = τ_{1} → ⋯ → τ_{n} → C, we set:

σ_{i} = \{ \begin{matrix}τ_{i} if 1 ≤ i ≤ n \\ undefined otherwise. \end{matrix}

We define the following additional operation ( )^{⋆} from types to basic types: (σ⃗ → κ)^{⋆} = κ. A typed λ strategy is a typed strategy ϕ relative to A and T which moreover satisfies the following condition:

(0) If ra^{σ}[α, ↩^{κ}]^{τ} ∈ ϕ, then σ^{⋆} = τ^{⋆}.

A typed λ pseudo-strategy is defined likewise as a typed pseudo-strategy satisfying condition (0).

We next define a compilation from finite name-free typed λ strategies (cf. definition 2.2 and remark 6) to finite closed typed Böhm trees. The translation involves a function that takes a name-free pseudo-strategy of type σ and a context Γ and yields an (open) finite typed Böhm tree. The translation is given in figure 7. Definition 4.2. We say that a context Γ agrees with a list of types Σ if Γ and Σ have the same length, and if for each vector x⃗ : τ⃗ of Γ the corresponding type in the list Σ has the form τ⃗ → C for some C. Proposition 4.3. The following properties hold: 1 If ⊢ M : σ, then M^{nil} is a finite name-free typed λ strategy. 2 If ϕ is a finite name-free typed λ strategy of type σ, then ϕ^{nil} is a finite typed Böhm

tree and ⊢ ϕ^{nil} : σ. 3 Moreover, these two transformations are inverse to each other. Proof hint. (1) We show a stronger result: if P is a subterm of M and Γ ⊢ P : σ,

\frac{ϕ ⇝ •^{σ⃗→C}[i, ↩^{j}], ϕ_{1}, …, ϕ_{n} Γ^{σ⃗→C} = Γ, x⃗ : σ⃗}{ϕ^{Γ} = λx⃗ : σ⃗.[i, ↩^{j}]^{Γ^{σ⃗→C}} ϕ_{1}^{Γ^{σ⃗→C}} ⋯ ϕ_{n}^{Γ^{σ⃗→C}} ⋯}

where Γ^{σ⃗→C} = Γ, x⃗ : σ⃗, with x_{1}, …, x_{n} distinct and new

[i, ↩^{0}]^{Γ,x⃗:σ⃗} = x_{i} [i, ↩^{j+1}]^{Γ,x⃗:σ⃗} = [i, ↩^{j}]^{Γ}

Fig. 7. Compilation of typed λ strategies

then P^{Γ} is a pseudo-strategy relative to a list Σ that agrees with Γ. We prove this by induction on the size of P, and the list Σ is constructed along the induction. Let

(λx⃗ : σ⃗.yM⃗)^{Γ} = {•^{σ⃗→C}y^{Γ,x⃗:σ⃗}} ⋃_{k=1···n}{•^{σ⃗→C}y^{Γ,x⃗:σ⃗}k^{τ_{k}}r | •^{τ_{k}}r ∈ (M_{k})^{Γ,x⃗:σ⃗}}.

Then, if Σ is associated with Γ, we associate Σ, σ⃗ → C with Γ, x⃗ : σ⃗, and the agreement is obvious by induction and by definition. Conditions (0) and (1) are immediate by construction and by the typing rules. We sketch the argument for conditions (2) and (3). If [i, ↩^{j}] occurs in (λx⃗ : σ⃗.yM⃗)^{Γ}, then it occurs either as the abstract head variable or in (M_{i})^{Γ,x⃗:σ⃗} for some i. Suppose the latter holds (the head variable case is similar). There are three cases (cf. proof of lemma 3.4):

(a) [i, ↩^{j}] occurs bound in (M_{i})^{Γ,x⃗:σ⃗}. Then it occurs a fortiori bound in (λx⃗ : σ⃗.yM⃗)^{Γ}, and condition (2) follows from condition (2) at M_{i}.

(b) [i, ↩^{j}] does not occur bound (λx⃗ : σ⃗.yM⃗)^{Γ}. Then, contraposing from the previous case, condition (3) follows from condition (3) at M_{i}.

(c) [i, ↩^{j}] occurs bound in (λx⃗ : σ⃗.yM⃗)^{Γ} and does not occur bound in (M_{i})^{Γ,x⃗:σ⃗}. Then [i, ↩^{j}] is bound to the head type Σ, σ⃗ → C in (M_{i})^{Γ,x⃗:σ⃗} and is bound to •^{σ⃗→C} in (λx⃗ : σ⃗.yM⃗)^{Γ}, so that condition (2) follows from condition (3) at M_{i}.

(2) One shows that, if ϕ is a typed λ pseudo-strategy of type σ relative to Σ and if Γ agrees with Σ, then Γ ⊢ ϕ^{Γ} : σ. This is proved by induction on the size of ϕ. The conditions (0)-(3) ensure the well-typing of ϕ^{Γ}.

(3) Let us consider ϕ^{Γ} arising in the recursive computation of some ψ^{nil}. We shall prove (ϕ^{Γ})^{Γ} = ϕ for all such ϕ’s, an hence a fortiori (ψ^{nil})^{nil} = ψ. Suppose that

ϕ ⇝ •^{σ⃗→C}[i, ↩^{j}], ϕ_{1}, …, ϕ_{n}

and that Γ^{σ⃗→C} = Γ, x⃗ : σ⃗. Then by construction

ϕ^{Γ} = λx⃗ : σ⃗.[i, ↩^{j}]^{Γ,x⃗:σ⃗}ϕ_{1}^{Γ^{σ⃗→C}} ⋯ ϕ_{n}^{Γ^{σ⃗→C}} · · ·.

If we now analyse the construction of (ϕ^{Γ})^{Γ}, we recover:

— •^{σ⃗→C} thanks to condition (0),

M ::= λx⃗ : σ⃗.W W ::= v case yM_{1} ⋯ M_{n} [v_{1} → W_{1}, …, v_{k} → W_{k}] .

\frac{v : C}{Γ ⊢ v : C}

\frac{\begin{matrix}Γ^{•}y = σ_{1} → ⋯ → σ_{n} → C v_{1}, …, v_{k} : C \\ Γ ⊢ M_{1} : σ_{1} ⋯ Γ ⊢ M_{n} : σ_{n} Γ ⊢ W_{1} : C_{1} ⋯ Γ ⊢ W_{k} : C_{1} \end{matrix}}{Γ ⊢ case yM_{1} ⋯ M_{n} [v_{1} → W_{1}, …, v_{k} → W_{k}] : C_{1}}

\frac{Γ, x⃗ : σ⃗ ⊢ W : C}{Γ ⊢ λx⃗ : σ⃗.W : σ⃗ → C}

Fig. 8. Typing rules for finite Pcf trees

— the correct type decoration for [i, ↩^{j}] thanks to conditions (2) and (3), and

— ϕ_{1}, …, ϕ_{n} by induction. The other direction (M^{Γ})^{Γ} can be handled similarly, choosing names according to the concrete syntax of M in the context extension operations. □

4.2. Pcf trees

In this section, we adapt the syntax of section 4.1 in order to cope with constants of basic 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 types are the same as in section 4.1, and the typing judgements have the same form. The terms 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 (Hyland and Ong 94; Abramsky and Jagadeesan and Malacaria 95). The syntax and the typing rules of Pcf trees are given in figure 8, which uses the notation Γ^{•}y defined in section 4.1. In the first rule, v_{1}, …, v_{k} : C should be read as: “v_{1}, …, v_{k} are all the constants of type C”. Remark 7. We make the simplifying assumption that there are only finitely many constants at any given basic type. This allows us to keep our representations finite. There is no difficulty in extending the results of this section to the case of infinite basic types, like the natural numbers: one then needs to consider terms that may be horizontally infinite, i.e. that may have infinite branching (at player’s moves). The induction arguments on the size of terms must then be replaced by arguments on the length of a maximal branch.

We compile Pcf trees much like finite typed Böhm trees. Definition 4.4. We set:

A = {v | v : C} ∪ {v_{1} | v_{1} : C_{1}} ∪ · · · .

Hence the moves are either natural numbers or constants, called questions and answers, respectively. We suppose that {v | v : C} ∩ {v_{1} | v_{1} : C_{1}} = ∅, for any distinct basic types C and C_{1}. Let T be as in definition 4.1. If σ = τ_{1} → ⋯ → τ_{n} → C, we set

σ_{a} = \{ \begin{matrix}τ_{i} & if a = i and 1 ≤ i ≤ n \\ C & if a = v and v : C \\ undefined & otherwise. \end{matrix}

A Pcf strategy is a typed strategy ϕ relative to A, T, and ( ), that moreover satisfies the following conditions:

(Q) If q[v, ↩^{i}]^{σ} ∈ ϕ, where v is an answer, and if [v, ↩^{i}] is bound to b^{τ} in q, then b is a question. (S) Moreover, all the opponent’s moves between the binding move b and the answer must be answers.

The conditions (Q) and (S) are called the question-answer discipline and the stack discipline, respectively. A Pcf pseudo-strategy is defined likewise as a typed pseudo-strategy satisfying conditions (Q) and (S). Remark 8. Conditions (1), (2), and (Q), together with the definition of σ_{v}, enforce that opponent’s moves of the form v, i.e. opponent’s questions, are never pointed to. Suppose not, and consider a player’s move that points to v. It cannot be an answer by condition (Q). Hence it is a question [i, ↩^{j}]. By condition (2), v should then be decorated with a type σ such that σ_{i} is defined. But by condition (1) σ = τ_{v} for some τ, which by definition of τ_{v} implies σ = C. Hence σ_{i} is undefined, which is a contradiction. Since questions are not pointed to, it is safe to omit them in the count of opponent’s moves from a player’s move to its binder. Therefore, in the setting of Pcf strategies (and of classical strategies), we shall modify the encoding of the pointers accordingly. When writing [a, ↩^{i}], we mean that there are i opponent’s questions between [a, ↩^{i}] and its binder. As a consequence, due to condition (S), all occurrences of player’s answers have

the form [v, ↩^{0}].

The compilation of closed Pcf trees is given via a function M^{Γ} whose definition is given in figure 9. The following are more informal explanations. 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 2. An occurrence of a basic constant v is compiled as [v, ↩^{0}] (cf. remark 8). Finally, we replace the head opponent’s moves • in the translations ϕ_{i} and ϕ′_{j} of M_{i} and W_{j} by i and v_{j}, respectively:

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

In figure 9, the assumption “W has type C” can be read in either of the following two ways. We may understand the compilation as translating typing judgements, in which

\frac{W has type C}{(λx⃗ : σ⃗.W)^{Γ} = \{•^{σ⃗→C}r | r ∈ W^{Γ,x⃗:σ⃗}\}}

\frac{v : C}{v^{Γ} = \{[v, ↩^{0}]^{C}\}}

\frac{v_{1}, …, v_{k} : C}{(case yM_{1} ⋯ M_{n} [v_{1} → W_{1} ⋯ v_{k} → W_{k}])^{Γ} = \{y^{Γ}\} _{⋃i=1···n} \{y^{Γ}i^{τ_{i}}r | •^{τ_{i}}r ∈ M_{i}^{Γ}\} _{⋃j=1···k} \{y^{Γ}v_{j}^{C}r | r ∈ W_{j}^{Γ}\}}

where y^{Γ} is as in figure 6.

Fig. 9. Compilation of Pcf trees

case the information C is immediately available, or we may retrieve C through a simple recursive exploration: we have C = W^{⋆}, where

(case yM⃗ [v_{1} → W_{1} ⋯ v_{k} → W_{k}])^{⋆} = W_{j}^{⋆}

for an arbitrary choice of j, and where v^{⋆} = C if v : C. The compilation of a term M is defined as M^{nil}. Example 4.5. We compile the following term:

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

where we take a basic type of Booleans and the two constant tt and ff of this type.

- Strategy for case f(tt) [ff → tt]:

•^{(} [f, ↩]^{case} \{ \begin{matrix}1^{(} [tt, ↩^{0}] \\ ff[tt, ↩^{0}] \end{matrix}

- Multi-strategy for [f ← (λx.case x [tt → ff, ff → tt])]:

f^{(λx} [1, ↩^{0}]^{case x} \{ \begin{matrix}tt[ff, ↩^{0}] \\ ff[tt, ↩^{0}] \end{matrix}

The execution of this example by the VAM is as follows:

\begin{matrix}• & f & ⟨1, 2⟩ & ⟨tt, 3⟩ & ⟨ff, 2⟩ & [tt, ↩^{0}] \\ 1 & 2 & 3 & 4 & 5 & 6 \end{matrix}

The successive views are as follows:

view_{Γ}(1) = •  view_{Γ}(2) = f view_{Γ}(3) = •1
view_{Γ}(4) = f tt view_{Γ}(5) = •ff

The displayed terminated history corresponds to a (B) final state, which can be seen as providing an answer to the following query: what is the value returned by the application of the functional λf.case f(tt) [ff → tt] to the negation function?

For Pcf trees, the correspondence between final states and “head normal forms” is as follows:

(λx⃗. case yM⃗ [v⃗ → W⃗]) (y free)  (F)
(λx⃗. case xM⃗ [v⃗ → W⃗]) (x bound) (B)
(λx⃗.v)  (B) .

Proposition 4.6. The compilation function of figure 9 maps finite closed Pcf trees to name-free Pcf strategies bijectively.

Proof hint. The proof is similar to the proof of proposition 4.3. It goes via the definition of an inverse compilations. We do not give the details, which are rather straightforward. We just remark that the counterpart of the stack condition (S) in the type system is to be found in the typing rule for case, where the common type C_{1} of the W_{j}’s is “passed” to the conclusion. □

4.3. Classical Böhm trees

Classical Böhm trees have been introduced in (Herbelin 97). They provide a classical version of Pcf trees, using the ideas of the λμ-calculus. We refer to (Parigot 92; Ong 96) for an introduction to the λμ-calculus (see also the comments at the end of the section). With respect to Böhm trees and Pcf trees, classical Böhm trees incorporate two new constructs: the μ abstraction, and the naming operation [α]. They correspond to a logical treatment of the classical absurdity, and involve a discipline of continuation variables separate from the discipline of ordinary variables. The syntax and the typing rules for classical Böhm trees are given in figure 10. The typing judgements are of the form Γ; Δ ⊢ M : σ, where Γ is a context of typed variables as usual, and Δ is a context of typed continuation variables. In classical Böhm trees, all the continuation variables have a basic type. In the figure, the notation Δ^{•}α is similar to the notation Γ^{•}y, and is defined by:

(Δ, β : C)^{•}α = \{ \begin{matrix}Δ^{•}α & if α ≠ β \\ C & if α = β . \end{matrix}

One should read v_{1}, …, v_{k} : C as “v_{1}, …, v_{k} are all the constants of type C” (cf. figure 8). All the bodies W receive a special type ⊥, which stands for absurdity.

Definition 4.7. Let A, T, and ( ), be as in definition 4.4. A classical strategy is a typed strategy ϕ relative to A and T which moreover satisfies the question-answer discipline (condition (Q) of definition 4.4).

In other words, classical strategies are the same as Pcf strategies, except that the stack condition (S) has been removed. Proposition 4.8. The compilation function of figure 11 maps bijectively finite closed classical Böhm trees to finite name-free classical strategies.

M ::= λx⃗ : σ⃗.μα.W W ::= [α]v case yM_{1} ⋯ M_{n} [v_{1} → W_{1}, …, v_{k} → W_{k}] .

\frac{Δ^{•}α = C v : C}{Γ; Δ ⊢ [α]v : ⊥}

\frac{Γ^{•}y = σ_{1} → ⋯ → σ_{n} → C v_{1}, …, v_{k} : C Γ; Δ ⊢ M_{1} : σ_{1} ⋯ Γ ⊢ M_{n} : σ_{n} Γ; Δ ⊢ W_{1} : ⊥ ⋯ Γ; Δ ⊢ W_{k} : ⊥}{Γ; Δ ⊢ case yM_{1} ⋯ M_{n} [v_{1} → W_{1}, …, v_{k} → W_{k}] : ⊥}

\frac{Γ, x⃗ : σ⃗; Δ, α : C ⊢ W : ⊥}{Γ ⊢ λx⃗ : σ⃗.μα.W : σ⃗ → C}

Fig. 10. Typing rules for classical Böhm trees

\overline{(λx⃗ : σ⃗.μα : C.W)^{Γ;Δ} = \{•^{σ⃗→C}r | r ∈ W^{Γ,x⃗:σ⃗}; Δ, α : C\}}

\frac{v : C}{([α]v)^{Γ;Δ} = \{[v, ↩^{α^{Δ}}]^{C}\}}

where α^{Δ,β:C} = \{ \begin{matrix}α^{Δ} + 1 if α ≠ β \\ 0 if α = β \end{matrix}

\frac{y^{Γ,x⃗:σ⃗} = [i, ↩^{j}]^{τ_{1}→···τ_{n}→C} v_{1}, …, v_{k} : C}{(case yM⃗ [v_{1} → W_{1} ⋯ v_{k} → W_{k}])^{Γ} = \{y^{Γ,x⃗:σ⃗}\} _{⋃i=1···n} \{y^{Γ,x⃗:σ⃗}i^{τ_{i}}r | •^{τ_{i}}r ∈ M_{i}^{Γ,x⃗:σ⃗}\} _{⋃j=1···k} \{y^{Γ,x⃗:σ⃗}v_{j}^{C}r | r ∈ W_{j}^{(Γ,x⃗:σ⃗}\}}

where y^{Γ} is as in figure 6.

Fig. 11. Compilation of classical Böhm trees

We can summarise the transition from Böhm trees to classical Böhm trees through Pcf trees as follows:

— In order to characterise typed Böhm trees we have to impose an explicit basic type discipline (condition (0) of definition 4.1). This condition becomes implied as soon as values, or answers are introduced (both in Pcf trees and classical Böhm trees). Answers allow to encode the continuations of the computations using pointers: they are bound, just as variables are.

— In order to characterise Pcf Böhm trees, we have to impose a discipline for answers: 1 Answers are bound to questions. 2 Moreover, this binding forces to answer the last pending question (stack disci-

pline).

— If the stack discipline is removed, then we have the classical Böhm trees.

From this analysis we conclude that classical Böhm trees provide the best fit for our abstract computational setting of abstract Böhm trees. Condition (0) is an ad hoc condition. The stack discipline is certainly not ad hoc, since it sets the boundary between intuitionistic and classical. But from the computational point of view, it makes no difference to have it or not.

In the rest of the section, we substantiate rather informally the claim that classical Böhm trees are to “λμ + Pcf” what Pcf trees are to Pcf. We first describe briefly the version of Parigot’s λμ-calculus (Parigot 92) given by Hofmann and Streicher (Hofmann and Streicher 97) (which is itself closely inspired by Ong’s version (Ong 96)). Let T be the collection of types considered so far, the basic types being now looked at as propositional atoms. There is also a special type ⊥, which Hofmann and Streicher allow in T (i.e., e.g. σ → ⊥ ∈ T), while we shall leave it apart. The terms of the λμ-calculus are given by the following syntax:

M ::= x MN λx : σ.M μα : A.M [α]M .

where x ranges over term variables as usual, and where α ranges over a disjoint set of continuation variables. Typing judgements have the form Γ; Δ ⊢ M : σ, where Δ is a list of typed continuation variables α : σ, with σ ≠ ⊥. The judgements are derived by the following rules:

\frac{x : σ in Γ}{Γ; Δ ⊢ x : σ}  \frac{Γ, x : σ; Δ ⊢ M : τ}{Γ; Δ ⊢ λx : σ.M : σ → τ}  \frac{Γ; Δ ⊢ M : σ → τ  Γ; Δ ⊢ N : σ}{Γ; Δ ⊢ MN : τ}

\frac{Γ; Δ, α : σ ⊢ M : ⊥}{Γ; Δ ⊢ μα : σ.M : σ}  \frac{Γ; Δ ⊢ M : σ  α : σ in Δ}{Γ; Δ ⊢ [α]M : ⊥}

In order to understand these rules, one should read α : σ as an assumption that the negation σ^{⊥} of σ holds. Then the typing rules for μ-abstractions μα : σ.M and for named terms [α]M read as absurdity introduction and elimination rules. The rewriting rules of the λμ-calculus are the following ¶:

\begin{matrix}(β) & (λx : σ.M)N = M[N/x] \\ (μ − ζ) & μα : σ → τ. M = λx : σ. μβ : τ. M[x :: β/α] \\ (μ − β) & [α](μβ : σ.M) = M[α/β] \end{matrix}

In these rules, three substitution operations are involved. The first is the ordinary substitution in the λ-calculus. The third is the substitution of (all free occurrences of) the continuation variable β by α. The second consists in spotting all subterms of the form [α]N of M and replacing them by [β](Nx).

In addition to these rules, we consider an expansion rule for a term M of type σ ≠ ⊥:

(μ − η) M → μα : σ. [α]M

¶ The rule (μ − ζ) in the case B = ⊥ is slightly different, since continuation variables of type ⊥ are not allowed, see (Hofmann and Streicher 97).

where α is new. It is easy to see that this rule, together with the other rules, implies the η-rule N = λx : σ. Nx for any term N of a non-basic type σ → τ. The following properties are easy to check: 1 There cannot be a well typed term of the form μα : σ. μβ : τ. M nor of the form

[α][β]M; for example, μβ : τ. M has type τ ≠ ⊥, but should have type ⊥ if μα : σ. μβ : τ. M were to be well typed.

2 Under the assumption ⊥ ∉ T, a term of type ⊥ can only be of the form [β]M. 3 In a normal form, all the continuation variables have a basic type, thanks to the rule

(μ − ζ). Let us analyse informally an expanded λμ normal form M, by which we mean the λμ version of η-long finite Böhm trees. Making use if needed of the expansion rule (μ − η) followed by the rule (μ − ζ), we see that M has the form λx⃗ : σ⃗.M_{1}, where M_{1} is of a basic type, which is ≠ ⊥ since we assume ⊥ ∉ T here. Possibly using the expansion rule, we have M_{1} = μα : C.M_{2} for some α and C. By property (2) above M_{2} must be of the form [β]M_{3}, where by property (3) M_{3} is of basic type. The first symbol of M_{3} cannot be a [γ] by property (1), nor a λ because of the type, nor a μγ as otherwise there would be a (μ − β) redex. It is thus either a variable x or an aplication M_{4}M_{5}; M_{4} has a non-basic type, hence cannot start with a μγ by property (3), nor with a λ as otherwise there would be a β-redex, nor with a [γ] because of the type. Pursuing in this way, we see that M_{3} has the form xM_{n} ⋯ M_{5}. Summarising, the expanded normal forms have (recursively) the form

λx⃗ : σ⃗. μα : C. [β](xM⃗)

where β has a basic type.

If we now incorporate the basic constants and the case construct, then we arrive at the classical Böhm trees of figure 10, thanks to the following additional rule that allows to distribute the naming operator [α] all the way down to the constants:

[α](case yM⃗ [v_{1} → W_{1}, …, v_{k} → W_{k}]) → (case yM⃗ [v_{1} → [α]W_{1}, …, v_{k} → [α]W_{k}]).

Remark 9. The bijective correspondences stated in propositions 4.3, 4.6, and 4.8 can be extended without difficulty to order-isomorphisms, by allowing a special player’s move [Ω, ↩]. We briefly indicate how this works. When we compile a partial term, we should include explicit player’s moves [Ω, ↩] corresponding to each of the occurrences of Ω. For example, (λx.xΩ(yΩ))^{nil} contains •[1, ↩^{0}]1[Ω, ↩] and •[1, ↩^{0}]2[y, ↩]1[Ω, ↩]. Here is how we justify that the composition operation is monotonic (hence Scott-continuous, being defined by means of finitary rules). First, we need a minor adjustment in the setting of the VAM. The special “free player’s move” [Ω, ↩] is allowed to occur in ϕ, without being bound in ψ. Hence we allow for (F) final states in ϕ that correspond to having reached an Ω of ϕ. Next, we define the order relation between strategies (and similarly between multi-strategies) as follows: ϕ ≤ ϕ′ if each position of ϕ′ is either in ϕ, or has a query prefix q such that q[Ω, ↩] ∈ ϕ. Suppose now that ϕ ≤ ϕ′ and ψ ≤ ψ′, and that r ∈ ϕ′ ∘ψ′. The corresponding computation of the strong VAM has explored parts of ϕ′ and ψ′. If those parts are also present in ϕ and ψ, then r is also in ϕ ∘ ψ. Otherwise, we run two executions of the strong VAM in parallel, the first for ϕ and ψ, the second for ϕ′ and ψ′, both executions being guided by r (cf. remark 5). The machines have the same history up to some step at which the view q in ϕ′ and ψ′ is answered by Ω in ϕ or ψ, and by something else in ϕ′ or ψ′. The first execution then returns an answer Ω to the current query, which is a prefix of r. Hence ϕ ∘ ψ ≤ ϕ′ ∘ ψ′.

4.4. Novikov’s logic

In this section, we present examples taken from Novikov’s classical infinitary propositional logic. The basic formulas of this logic are of the form ∃ x P (or ∃ x⃗ P), where P is a predicate over natural numbers, like x ≤ y or f(x) ≤ f(y) (where f is a function from natural numbers to natural numbers whose definition is given as an oracle outside the logic). The (existential) formulas are then built by the following rule:

If A is a formula, then ∃ x ∀ y A is a formula.

In this logic, one proves disjunctions of formulas, represented as sequences Γ = A_{1}, …, A_{n+1}. Proofs are formulated as strategies. At the beginning, the opponent objects the whole disjunction. Then the player chooses to justify one of the disjuncts, say A_{n+1} = ∃ x ∀ y A(x, y). To materialise his justification, the player also chooses a particular x_{0}. Then the proof of the formula amounts to proving each of the following disjunctions:

A_{1}, …, A_{n}, A_{n+1}, A(x_{0}, i)

for i = 0, 1, 2, . . .. Notice that we have kept A_{n+1}, because, in classical reasoning, it might be the case that the player discovers that he was wrong in his choice of x_{0}, and that another choice would have been wiser.

A proof of a universal quantification ∀ z A(z) is represented as an infinite multi-strategy […, m ← A(m), …]. All such proofs can be formulated as trees with pointers, and the (Strong) VAM can be used for cut-elimination. More precisely, in the examples presented below,

— the strategy proves a disjunction (∃ x ∀ y A(x, y)), Γ,

— the multi-strategy provides proofs of ∃ y ¬A(m, y) for all m, and

— the cut-elimination, or composition, yields a (cut-free) proof of Γ.

The alphabet for Novikov’s calculus is A = ω. The set T of abstract types is defined as follows (in first approximation):

T = {A | A is a formula} ∪ {∀ y A | A is a formula}.

We set:

(∀ y A)_{i} = A(i) (∃ x B)_{j} = B(j) .

We shall not give a formal statement that characterises the proofs of Novikov’s logic as typed strategies relative to A, T, and ( ), but it should be clear that such a bijection exists (see also remark 10). We shall just present two examples, taken from (Coquand 95) and from (Berardi and Bezem and Coquand 94), respectively. In example 4.9, given a function f from natural numbers to natural numbers, we show how to construct three numbers u_{1}, u_{2}, u_{3} such that f(u_{1}) ≤ f(u_{2}) ≤ f(u_{3}), relying on a lemma that asserts the existence of relative minima (the formula K(x) below). In example 4.10, we show a dialogue interpretation of the Axiom of Choice: given a predicate P (x, y) and a multistrategy witnessing (∃ x P (m, x)) for all m, we show how the interaction with the axiom of choice results in the progressive construction of f such that P (n, f(n)) (for all n in the domain of definition of f).

Example 4.9.

- Strategy for

L = (∃ x ∀ y ≥ x ∃ z ≥ x f(y) > f(z)) , (∃ u_{1} < u_{2} < u_{3} f(u_{1}) ≤ f(u_{2}) ≤ f(u_{3})) :

• [0, ↩]^{∃x} \{ y_{1} [y_{1} + 1, ↩]^{∃x} \{ \begin{matrix}y_{2}^{f(y_{1}) > f(y_{2})} & [y_{2}, ↩^{1}]^{∃z} \\ y_{2}^{f(y_{1}) ≤ f(y_{2})} & [y_{2} + 1, ↩]^{∃x} & \{ \begin{matrix}y_{3}^{f(y_{2}) > f(y_{3})} & [y_{3}, ↩^{1}]^{∃z} \\ y_{3}^{f(y_{2}) ≤ f(y_{3})} & [y_{1}, y_{2}, y_{3}, ↩^{3}]^{∃u_{1} < u_{2} < u_{3}} \end{matrix} \end{matrix}

- Multi-strategy for K(x) = ∃ y ≥ x ∀ z ≥ x f(y) ≤ f(z):

x [x, ↩^{0}]^{∃y} z_{1}^{f(x) > f(z_{1})} [z_{1}, ↩^{1}]^{∃y} z_{2}^{f(z_{1}) > f(z_{2})} [z_{2}, ↩^{2}]^{∃y} ⋯

We briefly explain how to read the strategy for L. The player chooses to justify the first disjunct of L, with x = 0. This is just to let opponent pick a value y_{1} ≥ 0 for y. Next the player retries the first disjunct, but now with x = y_{1} + 1. The opponent must then choose y_{2} > y_{1}. The player has access to the oracle defining f. If f(y_{1}) > f(y_{2}), then the player plays z = y_{2}, and he has justified the first disjunct. Otherwise, he retries the first disjunct from the very beginning, with x = y_{2} + 1. The opponent chooses y_{3} > y_{2}. If f(y_{2}) > f(y_{3}), then the player can justify the first disjunct by playing z = y_{3}. Otherwise, we have f(y_{1}) ≤ f(y_{2}) ≤ f(y_{3}), and the player justifies the second disjunct by playing u_{1}, u_{2}, u_{3} = y_{1}, y_{2}, y_{3}. We have omitted the type decorations in the above strategy and multi-strategy. Here are the typed positions corresponding to the first branch and to the third branch of the proof of L:

\begin{matrix}•^{∃ u_{1}<u_{2}<u_{3} f(u_{1})≤f(u_{2})≤f(u_{3})} & [0, ↩]^{∀ y≥0 ∃ z≥0 f(y)>f(z)} \\ y_{1}^{∃ z≥0 f(y_{1})>f(z)} & [y_{1} + 1, ↩]^{∀ y≥y_{1}+1 ∃ z≥y_{1}+1 f(y)>f(z)} \\ y_{2}^{∃ z≥y_{1}+1 f(y_{2})>f(z)} & [y_{2}, ↩^{1}]^{f(y_{1})>f(y_{2})} \\ •^{∃ u_{1}<u_{2}<u_{3} f(u_{1})≤f(u_{2})≤f(u_{3})} & [0, ↩]^{∀ y≥0 ∃ z≥0 f(y)>f(z)} \\ y_{1}^{∃ z≥0 f(y_{1})>f(z)} & [y_{1} + 1, ↩]^{∀ y≥y_{1}+1 ∃ z≥y_{1}+1 f(y)>f(z)} \\ y_{2}^{∃ z≥y_{1}+1 f(y_{2})>f(z)} & [y_{2} + 1, ↩]^{∀ y≥y_{2}+1 ∃ z≥y_{2}+1 f(y)>f(z)} \\ y_{3}^{∃ z≥y_{2}+1 f(y_{3})>f(z)} & [y_{1}, y_{2}, y_{3}, ↩^{3}]^{f(y_{1})≤f(y_{2})≤f(y_{3})} \end{matrix}

For K, we give only a typed position of length 4 (with x = 0, z_{1} = 1):

\begin{matrix}0^{∃ y≥0 ∀ z≥0 f(y)≤f(z)} & [0, ↩^{0}]^{∀ z≥0 f(0)≤f(z)} \\ 1^{f(0)≤f(1)} & [1, ↩^{1}]^{∀ z≥0 f(1)≤f(z)} \end{matrix}

Given f such that

f(0) = 10, f(1) = 5, f(2) = 3, f(3) = 7, f(4) = 4, f(5) = 11, f(6) = 29

the history of the proof of ∃ u_{1} < u_{2} < u_{3} f(u_{1}) ≤ f(u_{2}) ≤ f(u_{3}) by cut-elimination performed by the VAM is as follows.

\begin{matrix}• & 0 & ⟨0, 2⟩ & 1 & ⟨1, 4⟩ & ⟨1, 3⟩ & ⟨1, 2⟩ & 2 & ⟨2, 8⟩ & ⟨2, 7⟩ \\ 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 \\ ⟨2, 2⟩ & 3 & ⟨3, 12⟩ & 4 & ⟨4, 14⟩ & ⟨4, 13⟩ & ⟨4, 12⟩ & 5 & ⟨5, 18⟩ & [2, 4, 5, ↩^{0}] \\ 11 & 12 & 13 & 14 & 15 & 16 & 17 & 18 & 19 & 20 \end{matrix}

The successive views are as follows:

view_{Γ}(1) = •  view_{Γ}(2) = 0  view_{Γ}(3) = •0
view_{Γ}(4) = 1  view_{Γ}(5) = •01 view_{Γ}(6) = 01
view_{Γ}(7) = •1 view_{Γ}(8) = 2 view_{Γ}(9) = •12
view_{Γ}(10) = 012 view_{Γ}(11) = •2 view_{Γ}(12) = 3
view_{Γ}(13) = •23 view_{Γ}(14) = 4  view_{Γ}(15) = •234
view_{Γ}(16) = 34  view_{Γ}(17) = •24 view_{Γ}(18) = 5
view_{Γ}(19) = •245

Remark 10. The above type decorations do not fit on the nose with the framework of the typed VAM: if ϕ is the strategy associated to L, then ϕ(•) = [0, ↩]^{∀ y≥0 ∃ z≥0 f(y)>f(z)}, while the first move played in the multi-strategy is 0^{∃ y≥0 ∀ z≥0 f(y)≤f(z)}. What we need to do to repair this mismatch is to take as set of abstract types a quotient of the set of formulas by de Morgan duality.

Example 4.10.

- Strategy for AC = (∃ m ∀ x \overline{P} (m, x)) , (∃ f ∀ n P (n, f(n))):

• [⊥, ↩^{0}]^{∃f} \{ n^{0} [n^{0}, ↩]^{∃m} \{ x_{0} [( \begin{matrix}x^{0} \\ n^{0} \end{matrix} ) , ↩^{2}]^{∃f} \{ n_{1} [n^{1}, ↩]^{∃m} \{ x^{1} [( \begin{matrix}x^{0} & x^{1} \\ n^{0} & n^{1} \end{matrix} ) , ↩^{4}]^{∃f} …

where ( \begin{matrix}x^{0} \\ n^{0} \end{matrix} ), ( \begin{matrix}x^{0} & x^{1} \\ n^{0} & n^{1} \end{matrix} ) , … are the (partial) functions defined by:

( \begin{matrix}x^{0} \\ n^{0} \end{matrix} ) (n^{0}) = x^{0}

( \begin{matrix}x^{0} & x^{1} \\ n^{0} & n^{1} \end{matrix} ) (n^{0}) = x^{0} ( \begin{matrix}x^{0} & x^{1} \\ n^{0} & n^{1} \end{matrix} ) (n^{1}) = x^{1}
⋮

- Multi-strategy for (∃ x P (m, x)):

{ ⋮ ; m[x_{m}, ↩^{0}] ; ⋮

This example requires strong reduction: the demand for more values of f must come from the user. Thus we describe the execution in the framework of the Strong VAM. The first 10 steps of (generic) execution are as follows:

\begin{matrix}\underline{•_{ν}} & \underline{[⊥, ↩^{ν}]} & \underline{n_{ν^{0}}^{0}} & n^{0} & ⟨x_{n^{0}}, 4⟩ \\ 1 & 2 & 3 & 4 & 5 \\ \underline{[( \begin{matrix}x_{n^{0}} \\ n^{0} \end{matrix} ) , ↩^{ν}]} & \underline{n_{ν^{1}}^{1}} & n^{1} & ⟨x_{n^{1}}, 8⟩ & \underline{[( \begin{matrix}x_{n^{0}} & x_{n^{1}} \\ n^{0} & n^{1} \end{matrix} ) , ↩^{ν}]} \\ 6 & 7 & 8 & 9 & 10 \end{matrix}

with the following successive views:

view_{Γ}(1) = •  view_{Γ}(3) = •n^{0}
view_{Γ}(4) = n^{0}  view_{Γ}(5) = •n^{0}x_{n^{0}}
view_{Γ}(7) = •n^{0}x_{n^{0}}n^{1} view_{Γ}(8) = n^{1}  view_{Γ}(9) = •n^{0}x_{n^{0}}n^{1}x_{n^{1}}

5. Conclusion

Abstract Böhm trees seem to provide an adequate level of abstraction for the description of abstract machines for functional languages (and some of their extensions, e.g. with control operators) and for cut-elimination in a range of logical proof systems. They embody just as much structure as is needed to describe two sorts of interaction: tree interaction and pointer interaction (cf. remark 2). These two forms of interaction are not only present in calculi such as those presented as examples in section 4, they also suffice to account for the whole evaluation mechanism (restricted to η-long terms) of these calculi.

Developping a theory at this level of abstraction allows us to direct more efforts towards compilation than towards execution. For example, by compiling Pcf trees or classical Böhm trees in the language of abstract Böhm trees, we have freed ourselves from the need to design extensions of the execution model: the same abstract machine is prepared to handle any kind of abstract Böhm trees.

Here we have presented only one abstract machine (and its strong extension). It turns out that several abstract machines of the literature (including a call-by-name environment machine in the style of Landin’s SECD machine) can be expressed at this level of abstraction (Curien and Herbelin 97), and can be inter-translated, yielding step-to-step correspondences. Hence the framework of abstract Böhm trees can contribute to express what these abstract machines have in common, and how they differ (in data representation, or in memory management).

We would like to stress that the role played by types in this study is more typical of concurrency theory than of type theory. We have seen in section 2 that the abstract machine always terminates. We do not use types to prevent non-termination, but to ensure that the termination is satisfactory (no dead-lock). The non-termination, say, of the untyped λ-calculus, is then explained by the fact that untyped reduction infinitely expands the original term in the back of the scene (cf. remark 4). We formulate the following question:

Is there a characterisation – e.g, by some type system in the style of Coppo-Dezani’s intersection types – of the untyped λ-terms for which the VAM execution succeeds, i.e., ends in a legal final state? More informally, among the terms possessing a head normal form, which are those that can reach it without implicit η-expansions?

It would also be interesting to extend our approach to cover more sophisticated type systems like second-order types. This is certainly possible, at the price of a sophistication of the basic abstract machine presented here, that seems inherently linked with simple types.

References

M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit substitutions, Journal of Functional

Programming 1(4), 375-416 (1991). S. Abramsky, R. Jagadeesan, and P. Malacaria, Full abstraction for PCF, available by ftp at

theory.doc.ic.ac.uk/papers (1995). R. Amadio, and Pierre-Louis Curien, Domains and Lambda-calculi, to appear (1997). S. Berardi, M.A. Bezem, T. Coquand, On the computational content of the axiom of choice,

Technical Report of Utrech University (1994). T. Coquand, A semantics of evidence for classical arithmetic, revised version, Journal of Symbolic

Logic 60, 325–337 (1995). P.-L. Curien, An abstract framework for environment machines, TCS 82, 389–402 (1991). P.-L. Curien, and H. Herbelin, Computing with Abstract Böhm trees, submitted (1997). V. Danos, H. Herbelin, L. Regnier, Game semantics and abstract machines, in Proc. LICS 96. V. Danos, L. Regnier, Machina ex deo, ou encore quelque chose à dire sur la machine de Krivine,

unpublished (1990). W. Felscher, Dialogues as a foundation of intuitionistic logic, Handbook of Philosophical Logic

3, 341-372 (1986). H. Herbelin, Séquents qu’on calcule, Thèse de Doctorat, Université Paris VII (1995).

P.-L. Curien 34

H. Herbelin, Games and weak head reduction for classical Pcf, Proc. TLCA 96 (1997). G. Huet, An analysis of Böhm’s theorem, TCS 121, 145-167 (1993). M. Hofmann and T. Streicher, Continuation models are universal for λμ-calculus, submitted

(1997). M. Hyland, L. Ong, On full abstraction for PCF, available by ftp at ftp.comlab.ox.ac.uk/pub/

Documents/techpapers/Luke.Ong (1994). R. Milner, Fully abstract models of typed lambda-calculi, TCS 4 (1977). H. Nickau, Hereditary sequential functionals: a game-theoretic approach to sequentiality, Dis-

sertation, Universität GH Siegen, Shaker-Verlag (1996). L. Ong, A semantic view of classical proofs: type-theoretic, categorical, and denotational char-

acterisations, In Proc. LICS 96. M. Parigot, λμ-calculus, an algorithmic interpretation of classical natural deduction, in Proc.

LPAR 92, LNCS 624 (1992). G. Plotkin, LCF as a programming language, TCS 5 (1977).