Chuangjie Xu, 2013

This corresponds to part of Section 4.2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf


Now we interpret T in C-spaces.

\begin{code}

module C-interpretation-of-T where

open import MiniLibrary
open import Sequence
open import Space
open import Space-product
open import Space-exponential
open import Space-discrete
open import not-not
open import Inequality
open import UniformContinuity
open import Fan
open import T

\end{code}

Interpretation of types:

\begin{code}

【_】 : Ty → Space
【 ② 】 = ₂Space
【 Ⓝ 】 = ℕSpace
【 σ ⇨ τ 】 = 【 σ 】 ⇒ 【 τ 】

\end{code}

Interpretation of contexts:

\begin{code}

〖_〗 : {n : ℕ} → Cxt n → Space
〖 ε 〗      = ⒈Space
〖 σs ₊ σ 〗 = 〖 σs 〗 ⊗ 【 σ 】

\end{code}

Interpretation of the index function, which is continuous:

\begin{code}

_﹝_﹞ : {n : ℕ}{Γ : Cxt n} → U 〖 Γ 〗 → (i : Fin n) → U 【 Γ ₍ i ₎ 】
_﹝_﹞ {}      {ε}      ⋆        ()
_﹝_﹞ {succ n} {σs ₊ σ} (xs , x) zero     = x
_﹝_﹞ {succ n} {σs ₊ σ} (xs , x) (succ i) = xs ﹝ i ﹞

﹝﹞-is-continuous : {n : ℕ}{Γ : Cxt n}{i : Fin n} → continuous {〖 Γ 〗} {【 Γ ₍ i ₎ 】} (λ xs → xs ﹝ i ﹞)
﹝﹞-is-continuous {}      {ε}     {()}
﹝﹞-is-continuous {succ n} {Γ ₊ σ} {zero}   = λ _ → ∧-elim₁
﹝﹞-is-continuous {succ n} {Γ ₊ σ} {succ i} = λ p pΓσ → IH (π₀ ∘ p) (∧-elim₀ pΓσ)
 where
  IH : continuous {〖 Γ 〗} {【 Γ ₍ i ₎ 】} (λ xs → xs ﹝ i ﹞)
  IH = ﹝﹞-is-continuous {n} {Γ} {i}

\end{code}

Interpretation of terms in context, which are continuous functions from the
interpretations of contexts to the ones of types:

\begin{code}

⟦_⟧ : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Map 〖 Γ 〗 【 σ 】
⟦ ⊥ ⟧                      = (λ _ → ₀) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ ⊤ ⟧                      = (λ _ → ₁) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ IF {n} {Γ} {σ} ⟧         = (λ _ → continuous-if {【 σ 】}) , (λ _ _ p pσ _ _ → π₁ (continuous-if {【 σ 】}) p pσ)
⟦ ZERO ⟧                   = (λ _ → ) , (λ _ _ →  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero))
⟦ SUCC ⟧                   = (λ _ → continuous-succ) , (λ _ _ p pN _ _ → π₁ continuous-succ p pN)
⟦ REC {n} {Γ} {σ} ⟧        = (λ _ → continuous-rec {【 σ 】}) , (λ _ _ p pσ _ _ → π₁ (continuous-rec {【 σ 】}) p pσ)
⟦ VAR {n} {Γ} i ⟧          = (λ xs → xs ﹝ i ﹞) , ﹝﹞-is-continuous {n} {Γ} {i}
⟦ LAM {n} {Γ} {σ} {τ} M ⟧  = f , cts-f
 where
  f : U 〖 Γ 〗 → U 【 σ ⇨ τ 】
  f xs = g , cts-g
   where
    g : U 【 σ 】 → U 【 τ 】
    g x = π₀ ⟦ M ⟧ (xs , x)
    cts-g : continuous {【 σ 】} {【 τ 】} g
    cts-g p pσ = π₁ ⟦ M ⟧ q qΓσ
     where
      q : ₂ℕ → U 〖 Γ ₊ σ 〗
      q α = (xs , p α)
      qΓσ : q ∈ Probe 〖 Γ ₊ σ 〗
      qΓσ = cond₀ 〖 Γ 〗 (λ _ → xs) (λ _ _ → refl) , pσ
  cts-f : continuous {〖 Γ 〗} {【 σ ⇨ τ 】} f
  cts-f p pΓ q qσ t uc = π₁ ⟦ M ⟧ r rΓσ
   where
    r : ₂ℕ → U 〖 Γ ₊ σ 〗
    r α = (p(t α) , q α)
    rΓσ : r ∈ Probe 〖 Γ ₊ σ 〗
    rΓσ = cond₁ 〖 Γ 〗 t uc p pΓ , qσ
⟦ _∙_ {n} {Γ} {σ} {τ} M N ⟧ = f , cts-f
 where
  f : U 〖 Γ 〗 → U 【 τ 】
  f xs = π₀ (π₀ ⟦ M ⟧ xs) (π₀ ⟦ N ⟧ xs)
  cts-f : continuous {〖 Γ 〗} {【 τ 】} f
  cts-f p pΓ = π₁ ⟦ M ⟧ p pΓ ((π₀ ⟦ N ⟧) ∘ p) (π₁ ⟦ N ⟧ p pΓ) id Lemma[id-UC]
⟦ FAN ⟧ = (λ xs → fan) , (λ _ _ → λ p pP _ _ → π₁ fan p pP)

\end{code}

This extended system T can calculate the least moduli of uniform continuity of
the system T definable maps ₂ℕ → ℕ. Here we provide some examples. Evaluating
"modu F₀", for instance, gives you the least moduli of uniform continuity of the
map F₀.

\begin{code}

modu : Tm ε ((Ⓝ ⇨ ②) ⇨ Ⓝ) → ℕ
modu F = π₀ ⟦ FAN ∙ F ⟧ ⋆

ONE TWO THREE FOUR FIVE : {n : ℕ}{Γ : Cxt n} → Tm Γ Ⓝ
ONE   = SUCC ∙ ZERO
TWO   = SUCC ∙ ONE
THREE = SUCC ∙ TWO
FOUR  = SUCC ∙ THREE
FIVE  = SUCC ∙ FOUR

F₀ F₁ F₂ F₃ F₄ F₅ F₆ : Tm ε ((Ⓝ ⇨ ②) ⇨ Ⓝ)

\end{code}

F₀ is constant.

\begin{code}

F₀ = LAM ZERO

\end{code}

F₁ looks at the 6th bit of input to decide output.

\begin{code}

F₁ = LAM (IF ∙ TWO ∙ ONE ∙ (VAR zero ∙ FIVE))

\end{code}

F₂ is constant, though it looks at the 6th bit of input.

\begin{code}

F₂ = LAM (IF ∙ ONE ∙ ONE ∙ (VAR zero ∙ FIVE))

\end{code}

F₃ returns 5, if the 4th bit is ⊥.
F₃ returns 1, if the 4th bit is ⊤ and the 5th one is ⊥.
F₃ returns 2, if both the 4th and 5th bits are ⊤.

\begin{code}

F₃ = LAM (IF ∙ FIVE ∙ (IF ∙ ONE ∙ TWO ∙ (VAR zero ∙ FOUR)) ∙ (VAR zero ∙ THREE))

\end{code}

F₄ is constant. It looks at 3rd and 4th or 5th bits and then returns 5.

\begin{code}

F₄ = LAM (IF ∙ (IF ∙ FIVE ∙ FIVE ∙ (VAR zero ∙ FOUR)) ∙ (IF ∙ FIVE ∙ FIVE ∙ (VAR zero ∙ THREE)) ∙ (VAR zero ∙ TWO))

\end{code}

If the 4th bit is ⊥, then F₅ applies SUCC to ZERO 5 times, i.e. returns 5.
If the 4th bit is ⊤, then F₅ applies SUCC to ZERO twice, i.e. returns 2.

\begin{code}

F₅ = LAM (REC ∙ ZERO ∙ LAM SUCC ∙ (IF ∙ FIVE ∙ TWO ∙ (VAR zero ∙ THREE)))

\end{code}

If both the 1st and 2nd bits are ⊥, then F₆ applies SUCC to FIVE 3 times, i.e. returns 8.
If 1st bit is ⊥ and the 2nd one is ⊤, then F₆ applies SUCC to TWO 3 times, i.e. returns 5.
If 1st bit is ⊤ and the 2nd one is ⊥, then F₆ applies SUCC to FIVE twice, i.e. returns 7.
If both the 1st and 2nd bits are ⊤, then F₆ applies SUCC to TWO twice, i.e. returns 4.

\begin{code}

F₆ = LAM (REC ∙ (IF ∙ FIVE ∙ TWO ∙ (VAR zero ∙ ONE)) ∙ LAM SUCC ∙ (IF ∙ THREE ∙ TWO ∙ (VAR zero ∙ ZERO)))

\end{code}