An Agda implementation of Oliva & Steila's

  ------------------------------------------------------------------
   A direct proof of Schwichtenberg's bar recursion closure theorem
  ------------------------------------------------------------------

                          Chuangjie Xu

               August 2017, updated in March 2018


Schwichtenberg [3] shows that the terms of Gödel's System T are closed
under the rule of Spector's bar recursion of types 0 and 1.  Oliva and
Steila [2] provide a more direct proof of Schwichtenberg's theorem
based on an explicit construction of their general bar recursion.
Using Agda we implement the approach of Oliva and Steila with some
simplification using Escardó's construction of dialogue monad [1].
Our implementation is organized following the structure of Oliva and
Steila's paper, and is appended with a section of examples.


References

[1] M.H. Escardó.  Continuity of Gödel's system T functionals via
    effectful forcing.  MFPS'2013.  Electronic Notes in Theoretical
    Computer Science 01/2013; 298:119–141, 2013.

[2] P. Oliva and S. Steila.  A direct proof of Schwichtenberg's bar
    recursion closure theorem.  Accepted by The Journal of Symbolic
    Logic, 2017.

[3] H. Schwichtenberg.  On bar recursion of types 0 and 1.  The
    Journal of Symbolic Logic, vol. 44, no. 3, pp. 325–329, 1979.


\begin{code}

module BRCT where

open import Preliminaries  -- A mini library
open import FunExt         -- Axiom of function extensionality

\end{code}

Throughout the implementation we adopt the following conventions:

• We use τ, σ, ρ to denote finite (and Agda) types.

• We write τ * to denote the type of finite sequences s, u, v.

• We write τ ᴺ to denote the type of infinite sequences α.

• We write s ✶ x to denotes their concatenation, where x could be an
  element or an (in)finite sequence (with different star symbols).

\begin{code}

module BarRecursion (σ τ : Set) (ω : τ ᴺ) where

 infix  _^
 --
 -- s ^ is the extension of s with the canonically chosen sequence ω.
 --
 _^ : τ * → τ ᴺ
 s ^ = s ✵ ω

\end{code}

----------------------
-- §1. Introduction --
----------------------

■ Spector's bar recursion (Definition 1.1)

\begin{code}

 --
 -- ξ is a bar recursion functional regarding the termination functional Y
 --
 BR : ((τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ)
    → (τ ᴺ → ℕ)
    → Set
 BR ξ Y = ∀ (G : τ * → σ) (H : τ * → (τ → σ) → σ) (s : τ *) →
              (Y (s ^) < ∣ s ∣ → ξ G H s ≡ G s)
            ∧ (Y (s ^) ≥ ∣ s ∣ → ξ G H s ≡ H s (λ x → ξ G H (s ✶ x)))

\end{code}

-------------------------------
-- §2. General Bar Recursion --
-------------------------------

■ Constant bar recursion (Lemma 2.1)

  If Y : τ ᴺ → ℕ is a constant function, then bar recursion for such Y
  is T-definable (and hence also Agda-definable).

\begin{code}

 cBR : (ℕ → (τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ)
     → Set
 cBR F = ∀ (k : ℕ) → BR (F k) (λ α → k)

 φ : (τ * → σ) → (τ * → (τ → σ) → σ) → ℕ → τ * → σ
 φ G H         = G
 φ G H (succ n) = λ s → H s (λ x → φ G H n (s ✶ x))

 Ψ : ℕ → (τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ
 Ψ k G H s = if (Lm[≤-dec] ∣ s ∣ k)
                (G s)                       -- if  ∣ s ∣ > k
                (φ G H (succ k - ∣ s ∣) s)  -- if  ∣ s ∣ ≤ k

 --
 -- Ψ is a constant bar recursion functional.
 --
 Lemma_2·1 : cBR Ψ
 -- i.e.
 -- ∀ (k : ℕ) (G : τ * → σ) (H : τ * → (τ → σ) → σ) (s : τ *) →
 --     (∣ s ∣ > k → Ψ k G H s ≡ G s)
 --   ∧ (∣ s ∣ ≤ k → Ψ k G H s ≡ H s (λ x → Ψ k G H (s ✶ x)))
 Lemma_2·1 k G H s = base , step
  where
   base : ∣ s ∣ > k → Ψ k G H s ≡ G s
       -- by the definition of Ψ
   base = ifᵈ-specᴸ (Lm[≤-dec] ∣ s ∣ k)
   step : ∣ s ∣ ≤ k → Ψ k G H s ≡ H s (λ x → Ψ k G H (s ✶ x))
   step r = case claim₀ claim₁ (Lm[≤-cases] r)
    where
     E4 : Ψ k G H s ≡ φ G H (k +  - ∣ s ∣) s
       -- by the definition of Ψ
     E4 = ifᵈ-specᴿ (Lm[≤-dec] ∣ s ∣ k) r
     claim₀ : ∣ s ∣ ≡ k → Ψ k G H s ≡ H s (λ x → Ψ k G H (s ✶ x))
     claim₀ e =
                Ψ k G H s ≡⟨ E4 ⟩   φ G H (k +  - ∣ s ∣) s
                          ≡⟨ † ⟩    φ G H  s
                          ≡⟨ refl ⟩ H s (λ x → φ G H  (s ✶ x))
                          ≡⟨ refl ⟩ H s (λ x → G (s ✶ x))
                          ≡⟨ E4' ⟩  H s (λ x → Ψ k G H (s ✶ x)) ∎
      where
       † : φ G H (k +  - ∣ s ∣) s ≡ φ G H  s
        -- by the assumption ∣ s ∣ ≡ k
       † = trans (ap (λ x → φ G H (k +  - x) s) e)
                 (ap (λ x → φ G H x s) (Lm[n+1-n=1] k))
       r' : {x : τ} → ∣ s ✶ x ∣ > k
       r' = Lm[n=m>k→n>k] (Lm[|xs✶x|=|xs|+1] s) (Lm[n=m→n+1>m] e)
       E4' : H s (λ x → G (s ✶ x)) ≡ H s (λ x → Ψ k G H (s ✶ x))
          -- by the definition of Ψ
       E4' = ap (H s) (sym (funExt (λ x → ifᵈ-specᴸ (Lm[≤-dec] ∣ s ✶ x ∣ k) r')))
     claim₁ : ∣ s ∣ < k → Ψ k G H s ≡ H s (λ x → Ψ k G H (s ✶ x))
     claim₁ r' =
                 Ψ k G H s ≡⟨ E4 ⟩  φ G H (k +  - ∣ s ∣) s
                           ≡⟨ E3 ⟩  H s (λ x → φ G H (k+1-∣s∣-1) (s ✶ x))
                           ≡⟨ □ ⟩   H s (λ x → φ G H (k +  - ∣ s ✶ x ∣) (s ✶ x))
                           ≡⟨ E4' ⟩ H s (λ x → Ψ k G H (s ✶ x)) ∎
      where
       k+1-∣s∣-1 : ℕ
       k+1-∣s∣-1 = pr₁ (Lm[<→Σ] (Lm[n<m→n<m+1] r'))
       E3 : φ G H (k +  - ∣ s ∣) s ≡ H s (λ x → φ G H (k+1-∣s∣-1) (s ✶ x))
       E3 = ap (λ x → φ G H x s) (sym (pr₂ (Lm[<→Σ] (Lm[n<m→n<m+1] r'))))
       ex : (x : τ) → φ G H k+1-∣s∣-1 (s ✶ x) ≡ φ G H (k +  - ∣ s ✶ x ∣) (s ✶ x)
       ex x = ap (λ z → φ G H z (s ✶ x))
                 (trans (Lm[k+1=n+1-m→k=n-m] {k} (pr₂ (Lm[<→Σ] (Lm[n<m→n<m+1] r'))))
                        (sym (ap (λ z → k +  - z) (Lm[|xs✶x|=|xs|+1] s))))
       □ : H s (λ x → φ G H k+1-∣s∣-1 (s ✶ x))
         ≡ H s (λ x → φ G H (k +  - ∣ s ✶ x ∣) (s ✶ x))
       □ = ap (H s) (funExt ex)
       ∣sx∣<k : {x : τ} → ∣ s ✶ x ∣ ≤ k
       ∣sx∣<k = transport (λ x → x ≤ k) (sym (Lm[|xs✶x|=|xs|+1] s)) (Lm[n<m→n+1≤m] r')
       ex' : (x : τ) → Ψ k G H (s ✶ x) ≡ φ G H (succ k - ∣ s ✶ x ∣) (s ✶ x)
       ex' x = ifᵈ-specᴿ (Lm[≤-dec] ∣ s ✶ x ∣ k) ∣sx∣<k
       E4' : H s (λ x → φ G H (succ k - ∣ s ✶ x ∣) (s ✶ x))
           ≡ H s (λ x → Ψ k G H (s ✶ x))
          -- by the definition of Ψ
       E4' = ap (H s) (sym (funExt ex'))

\end{code}

■ General bar recursion (Definition 2.2)

Oliva and Steila introduce a variant of Spector's bar recursion where
the termination condition is given by a decidable, monotone bar.

As pointed out by Makoto Fujiwara, only decidability and monotonicity
are needed to prove the desired result.  Here we drop the bar
condition and use boolean-valued functions to represent decidable
predicates.

\begin{code}

 --
 -- Monotone
 --
 monotone : (τ * → 𝟚) → Set
 monotone S = (u v : τ *) → u ≼ v → u ∈ S → v ∈ S
 --
 -- where "u ∈ S" is S u ≡ 𝟏 and "u ≼ v" means v is an extension of u.
 --

 --
 -- ξ is a general bar recursion functional regarding S
 --
 gBR : (τ * → 𝟚)
     → ((τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ)
     → Set
 gBR S ξ = ∀ (G : τ * → σ) (H : τ * → (τ → σ) → σ) (s : τ *) →
               (s ∈ S → ξ G H s ≡ G s)
             ∧ (s ∉ S → ξ G H s ≡ H s (λ x → ξ G H (s ✶ x)))

 --
 -- S secures Y
 --
 _secures_ : (τ * → 𝟚) → (τ ᴺ → ℕ) → Set
 S secures Y = ∀ (s : τ *) → s ∈ S → ∀ (α : τ ᴺ) → s ∋ α → Y (s ^) ≡ Y α
 --
 -- where "s ∋ α" means s is an initial segment of α.
 --

\end{code}

■ General bar recursion implies Spector's bar recursion (Theorem 2.4)

\begin{code}

 --
 -- Construct step functional for general bar recursion
 --
 𝐻 : (τ ᴺ → ℕ)           -- termination functional
   → (τ * → σ)           -- base functional for Spector's bar recursion
   → (τ * → (τ → σ) → σ) -- step functional for Spector's bar recursion
   → τ * → (τ → σ) → σ   -- step functional for general bar recursion
 𝐻 t G H s f = if (Lm[≤-dec] ∣ s ∣ (t (s ^)))
                   (G s)    -- if  t(s^) < ∣ s ∣
                   (H s f)  -- o.w.

 --
 -- Convert general bar recursion functional to Spector's one
 --
 Φ : (τ ᴺ → ℕ)
   → ((τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ) -- gBR
   → ((τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ) --  BR
 Φ t Δ G H = Δ (λ s → Ψ (t (s ^)) G H s) (𝐻 t G H)

 Theorem_2·4 : (t : τ ᴺ → ℕ)
             → (S : τ * → 𝟚) → monotone S → S secures t
             → (Δ : (τ * → σ) → (τ * → (τ → σ) → σ) → τ * → σ)
             → gBR S Δ → BR (Φ t Δ) t
 Theorem_2·4 t S mS st Δ gbr G H s = base , step
  where
   base : t (s ^) < ∣ s ∣ → Φ t Δ G H s ≡ G s
   base r = case claim₀ claim₁ (decidable-predicate S)
    where
     claim₀ : s ∈ S → Φ t Δ G H s ≡ G s
     claim₀ u =
                Φ t Δ G H s ≡⟨ refl ⟩ Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
                            ≡⟨ ‡ ⟩    Ψ (t (s ^)) G H s
                            ≡⟨ L2·1 ⟩ G s ∎
      where
       ‡ : Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s ≡ Ψ (t (s ^)) G H s
        -- by  gBR S Δ
       ‡ = pr₁ (gbr (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s) u
       L2·1 : Ψ (t (s ^)) G H s ≡ G s
       L2·1 = pr₁ (Lemma_2·1 (t (s ^)) G H s) r
     claim₁ : s ∉ S → Φ t Δ G H s ≡ G s
     claim₁ v =
                Φ t Δ G H s ≡⟨ refl ⟩ Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
                            ≡⟨ ‡ ⟩    𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x))
                            ≡⟨ E6 ⟩   G s ∎
      where
       ‡ : Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
         ≡ 𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x))
        -- by  gBR S Δ
       ‡ = pr₂ (gbr (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s) v
       E6 : 𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x)) ≡ G s
         -- by the definition of 𝐻
       E6 = ifᵈ-specᴸ ((Lm[≤-dec] ∣ s ∣ (t (s ^)))) r
   step : t (s ^) ≥ ∣ s ∣ → Φ t Δ G H s ≡ H s (λ x → Φ t Δ G H (s ✶ x))
   step r = case claim₀ claim₁ (decidable-predicate S)
    where
     claim₀ : s ∈ S → Φ t Δ G H s ≡ H s (λ x → Φ t Δ G H (s ✶ x))
     claim₀ u =
                Φ t Δ G H s ≡⟨ refl ⟩ Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
                            ≡⟨ ‡ ⟩    Ψ (t (s ^)) G H s
                            ≡⟨ L2·1 ⟩ H s (λ x → Ψ (t (s ^)) G H (s ✶ x))
                            ≡⟨ ⋆ ⟩    H s (λ x → Ψ (t ((s ✶ x) ^)) G H (s ✶ x))
                            ≡⟨ ‡' ⟩   H s (λ x → Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) (s ✶ x))
                            ≡⟨ refl ⟩ H s (λ x → Φ t Δ G H (s ✶ x)) ∎
      where
       ‡ : Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s ≡ Ψ (t (s ^)) G H s
        -- by  gBR S Δ
       ‡ = pr₁ (gbr (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s) u
       L2·1 : Ψ (t (s ^)) G H s ≡ H s (λ x → Ψ (t (s ^)) G H (s ✶ x))
       L2·1 = pr₂ (Lemma_2·1 (t (s ^)) G H s) r
       ex : (x : τ) → Ψ (t (s ^)) G H (s ✶ x) ≡ Ψ (t ((s ✶ x) ^)) G H (s ✶ x)
       ex x = ap (λ z → Ψ z G H (s ✶ x)) (st s u ((s ✶ x) ^) (Lm[∋-✷✵] s))
       ⋆ : H s (λ x → Ψ (t (s ^)) G H (s ✶ x))
         ≡ H s (λ x → Ψ (t ((s ✶ x) ^)) G H (s ✶ x))
        -- t (s ^) ≡ t ((s ✶ x) ^)  because  S secures t
       ⋆ = ap (H s) (funExt ex)
       ex' : (x : τ) →  Ψ (t ((s ✶ x) ^)) G H (s ✶ x)
                      ≡ Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) (s ✶ x)
       ex' x = sym (pr₁ (gbr (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) (s ✶ x))
                        (mS _ _ (Lm[≼-✷] s) u))
       ‡' : H s (λ x → Ψ (t ((s ✶ x) ^)) G H (s ✶ x))
          ≡ H s (λ x → Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) (s ✶ x))
         -- by  gBR S Δ
       ‡' = ap (H s) (funExt ex')
     claim₁ : s ∉ S → Φ t Δ G H s ≡ H s (λ x → Φ t Δ G H (s ✶ x))
     claim₁ v =
                Φ t Δ G H s ≡⟨ refl ⟩ Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
                            ≡⟨ ‡ ⟩    𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x))
                            ≡⟨ E6 ⟩   H s (λ x → Φ t Δ G H (s ✶ x)) ∎
      where
       ‡ : Δ (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s
         ≡ 𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x))
        -- by  gBR S Δ
       ‡ = pr₂ (gbr (λ s' → Ψ (t (s' ^)) G H s') (𝐻 t G H) s) v
       E6 : 𝐻 t G H s (λ x → Φ t Δ G H (s ✶ x)) ≡ H s (λ x → Φ t Δ G H (s ✶ x))
         -- by the definition of 𝐻
       E6 = ifᵈ-specᴿ ((Lm[≤-dec] ∣ s ∣ (t (s ^)))) r

\end{code}

---------------------
-- §3. Main Result --
---------------------

From now on, we consider only the case τ = ℕ.

Given a closed T-term Y : ℕᴺ → ℕ, Oliva and Steila construct

 □ a general bar recurson functional F using their _ᵒ translation, and

 □ a bar S which secures Y using a logical relation.


Each closed Y : ℕᴺ → ℕ corresponds to a term t : ℕ containing only one
free variable Ω : ℕᴺ, i.e. Y = λΩ.t up to α-β-η-equivalence.  Hence we
extend T with an unspecified variable Ω (named α in the paper).


■ Gödel's System T with an unspecified variable Ω : ℕᴺ

\begin{code}

infixr  _⇾_
infixl  _₊_
infixl  _·_

--
-- Finite type hierarchy
--
data Ty : Set where
 ι   : Ty
 _⇾_ : Ty → Ty → Ty

--
-- Contexts as finite list of types
--
data Cxt : Set where
 ε   : Cxt
 _₊_ : Cxt → Ty → Cxt

--
-- Indices of variables in context
--
data ∥_∈_∥ (σ : Ty) : Cxt → Set where
 zero : {Γ : Cxt} → ∥ σ ∈ (Γ ₊ σ) ∥
 succ : {τ : Ty} {Γ : Cxt} → ∥ σ ∈ Γ ∥ → ∥ σ ∈ (Γ ₊ τ) ∥

--
-- Terms
--
-- Each t : TΩ Γ ρ represents a term λΩ.t : ρ in the context Γ.
--
data TΩ (Γ : Cxt) : Ty → Set where
 Var  : {σ : Ty} → ∥ σ ∈ Γ ∥ → TΩ Γ σ
 Lam  : {σ τ : Ty} → TΩ (Γ ₊ σ) τ → TΩ Γ (σ ⇾ τ)
 _·_  : {σ τ : Ty} → TΩ Γ (σ ⇾ τ) → TΩ Γ σ → TΩ Γ τ
 Zero : TΩ Γ ι
 Succ : TΩ Γ (ι ⇾ ι)
 Rec  : {σ : Ty} → TΩ Γ (σ ⇾ (ι ⇾ σ ⇾ σ) ⇾ ι ⇾ σ)
 Ω    : TΩ Γ (ι ⇾ ι)

\end{code}

■ Oliva-Steila translation _ᵒ (Definition 3.1 & 3.3)

Each TΩ-term t : ℕ will be interpreted as an element tᵒ : ℕᵒ whose

 □ first component is the value  λΩ.t : ℕᴺ → ℕ

 □ second component is a general bar recursion functional

\begin{code}

module Main (σ : Set) where

 open BarRecursion σ ℕ 0ʷ

 ℕᵒ : Set
 ℕᵒ = (ℕᴺ → ℕ) × ((ℕ* → σ) → (ℕ* → (ℕ → σ) → σ) → ℕ* → σ)

 Val : ℕᵒ → ℕᴺ → ℕ
 Val = pr₁

 B : ℕᵒ → (ℕ* → σ) → (ℕ* → (ℕ → σ) → σ) → ℕ* → σ
 B = pr₂

 --
 -- Translation of types (Definition 3.1)
 --
 ᵒ⟦_⟧ʸ : Ty → Set
 ᵒ⟦ ι ⟧ʸ       = ℕᵒ
 ᵒ⟦ ρ₀ ⇾ ρ₁ ⟧ʸ = ᵒ⟦ ρ₀ ⟧ʸ → ᵒ⟦ ρ₁ ⟧ʸ

 --
 -- Translation of contexts
 --
 ᵒ⟦_⟧ˣ : Cxt → Set
 ᵒ⟦ Γ ⟧ˣ = {ρ : Ty} → ∥ ρ ∈ Γ ∥ → ᵒ⟦ ρ ⟧ʸ

 ᵒ⟪⟫ : ᵒ⟦ ε ⟧ˣ
 ᵒ⟪⟫ ()

 _‚_ : {Γ : Cxt} {ρ : Ty} → ᵒ⟦ Γ ⟧ˣ → ᵒ⟦ ρ ⟧ʸ → ᵒ⟦ Γ ₊ ρ ⟧ˣ
 (γ ‚ a)  zero    = a
 (γ ‚ a) (succ i) = γ i

\end{code}

We use Escardó's construction of dialogue monad [1] to interpret the
primitive recursion constant for arbitrary finite types.

The following monad constructions were defined together with Paulo Oliva
during his visit in Munich in the summer of 2017.

\begin{code}

 --
 -- "η k" is the  kᵒ  introduced in the end of Definition 3.
 --
 η : ℕ → ℕᵒ
 η n = (λ α → n) , (λ G H → G)

 β : (ℕ → ℕᵒ) → ℕ → ℕᵒ
 β f n = (λ α → α (Val (f n) α)) ,
         (λ G H → B (f n) (λ s' → Ψ (Val (f n) (s' ^)) G H s') H)

 Kleisli-extension : {ρ : Ty} → (ℕ → ᵒ⟦ ρ ⟧ʸ) → ℕᵒ → ᵒ⟦ ρ ⟧ʸ
 Kleisli-extension {ι} f x = (λ α → Val (f (Val x α)) α) ,
                             (λ G H → B x (λ s → B (f (Val x (s ^))) G H s) H)
 Kleisli-extension {_ ⇾ _} f x = λ a → Kleisli-extension (λ n → f n a) x

 zeroᵒ : ℕᵒ
 zeroᵒ = η 
      -- (λ α → 0) , (λ G H → G)

 succᵒ : ℕᵒ → ℕᵒ
 succᵒ = Kleisli-extension (η ∘ succ)
      -- λ x → ((λ α → succ (Val x α)) , B x)

 recᵒ : {ρ : Ty}
      → ᵒ⟦ ρ ⟧ʸ → (ℕᵒ → ᵒ⟦ ρ ⟧ʸ → ᵒ⟦ ρ ⟧ʸ) → ℕᵒ → ᵒ⟦ ρ ⟧ʸ
 recᵒ a f = Kleisli-extension (rec a (f ∘ η))

 Ωᵒ : ℕᵒ → ℕᵒ
 Ωᵒ = Kleisli-extension (β η)
   -- λ x → (λ α → α (Val x α)) ,
   --       (λ G H → B x (λ s → Ψ (Val x (s ^)) G H s) H)

 --
 -- Translation of terms (Definition 3.3)
 --
 ᵒ⟦_⟧ᵐ : {Γ : Cxt} {ρ : Ty} → TΩ Γ ρ → ᵒ⟦ Γ ⟧ˣ → ᵒ⟦ ρ ⟧ʸ
 ᵒ⟦ Zero ⟧ᵐ  _ = zeroᵒ
 ᵒ⟦ Succ ⟧ᵐ  _ = succᵒ
 ᵒ⟦ Ω ⟧ᵐ     _ = Ωᵒ
 ᵒ⟦ Var i ⟧ᵐ γ = γ i
 ᵒ⟦ Lam t ⟧ᵐ γ = λ a → ᵒ⟦ t ⟧ᵐ (γ ‚ a)
 ᵒ⟦ f · a ⟧ᵐ γ = (ᵒ⟦ f ⟧ᵐ γ) (ᵒ⟦ a ⟧ᵐ γ)
 ᵒ⟦ Rec ⟧ᵐ   _ = recᵒ

 --
 -- Translation of closed terms
 --
 _ᵒ : {ρ : Ty} → TΩ ε ρ → ᵒ⟦ ρ ⟧ʸ
 t ᵒ = ᵒ⟦ t ⟧ᵐ ᵒ⟪⟫

 ⟦_⟧ : TΩ ε ι
     → ℕᴺ → ℕ
 ⟦ t ⟧ = Val (t ᵒ)

 Bᵒ : TΩ ε ι
    → (ℕ* → σ) → (ℕ* → (ℕ → σ) → σ) → ℕ* → σ
 Bᵒ t = B (t ᵒ)

\end{code}

■ For each TΩ-term t : ℕ, the second component B(tᵒ) of tᵒ defines a
  general bar recursion for some bar predicate S which secures t.
  (Theorem 3.4)

To prove the above, Oliva & Steila define a logical relation between
T-terms.  We adapt their proof by simplifying their logical relation
to a unary predicate 𝔅.

\begin{code}

 𝔅 : {ρ : Ty} → ᵒ⟦ ρ ⟧ʸ → Set
 𝔅 {ι} t = Σ \(S : ℕ* → 𝟚) → (monotone S) ∧ (S secures (Val t)) ∧ (gBR S (B t))
 𝔅 {ρ₀ ⇾ ρ₁} f = (x : ᵒ⟦ ρ₀ ⟧ʸ) → 𝔅 x → 𝔅 (f x)

 𝔅ˣ : {Γ : Cxt} → ᵒ⟦ Γ ⟧ˣ → Set
 𝔅ˣ {Γ} γ = {ρ : Ty} (i : ∥ ρ ∈ Γ ∥) → 𝔅 (γ i)

 --
 -- tᵒ satisfies 𝔅 for each T-term t.
 --
 Lemma[𝔅] : {Γ : Cxt} {ρ : Ty} (t : TΩ Γ ρ)
          → {γ : ᵒ⟦ Γ ⟧ˣ} → 𝔅ˣ γ → 𝔅 (ᵒ⟦ t ⟧ᵐ γ)
 --
 -- The (long) proof is given later.
 --

 𝔅ˣ⟪⟫ : 𝔅ˣ ᵒ⟪⟫
 𝔅ˣ⟪⟫ ()

 Theorem_3·4 : ∀ (t : TΩ ε ι)
             → Σ \(S : ℕ* → 𝟚) → (monotone S) ∧ (S secures ⟦ t ⟧) ∧ (gBR S (Bᵒ t))
 Theorem_3·4 t = Lemma[𝔅] t 𝔅ˣ⟪⟫

\end{code}

Before proving the main lemma, we need two lemmas.

\begin{code}

 --
 -- η satisfies 𝔅
 --
 Lemma[𝔅-η] : (k : ℕ) → 𝔅 (η k)
 Lemma[𝔅-η] k = S , mS , sc , gbr
  where
   S : ℕ* → 𝟚
   S _ = 𝟏
   mS : monotone S
   mS _ _ _ _ = refl
   sc : S secures (Val (η k))
   sc _ _ _ _ = refl
   gbr : gBR S (B (η k))
   gbr _ _ _ = (λ x → refl) , (λ ())

 --
 -- Kleisli-extension satisfies 𝔅
 --
 Lemma[𝔅-KE] : {ρ : Ty}
             → (g : ℕ → ᵒ⟦ ρ ⟧ʸ) → ((i : ℕ) → 𝔅 (g i))
             → 𝔅 (Kleisli-extension g)
 Lemma[𝔅-KE] {ι} g bg (f , ξ) (S , mS , sc , gbr) = S' , mS' , sc' , gbr'
 --
 -- The proof corresponds to the case "t = Rec" in the original proof
 -- of Theorem 3.4 in the paper.
 --
  where
   𝑆 : ℕ → ℕ* → 𝟚
   𝑆 i = pr₁ (bg i)
   m𝑆 : (i : ℕ) → monotone (𝑆 i)
   m𝑆 i = pr₁ (pr₂ (bg i))
   𝑠𝑐 : (i : ℕ) → (𝑆 i) secures (Val (g i))
   𝑠𝑐 i = pr₁ (pr₂ (pr₂ (bg i)))
   𝑔𝑏𝑟 : (i : ℕ) → gBR (𝑆 i) (B (g i))
   𝑔𝑏𝑟 i = pr₂ (pr₂ (pr₂ (bg i)))

   --
   -- The construction of S' was given in the proof of Claim 2.
   --
   S' : ℕ* → 𝟚
   S' s = (S s) ∧² (𝑆 (f (s ^)) s)
   mS' : monotone S'
   mS' s t r u = ∧²intro claim₀ claim₃
    where
     claim₀ : t ∈ S
     claim₀ = mS s t r (∧²elim₀ u)
     claim₁ : f (s ^) ≡ f (t ^)
     claim₁ = sc s (∧²elim₀ u) (t ^) (Lm[≼→∋] r)
     claim₂ : s ∈ 𝑆 (f (t ^))
     claim₂ = transport (λ i → s ∈ 𝑆 i) claim₁ (∧²elim₁ {S s} u)
     claim₃ : t ∈ 𝑆 (f (t ^))
     claim₃ = m𝑆 (f (t ^)) s t r claim₂
   sc' : S' secures (λ α → Val (g (f α)) α)
      -- (s : ℕ*) → s ∈ S' → (α : ℕᴺ) → s ∋ α → Val (g (f (s ^))) (s ^) ≡ Val (g (f α)) α
   sc' s u α v = trans claim₀ claim₁
    where
     claim₀ : Val (g (f (s ^))) (s ^) ≡ Val (g (f (s ^))) α
     claim₀ = 𝑠𝑐 (f (s ^)) s (∧²elim₁ {S s} u) α v
     claim₁ : Val (g (f (s ^))) α ≡ Val (g (f α)) α
     claim₁ = ap (λ x → Val (g x) α) (sc s (∧²elim₀ u) α v)

   --
   -- This was given in the proof of Claim 3.
   --
   gbr' : gBR S' (B (Kleisli-extension g (f , ξ)))
       -- gBR S' (λ G H → ξ (λ s → B (g (f (s ^))) G H s) H)
   gbr' G H s = base , step
    where
     G' : ℕ* → σ
     G' s' = B (g (f (s' ^))) G H s'
     base : s ∈ S' → ξ G' H s ≡ G s
     base u =
              ξ G' H s ≡⟨ † ⟩ B (g (f (s ^))) G H s -- ≡ G' s
                       ≡⟨ ‡ ⟩ G s ∎
      where
       † : ξ G' H s ≡ B (g (f (s ^))) G H s
        -- by  gBR S ξ
       † = pr₁ (gbr G' H s) (∧²elim₀ u)
       ‡ : B (g (f (s ^))) G H s ≡ G s
        -- by  gBR (𝑆 (f (s ^))) (B (g (f (s ^))))
       ‡ = pr₁ (𝑔𝑏𝑟 (f (s ^)) G H s) (∧²elim₁ {S s} u)
     step : s ∉ S' → ξ G' H s ≡ H s (λ x → ξ G' H (s ✶ x))
     step u = case claim₀ claim₁ (decidable-predicate S)
      where
       claim₀ : s ∈ S → ξ G' H s ≡ H s (λ x → ξ G' H (s ✶ x))
       claim₀ v =
                  ξ G' H s ≡⟨ † ⟩   B (g (f (s ^))) G H s
                           ≡⟨ ‡ ⟩   H s (λ x → B (g (f (s ^))) G H (s ✶ x))
                           ≡⟨ ⋆ ⟩   H s (λ x → B (g (f ((s ✶ x) ^))) G H (s ✶ x))
                           ≡⟨ †⋆⋆ ⟩ H s (λ x → ξ G' H (s ✶ x)) ∎
        where
         † : ξ G' H s ≡ B (g (f (s ^))) G H s
          -- by  gBR S ξ
         † = pr₁ (gbr (λ s' → B (g (f (s' ^))) G H s') H s) v
         v' : s ∉ 𝑆 (f (s ^))
         v' = ∧²elim₁' u v
         ‡ : B (g (f (s ^))) G H s
           ≡ H s (λ x → B (g (f (s ^))) G H (s ✶ x))
          -- by  gBR (𝑆 (f (s ^))) (B (g (f (s ^))))
         ‡ = pr₂ (𝑔𝑏𝑟 (f (s ^)) G H s) v'
         ex : (x : ℕ) →  B (g (f (s ^))) G H (s ✶ x)
                       ≡ B (g (f ((s ✶ x) ^))) G H (s ✶ x)
         ex x = ap (λ y → B (g y) G H (s ✶ x)) (sc s v ((s ✶ x) ^) (Lm[∋-✷✵] s))
         ⋆ : H s (λ x → B (g (f (s ^))) G H (s ✶ x))
           ≡ H s (λ x → B (g (f ((s ✶ x) ^))) G H (s ✶ x))
          -- by  f (s ^) ≡ f ((s x) ^)
         ⋆ = ap (H s) (funExt ex)
         ⋆⋆ : {x : ℕ} → (s ✶ x) ∈ S
         ⋆⋆ {x} = mS s (s ✶ x) (Lm[≼-✷] s) v
         ex' : (x : ℕ) →  B (g (f ((s ✶ x) ^))) G H (s ✶ x) -- G' (s ✶ x)
                        ≡ ξ G' H (s ✶ x)
         ex' x = sym (pr₁ (gbr G' H (s ✶ x)) ⋆⋆)
         †⋆⋆ : H s (λ x → B (g (f ((s ✶ x) ^))) G H (s ✶ x))
             ≡ H s (λ x → ξ G' H (s ✶ x))
            -- by  gBR S ξ  and  (s ✶ x) ∈ S
         †⋆⋆ = ap (H s) (funExt ex')
       claim₁ : s ∉ S → ξ G' H s ≡ H s (λ x → ξ G' H (s ✶ x))
       claim₁ = pr₂ (gbr (λ s' → B (g (f (s' ^))) G H s') H s)
             -- by  gBR S ξ

 Lemma[𝔅-KE] {ρ₀ ⇾ ρ₁} g bg n bn x bx = Lemma[𝔅-KE] (λ k → g k x) (λ k → bg k x bx) n bn

\end{code}

Here is the proof of the main lemma

 Lemma[𝔅] : {Γ : Cxt} {ρ : Ty} (t : TΩ Γ ρ)
          → (γ : ᵒ⟦ Γ ⟧ˣ) → 𝔅ˣ γ → 𝔅 (ᵒ⟦ t ⟧ᵐ γ)

\begin{code}

 Lemma[𝔅] Zero _ = Lemma[𝔅-η] 

 Lemma[𝔅] Succ _ x (S , mS , sc , gbr) = S , mS , sc' , gbr
  where
   sc' : S secures (Val (succᵒ x))
   sc' s u α β = ap succ (sc s u α β)

 Lemma[𝔅] (Var i) δ = δ i

 Lemma[𝔅] Ω _ (g , ξ) (S , mS , sc , gbr) = S' , mS' , sc' , gbr'
  where
   S' : ℕ* → 𝟚
   S' s = (S s) ∧² (g (s ^) <² ∣ s ∣)
   S'intro : {s : ℕ*} → s ∈ S → g (s ^) < ∣ s ∣ → s ∈ S'
   S'intro u r = ∧²intro u (<²intro r)
   S'elim₀ : {s : ℕ*} → s ∈ S' → s ∈ S
   S'elim₀ = ∧²elim₀
   S'elim₁ : {s : ℕ*} → s ∈ S' → g (s ^) < ∣ s ∣
   S'elim₁ {s} u = <²elim (∧²elim₁ {S s} u)
   S'elim₁' : {s : ℕ*} → s ∉ S' → s ∈ S → g (s ^) ≥ ∣ s ∣
   S'elim₁' u v = <²elim' (∧²elim₁' u v)
   mS' : monotone S'
   mS' s t r u = S'intro claim₁ claim₅
    where
     claim₀ : s ∈ S
     claim₀ = S'elim₀ u
     claim₁ : t ∈ S
     claim₁ = mS s t r claim₀
     claim₂ : g (s ^) < ∣ s ∣
     claim₂ = S'elim₁ u
     claim₃ : g (s ^) ≡ g (t ^)
     claim₃ = sc s claim₀ (t ^) (Lm[≼→∋] r)
     claim₄ : g (t ^) < ∣ s ∣
     claim₄ = transport (λ x → x < ∣ s ∣) claim₃ claim₂
     claim₅ : g (t ^) < ∣ t ∣
     claim₅ = <-≤-trans claim₄ (Lm[≼→∣≤∣] r)
   sc' : S' secures (λ α → α (g α))
      -- (s : ℕ*) → s ∈ S' → (α : ℕᴺ) → s ∋ α → (s ^) (g (s ^)) ≡ α (g α)
   sc' s u α v = claim₄
    where
     claim₀ : s ∈ S
     claim₀ = S'elim₀ u
     claim₁ : g (s ^) ≡ g α
     claim₁ = sc s claim₀ α v
     claim₂ : g (s ^) < ∣ s ∣
     claim₂ = S'elim₁ u
     claim₃ : (s ^) (g (s ^)) ≡ α (g (s ^))
     claim₃ = Lm[∋≤→≡] v claim₂
     claim₄ : (s ^) (g (s ^)) ≡ α (g α)
     claim₄ = trans claim₃ (ap α claim₁)
   ξ' : (ℕ* → σ) → (ℕ* → (ℕ → σ) → σ) → ℕ* → σ
   ξ' G H = ξ (λ s → Ψ (g (s ^)) G H s) H
   gbr' : gBR S' ξ'
   gbr' G H s = base , step
    where
     G' : ℕ* → σ
     G' s' = Ψ (g (s' ^)) G H s'
     base : s ∈ S' → ξ' G H s ≡ G s
     base u =
              ξ G' H s ≡⟨ † ⟩    Ψ (g (s ^)) G H s
                       ≡⟨ L2·1 ⟩ G s ∎
      where
       † : ξ G' H s ≡ Ψ (g (s ^)) G H s
        -- by  gBR S ξ
       † = pr₁ (gbr G' H s) (S'elim₀ u)
       L2·1 : Ψ (g (s ^)) G H s ≡ G s
       L2·1 = pr₁ (Lemma_2·1 (g (s ^)) G H s) (S'elim₁ u)
     step : s ∉ S' → ξ' G H s ≡ H s (λ y → ξ' G H (s ✶ y))
     step u = case claim₀ claim₁ Lm[1∨0]
      where
       claim₀ : s ∈ S → ξ' G H s ≡ H s (λ y → ξ' G H (s ✶ y))
       claim₀ v =
                  ξ G' H s ≡⟨ † ⟩    Ψ (g (s ^)) G H s
                           ≡⟨ L2·1 ⟩ H s (λ y → Ψ (g (s ^)) G H (s ✶ y))
                           ≡⟨ ‡ ⟩    H s (λ y → Ψ (g ((s ✶ y) ^)) G H (s ✶ y))
                           ≡⟨ †' ⟩   H s (λ y → ξ' G H (s ✶ y)) ∎
        where
         r : g (s ^) ≥ ∣ s ∣
         r = S'elim₁' u v
         † : ξ G' H s ≡ Ψ (g (s ^)) G H s
          -- by  gBR S ξ
         † = pr₁ (gbr G' H s) v
         L2·1 : Ψ (g (s ^)) G H s ≡ H s (λ y → Ψ (g (s ^)) G H (s ✶ y))
         L2·1 = pr₂ (Lemma_2·1 (g (s ^)) G H s) r
         e₀ : (y : ℕ) → g (s ^) ≡ g ((s ✶ y) ^)
         e₀ y = sc s v ((s ✶ y) ^) (Lm[∋-✷✵] s)
         e₁ : (y : ℕ) → Ψ (g (s ^)) G H (s ✶ y) ≡ Ψ (g ((s ✶ y) ^)) G H (s ✶ y)
         e₁ y = ap (λ x → Ψ x G H (s ✶ y)) (e₀ y)
         ‡ : H s (λ y → Ψ (g (s ^)) G H (s ✶ y))
           ≡ H s (λ y → Ψ (g ((s ✶ y) ^)) G H (s ✶ y))
          -- g (s ^) ≡ g ((s ⋆ y) ^)  because  S secures g
         ‡ = ap (H s) (funExt e₁)
         e₂ : (y : ℕ) → Ψ (g ((s ✶ y) ^)) G H (s ✶ y) ≡ ξ' G H (s ✶ y)
         e₂ y = sym (pr₁ (gbr G' H (s ✶ y)) (mS _ _ (Lm[≼-✷] s) v))
         †' : H s (λ y → Ψ (g ((s ✶ y) ^)) G H (s ✶ y))
            ≡ H s (λ y → ξ' G H (s ✶ y))
           -- by  gBR S ξ
         †' = ap (H s) (funExt e₂)
       claim₁ : s ∉ S → ξ' G H s ≡ H s (λ y → ξ' G H (s ✶ y))
       claim₁ = pr₂ (gbr G' H s)

 Lemma[𝔅] (Lam t) {γ} δ a θ = IH
  where
   δθ : 𝔅ˣ (γ ‚ a)
   δθ  zero    = θ
   δθ (succ i) = δ i
   IH : 𝔅 (ᵒ⟦ t ⟧ᵐ (γ ‚ a))
   IH = Lemma[𝔅] t δθ

 Lemma[𝔅] (f · a) {γ} δ = Lemma[𝔅] f δ (ᵒ⟦ a ⟧ᵐ γ) (Lemma[𝔅] a δ)

 Lemma[𝔅] (Rec {ρ}) _ a ba f bf = Lemma[𝔅-KE] g bg
  where
   g : ℕ → ᵒ⟦ ρ ⟧ʸ
   g k = rec a (f ∘ η) k
   bg : (k : ℕ) → 𝔅 (g k)
   bg         = ba
   bg (succ k) = bf (η k) (Lemma[𝔅-η] k) (g k) (bg k)

\end{code}

Therefore, from each TΩ-term t : ℕ (i.e. a closed T-term λΩ.t : ℕᴺ → ℕ)
we have an Agda term Β(t) which defines Spector's bar recursion.

\begin{code}

 Β : TΩ ε ι
   → (ℕ* → σ) → (ℕ* → (ℕ → σ) → σ) → ℕ* → σ
 Β t = Φ ⟦ t ⟧ (Bᵒ t)

 Theorem : ∀ (t : TΩ ε ι) → BR (Β t) ⟦ t ⟧
 Theorem t = Theorem_2·4 ⟦ t ⟧ S mS sc (Bᵒ t) gbr
  where
   ◻ : Σ \(S : ℕ* → 𝟚) → (monotone S) ∧ (S secures ⟦ t ⟧) ∧ (gBR S (Bᵒ t))
   ◻ = Theorem_3·4 t
   S : ℕ* → 𝟚
   S = pr₁ ◻
   mS : monotone S
   mS = pr₁ (pr₂ ◻)
   sc : S secures ⟦ t ⟧
   sc = pr₁ (pr₂ (pr₂ ◻))
   gbr : gBR S (Bᵒ t)
   gbr = pr₂ (pr₂ (pr₂ ◻))

\end{code}

------------------
-- §4. Examples --
------------------

We present some examples

 □ to show what the Agda-definition of the bar recursion functional
   looks like for a given T-definable termination functional Y, and

 □ to execute them with given base and step functionals G and H.

We firstly need some numerals to construct the examples.

\begin{code}

Num : ℕ → {Γ : Cxt} → TΩ Γ ι
Num         = Zero
Num (succ k) = Succ · Num k

\end{code}

The first two examples were provided by Paulo Oliva.

\begin{code}

open BarRecursion ℕ ℕ 0ʷ
open Main ℕ

t₀ : TΩ ε ι
t₀ = Num 
  -- λα.4

Agda-definition-of-Β[t₀] :

  Β t₀ ≡ Ψ 

Agda-definition-of-Β[t₀] = refl

t₁ : TΩ ε ι
t₁ = Ω · Num 
  -- λα.α4

Agda-definition-of-Β[t₁] :

  Β t₁ ≡ λ G H → Ψ  (λ s → Ψ ((s ^) ) G H s) (𝐻 (λ α → α ) G H)

Agda-definition-of-Β[t₁] = refl

G : ℕ* → ℕ -- G s = sum s
G ⟨⟩ = 
G (n , s) = n + G s

H : ℕ* → (ℕ → ℕ) → ℕ
H s f = max (f ) (f )

result-of-Β[t₀,G,H,⟨⟩] :

  Β t₀ G H ⟨⟩ ≡ 

result-of-Β[t₀,G,H,⟨⟩] = refl

result-of-Β[t₁,G,H,⟨⟩] :

  Β t₁ G H ⟨⟩ ≡ 

result-of-Β[t₁,G,H,⟨⟩] = refl

\end{code}

The following (more complicated) example is given in the paper.

\begin{code}

t₂ : TΩ ε ι
t₂ = Rec · Zero · Lam Ω · (Ω · Zero)
  -- λα.rec(0,(λk.α),α0)
  -- i.e.  α(α(…(α0)…))  with α0 applications of α

Y : ℕᴺ → ℕ
Y = ⟦ t₂ ⟧

r[_] : ℕ → ℕᵒ
r[ n ] = rec zeroᵒ (λ k → Ωᵒ) n

Agda-definition-of-Β[t₂] :

  Β t₂ ≡ λ G H → Ψ  (λ u → B r[ (u ^)  ] (λ v → Ψ (Y (v ^)) G H v) (𝐻 Y G H) u)
                     (𝐻 Y G H)

Agda-definition-of-Β[t₂] = refl

H' : ℕ* → (ℕ → ℕ) → ℕ
H' s f = max (f ) (max (f ) (f ))

result-of-Β[t₂,G,H',⟨⟩] :

  Β t₂ G H' ⟨⟩ ≡ 

result-of-Β[t₂,G,H',⟨⟩] = refl

\end{code}