Martin Escardo 2012-2013.

This is the file without comments for illustration. Maybe you wish to see

  http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.lagda
  http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.html
  http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf

instead.

\begin{code}

module laconic-dialogue where

Ķ : ∀{X Y : Set}  X  Y  X
Ķ x y = x

Ş : ∀{X Y Z : Set}  (X  Y  Z)  (X  Y)  X  Z
Ş f g x = f x (g x)

_∘_ : ∀{X Y Z : Set}  (Y  Z)  (X  Y)  (X  Z)
g  f = λ x  g(f x)

data ℕ₂ : Set where
   : ℕ₂
   : ℕ₂

data  : Set where 
  zero :               
  succ :          

rec : ∀{X : Set}  (X  X)  X    X
rec f x  zero    = x
rec f x (succ n) = f(rec f x n)

data List (X : Set) : Set where
  []  : List X
  _∷_ : X  List X  List X

data Tree (X : Set) : Set where
  empty  : Tree X
  branch : X  (ℕ₂  Tree X)  Tree X

data Σ {X : Set} (Y : X  Set) : Set where
  _,_ : ∀(x : X)(y : Y x)  Σ {X} Y

π₀ : ∀{X : Set} {Y : X  Set}  (Σ \(x : X)  Y x)  X
π₀(x , y) = x

π₁ : ∀{X : Set} {Y : X  Set}  ∀(t : Σ \(x : X)  Y x)  Y(π₀ t)
π₁(x , y) = y

data _≡_ {X : Set} : X  X  Set where
  refl : ∀{x : X}  x  x

sym : ∀{X : Set}  ∀{x y : X}  x  y  y  x
sym refl = refl

trans : ∀{X : Set}  ∀{x y z : X}  x  y  y  z  x  z
trans refl refl = refl

cong : ∀{X Y : Set}  ∀(f : X  Y)  ∀{x₀ x₁ : X}  x₀  x₁  f x₀  f x₁
cong f refl = refl

cong₂ : ∀{X Y Z : Set}  ∀(f : X  Y  Z) 
       ∀{x₀ x₁ : X}{y₀ y₁ : Y}  x₀  x₁  y₀  y₁  f x₀ y₀  f x₁ y₁
cong₂ f refl refl = refl

data D (X Y Z : Set) : Set where 
  η : Z  D X Y Z
  β : (Y  D X Y Z)  X  D X Y Z

dialogue : ∀{X Y Z : Set}  D X Y Z  (X  Y)  Z
dialogue (η z)   α = z
dialogue (β φ x) α = dialogue (φ(α x)) α

eloquent : ∀{X Y Z : Set}  ((X  Y)  Z)  Set
eloquent f = Σ \d   α  dialogue d α  f α

Baire : Set
Baire =   

B : Set  Set
B = D  

data _≡[_]_ {X : Set} : (  X)  List   (  X)  Set where
  []  : ∀{α α' :   X}  α ≡[ [] ] α' 
  _∷_ : ∀{α α' :   X}{i : }{s : List }  α i  α' i  α ≡[ s ] α'  α ≡[ i  s ] α'

continuous : (Baire  )  Set
continuous f = ∀(α : Baire)  Σ \(s : List )  ∀(α' : Baire)  α ≡[ s ] α'  f α  f α'

dialogue-continuity : ∀(d : B )  continuous(dialogue d)
dialogue-continuity (η n) α = ([] , lemma)
  where
   lemma :  α'  α ≡[ [] ] α'  n  n 
   lemma α' r = refl
dialogue-continuity (β φ i) α = ((i  s) , lemma) 
  where
   IH : ∀(i : )  continuous(dialogue(φ(α i)))
   IH i = dialogue-continuity (φ(α i))
   s : List 
   s = π₀(IH i α)
   claim₀ : ∀(α' : Baire)  α ≡[ s ] α'  dialogue(φ(α i)) α  dialogue(φ(α i)) α'
   claim₀ = π₁(IH i α)
   claim₁ : ∀(α' : Baire)  α i  α' i  dialogue (φ (α i)) α'  dialogue (φ (α' i)) α'
   claim₁ α' r = cong  n  dialogue (φ n) α') r
   lemma : ∀(α' : Baire)  α ≡[ i  s ] α'   dialogue (φ(α i)) α  dialogue(φ (α' i)) α'
   lemma α' (r  rs) = trans (claim₀ α' rs) (claim₁ α' r)

continuity-extensional : ∀(f g : Baire  )  (∀(α : Baire)  f α  g α)  continuous f  continuous g
continuity-extensional f g t c α = (π₀(c α) ,  α' r  trans (sym (t α)) (trans (π₁(c α) α' r) (t α'))))

eloquent-is-continuous : ∀(f : Baire  )  eloquent f  continuous f
eloquent-is-continuous f (d , e) = continuity-extensional (dialogue d) f e (dialogue-continuity d)

Cantor : Set
Cantor =   ℕ₂

C : Set  Set
C = D  ℕ₂

data _≡[[_]]_ {X : Set} : (  X)  Tree   (  X)  Set where
  empty  : ∀{α α' :   X}  α ≡[[ empty ]] α' 
  branch : ∀{α α' :   X}{i : }{s : ℕ₂  Tree } 
          α i  α' i  (∀(j : ℕ₂)  α ≡[[ s j ]] α')  α ≡[[ branch i s ]] α'

uniformly-continuous : (Cantor  )  Set
uniformly-continuous f = Σ \(s : Tree )  ∀(α α' : Cantor)  α ≡[[ s ]] α'  f α  f α'

dialogue-UC : ∀(d : C )  uniformly-continuous(dialogue d)
dialogue-UC (η n) = (empty , λ α α' n  refl)
dialogue-UC (β φ i) = (branch i s , lemma)
  where
    IH : ∀(j : ℕ₂)  uniformly-continuous(dialogue(φ j))
    IH j = dialogue-UC (φ j)
    s : ℕ₂  Tree 
    s j = π₀(IH j)
    claim :  j α α'  α ≡[[ s j ]] α'  dialogue (φ j) α  dialogue (φ j) α'
    claim j = π₁(IH j)
    lemma :  α α'  α ≡[[ branch i s ]] α'  dialogue (φ (α i)) α  dialogue (φ (α' i)) α' 
    lemma α α' (branch r l) = trans fact₀ fact₁ 
      where
       fact₀ : dialogue (φ (α i)) α  dialogue (φ (α' i)) α 
       fact₀ = cong  j  dialogue(φ j) α) r
       fact₁ : dialogue (φ (α' i)) α  dialogue (φ (α' i)) α'
       fact₁ = claim (α' i) α α' (l(α' i))

UC-extensional : ∀(f g : Cantor  )  (∀(α : Cantor)  f α  g α) 
               uniformly-continuous f  uniformly-continuous g
UC-extensional f g t (u , c) = (u ,  α α' r  trans (sym (t α)) (trans (c α α' r) (t α'))))

eloquent-is-UC : ∀(f : Cantor  )  eloquent f  uniformly-continuous f
eloquent-is-UC f (d , e) = UC-extensional (dialogue d) f e (dialogue-UC d)

embed-ℕ₂-ℕ : ℕ₂  
embed-ℕ₂-ℕ  = zero
embed-ℕ₂-ℕ  = succ zero

embed-C-B : Cantor  Baire
embed-C-B α = embed-ℕ₂-ℕ  α 
 
C-restriction : (Baire  )  (Cantor  )
C-restriction f = f  embed-C-B

prune : B   C 
prune (η n) = η n
prune (β φ i) = β  j  prune(φ(embed-ℕ₂-ℕ j))) i

prune-behaviour : ∀(d : B )(α : Cantor)  dialogue (prune d) α  C-restriction(dialogue d) α 
prune-behaviour (η n)   α = refl
prune-behaviour (β φ n) α = prune-behaviour (φ(embed-ℕ₂-ℕ(α n))) α

eloquent-restriction : ∀(f : Baire  )  eloquent f  eloquent(C-restriction f)
eloquent-restriction f (d , c) = (prune d , λ α  trans (prune-behaviour d α) (c (embed-C-B α))) 

data type : Set where
  ι   : type
  _⇒_ : type  type  type

data T : (σ : type)  Set where
  Zero : T ι
  Succ : T(ι  ι)
  Rec  : ∀{σ : type}      T((σ  σ)  σ  ι  σ)
  K    : ∀{σ τ : type}    T(σ  τ  σ)
  S    : ∀{ρ σ τ : type}  T((ρ  σ  τ)  (ρ  σ)  ρ  τ)
  _·_  : ∀{σ τ : type}    T(σ  τ)  T σ  T τ

infixr 1 _⇒_
infixl 1 _·_

Set⟦_⟧ : type  Set
Set⟦ ι  = 
Set⟦ σ  τ  = Set⟦ σ   Set⟦ τ 

⟦_⟧ : ∀{σ : type}  T σ  Set⟦ σ 
 Zero   = zero
 Succ   = succ
 Rec    = rec
 K      = Ķ
 S      = Ş
 t · u  =  t   u  

T-definable : ∀{σ : type}  Set⟦ σ   Set
T-definable x = Σ \t   t   x

data  : (σ : type)  Set where
  Ω    : (ι  ι)
  Zero :  ι
  Succ : (ι  ι)
  Rec  : ∀{σ : type}      ((σ  σ)  σ  ι  σ)
  K    : ∀{σ τ : type}    (σ  τ  σ)
  S    : ∀{ρ σ τ : type}  ((ρ  σ  τ)  (ρ  σ)  ρ  τ)
  _·_  : ∀{σ τ : type}    (σ  τ)   σ   τ

⟦_⟧' : ∀{σ : type}   σ  Baire  Set⟦ σ 
 Ω ⟧'     α = α
 Zero ⟧'  α = zero
 Succ ⟧'  α = succ
 Rec ⟧'   α = rec
 K ⟧'     α = Ķ
 S ⟧'     α = Ş
 t · u ⟧' α =  t ⟧' α ( u ⟧' α)

embed : ∀{σ : type}  T σ   σ
embed Zero = Zero
embed Succ = Succ
embed Rec = Rec
embed K = K
embed S = S
embed (t · u) = (embed t) · (embed u)

kleisli-extension : ∀{X Y : Set}  (X  B Y)  B X  B Y
kleisli-extension f (η x)   = f x
kleisli-extension f (β φ i) = β  j  kleisli-extension f (φ j)) i

B-functor : ∀{X Y : Set}  (X  Y)  B X  B Y
B-functor f = kleisli-extension(η  f)

decode : ∀{X : Set}  Baire  B X  X
decode α d = dialogue d α

decode-α-is-natural : ∀{X Y : Set}(g : X  Y)(d : B X)(α : Baire)  g(decode α d)  decode α (B-functor g d)
decode-α-is-natural g (η x)   α = refl
decode-α-is-natural g (β φ i) α = decode-α-is-natural g (φ(α i)) α

decode-kleisli-extension : ∀{X Y : Set}(f : X  B Y)(d : B X)(α : Baire) 
                          decode α (f(decode α d))  decode α (kleisli-extension f d)
decode-kleisli-extension f (η x)   α = refl
decode-kleisli-extension f (β φ i) α = decode-kleisli-extension f (φ(α i)) α

B-Set⟦_⟧ : type  Set
B-Set⟦ ι  = B(Set⟦ ι )
B-Set⟦ σ  τ  = B-Set⟦ σ   B-Set⟦ τ 

kleisli-extension' : ∀{X : Set} {σ : type}  (X  B-Set⟦ σ )  B X  B-Set⟦ σ 
kleisli-extension' {X} {ι} = kleisli-extension
kleisli-extension' {X} {σ  τ} = λ g d s  kleisli-extension' {X} {τ}  x  g x s) d 

generic : B   B 
generic = kleisli-extension(β η)

generic-diagram : ∀(α : Baire)(d : B )  α(decode α d)  decode α (generic d) 
generic-diagram α (η n) = refl
generic-diagram α (β φ n) = generic-diagram α (φ(α n))

zero' : B 
zero' = η zero

succ' : B   B 
succ' = B-functor succ

rec' : ∀{σ : type}  (B-Set⟦ σ   B-Set⟦ σ )  B-Set⟦ σ   B   B-Set⟦ σ 
rec' f x = kleisli-extension'(rec f x)

B⟦_⟧ : ∀{σ : type}   σ  B-Set⟦ σ 
B⟦ Ω      = generic
B⟦ Zero   = zero'
B⟦ Succ   = succ'
B⟦ Rec    = rec'
B⟦ K      = Ķ
B⟦ S      = Ş
B⟦ t · u  = B⟦ t  B⟦ u 

dialogue-tree : T((ι  ι)  ι)  B 
dialogue-tree t = B⟦ (embed t) · Ω 

preservation : ∀{σ : type}  ∀(t : T σ)  ∀(α : Baire)   t    embed t ⟧' α
preservation Zero    α = refl
preservation Succ    α = refl
preservation Rec     α = refl
preservation K       α = refl
preservation S       α = refl
preservation (t · u) α = cong₂  f x  f x) (preservation t α) (preservation u α)

R : ∀{σ : type}  (Baire  Set⟦ σ )  B-Set⟦ σ   Set
R {ι} n n' =  ∀(α : Baire)  n α  decode α n'
R {σ  τ} f f' = ∀(x : Baire  Set⟦ σ )(x' : B-Set⟦ σ )  R {σ} x x'  R {τ}  α  f α (x α)) (f' x')

R-kleisli-lemma : ∀(σ : type)(g :   Baire  Set⟦ σ )(g' :   B-Set⟦ σ )
   (∀(k : )  R (g k) (g' k)) 
   ∀(n : Baire  )(n' : B )  R n n'  R  α  g (n α) α) (kleisli-extension' g' n')

R-kleisli-lemma ι g g' rg n n' rn = λ α  trans (fact₃ α) (fact₀ α)
  where
    fact₀ :  α  decode α (g' (decode α n'))  decode α (kleisli-extension g' n') 
    fact₀ = decode-kleisli-extension g' n'
    fact₁ :  α  g (n α) α  decode α (g'(n α))
    fact₁ α = rg (n α) α 
    fact₂ :  α  decode α (g' (n α))  decode α (g' (decode α n'))
    fact₂ α = cong  k  decode α (g' k)) (rn α)
    fact₃ :  α  g (n α) α  decode α (g' (decode α n'))
    fact₃ α = trans (fact₁ α) (fact₂ α)

R-kleisli-lemma (σ  τ) g g' rg n n' rn 
  = λ y y' ry  R-kleisli-lemma τ  k α  g k α (y α))  k  g' k y')  k  rg k y y' ry) n n' rn 

main-lemma : ∀{σ : type}(t :  σ)  R  t ⟧' B⟦ t 

main-lemma Ω = lemma
  where 
    claim :  α n n'  n α  dialogue n' α  α(n α)  α(decode α n')
    claim α n n' s = cong α s 
    lemma : ∀(n : Baire  )(n' : B )  (∀ α  n α  decode α n') 
            α  α(n α)  decode α (generic n')
    lemma n n' rn α = trans (claim α n n' (rn α)) (generic-diagram α n') 

main-lemma Zero = λ α  refl

main-lemma Succ = lemma
  where 
    claim :  α n n'  n α  dialogue n' α  succ(n α)  succ(decode α n')
    claim α n n' s = cong succ s  
    lemma : ∀(n : Baire  )(n' : B )  (∀ α  n α  decode α n')
           ∀(α : Baire)  succ (n α)  decode α (B-functor succ n')
    lemma n n' rn α = trans (claim α n n' (rn α)) (decode-α-is-natural succ n' α)

main-lemma {(σ  .σ)  .σ  ι  .σ} Rec = lemma
  where
   lemma : ∀(f : Baire  Set⟦ σ   Set⟦ σ )(f' : B-Set⟦ σ   B-Set⟦ σ )  R {σ  σ} f f' 
      ∀(x : Baire  Set⟦ σ )(x' : B-Set⟦ σ ) 
      R {σ} x x'  ∀(n : Baire  )(n' : B )  R {ι} n n'
      R {σ}  α  rec (f α) (x α) (n α)) (kleisli-extension'(rec f' x') n')
   lemma f f' rf x x' rx = R-kleisli-lemma σ g g' rg
     where
       g :   Baire  Set⟦ σ 
       g k α = rec (f α) (x α) k
       g' :   B-Set⟦ σ 
       g' k = rec f' x' k
       rg : ∀(k : )  R (g k) (g' k)
       rg zero = rx  
       rg (succ k) = rf (g k) (g' k) (rg k)

main-lemma K = λ x x' rx y y' ry  rx 

main-lemma S = λ f f' rf g g' rg x x' rx  rf x x' rx  α  g α (x α)) (g' x') (rg x x' rx) 

main-lemma (t · u) = main-lemma t  u ⟧' B⟦ u  (main-lemma u)

dialogue-tree-correct : ∀(t : T((ι  ι)  ι))(α : Baire)   t  α  decode α (dialogue-tree t)
dialogue-tree-correct t α = trans claim₀ claim₁
  where
    claim₀ :  t  α   (embed t) · Ω ⟧' α
    claim₀ = cong  g  g α) (preservation t α)
    claim₁ :  (embed t) · Ω ⟧' α  decode α (dialogue-tree t)
    claim₁ = main-lemma ((embed t) · Ω) α

eloquence-theorem : ∀(f : Baire  )  T-definable f  eloquent f
eloquence-theorem f (t , r) = (dialogue-tree t , λ α  trans(sym(dialogue-tree-correct t α))(cong g  g α) r))

corollary₀ : ∀(f : Baire  )  T-definable f  continuous f
corollary₀ f d = eloquent-is-continuous f (eloquence-theorem f d)

corollary₁ : ∀(f : Baire  )  T-definable f  uniformly-continuous(C-restriction f)
corollary₁ f d = eloquent-is-UC (C-restriction f) (eloquent-restriction f (eloquence-theorem f d))

\end{code}

This concludes the development. Some experiments follow (results not
included, see the pdf version, or evaluate the examples please):

\begin{code}

mod-cont : T((ι  ι)  ι)  Baire  List 
mod-cont t α = π₀(corollary₀  t  (t , refl) α)

mod-cont-obs : ∀(t : T((ι  ι)  ι))(α : Baire)  mod-cont t α  π₀(dialogue-continuity (dialogue-tree t) α)
mod-cont-obs t α = refl

infixl 0 _∷_
infixl 1 _++_

_++_ : {X : Set}  List X  List X  List X
[] ++ u = u
(x  t) ++ u = x  t ++ u

flatten : {X : Set}  Tree X  List X
flatten empty = []
flatten (branch x t) = x  flatten(t ) ++ flatten(t )

mod-unif : T((ι  ι)  ι)  List 
mod-unif t = flatten(π₀ (corollary₁  t  (t , refl)))

{-# BUILTIN NATURAL  #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}

I : ∀{σ : type}  T(σ  σ)
I {σ} = S · K · (K {σ} {σ})

I-behaviour : ∀{σ : type}{x : Set⟦ σ }   I  x  x
I-behaviour = refl 

number :   T ι
number zero = Zero
number (succ n) = Succ · (number n)

t₀ : T((ι  ι)  ι)
t₀ = K · (number 17)

t₀-interpretation :  t₀   λ α  17
t₀-interpretation = refl

example₀ example₀' : List 
example₀ = mod-cont t₀  i  i)
example₀' = mod-unif t₀

v : ∀{γ : type}  T(γ  γ)
v = I

infixl 1 _•_

_•_ : ∀{γ σ τ : type}  T(γ  σ  τ)  T(γ  σ)  T(γ  τ)
f  x = S · f · x 

Number : ∀{γ}    T(γ  ι)
Number n = K · (number n)

t₁ : T((ι  ι)  ι)
t₁ = v  (Number 17)

t₁-interpretation :  t₁   λ α  α 17
t₁-interpretation = refl

example₁ : List 
example₁ = mod-unif t₁

t₂ : T((ι  ι)  ι)
t₂ = Rec  t₁  t₁

t₂-interpretation :  t₂   λ α  rec α (α 17) (α 17)
t₂-interpretation = refl

example₂ example₂' : List 
example₂ = mod-unif t₂
example₂' = mod-cont t₂  i  i)

Add : T(ι  ι  ι)
Add = Rec · Succ

infixl 0 _+_

_+_ : ∀{γ}  T(γ  ι)  T(γ  ι)  T(γ  ι)
x + y = K · Add  x  y

t₃ : T((ι  ι)  ι)
t₃ = Rec  (v  Number 1)  (v  Number 2 + v  Number 3)

t₃-interpretation :  t₃   λ α  rec α (α 1) (rec succ (α 2) (α 3))
t₃-interpretation = refl

example₃ example₃' : List 
example₃ = mod-cont t₃ succ
example₃' = mod-unif t₃

length : {X : Set}  List X  
length [] = 0
length (x  s) = succ(length s)

max :     
max 0 x = x
max x 0 = x
max (succ x) (succ y) = succ(max x y)

Max : List   
Max [] = 0
Max (x  s) = max x (Max s)

t₄ : T((ι  ι)  ι)
t₄ = Rec  ((v  (v  Number 2)) + (v  Number 3))  t₃

t₄-interpretation :  t₄   λ α  rec α (rec succ (α (α 2)) (α 3)) (rec α (α 1) (rec succ (α 2) (α 3)))
t₄-interpretation = refl

example₄ example₄' : 
example₄ = length(mod-unif t₄)
example₄' = Max(mod-unif t₄)

t₅ : T((ι  ι)  ι)
t₅ = Rec  (v  (v  t₂ + t₄))  (v  Number 2)

t₅-explicitly : t₅   (S · (S · Rec · (S · I · (S · (S · (K · (Rec · Succ)) · (S · I · (S 
                    · (S · Rec · (S · I · (K · (number 17)))) · (S · I · (K · (number 17)))))) 
                    · (S · (S · Rec · (S · (S · (K · (Rec · Succ)) · (S · I · (S · I · (K · (number 2))))) 
                    · (S · I · (K · (number 3))))) · (S · (S · Rec · (S · I · (K · (number 1)))) 
                    · (S · (S · (K · (Rec · Succ)) · (S · I · (K · (number 2)))) · (S · I · (K 
                    · (number 3))))))))) · (S · I · (K · (number 2))))

t₅-explicitly = refl

t₅-interpretation :  t₅   λ α  rec α (α(rec succ (α(rec α (α 17) (α 17))) 
                                              (rec α (rec succ (α (α 2)) (α 3))
                                              (rec α (α 1) (rec succ (α 2) (α 3)))))) (α 2)
t₅-interpretation = refl

example₅ example₅' example₅'' : 
example₅ = length(mod-unif t₅)
example₅' = Max(mod-unif t₅)
example₅'' = Max(mod-cont t₅ succ)

\end{code}