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₁   λ α  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}