---------------------------------------------
A syntactic approach to continuity
of Gödel's system T definable functionals
---------------------------------------------

Chuangjie Xu

February 2018, updated in June 2018

This is another short and self-contained Agda proof that

any Gödel's system T definable function (ℕ → ℕ) → ℕ is continuous.

We firstly perform a translation within T, which is inspired by Oliva
and Steila's proof of the bar recursion closure theorem [2].  By
structural induction on terms, we show that (the standard
interpretation of) the translation of any T term satisfies a certain
continuity predicate.  Then we use a parametrised logical relation due
to Escardó [1] to relate (the standard interpretations of) T terms and
their translations.  These together bring us the desired result.

Our Agda development is organised as follows:

§0. Mini library

§1. Gödel's system T and b-translation

§2. Continuity of T-definable functionals

§3. Experiments of computation

Reference.

[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.  The Journal of Symbolic Logic 83(1):
70-83, 2018.

\begin{code}

module TCont where

\end{code}

======================
=                    =
=  §0  Mini library  =
=                    =
======================

\begin{code}

--
-- identity types
--
data _≡_ {ℓ} {A : Set ℓ} (a : A) : A → Set ℓ where
refl : a ≡ a

ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A}
→ x ≡ y → y ≡ z → x ≡ z
trans refl p = p

--
-- (dependent) pairs
--
record Σ {A : Set} (B : A → Set) : Set where
constructor _,_
field
pr₁ : A
pr₂ : B pr₁

open Σ public

infixr 1 _×_ _,_

_×_ : Set → Set → Set
A × B = Σ \(_ : A) → B

--
-- the unit type
--
data 𝟙 : Set where
⋆ : 𝟙

--
-- natural numbers
--
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

rec : {A : Set} → A → (ℕ → A → A) → ℕ → A
rec a f  0       = a
rec a f (succ n) = f n (rec a f n)

infix 2 _≤_

data _≤_ : ℕ → ℕ → Set where
≤zero : {n : ℕ} → 0 ≤ n
≤succ : {n m : ℕ} → n ≤ m → succ n ≤ succ m

≤refl : {n : ℕ} → n ≤ n
≤refl {0}      = ≤zero
≤refl {succ n} = ≤succ ≤refl

max : ℕ → ℕ → ℕ
max  0        m       = m
max (succ n)  0       = succ n
max (succ n) (succ m) = succ (max n m)

max-spec₀ : (n m : ℕ) → n ≤ max n m
max-spec₀  0        m       = ≤zero
max-spec₀ (succ n)  0       = ≤refl
max-spec₀ (succ n) (succ m) = ≤succ (max-spec₀ n m)

max-spec₁ : (n m : ℕ) → m ≤ max n m
max-spec₁  0        m       = ≤refl
max-spec₁ (succ n)  0       = ≤zero
max-spec₁ (succ n) (succ m) = ≤succ (max-spec₁ n m)

--
-- infinite sequences as functions from ℕ
--
_ᴺ : Set → Set
A ᴺ = ℕ → A

ℕᴺ : Set
ℕᴺ = ℕ ᴺ

head : {A : Set} → A ᴺ → A

tail : {A : Set} → A ᴺ → A ᴺ
tail α i = α (succ i)

\end{code}

============================================
=                                          =
=  §1  Gödel's system T and b-translation  =
=                                          =
============================================

■ Types, contexts and terms of T

Here we work with the lambda-calculus version of system T, and with de

\begin{code}

infixr 30 _⇾_
infixl 20 _₊_
infixl 20 _·_

--
-- finite types
--
data Ty : Set where
ι   : Ty
_⇾_ : Ty → Ty → Ty

--
-- contexts as finite lists of types
--
data Cxt : Set where
ε   : Cxt
_₊_ : Cxt → Ty → Cxt

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

--
-- terms
--
data T (Γ : Cxt) : Ty → Set where
Var  : {σ : Ty} → ∥ σ ∈ Γ ∥ → T Γ σ
Lam  : {σ τ : Ty} → T (Γ ₊ σ) τ → T Γ (σ ⇾ τ)
_·_  : {σ τ : Ty} → T Γ (σ ⇾ τ) → T Γ σ → T Γ τ
Zero : T Γ ι
Succ : T Γ (ι ⇾ ι)
Rec  : {σ : Ty} → T Γ (σ ⇾ (ι ⇾ σ ⇾ σ) ⇾ ι ⇾ σ)

ν₀ : {Γ : Cxt} {ρ : Ty} → T (Γ ₊ ρ) ρ
ν₀ = Var zero

ν₁ : {Γ : Cxt} {ρ σ : Ty} → T (Γ ₊ ρ ₊ σ) ρ
ν₁ = Var (succ zero)

ν₂ : {Γ : Cxt} {ρ σ₀ σ₁ : Ty} → T (Γ ₊ ρ ₊ σ₀ ₊ σ₁) ρ
ν₂ = Var (succ (succ zero))

ν₃ : {Γ : Cxt} {ρ σ₀ σ₁ σ₂ : Ty} → T (Γ ₊ ρ ₊ σ₀ ₊ σ₁ ₊ σ₂) ρ
ν₃ = Var (succ (succ (succ zero)))

\end{code}

■ The standard interpretation of T into Agda

\begin{code}

⟦_⟧ʸ : Ty → Set
⟦ ι ⟧ʸ     = ℕ
⟦ σ ⇾ τ ⟧ʸ = ⟦ σ ⟧ʸ → ⟦ τ ⟧ʸ

⟦_⟧ˣ : Cxt → Set
⟦ ε ⟧ˣ     = 𝟙
⟦ Γ ₊ ρ ⟧ˣ = ⟦ Γ ⟧ˣ × ⟦ ρ ⟧ʸ

_₍_₎ : {Γ : Cxt} {ρ : Ty} → ⟦ Γ ⟧ˣ → ∥ ρ ∈ Γ ∥ → ⟦ ρ ⟧ʸ
(_ , a) ₍ zero ₎   = a
(γ , _) ₍ succ i ₎ = γ ₍ i ₎

⟦_⟧ᵐ : {Γ : Cxt} {σ : Ty} → T Γ σ → ⟦ Γ ⟧ˣ → ⟦ σ ⟧ʸ
⟦ Var i ⟧ᵐ γ = γ ₍ i ₎
⟦ Lam t ⟧ᵐ γ = λ a → ⟦ t ⟧ᵐ (γ , a)
⟦ f · a ⟧ᵐ γ = ⟦ f ⟧ᵐ γ (⟦ a ⟧ᵐ γ)
⟦ Zero ⟧ᵐ  _ = 0
⟦ Succ ⟧ᵐ  _ = succ
⟦ Rec ⟧ᵐ   _ = rec

⟦_⟧ : {ρ : Ty} → T ε ρ → ⟦ ρ ⟧ʸ
⟦ t ⟧ = ⟦ t ⟧ᵐ ⋆

--
-- An (Agda) element a is "T-definable" if one can find a closed T
-- term whose standard interpretation is a.
--
T-definable : {ρ : Ty} → ⟦ ρ ⟧ʸ → Set
T-definable {ρ} a = Σ \(t : T ε ρ) → ⟦ t ⟧ ≡ a

\end{code}

■ b-translation

The first step of a usual syntactic treatment (e.g. of totality or
majorisability) is to inductively define a predicate on elements of
finite types whose base case is on natural numbers.  However, what we
want to prove is continuity of functions (ℕ → ℕ) → ℕ.  So we firstly
perform a translation within T to make it the base case of our
predicate.

\begin{code}

⟨_⟩ʸ : Ty → Ty
⟨ ι ⟩ʸ     = (ι ⇾ ι) ⇾ ι
⟨ σ ⇾ τ ⟩ʸ = ⟨ σ ⟩ʸ ⇾ ⟨ τ ⟩ʸ

⟨_⟩ˣ : Cxt → Cxt
⟨ ε ⟩ˣ     = ε
⟨ Γ ₊ ρ ⟩ˣ = ⟨ Γ ⟩ˣ ₊ ⟨ ρ ⟩ʸ

⟨_⟩ᵛ : {Γ : Cxt} {ρ : Ty} → ∥ ρ ∈ Γ ∥ → ∥ ⟨ ρ ⟩ʸ ∈ ⟨ Γ ⟩ˣ ∥
⟨ zero ⟩ᵛ   = zero
⟨ succ i ⟩ᵛ = succ ⟨ i ⟩ᵛ

KEᶥ : {Γ : Cxt} (ρ : Ty)
→ T Γ ((ι ⇾ ⟨ ρ ⟩ʸ) ⇾ ⟨ ι ⟩ʸ ⇾ ⟨ ρ ⟩ʸ)
KEᶥ  ι      = Lam (Lam (Lam (ν₂ · (ν₁ · ν₀) · ν₀)))
KEᶥ (_ ⇾ ρ) = Lam (Lam (Lam (KEᶥ ρ · Lam (ν₃ · ν₀ · ν₁) · ν₁)))

⟨_⟩ᵐ : {Γ : Cxt} {ρ : Ty} → T Γ ρ → T ⟨ Γ ⟩ˣ ⟨ ρ ⟩ʸ
⟨ Var i ⟩ᵐ   = Var ⟨ i ⟩ᵛ
⟨ Lam t ⟩ᵐ   = Lam ⟨ t ⟩ᵐ
⟨ f · a ⟩ᵐ   = ⟨ f ⟩ᵐ · ⟨ a ⟩ᵐ
⟨ Zero ⟩ᵐ    = Lam Zero
⟨ Succ ⟩ᵐ    = Lam (Lam (Succ · (ν₁ · ν₀)))
⟨ Rec {ρ} ⟩ᵐ = Lam (Lam (KEᶥ ρ · (Rec · ν₁ · Lam (ν₁ · Lam ν₁))))

--
-- A T-definable generic sequence in the sense of [1].
--
Ω : {Γ : Cxt} → T Γ (⟨ ι ⇾ ι ⟩ʸ)
Ω = Lam (Lam (ν₀ · (ν₁ · ν₀)))

\end{code}

■ Relating terms and their b-translations

Following Escardo [1], we define a parametrised logical relation R
between the interpretations of terms and their b-translations.

\begin{code}

R : {ρ : Ty} → ℕᴺ → ⟦ ⟨ ρ ⟩ʸ ⟧ʸ → ⟦ ρ ⟧ʸ → Set
R {ι    } α f n = f α ≡ n
R {σ ⇾ τ} α f g = {x : ⟦ ⟨ σ ⟩ʸ ⟧ʸ} {y : ⟦ σ ⟧ʸ} → R α x y → R α (f x) (g y)

Rˣ : {Γ : Cxt} → ℕᴺ → ⟦ ⟨ Γ ⟩ˣ ⟧ˣ → ⟦ Γ ⟧ˣ → Set
Rˣ {ε}     _  _       _      = 𝟙
Rˣ {Γ ₊ ρ} α (γ , a) (ξ , b) = Rˣ α γ ξ × R α a b

--
-- The Kleisli extension preserves R.
--
R[KEᶥ] : (ρ : Ty) (α : ℕᴺ) {f : ℕ → ⟦ ⟨ ρ ⟩ʸ ⟧ʸ} {g : ℕ → ⟦ ρ ⟧ʸ}
→ ((i : ℕ) → R α (f i) (g i))
→ {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ}
→ R α (⟦ KEᶥ ρ ⟧ᵐ γ f) g
R[KEᶥ]  ι      α ζ χ = trans (ζ _) (ap _ χ)
R[KEᶥ] (_ ⇾ ρ) α ζ χ = λ η → R[KEᶥ] ρ α (λ i → ζ i η) χ

--
-- Variables in related contexts are related.
--
R[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ} {ξ : ⟦ Γ ⟧ˣ} (α : ℕᴺ)
→ Rˣ α γ ξ → (i : ∥ ρ ∈ Γ ∥) → R α (γ ₍ ⟨ i ⟩ᵛ ₎) (ξ ₍ i ₎)
R[Var] {ε}     α  _      ()
R[Var] {Γ ₊ ρ} α (_ , θ)  zero    = θ
R[Var] {Γ ₊ ρ} α (ζ , _) (succ i) = R[Var] α ζ i

--
-- Terms are related to their b-translations.
--
Lemma[R] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ) (α : ℕᴺ)
→ {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ} {ξ : ⟦ Γ ⟧ˣ} → Rˣ α γ ξ
→ R α (⟦ ⟨ t ⟩ᵐ ⟧ᵐ γ) (⟦ t ⟧ᵐ ξ)
Lemma[R] (Var i)  α ζ = R[Var] α ζ i
Lemma[R] (Lam t)  α ζ = λ χ → Lemma[R] t α (ζ , χ)
Lemma[R] (f · a)  α ζ = Lemma[R] f α ζ (Lemma[R] a α ζ)
Lemma[R] Zero     _ _ = refl
Lemma[R] Succ     α _ = ap succ
Lemma[R] (Rec{ρ}) α _ {x} {y} χ {f} {g} η = goal
where
claim : (i : ℕ) → R {ρ} α (rec x (λ k → f (λ _ → k)) i) (rec y g i)
claim  0       = χ
claim (succ i) = η refl (claim i)
goal : R {ι ⇾ ρ} α (⟦ KEᶥ ρ ⟧ᵐ _ (rec x (λ k → f (λ _ → k)))) (rec y g)
goal = R[KEᶥ] ρ α claim

--
-- A particular case of Lemma[R]
--
Lemma[R]ᶥ : (t : T ε ((ι ⇾ ι) ⇾ ι))
→ (α : ℕᴺ) → ⟦ ⟨ t ⟩ᵐ · Ω ⟧ α ≡ ⟦ t ⟧ α
Lemma[R]ᶥ t α = Lemma[R] t α ⋆ (ap α)

\end{code}

===============================================
=                                             =
=  §2  Continuity of T-definable functionals  =
=                                             =
===============================================

■ Continuity of functions ℕᴺ → ℕ

\begin{code}

--
-- α ≡[ n ] β  expresses that the first n bits of α and β are equal
--
data _≡[_]_ {A : Set} : A ᴺ → ℕ → A ᴺ → Set where
≡[zero] : {α β : A ᴺ} → α ≡[ 0 ] β
≡[succ] : {α β : A ᴺ} {n : ℕ} → head α ≡ head β → tail α ≡[ n ] tail β → α ≡[ succ n ] β

≡[≤] : {A : Set} {α β : A ᴺ} {n m : ℕ}
→ α ≡[ n ] β → m ≤ n → α ≡[ m ] β
≡[≤]  en             ≤zero    = ≡[zero]
≡[≤] (≡[succ] e en) (≤succ r) = ≡[succ] e (≡[≤] en r)

≡[]-< : {A : Set} {α β : A ᴺ} {n i : ℕ}
→ α ≡[ n ] β → succ i ≤ n → α i ≡ β i
≡[]-< (≡[succ] e en) (≤succ ≤zero)     = e
≡[]-< (≡[succ] e en) (≤succ (≤succ r)) = ≡[]-< en (≤succ r)

continuous : (ℕᴺ → ℕ) → Set
continuous f = (α : ℕᴺ) → Σ \(m : ℕ) → (β : ℕᴺ) → α ≡[ m ] β → f α ≡ f β

continuity-extensional : {f g : ℕᴺ → ℕ}
→ ((α : ℕᴺ) → f α ≡ g α) → continuous f → continuous g
continuity-extensional {f} {g} e cf α = m , prf
where
m : ℕ
m = pr₁ (cf α)
prf : (β : ℕᴺ) → α ≡[ m ] β → g α ≡ g β
prf β em = trans (sym (e α)) (trans (pr₂ (cf α) β em) (e β))

\end{code}

■ A continuity predicate

\begin{code}

C : (ρ : Ty) → ⟦ ⟨ ρ ⟩ʸ ⟧ʸ → Set
C  ι      f = continuous f
C (σ ⇾ τ) f = {a : ⟦ ⟨ σ ⟩ʸ ⟧ʸ} → C σ a → C τ (f a)

Cˣ : {Γ : Cxt} → ⟦ ⟨ Γ ⟩ˣ ⟧ˣ → Set
Cˣ {ε}      ⋆      = 𝟙
Cˣ {Γ ₊ ρ} (γ , a) = Cˣ γ × C ρ a

--
-- The generic sequence satisfies C
--
C[Ω] : C (ι ⇾ ι) ⟦ Ω ⟧
C[Ω] {f} cf α = m , prf
where
n₀ : ℕ
n₀ = pr₁ (cf α)
n₁ : ℕ
n₁ = succ (f α)
m : ℕ
m = max n₀ n₁
prf : (β : ℕᴺ) → α ≡[ m ] β → α (f α) ≡ β (f β)
prf β em = trans e₂ e₁
where
e₀ : f α ≡ f β
e₀ = pr₂ (cf α) β (≡[≤] em (max-spec₀ n₀ n₁))
e₁ : β (f α) ≡ β (f β)
e₁ = ap β e₀
e₂ : α (f α) ≡ β (f α)
e₂ = ≡[]-< em (max-spec₁ n₀ n₁)

--
-- The Kleisli extension preserves C.
--
C[KEᶥ] : (ρ : Ty)
→ {g : ℕ → ⟦ ⟨ ρ ⟩ʸ ⟧ʸ} → ((i : ℕ) → C ρ (g i))
→ {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ}
→ C (ι ⇾ ρ) (⟦ KEᶥ ρ ⟧ᵐ γ g)
C[KEᶥ] ι {g} cg {_} {_} {f} cf = goal
where
goal : continuous (λ α → g (f α) α)
goal α = m , prf
where
n₀ n₁ : ℕ
n₀ = pr₁ (cg (f α) α)
n₁ = pr₁ (cf α)
m : ℕ
m = max n₀ n₁
prf : (β : ℕᴺ) → α ≡[ m ] β → g (f α) α ≡ g (f β) β
prf β em = trans e₂ e₁
where
e₀ : f α ≡ f β
e₀ = pr₂ (cf α) β (≡[≤] em (max-spec₁ n₀ n₁))
e₁ : g (f α) β ≡ g (f β) β
e₁ = ap (λ i → g i β) e₀
e₂ : g (f α) α ≡ g (f α) β
e₂ = pr₂ (cg (f α) α) β (≡[≤] em (max-spec₀ n₀ n₁))
C[KEᶥ] (_ ⇾ ρ) cg cf = λ ca → C[KEᶥ] ρ (λ i → cg i ca) cf

--
-- Variables satisfy C.
--
C[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ}
→ Cˣ γ → (i : ∥ ρ ∈ Γ ∥) → C ρ (γ ₍ ⟨ i ⟩ᵛ ₎)
C[Var] {ε}      _      ()
C[Var] {Γ ₊ ρ} (δ , θ)  zero    = θ
C[Var] {Γ ₊ ρ} (δ , θ) (succ i) = C[Var] δ i

--
-- The b-translation of any T term satisfies C.
--
Lemma[C] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ)
→ {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ} → Cˣ γ → C ρ (⟦ ⟨ t ⟩ᵐ ⟧ᵐ γ)
Lemma[C] (Var i) δ = C[Var] δ i
Lemma[C] (Lam t) δ = λ θ → Lemma[C] t (δ , θ)
Lemma[C] (f · a) δ = Lemma[C] f δ (Lemma[C] a δ)
Lemma[C] Zero _ = λ α → (0 , λ _ _ → refl)
Lemma[C] Succ _ {f} cf α = m , prf
where
m : ℕ
m = pr₁ (cf α)
prf : (β : ℕᴺ) → α ≡[ m ] β → succ (f α) ≡ succ (f β)
prf β em = ap succ (pr₂ (cf α) β em)
Lemma[C] (Rec {ρ}) _ {a} ca {f} cf = C[KEᶥ] ρ cg
where
g : ℕ → ⟦ ⟨ ρ ⟩ʸ ⟧ʸ
g = rec a (λ k → f (λ _ → k))
cg : (i : ℕ) → C ρ _
cg  0       = ca
cg (succ i) = cf (λ _ → 0 , (λ _ _ → refl)) (cg i)

\end{code}

■ Main result

\begin{code}

Theorem[TCont] : (f : ℕᴺ → ℕ) → T-definable f → continuous f
Theorem[TCont] f (t , refl) = cont-f
where
claim₀ : (α : ℕᴺ) → ⟦ ⟨ t ⟩ᵐ · Ω ⟧ α ≡ ⟦ t ⟧ α
claim₀ = Lemma[R]ᶥ t
claim₁ : continuous (⟦ ⟨ t ⟩ᵐ · Ω ⟧)
claim₁ = Lemma[C] t ⋆ C[Ω]
cont-f : continuous f
cont-f = continuity-extensional claim₀ claim₁

\end{code}

====================================
=                                  =
=  §3  Experiments of computation  =
=                                  =
====================================

Because MLTT/Agda proofs are programs, we can run the main theorem to
compute moduli of continuity of T-definable functions.  We develop
some experiments to illustrate this.

■ (External) modulus-of-continuity functional M

\begin{code}

M : T ε ((ι ⇾ ι) ⇾ ι) → ℕᴺ → ℕ
M t α = pr₁ (Theorem[TCont] ⟦ t ⟧ (t , refl) α)

M-spec : (t : T ε ((ι ⇾ ι) ⇾ ι))
→ (α β : ℕᴺ) → α ≡[ M t α ] β → ⟦ t ⟧ α ≡ ⟦ t ⟧ β
M-spec t α = pr₂ (Theorem[TCont] ⟦ t ⟧ (t , refl) α)

\end{code}

■ Some auxiliaries

\begin{code}

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

Plus : {Γ : Cxt} → T Γ ι → T Γ ι → T Γ ι
Plus N M = Rec · N · Lam Succ · M

_+_ : ℕ → ℕ → ℕ
n + m = rec n (λ _ → succ) m

0ʷ : ℕᴺ
0ʷ i = 0

δ : ℕᴺ
δ i = i

infixr 1 _✶_

_✶_ : ℕ → ℕᴺ → ℕᴺ
(k ✶ α)  0       = k
(k ✶ α) (succ i) = α i

\end{code}

■ Examples of closed T terms

t₀ is a constant function

\begin{code}

t₀ : T ε ((ι ⇾ ι) ⇾ ι)
t₀ = Lam (Num 4)

t₀-interpretation : ⟦ t₀ ⟧ ≡ λ α → 4
t₀-interpretation = refl

result₀ :  M t₀ 0ʷ ≡ 0
×  M t₀ δ ≡ 0
×  M t₀ succ ≡ 0
×  M t₀ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 0
result₀ = refl , refl , refl , refl

\end{code}

t₁ is a non-trivial constant function: it applies the identity
function α₁₇ (the 18th bit of α) times on value 4.

\begin{code}

t₁ : T ε ((ι ⇾ ι) ⇾ ι)
t₁ = Lam (Rec · Num 4 · Lam (Lam ν₀) · (ν₀ · Num 17))

t₁-interpretation : ⟦ t₁ ⟧ ≡ λ α → rec 4 (λ _ k → k) (α 17)
t₁-interpretation = refl

result₁ :  M t₁ 0ʷ ≡ 18
×  M t₁ δ ≡ 18
×  M t₁ succ ≡ 18
×  M t₁ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 18
result₁ = refl , refl , refl , refl

\end{code}

t₂ is a simple function returning the 18th bit of the input.

\begin{code}

t₂ : T ε ((ι ⇾ ι) ⇾ ι)
t₂ = Lam (ν₀ · Num 17)

t₂-interpretation : ⟦ t₂ ⟧ ≡ λ α → α 17
t₂-interpretation = refl

result₂ :  M t₂ 0ʷ ≡ 18
×  M t₂ δ ≡ 18
×  M t₂ succ ≡ 18
×  M t₂ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 18
result₂ = refl , refl , refl , refl

\end{code}

t₃ is taken from [2]:  λα.α(α(…(α0)…))  with α0 applications of α.

\begin{code}

t₃ : T ε ((ι ⇾ ι) ⇾ ι)
t₃ = Lam (Rec · Num 0 · Lam ν₁ · (ν₀ · Num 0))

t₃-interpretation : ⟦ t₃ ⟧ ≡ λ α → rec 0 (λ _ → α) (α 0)
t₃-interpretation = refl

result₃ :  M t₃ 0ʷ ≡ 1
×  M t₃ δ ≡ 1
×  M t₃ succ ≡ 1
×  M t₃ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 13
result₃ = refl , refl , refl , refl

\end{code}

t₄ is taken from [1] in which is named t₃.

\begin{code}

t₄ : T ε ((ι ⇾ ι) ⇾ ι)
t₄ = Lam (Rec · (ν₀ · Num 1) · (Lam ν₁) · (Plus (ν₀ · Num 2) (ν₀ · Num 3)))

t₄-interpretation : ⟦ t₄ ⟧ ≡ λ α → rec (α 1) (λ _ → α) (α 2 + α 3)
t₄-interpretation = refl

result₄ :  M t₄ 0ʷ ≡ 4
×  M t₄ δ ≡ 4
×  M t₄ succ ≡ 9
×  M t₄ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 68
result₄ = refl , refl , refl , refl

\end{code}

t₅ is also taken from [1]. The evaluations of this complicated example
are instantaneous.

\begin{code}

t₅ : T ε ((ι ⇾ ι) ⇾ ι)
t₅ = Lam (Rec · (ν₀ · (Rec · (ν₀ · (Rec · (ν₀ · Num 17) · Lam ν₁ · (ν₀ · Num 17)))
· Lam ν₁
· (Rec · (Plus (ν₀ · (ν₀ · Num 2)) (ν₀ · Num 3))
· Lam ν₁
· (Rec · (ν₀ · Num 1) · Lam ν₁ · (Plus (ν₀ · Num 2) (ν₀ · Num 3))))))
· (Lam ν₁)
· (ν₀ · Num 2))

t₅-interpretation : ⟦ t₅ ⟧ ≡ λ α → rec (α (rec (α (rec (α 17) (λ _ → α) (α 17)))
(λ _ → α)
(rec (α (α 2) + α 3)
(λ _ → α)
(rec (α 1) (λ _ → α) (α 2 + α 3)))))
(λ _ → α)
(α 2)
t₅-interpretation = refl

result₅ :  M t₅ 0ʷ ≡ 18
×  M t₅ δ ≡ 18
×  M t₅ succ ≡ 58
×  M t₅ (12 ✶ 67 ✶ 8 ✶ 99 ✶ 3 ✶ 0ʷ) ≡ 68
result₅ = refl , refl , refl , refl

\end{code}