BRICS RS-02-14 Berger & Oliva: Modified Bar Recursion BRICS

Basic Research in Computer Science

Modified Bar Recursion

Ulrich Berger Paulo B. Oliva BRICS Report Series RS-02-14 ISSN 0909-0878 April 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Ulrich Berger & Paulo B. Oliva.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/14/

Modified Bar Recursion

Ulrich Berger u.berger@swan.ac.uk Paulo Oliva^{∗} pbo@brics.dk

Abstract

We introduce a variant of Spector’s bar recursion (called “modified bar recursion”) in finite types to give a realizability interpretation of the classical axiom of countable choice allowing for the extraction of witnesses from proofs of Σ_{1} formulas in classical analysis. As a second application of modified bar recursion we present a bar recursive definition of the fan functional. Moreover, we show that modified bar recursion exists in M (the model of strongly majorizable functionals) and is not S1-S9 computable in C (the model of total functionals). Finally, we show that modified bar recursion defines Spector’s bar recursion primitive recursively.

1 Introduction

In [24] Spector extended Gödel’s Dialectica Interpretation of Peano Arithmetic [11] to classical analysis using bar recursion in finite types. Although considered questionable from an intuitionistic point of view ([1], 6.6) there has been considerable interest in bar recursion, and several variants of this definition scheme and their interrelations have been studied by, e.g. Schwichtenberg [21], Bezem [8] and Kohlenbach [16]. In this paper we add another variant of bar recursion (so-called modified bar recursion) and use it to give a realizability interpretation of the classical, i.e. negatively translated, axiom of dependent choice that can be used to extract witnesses from proofs of Σ_{1}-formulas in full classical analysis. Our interpretation is inspired by a paper by Berardi, Bezem and Coquand [2] who use a similar kind of recursion in order to interpret dependent choice. The main difference to our paper is that in [2] a rather ad-hoc infinitary term calculus and a non-standard notion of realizability are used whereas we work with a straightforward combination of negative translation, A-translation, modified realizability, and Plotkin’s adequacy result for the partial continuous functional semantics of PCF [20].

As a second application of bar recursion (in section 4) we show that the definition of the fan functional within PCF given in [3] and [19] can be derived from Kohlenbach’s and our variant of bar recursion.

∗BRICS - Basic Research in Computer Science, funded by the Danish National Research Foundation.

The final part of the paper deals with the question of defining (primitive recursively) modified bar recursion MBR in other bar recursive definitions (namely, Spector’s original bar recursion SBR and Kohlenbach’s bar recursion KBR – see [24] and [16] respectively) and vice versa. In section 5 we show that modified bar recursion exists in M (the model of strongly majorizable functionals), ^{1} from which we can conclude that MBR cannot be used to define KBR primitive recursively. In section 6 we show that modified bar recursion is primitive recursively definable in SBR. Finally, (in section 7,) we prove that (as the fan functional) modified bar recursion is not S1-S9 computable in C (the model of total continuous functionals), which implies that MBR is not (primitive recursively) definable in SBR nor in KBR.

2 Bar recursion in finite types

We work in a suitable extension of Heyting Arithmetic in finite types, HA^{ω}. For convenience we enrich the type system by the formation of finite sequences. So, our Types are ℕ, function types ρ → σ, product types ρ × σ, and finite sequences ρ^{∗}. We set ρ^{ω} :≡ ℕ → ρ. The level of a type is defined by level(ℕ) = 0, level(ρ × σ) = max(level(ρ), level(σ)), level(ρ^{∗}) = level(ρ), level(ρ → σ) = max(level(ρ) + 1, level(σ)). By o we will denote an arbitrary but fixed type of level 0, and by ρ, τ, σ arbitrary. The terms of our version of HA^{ω} are a suitable extension of the terms of Gödel’s system T [11] in lambda calculus notation. We use the variables i, j, k, l, m, n: ℕ; s, t: ρ^{∗}; α, β: ρ^{ω} unless the type of these variables is stated explicitly otherwise. Other letters will be used for different types in different contexts. By =^{τ} we denote equality of type τ for which we assume the usual equality axioms. However, equality between functions is not assumed to be extensional. We also do not assume decidability for =^{τ}, when level(τ) > 0. Type information will be frequently omitted, when it is irrelevant or inferable from the context. We let k^{ρ} denote the canonical lifting of a number k ∈ ℕ to type ρ, e.g. k^{ρ→σ} :≡ λx^{ρ}.k^{σ}. By an ∃-formula respectively ∀∃-formula we mean a formula of the form ∃y^{τ} B respectively ∀z^{σ} ∃y^{τ} B, where B is provably equivalent to an atomic formulaquantifier free and contains only decidable predicates. We will also use the following operations:

⟨x_{0}, …, x_{n−1}⟩ :≡ the finite sequence with elements x_{0}, …, x_{n−1}
|s| :≡ the length of s, i.e. |⟨x_{0}, …, x_{n−1}⟩| = n
s_{k} :≡ the k-th element of s provided k < |s|
s ∗ t :≡ the concatenation of s and t
s ∗ x :≡ s ∗ ⟨x⟩
s ∗ α :≡ appending α to s, i.e.
(s ∗ α)(k) = [if k<|s| then s_{k} else α(k−|s|)]
s @ α :≡ overwriting α with s, i.e.
(s @ α)(k) = [if k < |s| then s_{k} else α(k)]
s @ x :≡ s @ λk.x, i.e.

1Nonetheless, the realizers for the countable and dependent choice presented by the authors does not necessarily exist in M since continuity is assumed for the proof of the soundness of the interpretation.

(s @ x)(k) = [if k < |s| then s_{k} else x]
\overline{α}k :≡ ⟨α(0), …, α(k − 1)⟩
\overline{α, k} :≡ \overline{α}k @ λx.0
β ∈ \overline{α}k :≡ \overline{β}k = \overline{α}k.

Definition 2.1 Spector’s definition of bar recursion [24] reads in our notation as follows:

SBR_{ρ,τ} : Φ(s) =^{τ} \{ \begin{matrix}G(s) & if Y (s @ 0^{ρ}) <^{o} |s| \\ H(s, λx^{ρ}.Φ(s ∗ x)) & otherwise, \end{matrix}

where =^{τ} denotes equality of type τ and 0^{ρ} denotes the constant functional zero of type ρ.

In his thesis [16] Kohlenbach introduced the following kind of bar recursion which differs from Spector’s only in the stopping condition:

KBR_{ρ,τ} : Φ(s) =^{τ} \{ \begin{matrix}G(s) & if Y (s @ 0^{ρ}) =^{o} Y (s @ 1^{ρ}) \\ H(s, λx^{ρ}.Φ(s ∗ x)) & otherwise. \end{matrix}

Finally, we define modified bar recursion at type ρ:

MBR_{ρ} : Φ(s) =^{o} Y (s @ H(s, λx^{ρ}.Φ(s ∗ x))).

Instead of Φ(s) we should have written more precisely Φ(Y, G, H, s) in SBR_{ρ,τ}, KBR_{ρ,τ}, and Φ(Y, H, s) in MBR_{ρ} in order to make clear that these equations specify functionals Φ of the respective types

(ρ^{ω} → o) → (ρ^{∗} → τ) → (ρ^{∗} → (ρ → τ) → τ) → ρ^{∗} → τ
(ρ^{ω} → o) → (ρ^{∗} → τ) → (ρ^{∗} → (ρ → τ) → τ) → ρ^{∗} → τ
(ρ^{ω} → o) → (ρ^{∗} → (ρ → o) → ρ^{ω}) → ρ^{∗} → o

By SBR we mean ⋃_{τ,ρ} SBR_{ρ,τ} and the same applies to KBR and MBR. We say a model S satisfies one of the respective variants of bar recursion if in S (for any given types τ and ρ) a functional exists satisfying SBR_{ρ,τ}, KBR_{ρ,τ}, or MBR_{ρ} for all possible values of Y, G, H, s.

Recursive definitions similar to MBR occur in [2], and, in a slightly different form in [3] and [19] in connection with the fan functional (cf. section 4).

Remark 2.2 Note that in the definition of MBR it is inessential whether we use the operation @ (overwrite) or ∗ (concatenation). However it is essential that the type of Φ(s) is of level 0. If, for example, the type of Φ(s) were ℕ → ℕ we could set Y (α)(m) :≡^{o} α(m) + 1 and H(s, F)(k) :≡^{o} F (0)(|s| + 1), and obtain the equation

Φ(s)(m) =^{o} (s @ λk.Φ(s ∗ ⟨0⟩)(|s| + 1))(m) + 1

implying

Φ(⟨ ⟩)(0) = Φ(⟨0⟩)(1) + 1 = Φ(⟨0, 0⟩)(2) + 2 = …

which is inconsistent with HA^{ω}.

The structures of primary interest to interpret bar recursion are the model C of total continuous functionals of Kleene [14] and Kreisel [17], the model Ĉ of partial continuous functionals of Scott [22] and Ershov [9], and the model M of (strongly) majorizable functionals introduced by Howard [12] and Bezem [7].

Theorem 2.3 The models C and Ĉ satisfy all three variants of bar recursion.

Proof. In the model Ĉ all three forms of bar recursion can simply be defined as the least fixed points of suitable continuous functionals. For C we use Ershov’s result in [9] according to which the model C can be identified with the total elements of Ĉ. Therefore it suffices to show that all three versions of bar recursion are total in Ĉ. For Spector’s version this has been shown by Ershov [9], and for the other versions similar argument apply. For example, in order to see that Φ(s) defined recursively by MBR is total for given total Y, H and s one uses bar induction on the bar

P (s) :≡ Y (s @ ⊥_{ρ}) is total

where ⊥_{ρ} denotes the undefined element of type ρ. P (s) is a bar because Y is continuous. □

Theorem 2.4 ([7], [16]) M satisfies SBR but not KBR.

We show in section 5 that M satisfies MBR.

3 Using MBR to realize countable choice

The aim of this section is to show how modified bar recursion can be used to extract witnesses from proofs of Σ_{1}^{0}-formulas in classical arithmetic plus the axiom (scheme) of countable choice

AC ∀n ∃y A(n, y) → ∃f ∀n A(n, f(n)).

Actually we will need only the following weak modified bar recursion which is a special case of MBR where H is constant:

wMBR_{ρ} : Φ(s) =^{o} Y (s @ λk.H(s, λx.Φ(s ∗ x))).

Note that in wMBR the returning type of H is ρ, i.e., the argument of Y consists of s followed by an infinite sequence with constant value of type ρ.

Remark 3.1 In [4] the authors have shown how the same idea for the realizer of AC can be extended to give a realizer for the dependent choice [13]

DC ∀n ∀x ∃y A(n, x, y) → ∀x∃f (f(0) = x ∧ ∀n A(n, f(n), f(n + 1))).

3.1 Witnesses from classical proofs

The method we use to extract witnesses from classical proofs is a combination of Gödel’s negative translation (translation P^{o} in [18] page 42, see also [25]), the Dragalin/Friedman/Leivant trick, also called A-translation [27], and Kreisel’s (formalized) modified realizability [26]. The method works in general for proofs in PA^{ω}, the classical variant of HA^{ω}. In order to extend it to PA^{ω} plus extra axioms Γ (e.g. Γ ≡ DC) one has to find realizers for Γ^{N}, the negative translation of Γ^{2}, where ⊥ is replaced by an ∃-formula (regarding negation, ¬C, is defined by C → ⊥). However, it is more direct and technically simpler to follow [5] and combine the Dragalin/Friedman/Leivant trick and modified realizability: instead of replacing ⊥ by a ∃-formula we slightly change the definition of modified realizability by regarding y mr ⊥ as an (uninterpreted) atomic formula. More formally we define

y^{τ} mr_{τ} ⊥ :≡ P_{⊥}(y),

where P_{⊥} is a new unary predicate symbol and τ is the type of the witness to be extracted. Therefore, we have a modified realizability for each type τ, according to the type of the existential quantifier in the ∀∃-formula we are realizing. The other clauses of modified realizability are as usual, e.g.

f mr_{τ} (A → B) :≡ ∀x (x mr_{τ} A → fx mr_{τ} B).

In the following proposition Δ is an axiom system possibly containing P_{⊥} and further constants, which has the following closure property: If D ∈ Δ and B is a quantifier free formula with decidable predicates, then also the universal closure of D[λy^{τ} .B/P_{⊥}] is in Δ, where D[λy^{τ} .B/P_{⊥}] is obtained from D by replacing any occurrence of a formula P_{⊥}(L) in D by B[L/y].

Proposition 3.2 Assume that Φ is a closed term such that

HA^{ω} + Δ ⊢ Φ mr_{τ} Γ^{N}

Then from any proof of

PA^{ω} + Γ ⊢ ∀z^{σ} ∃y^{τ} B(z, y)

where ∀z^{σ} ∃y^{τ} B(z, y) is a ∀∃-formula in the language of HA^{ω}, one can extract a closed term M^{σ→τ} such that

HA^{ω} + Δ ⊢ ∀z B(z, Mz).

Proof. The proof is folklore. The main steps are as follows. Assuming w.l.o.g. that B(z, y) is atomic (P_{⊥} does not occur in B(z, y)) we obtain from PA^{ω} + Γ ⊢ ∀z^{σ} ∃y^{τ} B(z, y) via negative translation

HA^{ω} + Γ^{N} ⊢_{m} ∀y (B(z, y) → ⊥) → ⊥

where ⊢_{m} denotes derivability in minimal logic, i.e. ex-falso-quodlibet is not used. Now, soundness of modified realizability (which holds for our abstract version of modified realizability and minimal logic [5]), together with the assumption on Φ allows us to extract from this proof a closed term M such that

2The negative translation double-negates atomic formulas, replaces ∃x by ¬∀x¬ and A ∨ B by ¬(¬A ∧ ¬B).

HA^{ω} + Δ ⊢ Mz mr_{τ} (∀y (B(z, y) → ⊥) → ⊥)

i.e.

HA^{ω} + Δ ⊢ ∀f^{o→o} (∀y (B(z, y) → P_{⊥}(fy)) → P_{⊥}(Mzf)).

Replacing P_{⊥} by λy.B(z, y) (remember the closure property of Δ) and instantiating f by the identity function we conclude

HA^{ω} + Δ ⊢ ∀z B(z, Mz(λy.y)). □

We will apply this proposition with τ :≡ o (and therefore we write just mr instead of mr_{o}), Γ :≡ DC, or Γ :≡ AC (countable choice, see below), and an axiom system Δ consisting of MBR (the defining equations), where the defined functional Φ is a new constant, together with the axiom

Continuity ∀F^{ρ^{ω}→o}, α ∃n ∀β (\overline{α}n = \overline{β}n → F (α) = F (β))

(we call any n such that ∀β (\overline{α}n = \overline{β}n → F (α) = F (β)) a point of continuity of F at α), and the following schema of

Relativized quantifier free pointwise bar induction

∀α ∈ S ∃n P (\overline{α}n) ∧ ∀s ∈ S (∀x [S(x, |s|) → P (s ∗ x)] → P (s)) → P (⟨⟩)

where S(x, n) is arbitrary, P (s) is quantifier free, and α ∈ S, s ∈ S are shorthands for ∀n S(α(n), n) and ∀i < |s| S(s_{i}, i), respectively. Clearly the condition on Δ in Proposition 3.2 is satisfied. This is similar to Luckhardt’s higher bar induction over species, (hBI)_{D}^{ρ} ([18], page 144). ^{3}

In order to make sure that realizers can indeed be used to compute witnesses one needs to know that, 1. the axioms of HA^{ω} + Δ hold in a suitable model – we can choose the model C of continuous functionals – and, 2. every closed term of type level 0 (e.g. of type ℕ) can be reduced to a numeral in an effective and provably correct way. In [2] this is solved by building the notion of reducibility to normal form into the definition of realizability. In our case we solve this problem by applying Plotkin’s adequacy result [20] as follows: each term in the language of HA^{ω} plus the bar recursive constants can be naturally viewed as a term in the language PCF [20], by defining the bar recursors by means of the general fixed point combinator. In this way our term calculus also inherits PCF’s call-by-name reduction, i.e. if M is bar recursive and M reduces to M′ then M′ is bar recursive. Furthermore reduction is provably correct in our system, i.e. if M reduces to M′ then M = M′ is provable. Now let M be a closed term of type ℕ. By Theorem 2.3 M has a total value, which is a natural number n, in the model of partial continuous functionals. Hence, by Plotkin’s adequacy theorem M reduces to the numeral denoting n.

3.2 Realizing AC^{N}

We now construct a realizer of the classical (i.e. negatively translated) axiom of countable choice,

AC^{N} ∀n (∀y (A(n, y)^{N} → ⊥) → ⊥) → ∀f (∀n A(n, f(n))^{N} → ⊥) → ⊥.

3The verification of the realizer for DC makes use of (aBI)_{D}^{ρ} ([18], page 144). (cf. [4])

Following Spector [24] we reduce AC^{N} to the double negation shift

DNS ∀n ((B(n) → ⊥) → ⊥) → (∀n B(n) → ⊥) → ⊥

observing that AC + DNS ⊢_{m} AC^{N}, where DNS is used with the formula B(n) :≡ ∃y A(n, y)^{N}. Therefore it suffices to show that this instance of DNS is realizable. The following lemma, whose proof is trivial, is necessary to see that the weak form of modified bar recursion wMBR suffices in the interpretation of AC and DC.

Lemma 3.3 Let B be a formula such that all of its atomic sub-formulas occur in negated form. Then there is a closed term H such that ∀z⃗ H mr (⊥ → B) is provable (in minimal logic), where z⃗ are the free variables of B (it is important here that H is closed, i.e. does not depend on z⃗).

Note that the formula B(n) :≡ ∃y A(n, y)^{N} to which we apply DNS is of the form specified in Lemma 3.3.

Theorem 3.4 The double negation shift DNS for a formula B(n) is realizable using wMBR provided B(n) is of the form specified in Lemma 3.3.

Proof. In order to realize the formula

∀n((B(n) → ⊥) → ⊥) → (∀nB(n) → ⊥) → ⊥

we assume we are given realizers

Y^{ρ^{ω}→o} mr (∀nB(n) → ⊥)
G^{ℕ→(ρ→o)→o} mr ∀n((B(n) → ⊥) → ⊥)

and try to build a realizer for ⊥. Using wMBR we define

Ψ(s) = Y (s @ λn.H(G(|s|, λx^{ρ}.Ψ(s ∗ x))))

where H^{o→ρ} is a closed term such that ∀n H mr (⊥ → B(n)) is provable, according to Lemma 3.3. We set

S(x, n) :≡ x mr B(n),
P (s) :≡ Ψ(s) mr ⊥,

and, by quantifier free pointwise bar induction relativized to S, we show P (⟨ ⟩), i.e. Ψ(⟨ ⟩) mr ⊥.

i) ∀α ∈ S ∃n P (\overline{α}n). Let α ∈ S be fixed, and let n be the point of continuity of Y at α, according to the continuity axiom. By assumptions on α and Y we get ∀β (Y (\overline{α}n @ β) mr ⊥), which implies Ψ(\overline{α}n) mr ⊥.

ii) ∀s ∈ S(∀x [S(x, |s|) → P (s ∗ x)] → P (s)). Let s ∈ S be fixed. Suppose ∀x [S(x, |s|) → P (s ∗ x)], i.e. ∀x [x mr B(|s|) → Ψ(s ∗ x) mr ⊥], or in another words

λx^{ρ}.Ψ(s ∗ x) mr (B(|s|) → ⊥).

Using the assumption on G we obtain

G(|s|, λx^{ρ}.Ψ(s ∗ x)) mr ⊥,

and from that, setting w :≡^{ρ} H(G(|s|, λx^{ρ}.Ψ(s ∗ x))), we obtain w mr B(n), for all n. Because s ∈ S it follows that s @ λn.w mr ∀n B(n) and therefore

Y (s @ λn.w) mr ⊥.

Since Ψ(s) = Y (s @ λn.w) we have P (s). □

As explained above Theorem 3.4 yields

Corollary 3.5 The negative translation of the countable axiom of choice, AC^{N} is realizable using wMBR.

4 Bar recursion and the fan functional

A functional Ψ^{(ℕ^{ω}→o)→ℕ} is called fan functional if it computes a modulus of uniform continuity for every continuous functional Y^{ℕ^{ω}→o} restricted to infinite 0, 1-sequences, i.e.

FAN(Ψ) :≡ ∀Y; α, β ≤ λx.1(\overline{α}(Ψ(Y)) = \overline{β}(Ψ(Y)) → Y α =^{o} Y β)

(note that ρ = ℕ here). A recursive fan functional which is presented [3] and [19] uses two procedures,

Φ(s, v) = s @ [if Y (Φ(s ∗ 0, v)) ≠ v then Φ(s ∗ 0, v) else Φ(s ∗ 1, v)]  (1)

Ψ(Y, s) =^{ℕ} \{ \begin{matrix}0 & if Y (α) = Y (s @ 0), \\ & where α = Φ(s, Y (s @ 0)) \\ 1 + max\{Ψ(Y, s ∗ 0), Ψ(Y, s ∗ 1)\} & otherwise. \end{matrix} (2)

The first functional, Φ(s, v), returns an infinite path α having s as a prefix, such that Y (s @ α) ≠ v, if such a path exists, and returns s extended by λx.1, otherwise, i.e. if Y is constant v on all paths extending s. The second functional, Ψ(Y, s), returns the maximum point of continuity for Y on all extension of s. We show that the functional λY.Ψ(Y, ⟨ ⟩) is a fan functional and is primitive recursive in MBR and KBR. The proof of the following two lemmas (which can be formalized in HA^{ω}+ rBI) can be found in [4].

Lemma 4.1 MBR is equivalent to

Φ(s^{ρ^{∗}}) =^{ρ^{ω}} s @ H(s, λt^{ρ^{∗}}λx^{ρ}.Y^{ρ^{ω}→o}(Φ(s ∗ t ∗ x))).  (3)

Lemma 4.2 KBR is equivalent to,

Φ(s) =^{τ} \{ \begin{matrix}G(s) & if Y (s @ 0^{ρ}) =^{o} Y (s @ J(s)) \\ H(s, λx^{ρ}.Φ(s ∗ x)) & otherwise, \end{matrix}  (4)

where the new parameter J is of type ρ^{∗} → ρ^{ω} and, as usual, Φ(s) is shorthand for the more accurate Φ(Y, G, H, J, s).

Theorem 4.3 The functional λY.Ψ(Y, ⟨ ⟩) is primitive recursively definable in MBR and KBR together.

Proof. We show that procedures Φ and Ψ satisfying the equations (1) and (2) respectively can be defined using MBR and KBR.

For defining the functional Φ(s, v) we use equation (3) of Lemma 4.1.

Φ(s, v) =^{o^{ω}} s @ H(s, v, λtλx.Y (Φ(s ∗ t ∗ x)))

where H is defined by course of value primitive recursion as

H(s, v, F)(n) =^{o} \{ \begin{matrix}s_{n} & if n < |s| \\ 0 & if n ≥ |s| ∧ F (c, 0) ≠ v \\ 1 & if n ≥ |s| ∧ F (c, 0) = v, \end{matrix}

with c :≡ ⟨H(s, v, F)(|s|), …, H(s, v, F)(n − 1)⟩. Clearly Φ satisfies equation (1) at all n < |s|. For n ≥ |s| we first observe that

Φ(s, v)(n) =^{o} \{ \begin{matrix}0 & if Y (Φ(s ∗ c_{s,n} ∗ 0, v)) ≠ v \\ 1 & if Y (Φ(s ∗ c_{s,n} ∗ 0, v)) = v, \end{matrix}

where c_{s,n} :≡ ⟨Φ(s, v)(|s|), …, Φ(s, v)(n − 1)⟩. Now if Y (Φ(s ∗ 0, v)) ≠ v then Φ(s, v)(|s|) = 0 and therefore s ∗ c_{s,n} = s ∗ 0 ∗ c_{s∗0,n}. Hence Φ(s, v)(n) = Φ(s ∗ 0, v)(n) as required by (1). The case Y (Φ(s ∗ 0, v)) = v is similar.

One immediately sees that a functional Ψ satisfying (2) can be defined from an instance of equation (4) using the functional Φ above. □

Theorem 4.4 λY.Ψ(Y, ⟨ ⟩) is a fan functional.

Proof. See [3] and [19]. □

Remark 4.5 Kohlenbach [16] has shown that KBR is primitive recursively definable in SBR and μ̂ (where μ̂ is the functional defined as,

μ̂(Y, α) :≡ min k [Y (\overline{α}k ∗ 0) = Y (\overline{α}k ∗ 1)]).

Since in section 6 we show that MBR defines SBR primitive recursively, we can indeed say that FAN is primitive recursively definable in MBR + μ̂.

5 Modified bar recursion and the model M

The model M (= ⋃ M_{ρ}) of strongly majorizable functionals (introduced in [7] as a variation of Howard’s majorizable functionals [12]) and the strongly majorizability relation s-maj_{ρ} ⊆ M_{ρ} × M_{ρ} are defined by induction on types as follows:

n s-maj_{o} m :≡ n ≥ m, M_{o} :≡ ℕ,
F^{∗} s-maj_{ρ→τ} F :≡ F^{∗}, F ∈ M_{ρ} → M_{τ} ∧

∀G^{∗}, G ∈ M_{ρ} [G^{∗} s-maj_{ρ} G → F^{∗}G^{∗} s-maj_{τ} F^{∗}G, F G],

M_{ρ→τ} :≡ {F ∈ M_{ρ} → M_{τ} : ∃F^{∗} ∈ M_{ρ} → M_{τ} F^{∗} s-maj_{ρ→τ} F }.

In the following we abbreviate s-maj_{ρ} by maj_{ρ} and by “majorizable” always mean “strongly majorizable”. We often omit the type in the relation maj_{ρ}.

In [16] it is shown that KBR is provably not primitive recursively definable from SBR, since SBR yields a well defined functional in the model of (strongly) majorizable functionals M (cf. [7]) and KBR does not (in the following we will by “majorizable” always mean “strongly majorizable”). SBR, however, can be primitive recursively defined from KBR (cf. [16]).^{4} In this section we show that a functional satisfying MBR exists in M. We first show that there exists a functional ^{5}

Φ : M_{ρ^{ω}→o} × M_{ρ^{∗}×(ρ→o)→ρ^{ω}} × M_{ρ^{∗}} → M_{o}

satisfying MBR, then we show that any such Φ has a majorant and therefore belongs to M.

Most of our results in this section rely on Lemma 5.2 which can be viewed as a weak continuity property of functionals Y (of type ρ^{ω} → o) in M. It says that a bound on the value of Y (α) can be determined from an initial segment of α. For the rest of this section all variables (unless stated otherwise) are assumed to range over the type structure M.

Lemma 5.1 ([7], 1.4, 1.5) Let max^{ρ} be inductively defined as,

max_{i≤n}^{o}m_{i} :≡ max{m_{0}, …, m_{n}},

max_{i≤n}^{τ→ρ}X_{i} :≡ λY^{τ} . max_{i≤n}^{ρ}X_{i} Y,

and for α^{ρ^{ω}}, define α^{+}(n) :≡ max_{i≤n}^{ρ}α(i). Then,

∀n(α(n) maj β(n)) → α^{+} maj β^{+}, β.

We also use addition in all types, which is done pointwise, e.g. if x, y are of type τ → ρ then x +_{τ→ρ} y :≡ λz^{τ} (x(z) +_{ρ} y(z)).

Lemma 5.2 (Weak continuity for M) ∀Y^{ρ^{ω}→ℕ}, α ∃n^{ℕ} ∀β ∈ \overline{α}n (Y (β) ≤ n).

Proof. Let Y and α be fixed, α^{∗} maj α and Y^{∗} maj Y. From the assumption

(a) ∀n ∃β ∈ \overline{α}n(Y (β) > n)

we derive a contradiction. For any n, let β_{n} be the function whose existence we are assuming in (a). Let

β_{n}^{∗}(i) :≡ \{ \begin{matrix}0^{ρ} & i < n \\ [β_{n}(i)]^{∗} & i ≥ n, \end{matrix}

where [β_{n}(i)]^{∗} denotes some majorant of β_{n}(i). Having defined the functional β_{n}^{∗} we note two of its properties,

i) ∀i < n(β_{n}^{∗}(i) = 0^{ρ}),

ii) (α^{∗} +_{ρ^{ω}} β_{n}^{∗})^{+} maj β_{n}. (by Lemma 5.1)

4For the rest of the paper “s_{1} is primitive recursively definable in s_{2}” should be understood as “there exists a closed term t such that E-HA^{ω} ⊢ s_{1} = t(s_{2})”

5By M_{ρ} → M_{τ} we mean an arbitrary function from M_{ρ} to M_{τ}. By M_{ρ→τ} we mean a functional from M_{ρ} to M_{τ} which belongs to M.

Consider the functional α̂ defined as, α̂(n) :≡ α^{∗}(n) +_{ρ} ∑_{i∈ℕ} β_{i}^{∗}(n). Since at each point n only finitely many β_{i}^{∗} are non-zero, α^{∗} is well defined. Let Y^{∗}(α̂^{+}) = m. Note that α̂^{+} maj β_{i}, for all i ∈ ℕ, and from (a) we should have m < Y (β_{m}) ≤ m, a contradiction. □

We extend, for convenience, the definition of majorizability for finite sequences as follows:

s^{∗} maj_{ρ^{∗}} s :≡ ⟨s^{∗} ∗ λk.s_{|s^{∗}|−1}^{∗}, |s^{∗}|⟩ maj ⟨s ∗ λk.s_{|s|−1}, |s|⟩,

(s^{∗} and s not begin the empty sequence) where ⟨α, m⟩ maj ⟨β, n⟩ stands for α maj β ∧ m ≥ n. For the special case when one of the sequences is empty we set, s^{∗} maj ⟨ ⟩ if s^{∗} maj s^{∗}. Moreover, ⟨ ⟩ majorizes only itself.

5.1 Finding Φ ∈ M_{ρ^{ω}→o} × M_{ρ^{∗}×(ρ→o)→ρ^{ω}} × M_{ρ^{∗}} → M_{o} satisfying MBR

For any type ρ, the elements s of M_{ρ^{∗}} (finite sequences of elements in ρ) can be viewed as nodes of an infinite tree which we call T. The infinite paths of T are the elements of M_{ρ^{ω}} (which is just M_{ρ}^{ω} as shown in [7]). For fixed Y and H, the functional Φ we are looking for should assign values to the nodes of T according to MBR. For each node s the set of nodes s′ extending s is denoted by B_{s}.

Let Y, H ∈ M be fixed. We show that at each infinite path α there exists a point n such that a functional Φ_{α,n} : M_{ρ^{∗}} → M_{o} can be defined satisfying MBR for all s ∈ B_{\overline{α}n}. Then, by bar induction, a functional Φ can be defined for all nodes of T.

Let α ∈ M_{ρ}^{ω} be fixed, n the number whose existence is stated in Lemma 5.2, and K :≡ {0, 1, …, n}. We show how to define a functional Φ_{α,n}(s) such that, for s ∈ B_{\overline{α}n}, equation

Φ_{α,n}(s) = Y (s @ H(s, λx.Φ_{α,n}(s ∗ x)))

holds. Here we note that, for s ∈ B_{\overline{α}n}, by Lemma 5.2, Φ_{α,n}(s) must belong to the finite set K. Therefore, for those s ∈ B_{\overline{α}n}, what we have is an instance of the more general equation,

(∗) Ψ(s) = G(s, λx.Ψ(s ∗ x)),

where Img(G) ⊆ K (K as above). To see that modified bar recursion becomes an instance of (∗), let

G(s, F) :≡ Y (\overline{α}n ∗ s @ H(\overline{α}n ∗ s, F)),

and, clearly, Img(G) = Img(λsλF.Y (\overline{α}n ∗ s @ H(\overline{α}n ∗ s, F))) ⊆ K. Hence, it suffices to show that equations of the form (∗) (with the mentioned restriction on G) always have a solution Ψ. That is what we will do now.

Consider the set T = T → 2^{K}\{∅}. The set T can be viewed as the set of labelled trees whose labels range over non-empty subsets of K. We define a partial order ⊑ on T as follows (for f, g ∈ T )

f ⊑ g :≡ ∀s (f(s) ⊆ g(s)).

Finally, we define an operation χ : T → T ,

χ(f)(s) :≡ Img(λF ∈ Cons_{s}^{f}.G(s, F)),

where Cons_{s}^{f} :≡ {F : ∀x^{ρ}.F (x) ∈ f(s ∗ x)}. We first observe the following.

Lemma 5.3 (T , ⊑) is a directed complete semi-lattice.

Proof. Let S be a directed subset of T . Since we assign non-empty finite sets to the nodes of T, it is easy to see that ⋂ S belongs to T and it is smaller than any element in S. □

Lemma 5.4 χ : T → T is monotone.

Proof. Let f ⊑ g and s be fixed. We get that Cons_{s}^{f} ⊆ Cons_{s}^{g}, which implies χ(f)(s) ⊆ χ(g)(s). □

By the Knaster-Tarski fixed point theorem we obtain an f ∈ T such that χ(f) = f, i.e. f(s) = Img(λF ∈ Cons_{s}^{f}.G(s, F)), for all s. Let χ_{f,s}^{−1} be a functional from the set f(s) to Cons_{s}^{f} such that c = G(s, χ_{f,s}^{−1}(c)), for all c ∈ f(s). Define the functional Ψ(s) recursively as follows,

Ψ(⟨ ⟩) :≡ arbitrary element of f(⟨ ⟩);

Ψ(s ∗ x) :≡ χ_{f,s}^{−1}(Ψ(s))(x).

Lemma 5.5 The functional Ψ is total and satisfies equation (∗).

Proof. We have just shown that Ψ is total. Moreover, note that, for all s, the values assigned to Ψ(s ∗ x) are such that Ψ(s) = G(s, λx.Ψ(s ∗ x)). □

Corollary 5.6 There exists a functional

Φ : M_{ρ^{ω}→o} × M_{ρ^{∗}×(ρ→o)→ρ^{ω}} × M_{ρ^{∗}} → M_{o}

satisfying modified bar recursion.

5.2 Finding a majorant for Φ

Now we show that Φ (from corollary above) has a majorant, and therefore belongs to M.

Lemma 5.7 Let s^{∗} and s s.t. |s^{∗}| = |s| be fixed. If s^{∗} maj s then

∀β ∈ s∃β^{∗} ∈ s^{∗} (β^{∗} maj β).

Proof. Let s^{∗}, s and β ∈ s be fixed. Moreover, assume |s^{∗}| = |s| = n and s^{∗} maj s. Define β^{∗} as,

β^{∗}(i) :≡ \{ \begin{matrix}s_{i}^{∗} & if i < n \\ max^{ρ}\{max_{j<i}^{ρ}β^{∗}(j), [β(i)]^{∗}\} & otherwise, \end{matrix}

where [β(i)]^{∗} is some majorant of β(i). First note that, for all i, β^{∗}(i) maj β(i). We show that β^{∗} maj β. Let k ≥ i.

If k < n then β^{∗}(k) = s_{k}^{∗} maj s_{i}^{∗} maj s_{i} = β(i).

If k ≥ n then β^{∗}(k) = max^{ρ}{max_{j<k}^{ρ}β^{∗}(j), [β(k)]^{∗}} maj β^{∗}(i) maj β(i). □

In the following we shall make use of two functionals Ω and Γ which we define now. The functional Ω was first introduced in [15], 3.40.

Lemma 5.8 ([15], 3.41) Define functionals min^{ρ} (from non-empty sets X ⊆ M_{ρ} to elements of M_{ρ}) and Ω : M_{ρ} → M_{ρ} as

min^{ℕ}X :≡ min X, for ∅ ≠ X ⊆ ℕ,
min^{ρ→τ} X :≡ λy^{ρ}. min^{τ} {F y : F ∈ X}, for ∅ ≠ X ⊆ M_{ρ→τ},
Ω(F) :≡ min^{ρ}{F^{∗} : F^{∗} maj F }.

Then,

i) For all F, Ω(F) maj F,

ii) Ω maj Ω. (Therefore, Ω ∈ M.)

Lemma 5.9 Define Γ : M_{ρ^{ω}→ℕ} → M_{ρ^{ω}} → M_{ℕ} as,

Γ(Y)(α) :≡ min n [∀β ∈ \overline{α}n(Ω(Y)(β) ≤ n)].

Then,

i) Γ(Y) maj Y,

ii) Γ(Y) is continuous and Γ(Y)(α) is a point of continuity for Γ(Y) on α,

iii) Γ maj Γ. (therefore, Γ ∈ M)

Proof. First of all, we note that, by Lemma 5.2, the functional Γ is well defined. By Lemma 5.8 (i), Ω(Y) maj Y.

i) Let α^{∗} maj α. We have to show Γ(Y)(α^{∗}) ≥ Γ(Y)(α), Y (α). By the definition of Γ(Y), and Lemma 5.8 (i), we have Γ(Y)(α^{∗}) ≥ Ω(Y)(α^{∗}) ≥ Y (α). It is only left to show that Γ(Y)(α^{∗}) ≥ Γ(Y)(α). Suppose that n = Γ(Y)(α^{∗}) < Γ(Y)(α) = m. Note that there exists a β ∈ \overline{α}(m − 1) such that Ω(Y)(β) ≥ m (otherwise we get a contradiction to the minimality in the definition of Γ(Y)). But since m > n, by Lemma 5.7, there exists a β^{∗} ∈ \overline{α^{∗}}n such that β^{∗} maj β. Therefore, Ω(Y)(β^{∗}) ≤ n < m ≤ Ω(Y)(β). But by Lemma 5.8 (i) also Ω(Y)(β^{∗}) ≥ Ω(Y)(β), a contradiction.

ii) Let α be fixed and take n = Γ(Y)(α). Suppose there exists a β ∈ \overline{α}n such that Γ(Y)(β) ≠ n. If Γ(Y)(β) < n we get, since α ∈ \overline{β}n, that Γ(Y)(α) < n, a contradiction. Suppose Γ(Y)(β) > n. Since β ∈ \overline{α}n we have, ∀γ ∈ \overline{β}n(Ω(Y)(γ) ≤ n), also a contradiction.

iii) Assume Y^{∗} maj Y and α^{∗} maj α. We show Γ(Y^{∗})(α^{∗}) ≥ Γ(Y)(α). By the self majorizability of Γ(Y) we have Γ(Y)(α^{∗}) ≥ Γ(Y)(α). We now show Γ(Y^{∗})(α^{∗}) ≥ Γ(Y)(α^{∗}). Let n = Γ(Y^{∗})(α^{∗}) and suppose m = Γ(Y)(α^{∗}) > n. By the definition of Γ(Y), there exists a β ∈ \overline{α^{∗}}(m − 1) s.t. Ω(Y)(β) ≥ m. But, since m > n, by Lemma 5.7, there exists a β^{∗} ∈ \overline{α^{∗}}n s.t. β^{∗} maj β, and by Lemma 5.8 (ii), Ω(Y^{∗})(β^{∗}) ≥ m > n, a contradiction. □

Lemma 5.10 Let Y^{∗} maj Y (of type ρ^{ω} → ℕ) and α be fixed, and n = Γ(Y^{∗})(α). If \overline{α}n maj s and |s| = n then for all sequences β we have

Γ(Y^{∗})(s @ β), Γ(Y)(s @ β), Y (s @ β) ≤ n.

Proof. We prove just that Γ(Y^{∗})(s @ β) ≤ n. The other two cases follow similarly. Suppose there exists a β such that n < Γ(Y^{∗})(s @ β). Since \overline{α}n maj s, by Lemma 5.7, there exists a β^{∗} such that \overline{α}n ∗ β^{∗} maj s @ β. Therefore, by Lemma 5.9 (iii), we must have n < Γ(Y^{∗})(\overline{α}n ∗ β^{∗}). And by the fact that n is a point of continuity for Γ(Y^{∗}) on α we get Γ(Y^{∗})(\overline{α}n ∗ β^{∗}) = n, a contradiction. □

In the following we extend the (·)^{+} operator of Lemma 5.1 for functionals F of type ρ^{∗} → ℕ as

F^{+} :≡ λs. max_{s′≺s} F (s′),

where s′ ≺ s :≡ |s′| ≤ |s| ∧ ∀i < |s′| (s′_{i} = s_{i}).

Lemma 5.11 Let F and G be of type ρ^{∗} → ℕ. If

∀s^{∗}, s [s^{∗} maj s ∧ |s^{∗}| = |s| → F (s^{∗}) ≥ F (s), G(s)]

then F^{+} maj G^{+}, G.

Proof. Let s^{∗} maj s be fixed. For all prefixes t^{∗} (of s^{∗}) and t (of s) of the same length, by the assumption of the lemma, we have F (t^{∗}) ≥ F (t), G(t). Therefore,

max_{s′≺s^{∗}} F (s′) ≥ max_{s′≺s} F (s′), max_{s′≺s} G(s′).

Therefore, F^{+} maj G^{+}, G. □

Theorem 5.12 If Φ is a functional of type

M_{ρ^{ω}→ℕ} × M_{ρ^{∗}×(ρ→ℕ)→ρ^{ω}} × M_{ρ^{∗}} → M_{ℕ},

which for any given Y, H, s ∈ M (of appropriate types) satisfies MBR, then Φ ∈ M.

Proof. Our proof is based on the proof of the main result of [7]. The idea is that, if Φ satisfies MBR then the functional

Φ^{∗} :≡ λY, H.[λs.Φ(Ŷ , Ĥ, s)]^{+} maj Φ,

where

Ŷ (α) :≡ Γ(Y)(α^{+}) and
Ĥ(s, F) :≡ H(s, λx.F ({x}_{s})),

and {x}_{s} abbreviates max^{ρ}{max_{i<|s|}^{ρ}s_{i}, x} . Let Y^{∗} maj Y and H^{∗} maj H be fixed. The

fact that Φ^{∗} maj Φ follows from,

[λs.Φ(Ŷ^{∗}, Ĥ^{∗}, s)]^{+} maj [λs.Φ(Ŷ , Ĥ, s)]^{+}, λs.Φ(Y, H, s),

which follows, by Lemma 5.11, from ∀s^{∗} P (s^{∗}) where (For the rest of the proof s^{∗} maj s is a shorthand for s^{∗} maj s ∧ |s^{∗}| = |s|, i.e. majorizability is only considered for sequences of equal length.)

P (s^{∗}) :≡ ∀s [s^{∗} maj s → Φ(Ŷ^{∗}, Ĥ^{∗}, s^{∗}) ≥ Φ(Ŷ^{∗}, Ĥ^{∗}, s), Φ(Ŷ , Ĥ, s), Φ(Y, H, s)].

We prove ∀s^{∗} P (s^{∗}) by bar induction: i) ∀α∃n P (\overline{α}n). Let α be fixed and n :≡ Ŷ^{∗}(α) = Γ(Y^{∗})(α^{+}). If \overline{α}n does not majorize any sequence s we are done. Let s be such that \overline{α}n maj s. Note that \overline{α^{+}}n = \overline{(\overline{α}n @ β)^{+}}n, for all β. Therefore, by Lemma 5.9 (ii) and our assumption that Φ satisfies MBR we get Φ(Ŷ^{∗}, Ĥ^{∗}, \overline{α}n) = n. Since \overline{α^{+}}n maj \overline{(s @ β)^{+}}n (for all β), by Lemma 5.10, we have n ≥ Φ(Ŷ^{∗}, Ĥ^{∗}, s), Φ(Ŷ , Ĥ, s), Φ(Y, H, s). ii) ∀s^{∗}(∀x P (s^{∗} ∗ x) → P (s^{∗})). Let s^{∗} be fixed. Assume that ∀x P (s^{∗} ∗ x), i.e.

∀x, s [s^{∗} ∗ x maj s → Φ(Ŷ^{∗}, Ĥ^{∗}, s^{∗} ∗ x) ≥ Φ(Ŷ^{∗}, Ĥ^{∗}, s), Φ(Ŷ , Ĥ, s), Φ(Y, H, s)]. Note that if s^{∗} does not majorize any sequence we are again done. Assume s is such that s^{∗} maj s. If x^{∗} maj x then (by ∀x P (s^{∗} ∗ x)),

\underbrace{Φ(Ŷ^{∗}, Ĥ^{∗}, s^{∗} ∗ \{x^{∗}\}_{s^{∗}})}_{≡: Φ_{1}(\{x^{∗}\}_{s^{∗}})} ≥ \underbrace{Φ(Ŷ^{∗}, Ĥ^{∗}, s ∗ \{x\}_{s})}_{≡: Φ_{2}(\{x\}_{s})}, \underbrace{Φ(Ŷ , Ĥ, s ∗ \{x\}_{s})}_{≡: Φ_{3}(\{x\}_{s})}, \underbrace{Φ(Y, H, s ∗ x)}_{≡: Φ_{4}(x)} .

and also Φ_{1}({x^{∗}}_{s^{∗}}) ≥ Φ_{1}({x}_{s^{∗}}), which implies

λx.Φ_{1}({x}_{s^{∗}}) maj λx.Φ_{2}({x}_{s}), λx.Φ_{3}({x}_{s}), λx.Φ_{4}(x), and by the definition of majorizability

\underbrace{H^{∗}(s^{∗}, λx.Φ_{1}(\{x\}_{s^{∗}}))}_{Ĥ^{∗}(s^{∗},λx.Φ_{1}(x))} maj \underbrace{H^{∗}(s, λx.Φ_{2}(\{x\}_{s}))}_{Ĥ^{∗}(s,λx.Φ_{2}(x))}, \underbrace{H(s, λx.Φ_{3}(\{x\}_{s}))}_{Ĥ(s,λx.Φ_{3}(x))}, H(s, λx.Φ_{4}(x)),

which implies

(s^{∗} @ Ĥ^{∗}(s^{∗}, λx.Φ_{1}(x)))^{+} maj (s @ Ĥ^{∗}(s, λx.Φ_{2}(x)))^{+},
(s @ Ĥ(s, λx.Φ_{3}(x)))^{+},
s @ H(s, λx.Φ_{4}(x)).

And finally, by Lemma 5.9 (i) and (iii), (Φ(Ŷ^{∗}, Ĥ^{∗}, s^{∗}) =)

Ŷ^{∗}(s^{∗} @ Ĥ^{∗}(s^{∗}, λx.Φ_{1}(x))) ≥ Ŷ^{∗}(s @ Ĥ^{∗}(s, λx.Φ_{2}(x))), (= Φ(Ŷ^{∗}, Ĥ^{∗}, s))
Ŷ (s @ Ĥ(s, λx.Φ_{3}(x))), (= Φ(Ŷ , Ĥ, s))
Y (s @ H(s, λx.Φ_{4}(x))). (= Φ(Y, H, s))

□ Corollary 5.13 There exists a Φ ∈ M (not unique) satisfying MBR. Proof. In section 5.1 we have constructed a

Φ ∈ M_{ρ^{ω}→o} × M_{ρ^{∗}→(ρ→o)→ρ^{ω}} × M_{ρ^{∗}} → M_{o} satisfying MBR. By Theorem 5.12, Φ ∈ M. The fact that Φ is not unique follows by taking, e.g.,

F (α) = \{ \begin{matrix}1 & if α = λx.1 \\ 0 & otherwise, \end{matrix} which means that the sets Set_{s}^{σ} (cf. section 5.1) will not be singletons. □ Corollary 5.14 KBR is not primitive recursively definable in MBR.

6 Defining SBR primitive recursively in MBR

Assuming we have a term t satisfying MBR we build a term t′ (primitive recursively in t) which satisfies SBR.

Definition 6.1 μ̃(Y, α^{ρ^{ω}}, k) :≡ min n ≥ k [Y (\overline{α, n}) < n].

Kohlenbach [16] has shown that μ̃ is primitive recursively definable in SBR.

Theorem 6.2 μ̃ is primitive recursively definable in MBR.

Proof. Let n be the value of μ̃(Y, α, k). The case when n = k is simple and will be treated at the end of the proof. We will assume that n > k. In this case we note that, by the minimality condition, Y (\overline{α, n − 1}) ≥ n − 1. Hence, Y (\overline{α, n − 1}) + 1 can be used (for bounded search) as an upper bound for the value of n. Using MBR, in order for Y to return the required upper bound we have to give as input the sequence \overline{α, n − 1}. We show how this sequence can be computed by an appropriate H (in the definition of MBR). By MBR we can define a Φ_{α} satisfying Φ_{α}(s) = Y (s @ (\overline{α, m − 1})), where,

(∗) m =^{o} \{ \begin{matrix}|s| + 1 & if Y (\overline{α, |s| + 1}) < |s| + 1 \\ μ̃^{b}(Y, α, k, Φ_{α}(s ∗ α(|s|)) + 1) & otherwise, \end{matrix}

and μ̃^{b} is the bounded version of μ̃ (which is primitive recursive). We then define,

μ̃(Y, α, k) :≡ \{ \begin{matrix}k & if Y (\overline{α, k}) < k \\ μ̃^{b}(Y, α, k, Φ_{α}(\overline{α}k) + 1) & otherwise. \end{matrix}

We show that this is a good definition of μ̃ by showing that Φ_{α}(\overline{α}k) + 1 is a good upper bound on the value of μ̃(Y, α, k) (assume this value is n > k). In fact, we show by induction on j that, for k ≤ j < n, n is bounded by Φ_{α}(\overline{α}j) + 1.

i) j = n − 1. We see that the first case of (∗) will be satisfied, m is equal n and Φ_{α}(\overline{α}j) + 1 = Y (\overline{α}j @ (\overline{α, m − 1})) + 1 = Y (\overline{α, n − 1}) + 1 ≥ n.

ii) j < n−1. By induction hypothesis Φ_{α}(\overline{α}j∗α(j))+1 is a bound for n. Therefore, m (see second case of (∗)) has value n, and as above we get Φ_{α}(\overline{α}j) + 1 ≥ n. □

Theorem 6.3 SBR_{ρ,o} is primitive recursively definable in MBR_{ρ}.

Proof. We show how to define (primitive recursively in MBR) a Ψ satisfying the equation (SBR_{ρ,o}),

(i) Ψ(Y, G, H, s) =^{o} \{ \begin{matrix}G(s) & if Y (s ∗ 0) < |s| \\ H(s, λx.Ψ(Y, G, H, s ∗ x)) & otherwise. \end{matrix}

Let Φ be a functional satisfying MBR. In the following π_{0} and π_{1} will denote the projection functional, i.e. π_{i}(⟨x_{0}^{ρ}, x_{1}^{ρ}⟩) = x_{i}, i ∈ {0, 1}. If s^{⟨ρ,ρ⟩^{∗}} = ⟨s_{0}, …, s_{n}⟩, π_{i}(s) also denotes ⟨π_{i}(s_{0}), …, π_{i}(s_{n})⟩. In the same way we define π_{i}(α^{⟨ρ,ρ⟩^{ω}}). Note that s, for the rest of the proof, has type ⟨ρ, ρ⟩^{ω}. We first define two tilde operations,

(ii) H̃(s, F) :≡ λn.⟨1, H(π_{1}(s), λx.F (⟨0, x⟩))⟩

and ^{6}

6Since, by our construction, the first element of the pair will either be 0^{ρ} or 1^{ρ}, the test π_{0}(s_{i}) = 0 in the definition (iii) is primitive recursive.

(iii) Ỹ_{G,k}(α) :≡ \{ \begin{matrix}G(π_{1}(s)) & if ⋀_{i=0}^{n} (π_{0}(s_{i}) = 0) \\ π_{1}(s_{n}) & otherwise, \end{matrix}

where (in the definition of Ỹ_{G,k}) s = ⟨s_{0}, …, s_{n}⟩ = \overline{α} μ̃(Y, π_{1}(α), k). Note that the first operation is primitive recursive in H, s and F; and the second is primitive recursive in Y, G, k, α and MBR (since it uses μ̃). Moreover, (∗) if Y (s ∗ 0) ≥ |s| then Ỹ_{G,|s|} = Ỹ_{G,|s|+1}.

We abbreviate ⟨⟨0, s_{0}⟩, …, ⟨0, s_{|s|−1}⟩⟩ by ⟨0, s⟩. Define

(iv) Ψ(Y, G, H, s) :≡ Φ(Ỹ_{G,|s|}, H̃, ⟨0, s⟩).

We show that Ψ satisfies equation (i), i.e.

(v) Φ(Ỹ_{G,|s|}, H̃, ⟨0, s⟩) = \{ \begin{matrix}G(s) & if Y (s ∗ 0) < |s| \\ H(s, λx.Φ(Ỹ_{G,|s|+1}, H̃, ⟨0, s ∗ x⟩)) & otherwise. \end{matrix}

We first note that, by the definition of MBR (and (ii)),

(vi) Φ(Ỹ_{G,|s|}, H̃, ⟨0, s⟩) = Ỹ_{G,|s|}(⟨0, s⟩ @ λn.⟨1, H(s, λx.Φ(Ỹ_{G,|s|}, H̃, ⟨0, s ∗ x⟩))⟩).

We will show that (v) holds. Assume Y (s ∗ 0) < |s|, we have,

Φ(Ỹ_{G,|s|}, H̃, ⟨0, s⟩) =^{(vi)} Ỹ_{G,|s|}(⟨0, s⟩ @ …) =^{(iii)} G(s).

On the other hand, if Y (s ∗ 0) ≥ |s| then,

Φ(Ỹ_{G,|s|}, H̃, ⟨0, s⟩) =^{(vi)} Ỹ_{G,|s|}(⟨0, s⟩ @ λn.⟨1, H(s, λx.Φ(Ỹ_{G,|s|}, H̃, ⟨0, s ∗ x⟩))⟩)
=^{(iii)} H(s, λx.Φ(Ỹ_{G,|s|}, H̃, ⟨0, s ∗ x⟩))
=^{(∗)} H(s, λx.Φ(Ỹ_{G,|s|+1}, H̃, ⟨0, s ∗ x⟩)),

and the proof is concluded. □

Theorem 6.4 SBR_{ρ,τ} is primitive recursively definable in SBR_{ρ′,o}, where if τ = τ_{1} → … → τ_{n} → o then ρ′ = ρ × τ_{1} × … × τ_{n}.

Proof. Let τ = τ_{1} → … → τ_{n} → o. We will show that SBR_{ρ,τ} can be defined from SBR_{ρ×τ_{1}×...×τ_{n},o}. Let G, H and Y be given, we have to define a functional Φ such that,

(i) Φ(Y, G, H, s) =^{τ} \{ \begin{matrix}G(s) & if Y (s @ 0^{ρ}) <^{ℕ} |s| \\ H(s, λx^{ρ}.Φ(s ∗ x)) & otherwise. \end{matrix}

From Y, G and H we define,

(ii) Ỹ (α) :≡ Y (π_{0}^{n+1}(α));

(iii) G̃(t) :≡ G(π_{0}^{n+1}(t))(y);

(iv) H̃(t, F) :≡ H(π_{0}^{n+1}(t), λx^{ρ}, z_{1}^{τ_{1}}, …, z_{n}^{τ_{n}}.F (⟨x, z_{1}, …, z_{n}⟩))(y); where y denotes π_{1}^{n+1}(t_{|t|−1}), …, π_{n}^{n+1}(t_{|t|−1}) and the types are,

α : (ρ × τ_{1} × … × τ_{n})^{ω}
y : τ_{1} × … × τ_{n}
t : (ρ × τ_{1} × … × τ_{n})^{∗}
F : (ρ × τ_{1} × … × τ_{n}) → o.

We define (using SBR_{ρ×τ_{1}×...×τ_{n},o}),

(v) Ψ(Ỹ , G̃, H̃, t) =^{o} \{ \begin{matrix}G̃(t) & if Ỹ (t @ 0) <^{ℕ} |t| \\ H̃(t, λx^{ρ×τ_{1}×...×τ_{n}}.Ψ(t ∗ x)) & otherwise. \end{matrix}

Finally we set, (⟨s, y⟩ abbreviates ⟨⟨s_{0}, y⟩, …, ⟨s_{|s|−1}, y⟩⟩)

(vi) Φ(Y, G, H, s) :≡^{τ} λy.Ψ(Ỹ , G̃, H̃, ⟨s, y⟩).

We show that equation (i) is satisfied by Φ. One easily verifies that (vii) Ψ(Ỹ , G̃, H̃, ⟨s, y⟩) = Ψ(Ỹ , G̃, H̃, ⟨⟨s_{0}, z⟩, …, ⟨s_{|s|−2}, z⟩, ⟨s_{|s|−1}, y⟩⟩), for arbitrary z. Let Y, G, H and s be fixed and t abbreviate ⟨s, y⟩. By (ii), Y (s @ 0) < |s| iff Ỹ (t @ 0) < |t|. Therefore, if Y (s @ 0) < |s| then

Φ(Y, G, H, s) =^{(vi)} λy.Ψ(Ỹ , G̃, H̃, ⟨s, y⟩)
=^{(v)} λy.G̃(⟨s, y⟩) =^{(iii)} λy.G(s)(y) = G(s).

On the other hand, if Y (s @ 0) ≥ |s| then

Φ(Y, G, H, s) =^{(vi)} λy.Ψ(Ỹ , G̃, H̃, ⟨s, y⟩) =^{(v)} λy.H̃(t, λx.Ψ(t ∗ x))
=^{(iv)} λy.H(s, λx, z.Ψ(t ∗ ⟨x, z⟩))(y)
=^{(vii)} λy.H(s, λx, z.Ψ(⟨s, z⟩))(y)
=^{(vi)} λy.H(s, λx.Φ(s ∗ x))(y) = H(s, λx.Φ(s ∗ x))

□ Corollary 6.5 SBR is primitive recursively definable in MBR.

7 S1-S9 Computability and MBR

Definition 7.1 (Axioms S1-S9) In any applicative type structure S (containing ℕ) we define a set of relations Γ (parametrized by their arity and type of arguments) on S inductively as follows, ^{7}

S1 \{e\}^{S}(m, \overrightarrow{y}) = m + 1, where e = ⟨1, σ⟩.

7We abbreviate y_{1}, …, y_{n} (of arbitrary type) by \overrightarrow{y}. The variables e_{1}, e_{2}, m, n, i, k, k_{1}, k_{2} range over natural numbers, σ ranges over codes for finite types and f, x, \overrightarrow{y} over functionals of appropriate types. We write \{e\}^{S}(\overrightarrow{y}) = k instead of S ⊧ Γ(e, \overrightarrow{y}, k).

S2 \{e\}^{S}(\overrightarrow{y}) = k, where e = ⟨2, σ, k⟩.

S3 \{e\}^{S}(m, \overrightarrow{y}) = m, where e = ⟨3, σ⟩.

S4 If \{e_{1}\}^{S}(\overrightarrow{y}) = k_{1} and \{e_{2}\}^{S}(k_{1}, \overrightarrow{y}) = k_{2} then \{e\}^{S}(\overrightarrow{y}) = k_{2}, where e = ⟨4, e_{1}, e_{2}, σ⟩.

S5 Can be omitted in the presence of S9,

S6 If \{e_{1}\}^{S}(τ(\overrightarrow{y})) = k then \{e\}^{S}(\overrightarrow{y}) = k, where e = ⟨6, e_{1}, τ, σ⟩.

S7 \{e\}^{S}(f, x, \overrightarrow{y}) = f(x), where e = ⟨7, σ⟩.

S8 If \{e_{1}\}^{S}(x, \overrightarrow{y}) = f(x), for all x, then \{e\}^{S}(\overrightarrow{y}) = y_{1}(f), where e = ⟨8, e_{1}, σ⟩.

S9 If \{e_{1}\}^{S}(y_{1}, …, y_{i}) = k then \{e\}^{S}(e_{1}, \overrightarrow{y}) = k, where i ≤ n and e = ⟨9, i, σ⟩.

One can prove by induction on S1-S9 that for each e and \overrightarrow{y} there exists at most one k such that \{e\}^{S}(\overrightarrow{y}) = k. Therefore, each index e gives rise to a partial functional (denoted by \{e\}^{S}) which on input \overrightarrow{y} takes value k if \{e\}^{S}(\overrightarrow{y}) = k and is undefined otherwise. It is important to note that the functional {e}^{S} yielded by an index e need not belong to S. The set of all indices e such that {e}^{S} ∈ S is denoted by Rec^{S}. If \{e\}^{S} is a functional of the form λΨ, \overrightarrow{y}.\{e\}^{S}(Ψ, \overrightarrow{y}) then \{e\}_{Ψ}^{S} denotes the functional λ\overrightarrow{y}.\{e\}(Ψ, \overrightarrow{y}).

Definition 7.2 A formula P in the language of HA^{ω} having a unique free variable is called an specification of a functional or just functional. (e.g. SBR having variables Y, G, H and s universally quantified is an specification for Spector’s bar recursor.)

Definition 7.3 (S1-S9 computability) Let P, Q be specifications and S any applicative type structure (containing ℕ). Then,

P is S1-S9 computable in S if S ⊧ ∃e ∈ Rec^{S}.P({e}^{S}).
P is S1-S9 + Q computable in S if S ⊧ ∃Ψ (Q(Ψ) ∧ ∃e ∈ Rec^{S}.P({e}_{Ψ}^{S})).

Lemma 7.4 KBR and SBR are S1-S9 computable in C.

Proof. One shows C ⊧ ∃e ∈ Rec^{C}.KBR({e}^{C}) and C ⊧ ∃e ∈ Rec^{C}.SBR({e}^{C}) using the recursion theorem. □

The total elements of C can be viewed as equivalence classes of elements of Ĉ. We denote these equivalence classes by [F], i.e. if F ∈ Ĉ is total then [F] ∈ C. We have a transfer principle which says that if {e}^{C}([F]) = k then {e}Ĉ(F) = k. Moreover, (+) if {e}Ĉ(F) = k then there exists a compact element G ∈ Ĉ such that G ⊑ F and {e}Ĉ(G) = k.

Lemma 7.5 If

(i) e is a S1-S9 code of type 3,

(ii) \overrightarrow{x}, \overrightarrow{y} ∈ Ĉ (of type 2) coincide in all total recursive arguments, (iii) \overrightarrow{x} total S1-S9 computable in Ĉ,

(iv) \{e\}^{C}([\overrightarrow{x}]) = k,

then \{e\}Ĉ(\overrightarrow{y}) = k.

Proof. By induction on S1-S9 codes, the critical point being S8. Assume e is of the form ⟨8, e_{1}, σ⟩ and that (i) − (iv) hold. From (iv), by the definition of S1-S9, there must exist a function f ∈ C such that

(v) f(n) = \{e_{1}\}^{C}(n, [\overrightarrow{x}]), for all n ∈ ℕ, and

(vi) [x_{1}](f) = k,

By (iii) and (v) we get that f is recursive. Let n be fixed and assume that \{e_{1}\}^{C}(n, [\overrightarrow{x}]) = l. By induction hypothesis we have that

\{e_{1}\}Ĉ(n, \overrightarrow{y}) = l,

i.e. λn^{ℕ}.\{e_{1}\}Ĉ(n, \overrightarrow{y}) (= [λp^{ℕ_{⊥}}.\{e_{1}\}Ĉ(p, \overrightarrow{y})]) is identical to f. By (vi),

[x_{1}]([λp^{ℕ_{⊥}}.\{e_{1}\}Ĉ(p, \overrightarrow{y})]) = k.

Hence,

x_{1}(λp.\{e_{1}\}Ĉ(p, \overrightarrow{y})) = k.

Note that λp.\{e_{1}\}Ĉ(p, \overrightarrow{y}) is total and recursive. Therefore, by assumption (ii),

y_{1}(λp.\{e_{1}\}Ĉ(p, \overrightarrow{y})) = k,

and by the definition of S1-S9, \{e\}Ĉ(\overrightarrow{y}) = k. □

Theorem 7.6 ([10]) FAN is not S1-S9 computable in C.

Proof. Assume e ∈ Rec^{C} is such that C ⊧ FAN({e}^{C}). Let O be a total (S1-S9 computable) element of Ĉ which is constant zero. Assume {e}^{C}([O]) = k. Let F be another type two functional (in Ĉ) such that F (f) = 0 whenever f is total and recursive, but which is ⊥ for other f. By Lemma 7.5 {e}Ĉ(F) = k. By (+) there must be a compact G ⊑ F (still in Ĉ) such that {e}Ĉ(G) = k, G defined on a closed-open set that does not cover all of Ĉ. We can then extend G to a total G′ that is not constant and that k is not a modulus of uniform continuity for G′. Assume {e}^{C}([G′]) = l. By the transfer principle {e}Ĉ(G′) = l and l must equal k, i.e. {e}^{C}([G′]) = k, a contradiction. □

Lemma 7.7 FAN is S1-S9 + MBR computable in C.

Proof. By Theorem 2.3 there exists a Ψ ∈ C such that C ⊧ MBR(Ψ). In Theorem 4.4 we have shown that C ⊧ ∃e ∈ Rec^{C}.FAN({e}_{Ψ}^{C}). □

Corollary 7.8 MBR is not S1-S9 computable in C.

Proof. Assume C ⊧ ∃e ∈ Rec^{C}.MBR({e}^{C}). By Lemma 7.7 we have that FAN is S1-S9 computable in C, contradicting Theorem 7.6. □

Corollary 7.9 MBR is not primitive recursively definable in KBR nor SBR.

Proof. Follows from the corollary above, Lemma 7.4 and the fact that the set of functionals S1-S9 computable in C is closed under primitive recursion. □

8 Conclusion

In this paper we discussed modified bar recursion a variant of Spector’s bar recursion that seems to be of some significance in proof theory and the theory and higher type recursion theory. Our main result was an abstract modified realizability interpretation (where realizability for falsity is uninterpreted) of the axioms of countable and dependent choice that can be used to extract programs from non-constructive proofs using this axiom. A similar result is in [2], but we claim that our solution is more accessible and, in a sense, more ‘civilised’. It can be noted here that the weak form of modified bar recursion used for the realization of dependent choice can be implemented quite efficiently by equipping the functional with an internal memory that records the value of H(s, λx.Φ(s∗x)) (which is of type o) and thus avoids its repeated computation. Such an optimisation does not seem to be possible for the (allegedly more efficient) solution given in [2]. In order to make the realizability interpretation of dependent choice useful for program synthesis it seems necessary to combine it with optimisations of the A-translation as development e.g. in [5] and [6]. To find out whether this is possible will be a subject of further research.

Another important result was a definition of the fan functional using modified bar recursion and a version of bar recursion due to Kohlenbach, improving [3] and [19] where a PCF definition of the fan functional was given. In [23] this definition of the fan functional has been applied to give a purely functional algorithm for exact integration of real functions.

Finally, we have also established the relation between modified bar recursion, Spector’s and Kohlenbach’s bar recursions. It turns out that MBR and KBR are primitive recursively incomparable (none is primitive recursively definable in the other). Spector’s bar recursion, however, is primitive recursively definable in MBR but not the other way around. All these results hold in HA^{ω}. A by-product of this investigation is that modified bar recursion exists in M, the model of strongly majorizable functionals. We also proved a weak continuity property for the model M.

References

[1] J. Avigad and S. Feferman. Gödel’s functional (”Dialectica”) interpretation. In S. R. Buss, editor, Handbook of proof theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 337–405. Elsevier, North-Holland, Amsterdam, 1998.

[2] S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. Journal of Symbolic Logic, 63(2):600–622, 1998.

[3] U. Berger. Totale Objekte und Mengen in der Bereichstheorie. PhD thesis, Mathematisches Institut der Universität München, 1990.

[4] U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. accepted for publication, 2001.

[5] U. Berger and H. Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity Workshop (LCC’94), volume 960 of Lecture Notes in Computer Science, pages 77–97. Springer Verlag, 1995.

[6] U. Berger, H. Schwichtenberg, and W. Buchholz. Refined program extraction from classical proofs. Annals of Pure and Applied Logic, 114, 2002.

[7] M. Bezem. Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. Journal of Symbolic Logic, 50:652–660, 1985.

[8] M. Bezem. Equivalence of bar recursors in the theory of functionals of finite type. Archive for Mathematical Logic, 27:149–160, 1988.

[9] Y.L. Ershov. Model C of partial continuous functionals. In R. Gandy and M. Hyland, editors, Logic Colloquium 1976, pages 455–467. North Holland, Amsterdam, 1977.

[10] R. O. Gandy and M. Hyland. Computable and recursively countable functionals of higher type. In R. Gandy and M. Hyland, editors, Logic Colloquium 1976, pages 407–438. North Holland, Amsterdam, 1977.

[11] K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280–287, 1958.

[12] W. A. Howard. Hereditarily majorizable functionals of finite type. In A. S. Troestra, editor, Metamathematical investigation of intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454–461. Springer Verlag, 1973.

[13] W. A. Howard and G. Kreisel. Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. Journal of Symbolic Logic, 31(3):325–358, 1966.

[14] S. C. Kleene. Countable functionals. In A. Heyting, editor, Constructivity in Mathematics, pages 81–100. North–Holland, Amsterdam, 1959.

[15] U. Kohlenbach. Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen. PhD thesis, Frankfurt, pp. xxii+278, 1990.

[16] U. Kohlenbach. Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD thesis, Frankfurt, pp. xxii+278, 1990.

[17] G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, pages 101–128, 1959.

[18] H. Luckhardt. Extensional Gödel Functional Interpretation – A Consistency Proof of Classical Analysis, volume 306. Springer Verlag, 1973.

[19] D. Normann. The continuous functionals. In Griffor E. R., editor, Handbook of Computability Theory, chapter 8, pages 251–275. North Holland, 1999.

[20] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[21] H. Schwichtenberg. On bar recursion of types 0 and 1. Journal of Symbolic Logic, 44:325–329, 1979.

[22] D. S. Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pages 169–176, 1970.

[23] A. Simpson. Lazy functional algorithms for exact real functionals. In L. Brim, J. Gruska, and J. Zlatuska, editors, Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 456–464, 1998.

[24] C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathmatics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics, volume 5, pages 1–27. American Mathematical Society, Providence, Rhode Island, 1962.

[25] A. S. Troelstra. Metamathematical investigation of intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer Verlag, 1973.

[26] A. S. Troelstra. Realizability. In S.R. Buss, editor, Handbook of proof theory, volume 137, pages 408–473. North Holland, Amsterdam, 1998.

[27] A. S. Troelstra and Dalen D. van. Constructivism in Mathematics. An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1988.

Recent BRICS Report Series Publications

RS-02-14 Ulrich Berger and Paulo B. Oliva. Modified Bar Recursion. April 2002. 23 pp.

RS-02-13 Gerth Stølting Brodal, Rune B. Lyngsø, Anna Östlin, and Christian N.S̃. Pedersen. Solving the String Statistics Problem in Time O(n log n). March 2002. To appear in ICALP ’02.

RS-02-12 Olivier Danvy and Mayer Goldberg. There and Back Again. March 2002. This report supersedes the earlier report BRICS RS-01-39.

RS-02-11 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Extending Java for High-Level Web Service Construction. March 2002.

RS-02-10 Ulrich Kohlenbach. Uniform Asymptotic Regularity for Mann Iterates. March 2002. 17 pp.

RS-02-9 Anna Östlin and Rasmus Pagh. One-Probe Search. February 2002. 17 pp.

RS-02-8 Ronald Cramer and Serge Fehr. Optimal Black-Box Secret Sharing over Arbitrary Abelian Groups. February 2002. 19 pp.

RS-02-7 Anna Ingólfsdóttir, Anders Lyhne Christensen, Jens Alsted Hansen, Jacob Johnsen, John Knudsen, and Jacob Illum Rasmussen. A Formalization of Linkage Analysis. February 2002. vi+109 pp.

RS-02-6 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Axioms for Probabilistic Bisimilarity (Preliminary Report). February 2002. 22 pp.

RS-02-5 Federico Crazzolara and Glynn Winskel. Composing Strand Spaces. February 2002. 30 pp.

RS-02-4 Olivier Danvy and Lasse R. Nielsen. Syntactic Theories in Practice. January 2002. 34 pp. This revised report supersedes the earlier BRICS report RS-01-31.

RS-02-3 Olivier Danvy and Lasse R. Nielsen. On One-Pass CPS Transformations. January 2002. 18 pp.

RS-02-2 Lasse R. Nielsen. A Simple Correctness Proof of the Direct-Style Transformation. January 2002.