Chuangjie Xu and Martin Escardo 2014 (updated in February 2015)

Experiment of computing moduli of uniform continuity

\begin{code}

{-# OPTIONS --without-K #-}

module AddingProbeAxiom.ModellingUC.ComputationExperiments where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import AddingProbeAxiom.Space.Space
open import AddingProbeAxiom.Space.DiscreteSpace
open import AddingProbeAxiom.Space.CartesianClosedness
open import AddingProbeAxiom.Space.YonedaLemma
open import AddingProbeAxiom.Space.Fan
open import AddingProbeAxiom.ModellingUC.UCinT

\end{code}

We define an abbreviation of the interpretation of closed terms with
meaning in the function space ₂ℕ → ℕ:

\begin{code}

⟦_⟧ : Tm ε ( ((Ⓝ ⇨ ②) ⇨ Ⓝ)) → ₂ℕ → ℕ
⟦ t ⟧ α = pr₁ (pr₁ ⟦ t ⟧ᵐ ⋆) (ID α)

modu : Tm ε ((Ⓝ ⇨ ②) ⇨ Ⓝ) → ℕ
modu F = pr₁ fan (pr₁ ⟦ 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₆ : {n : ℕ} {Γ : Cxt n} → Tm Γ ((Ⓝ ⇨ ②) ⇨ Ⓝ)

\end{code}

F₁ is constant.

\begin{code}

F₁ = LAM TWO

F₁-interpretation : ⟦ F₁ ⟧ ≡ λ α →  
F₁-interpretation = refl

\end{code}

F₂ is constant, though it looks at the 1st bit of input.

\begin{code}

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

F₂-interpretation : ⟦ F₂ ⟧ ≡ λ α → if (α )  
F₂-interpretation = refl

\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 ∙ (VAR zero ∙ THREE) ∙ FIVE
             ∙ (IF ∙ (VAR zero ∙ FOUR) ∙ ONE ∙ TWO))

F₃-interpretation : ⟦ F₃ ⟧ ≡ λ α → if (α )  (if (α )  ) 
F₃-interpretation = refl

\end{code}

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

\begin{code}

F₄ = LAM (IF ∙ (VAR zero ∙ ONE) ∙ (IF ∙ (VAR zero ∙ TWO) ∙ ZERO ∙ ZERO)
             ∙ (IF ∙ (VAR zero ∙ THREE) ∙ ZERO ∙ ZERO))

F₄-interpretation : ⟦ F₄ ⟧ ≡ λ α → if (α ) (if (α )  ) (if (α )  )
F₄-interpretation = refl

\end{code}

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

\begin{code}

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

F₅-interpretation : ⟦ F₅ ⟧ ≡ λ α → rec zero (λ _ → succ) (if (α )  )
F₅-interpretation = refl

\end{code}

A more complicated example

\begin{code}

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

F₆-interpretation : ⟦ F₆ ⟧ ≡ λ α → rec (if (α (⟦ F₅ ⟧ α))  ) (λ _ → succ)
                                       (if (α (⟦ F₄ ⟧ α))  )
F₆-interpretation = refl

\end{code}