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

Experiment of computing moduli of uniform continuity

\begin{code}

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

module UsingSetoid.ModellingUC.ComputationExperiments where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness
open import UsingSetoid.Space.DiscreteSpace
open import UsingSetoid.Space.YonedaLemma
open import UsingSetoid.Space.Fan
open import UsingSetoid.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₁ (pr₁ (pr₁ ⟦ t ⟧ᵐ) ⋆)) (pr₁ ID α)

modu : Tm ε ((Ⓝ ⇨ ②) ⇨ Ⓝ) → ℕ
modu F = pr₁ (pr₁ fan) (pr₁ (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₁ ⟧ ≡ λ α → 2 
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 (α 0) 1 1
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 (α 3) 5 (if (α 4) 1 2) 
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 (α 1) (if (α 2) 0 0) (if (α 3) 0 0)
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 (α 1) 3 2)
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₅ ⟧ α)) 5 2) (λ _ → succ)
                                       (if (α (⟦ F₄ ⟧ α)) 3 2)
F₆-interpretation = refl

\end{code}