\begin{code}
module TCont where
\end{code}\begin{code}
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
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
data 𝟙 : Set where
⋆ : 𝟙
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)
_ᴺ : Set → Set
A ᴺ = ℕ → A
ℕᴺ : Set
ℕᴺ = ℕ ᴺ
head : {A : Set} → A ᴺ → A
head α = α 0
tail : {A : Set} → A ᴺ → A ᴺ
tail α i = α (succ i)
\end{code}\begin{code}
infixr 30 _⇾_
infixl 20 _₊_
infixl 20 _·_
data Ty : Set where
ι : Ty
_⇾_ : Ty → Ty → Ty
data Cxt : Set where
ε : Cxt
_₊_ : Cxt → Ty → Cxt
data ∥_∈_∥ (σ : Ty) : Cxt → Set where
zero : {Γ : Cxt} → ∥ σ ∈ (Γ ₊ σ) ∥
succ : {τ : Ty} {Γ : Cxt} → ∥ σ ∈ Γ ∥ → ∥ σ ∈ Γ ₊ τ ∥
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}\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 ⟧ᵐ ⋆
T-definable : {ρ : Ty} → ⟦ ρ ⟧ʸ → Set
T-definable {ρ} a = Σ \(t : T ε ρ) → ⟦ t ⟧ ≡ a
\end{code}\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 ν₁))))
Ω : {Γ : Cxt} → T Γ (⟨ ι ⇾ ι ⟩ʸ)
Ω = Lam (Lam (ν₀ · (ν₁ · ν₀)))
\end{code}\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
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 η) χ
R[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ} {ξ : ⟦ Γ ⟧ˣ} (α : ℕᴺ)
→ Rˣ α γ ξ → (i : ∥ ρ ∈ Γ ∥) → R α (γ ₍ ⟨ i ⟩ᵛ ₎) (ξ ₍ i ₎)
R[Var] {ε} α _ ()
R[Var] {Γ ₊ ρ} α (_ , θ) zero = θ
R[Var] {Γ ₊ ρ} α (ζ , _) (succ i) = R[Var] α ζ i
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
Lemma[R]ᶥ : (t : T ε ((ι ⇾ ι) ⇾ ι))
→ (α : ℕᴺ) → ⟦ ⟨ t ⟩ᵐ · Ω ⟧ α ≡ ⟦ t ⟧ α
Lemma[R]ᶥ t α = Lemma[R] t α ⋆ (ap α)
\end{code}\begin{code}
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}\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
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₁)
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
C[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟨ Γ ⟩ˣ ⟧ˣ}
→ Cˣ γ → (i : ∥ ρ ∈ Γ ∥) → C ρ (γ ₍ ⟨ i ⟩ᵛ ₎)
C[Var] {ε} _ ()
C[Var] {Γ ₊ ρ} (δ , θ) zero = θ
C[Var] {Γ ₊ ρ} (δ , θ) (succ i) = C[Var] δ i
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}\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}\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}\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}\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}\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}\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}\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}\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}\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}