C-Spaces.UsingFunExt.ComputationExperiments
Chuangjie Xu and Martin Escardo 2014 (updated in February 2015) (Revised and ported to TypeTopology in 2026 by Chuangjie Xu) Experiments in computing moduli of uniform continuity{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan hiding (_+_) open import UF.FunExt using (DN-funext) module C-Spaces.UsingFunExt.ComputationExperiments (fe : DN-funext 𝓤₀ 𝓤₀) where open import C-Spaces.Preliminaries.Booleans.Functions using (if) open import C-Spaces.Preliminaries.Sequence open import C-Spaces.Syntax.SystemTWithFan open import C-Spaces.UsingFunExt.DiscreteSpace fe open import C-Spaces.UsingFunExt.YonedaLemma fe open import C-Spaces.UsingFunExt.Fan fe open import C-Spaces.UsingFunExt.UCinT feThis module records a small computational experiment with the Fan functional in the presence of full function extensionality. Because function extensionality is used as an outright assumption, the computational content of the model is lost. In particular, even when the least modulus is mathematically `0`, the corresponding closed Agda term computed by the model need not normalize to `0`. The example below illustrates this phenomenon. We write `⟦ t ⟧` for the interpretation of a closed System-T-with-Fan term `t : ((Ⓝ ⇨ ②) ⇨ Ⓝ)` as an ordinary function `₂ℕ → ℕ`, and `modu t` for the modulus computed for `t` by the Fan functional:⟦_⟧ : Tm ε ( ((Ⓝ ⇨ ②) ⇨ Ⓝ)) → ₂ℕ → ℕ ⟦ t ⟧ α = pr₁ (pr₁ ⟦ t ⟧ᵐ ⋆) (ID α) modu : Tm ε ((Ⓝ ⇨ ②) ⇨ Ⓝ) → ℕ modu F = pr₁ fan (pr₁ ⟦ F ⟧ᵐ ⋆)`F₀` is constant, even though it inspects the first input bit.F₀ : {Γ : Cxt} → Tm Γ ((Ⓝ ⇨ ②) ⇨ Ⓝ) F₀ = LAM (IF · (VAR zero · ZERO) · ZERO · ZERO) F₀-interpretation : ⟦ F₀ ⟧ ＝ λ α → if (α 0) 0 0 F₀-interpretation = reflAlthough the least modulus of `F₀` is mathematically `0`, the closed Agda term `modu F₀` does not normalize to a numeral under the assumption of function extensionality. Its unreduced form is the following: C-Spaces.UniformContinuity.LM _＝_ UF.DiscreteAndSeparated.ℕ-is-discrete (λ α → 𝟚-induction 0 0 (α 0)) (1 Naturals.Addition.+ C-Spaces.Preliminaries.Naturals.Order.max (pr₁ (transport (λ x → Σ (λ n → Σ (λ x₁ → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → 𝟚-induction 0 0 (x α 0) ＝ 𝟚-induction 0 0 (x β 0)) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) (transport (_＝ (λ x → cons (₀ ∷ ⟨⟩) x)) (fe (λ α → fe (λ i → transport (_＝ cons (₀ ∷ ⟨⟩) (λ x → α x) i) (Lemma[cons-take-drop] 1 (cons (₀ ∷ ⟨⟩) α) i) refl))) refl) (transport (λ x → (p : (ℕ → 𝟚) → ℕ) → Σ (λ n → Σ (λ x₁ → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → p α ＝ p β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n')) → (t : (ℕ → 𝟚) → ℕ → 𝟚) → ((m : ℕ) → Σ (λ n → Σ (λ x₁ → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → t α ＝⟦ m ⟧ t β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) → Σ (λ n → Σ (λ x₁ → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → 𝟚-induction 0 (p α) (x (t α) 0) ＝ 𝟚-induction 0 (p β) (x (t β) 0)) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) (transport (_＝ (λ x → cons (₀ ∷ ⟨⟩) x)) (fe (λ α → fe (λ i → transport (_＝ cons (₀ ∷ ⟨⟩) (λ x → α x) i) (Lemma[cons-take-drop] 1 (cons (₀ ∷ ⟨⟩) α) i) refl))) refl) (transport (λ r → (p : (ℕ → 𝟚) → ℕ) → Σ (λ n → Σ (λ x → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → p α ＝ p β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n')) → (t : (ℕ → 𝟚) → ℕ → 𝟚) → ((m : ℕ) → Σ (λ n → Σ (λ x → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → t α ＝⟦ m ⟧ t β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) → (p₁ : (ℕ → 𝟚) → ℕ) → Σ (λ n → Σ (λ x → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → p₁ α ＝ p₁ β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n')) → (t₁ : (ℕ → 𝟚) → ℕ → 𝟚) → ((m : ℕ) → Σ (λ n → Σ (λ x → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → t₁ α ＝⟦ m ⟧ t₁ β) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) → Σ (λ n → Σ (λ x → (n' : ℕ) → ((α β : ℕ → 𝟚) → α ＝⟦ n' ⟧ β → pr₁ (pr₁ (r (t (t₁ α))) (p (t₁ α))) (p₁ α) ＝ pr₁ (pr₁ (r (t (t₁ β))) (p (t₁ β))) (p₁ β)) → n C-Spaces.Preliminaries.Naturals.Order.≤ n'))) (fe (λ α → refl)) (λ p pP t uc q qA t₁ tC → C-Spaces.UniformContinuity.LM _＝_ UF.DiscreteAndSeparated.ℕ-is-discrete (λ x → p (t₁ x)) (pr₁ (tC (pr₁ pP))) , C-Spaces.UniformContinuity.Lemma[LM-modulus] _＝_ UF.DiscreteAndSeparated.ℕ-is-discrete (λ p₁ → transport (_＝ z) p₁ refl) (λ p₁ q₁ → transport (_＝_ z) q₁ p₁) (λ x → p (t₁ x)) (pr₁ (tC (pr₁ pP))) (λ α β en → pr₁ (pr₂ pP) (t₁ α) (t₁ β) (pr₁ (pr₂ (tC (pr₁ pP))) α β en)) , C-Spaces.UniformContinuity.Lemma[LM-least] _＝_ UF.DiscreteAndSeparated.ℕ-is-discrete (λ p₁ → transport (_＝ z) p₁ refl) (λ p₁ q₁ → transport (_＝_ z) q₁ p₁) (λ x → p (t₁ x)) (pr₁ (tC (pr₁ pP))) (λ α β en → pr₁ (pr₂ pP) (t₁ α) (t₁ β) (pr₁ (pr₂ (tC (pr₁ pP))) α β en))) (λ x → 0) (0 , (λ α β e → refl) , (λ k prk → C-Spaces.Preliminaries.Naturals.Order._≤_.≤-zero)) (λ α x → α x) (λ k → C-Spaces.UniformContinuity.LM (λ α → _＝⟦_⟧_ α k) Lemma[＝⟦⟧-decidable] (λ α x → α x) (C-Spaces.UniformContinuity.LM (λ α → _＝⟦_⟧_ α (succ k)) (λ α β → dep-cases (λ em → dep-cases (λ e → inl (＝⟦succ⟧ em e)) (λ f → inr (λ e → f (Lemma[＝⟦succ⟧]₁ e))) (UF.DiscreteAndSeparated.𝟚-is-discrete (α k) (β k))) (λ f → inr (λ e → f (Lemma[＝⟦succ⟧]₀ e))) (Lemma[＝⟦⟧-decidable] α β)) (λ x → cons (₀ ∷ ⟨⟩) x) k) , C-Spaces.UniformContinuity.Lemma[LM-modulus] (λ α → _＝⟦_⟧_ α k) Lemma[＝⟦⟧-decidable] ＝⟦⟧-sym ＝⟦⟧-trans (λ α x → α x) (C-Spaces.UniformContinuity.LM (λ α → _＝⟦_⟧_ α (succ k)) (λ α β → dep-cases (λ em → dep-cases (λ e → inl (＝⟦succ⟧ em e)) (λ f → inr (λ e → f (Lemma[＝⟦succ⟧]₁ e))) (UF.DiscreteAndSeparated.𝟚-is-discrete (α k) (β k))) (λ f → inr (λ e → f (Lemma[＝⟦succ⟧]₀ e))) (Lemma[＝⟦⟧-decidable] α β)) (λ x → cons (₀ ∷ ⟨⟩) x) k) (λ α β el → Lemma[<-＝⟦⟧] (λ i i