Internal
Martin Escardo 25 May 2013
This is an extension of The MFPS paper
https://doi.org/10.1016/j.entcs.2013.09.010 in which dialogue trees
are constructed internally in system T, rather than externally in
Agda, using Church encoding of trees (as system T doesn't directly
support trees). We work with the lambda-calculus version of the MFPS
paper.
{-# OPTIONS --safe --without-K #-}
module EffectfulForcing.MFPSAndVariations.Internal where
open import MLTT.Spartan hiding (rec ; _^_) renaming (⋆ to 〈〉)
open import MLTT.Fin
open import EffectfulForcing.MFPSAndVariations.Combinators
open import EffectfulForcing.MFPSAndVariations.SystemT
open import EffectfulForcing.MFPSAndVariations.Church
We now internalize Church encodings in system T.
⌜D⋆⌝ : type → type → type → type → type
⌜D⋆⌝ X Y Z A = (Z ⇒ A) ⇒ ((Y ⇒ A) ⇒ X ⇒ A) ⇒ A
⌜η⌝ : {X Y Z A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ (Z ⇒ ⌜D⋆⌝ X Y Z A)
⌜η⌝ = ƛ (ƛ (ƛ (ν₁ · ν₂)))
η-meaning : {X Y Z A : type} → ⟦ ⌜η⌝ {X} {Y} {Z} {A} ⟧₀ ＝ η⋆
η-meaning = refl
⌜β⌝ : {X Y Z A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ (((Y ⇒ ⌜D⋆⌝ X Y Z A) ⇒ X ⇒ ⌜D⋆⌝ X Y Z A))
⌜β⌝ = ƛ (ƛ (ƛ (ƛ (ν₀ · ƛ (ν₄ · ν₀ · ν₂ · ν₁) · ν₂))))
β-meaning : {X Y Z A : type} → ⟦ ⌜β⌝ {X} {Y} {Z} {A} ⟧₀ ＝ β⋆
β-meaning = refl
⌜B⌝ : type → type → type
⌜B⌝ = ⌜D⋆⌝ ι ι
⌜kleisli-extension⌝ : {X Y A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ ((X ⇒ ⌜B⌝ Y A) ⇒ ⌜B⌝ X A ⇒ ⌜B⌝ Y A)
⌜kleisli-extension⌝ = ƛ (ƛ (ƛ (ƛ (ν₂ · ƛ (ν₄ · ν₀ · ν₂ · ν₁) · ν₀))))
kleisli-extension-meaning : {X Y A : type}
→ ⟦ ⌜kleisli-extension⌝ {X} {Y} {A} ⟧₀
＝ kleisli-extension⋆
kleisli-extension-meaning = refl
⌜B-functor⌝ : {X Y A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ ((X ⇒ Y) ⇒ ⌜B⌝ X A ⇒ ⌜B⌝ Y A)
⌜B-functor⌝ = ƛ (⌜kleisli-extension⌝ · ƛ (⌜η⌝ · (ν₁ · ν₀)))
B-functor-meaning : {X Y A : type}
→ ⟦ ⌜B-functor⌝ {X} {Y} {A} ⟧₀
＝ B⋆-functor
B-functor-meaning = refl
B-type〖_〗 : type → type → type
B-type〖 ι 〗 A = ⌜B⌝ ι A
B-type〖 σ ⇒ τ 〗 A = B-type〖 σ 〗 A ⇒ B-type〖 τ 〗 A
⌜Kleisli-extension⌝ : {X A : type} {σ : type} {n : ℕ} {Γ : Cxt n}
→ T Γ ((X ⇒ B-type〖 σ 〗 A) ⇒ ⌜B⌝ X A ⇒ B-type〖 σ 〗 A)
⌜Kleisli-extension⌝ {X} {A} {ι} = ⌜kleisli-extension⌝
⌜Kleisli-extension⌝ {X} {A} {σ ⇒ τ} =
ƛ (ƛ (ƛ (⌜Kleisli-extension⌝ {X} {A} {τ} · ƛ (ν₃ · ν₀ · ν₁) · ν₁)))
Kleisli-extension-meaning : {X A : type} {σ τ : type}
→ ⟦ ⌜Kleisli-extension⌝ {X} {A} {σ ⇒ τ}⟧₀
＝ λ g d s → ⟦ ⌜Kleisli-extension⌝ {X} {A} {τ} ⟧
(⟨⟩ ‚ g ‚ d ‚ s)
(λ x → g x s)
d
Kleisli-extension-meaning = refl
⌜zero⌝ : {A : type} {n : ℕ} {Γ : Cxt n} → T Γ (⌜B⌝ ι A)
⌜zero⌝ = ⌜η⌝ · Zero
⌜succ⌝ : {A : type} {n : ℕ} {Γ : Cxt n} → T Γ (⌜B⌝ ι A ⇒ ⌜B⌝ ι A)
⌜succ⌝ = ⌜B-functor⌝ · Succ
⌜rec⌝ : {σ A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ ((⌜B⌝ ι A
⇒ B-type〖 σ 〗 A
⇒ B-type〖 σ 〗 A)
⇒ B-type〖 σ 〗 A
⇒ ⌜B⌝ ι A
⇒ B-type〖 σ 〗 A)
⌜rec⌝ {σ} {A} = ƛ (ƛ (⌜Kleisli-extension⌝ {ι} {A} {σ}
· (Rec · (ƛ (ν₂ · (⌜η⌝ · ν₀))) · ν₀)))
rec-meaning : {σ A : type}
→ ⟦ ⌜rec⌝ {σ} {A} ⟧₀
＝ λ f x → ⟦ ⌜Kleisli-extension⌝ {ι} {A} {σ} ⟧
(⟨⟩ ‚ f ‚ x)
(rec (f ∘ ⟦ ⌜η⌝ {ι} {ι} {ι} {A} ⟧₀) x)
rec-meaning = refl
B-context【_】 : {n : ℕ} → Cxt n → type → Cxt n
B-context【_】 {0} 〈〉 A = 〈〉
B-context【_】 {succ n} (Γ , σ) A = (B-context【_】 {n} Γ A , B-type〖 σ 〗 A)
infix 10 B-context【_】
⌜ν⌝ : {n : ℕ} {Γ : Cxt n} {A : type} (i : Fin n)
→ T (B-context【 Γ 】 A) (B-type〖 Γ [ i ] 〗 A)
⌜ν⌝ i = transport (T (B-context【 _ 】 _)) (p i) (ν i)
where
p : {n : ℕ} {Γ : Cxt n} {A : type} (i : Fin n)
→ B-context【 Γ 】 A [ i ] ＝ B-type〖 Γ [ i ] 〗 A
p {0} {〈〉} ()
p {succ n} {Γ , x} 𝟎 = refl
p {succ n} {Γ , x} (suc i) = p i
(Compositional) translation of terms:
⌜_⌝ : {n : ℕ} {Γ : Cxt n} {σ : type} {A : type}
→ T Γ σ
→ T (B-context【 Γ 】 A) (B-type〖 σ 〗 A)
⌜ Zero ⌝ = ⌜zero⌝
⌜ Succ ⌝ = ⌜succ⌝
⌜ Rec {_} {_} {σ} ⌝ = ⌜rec⌝ {σ}
⌜ ν i ⌝ = ⌜ν⌝ i
⌜ ƛ t ⌝ = ƛ ⌜ t ⌝
⌜ t · u ⌝ = ⌜ t ⌝ · ⌜ u ⌝
Given a term of type (ι ⇒ ι) ⇒ ι, we calculate a term defining its dialogue tree.
⌜generic⌝ : {A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ (⌜B⌝ ι A ⇒ ⌜B⌝ ι A)
⌜generic⌝ = ⌜kleisli-extension⌝ · (⌜β⌝ · ⌜η⌝)
⌜dialogue-tree⌝ : {A : type} {n : ℕ} {Γ : Cxt n}
→ T Γ ((ι ⇒ ι) ⇒ ι)
→ T (B-context【 Γ 】 A) (⌜B⌝ ι A)
⌜dialogue-tree⌝ t = ⌜ t ⌝ · ⌜generic⌝
The correctness of ⌜dialogue-tree⌝ is formulated and proved in
EffectfulForcing.Internal.Correctness.
Given a term t of type (ι ⇒ ι) ⇒ ι, we calculate a term defining a
modulus of continuity for t.
max' : ℕ → ℕ → ℕ
max' 0 n = n
max' (succ m) 0 = succ m
max' (succ m) (succ n) = succ (max' m n)
max : ℕ → ℕ → ℕ
max = rec (λ (m : ℕ) (f : ℕ → ℕ) → rec (λ (n : ℕ) _ → succ (f n)) (succ m)) (λ n → n)
max-agreement : (m n : ℕ) → max m n ＝ max' m n
max-agreement 0 n = refl
max-agreement (succ m) 0 = refl
max-agreement (succ m) (succ n) = ap succ (max-agreement m n)
maxᵀ : {n : ℕ} {Γ : Cxt n} → T Γ (ι ⇒ ι ⇒ ι)
maxᵀ = Rec · ƛ (ƛ (Rec · ƛ (ƛ (Succ · (ν₂ · ν₁))) · (Succ · ν₁))) · ƛ ν₀
maxᵀ-meaning : ⟦ maxᵀ ⟧₀ ＝ max
maxᵀ-meaning = refl
A modulus of continuity can be calculated from a dialogue tree.
max-question-in-path : {n : ℕ} {Γ : Cxt n}
→ T (B-context【 Γ 】 ((ι ⇒ ι) ⇒ ι))
((⌜B⌝ ι ((ι ⇒ ι) ⇒ ι)) ⇒ (ι ⇒ ι) ⇒ ι)
max-question-in-path =
ƛ (ν₀ · ƛ (ƛ Zero) · ƛ (ƛ (ƛ (maxᵀ · (Succ · ν₁) · (ν₂ · (ν₀ · ν₁) · ν₀)))))
max-question-in-path-meaning-η :
∀ n α → ⟦ max-question-in-path ⟧₀ (⟦ ⌜η⌝ ⟧₀ n) α ＝ 0
max-question-in-path-meaning-η n α = refl
max-question-in-path-meaning-β :
∀ φ n α → ⟦ max-question-in-path ⟧₀ (⟦ ⌜β⌝ ⟧₀ φ n) α
＝ max (succ n) (⟦ max-question-in-path ⟧₀ (φ (α n)) α)
max-question-in-path-meaning-β φ n α = refl
internal-mod-cont : {n : ℕ} {Γ : Cxt n}
→ T Γ ((ι ⇒ ι) ⇒ ι)
→ T (B-context【 Γ 】 ((ι ⇒ ι) ⇒ ι)) ((ι ⇒ ι) ⇒ ι)
internal-mod-cont t = max-question-in-path · (⌜dialogue-tree⌝ {(ι ⇒ ι) ⇒ ι} t)
internal-mod-cont₀ : T₀ ((ι ⇒ ι) ⇒ ι) → T₀ ((ι ⇒ ι) ⇒ ι)
internal-mod-cont₀ = internal-mod-cont
external-mod-cont : T₀ ((ι ⇒ ι) ⇒ ι) → (ℕ → ℕ) → ℕ
external-mod-cont t = ⟦ internal-mod-cont₀ t ⟧₀
TODO. Prove the correctness of the internal modulus of continuity.
Examples to be compared with those of the lambda-calculus version of
the MFPS paper file.
module examples2 where
m₁ : (ℕ → ℕ) → ℕ
m₁ = external-mod-cont (ƛ (ν₀ · numeral 17))
m₁-explicitly : m₁ ＝ λ α → 18
m₁-explicitly = refl
example₁ : m₁ id ＝ 18
example₁ = refl
example₁' : m₁ (λ i → 0) ＝ 18
example₁' = refl
f₂ : T₀ ((ι ⇒ ι) ⇒ ι)
f₂ = ƛ (ν₀ · (ν₀ · numeral 17))
f₂-meaning : ⟦ f₂ ⟧₀ ＝ λ α → α (α 17)
f₂-meaning = refl
m₂ : (ℕ → ℕ) → ℕ
m₂ = external-mod-cont (ƛ (ν₀ · (ν₀ · numeral 17)))
m₂-explicitly : m₂ ＝ λ α → succ (max 17 (α 17))
m₂-explicitly = refl
This is what m₂ evaluates to with Agda normalization:
m₂-explicitly' : m₂ ＝
λ α → succ (rec (λ x₁ x₂ → succ (rec (λ x₃ x₄ → succ (rec (λ x₅ x₆
→ succ (rec (λ x₇ x₈ → succ (rec (λ x₉ x₁₀ → succ (rec (λ x₁₁ x₁₂ →
succ (rec (λ x₁₃ x₁₄ → succ (rec (λ x₁₅ x₁₆ → succ (rec (λ x₁₇ x₁₈ →
succ (rec (λ x₁₉ x₂₀ → succ (rec (λ x₂₁ x₂₂ → succ (rec (λ x₂₃ x₂₄ →
succ (rec (λ x₂₅ x₂₆ → succ (rec (λ x₂₇ x₂₈ → succ (rec (λ x₂₉ x₃₀ →
succ (rec (λ x₃₁ x₃₂ → succ (rec (λ x₃₃ x₃₄ → succ x₃₃) 1 x₃₁)) 2
x₂₉)) 3 x₂₇)) 4 x₂₅)) 5 x₂₃)) 6 x₂₁)) 7 x₁₉)) 8 x₁₇)) 9 x₁₅)) 10
x₁₃)) 11 x₁₁)) 12 x₉)) 13 x₇)) 14 x₅)) 15 x₃)) 16 x₁)) 17 (α 17))
m₂-explicitly' = refl
example₂ : m₂ succ ＝ 19
example₂ = refl
example₂' : m₂ (λ i → 0) ＝ 18
example₂' = refl
example₂'''' : m₂ (λ i → 1000) ＝ 1001
example₂'''' = refl
example₂'' : m₂ id ＝ 18
example₂'' = refl
example₂''' : m₂ (succ ∘ succ) ＝ 20
example₂''' = refl
Add : {n : ℕ} {Γ : Cxt n} → T Γ (ι ⇒ ι ⇒ ι)
Add = Rec · (ƛ Succ)
t₃ : T₀ ((ι ⇒ ι) ⇒ ι)
t₃ = ƛ (ν₀ · (ν₀ · (Add · (ν₀ · numeral 17) · (ν₀ · numeral 34))))
add : ℕ → ℕ → ℕ
add = rec (λ _ → succ)
t₃-meaning : ⟦ t₃ ⟧₀ ＝ λ α → α (α (add (α 17) (α 34)))
t₃-meaning = refl
m₃ : (ℕ → ℕ) → ℕ
m₃ = external-mod-cont t₃
example₃ : m₃ succ ＝ 55
example₃ = refl
example₃' : m₃ id ＝ 52
example₃' = refl
example₃'' : m₃ (λ i → 0) ＝ 35
example₃'' = refl
example₃''' : m₃ (λ i → 300) ＝ 601
example₃''' = refl
example₃'''' : m₃ (λ i → add i i) ＝ 205
example₃'''' = refl
f : T₀ ((ι ⇒ ι) ⇒ ι)
f = ƛ (ν₀ · (ν₀ · (ν₀ · numeral 17)))
m₄ : (ℕ → ℕ) → ℕ
m₄ = external-mod-cont f
example₄ : m₄ id ＝ 18
example₄ = refl
example₄' : m₄ (λ i → 0) ＝ 18
example₄' = refl
example₄'' : m₄ succ ＝ 20
example₄'' = refl
example₄''' : m₄ (λ i → add i i) ＝ 69
example₄''' = refl
example₄'''' : ⟦ f ⟧₀ (λ i → add i i) ＝ 136
example₄'''' = refl