Amann分析中recursion theorem的证明

目录

原命题 ▹

前置知识 ▹

命题的表述 ▹

命题的证明 ▹

免责声明：本文仅仅是展示如何在类型论 (Agda) 中证明原题所引用的命题, 而不构成对原题的回答, 毕竟, 原题可能是在集合论背景下的问题.

集合论里, 严格来讲只有演绎, 没有归纳, 因为归纳是公理的结果, 是需要先证明的. 但是类型论里, 消去规则就是归纳, 是内生的, 不需要被证明的.

原命题

5.11 Proposition Let X be a nonempty set and α ∈ X. For each n ∈ ℕ×，let Vₙ：Xⁿ → X be a function. Then there is a unique function f：ℕ → X with the following properties：

(i) f(0)＝α.

(ii) f(n＋1)＝Vₙ₊₁(f(0)，f(1)，. . .，f(n))，n ∈ ℕ.

前置知识

我们知道什么是空类型⊥, 自然数类型 ℕ, 积类型 _×_ 以及相等类型 _≡_. 直接从标准库中导入这些内容.

{-# OPTIONS --safe #-}

open import Data.Empty

open import Data.Nat hiding (_^_)

open import Data.Product

open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

定义 给定集合 X 以及自然数 n，我们递归定义 Xⁿ 如下

X¹＝X

Ⅹⁿ⁺²＝Xⁿ⁺¹ × X

也就是说，Ⅹⁿ⁺¹＝Xⁿ × X.∎

_^_ : (X : Set) (n : ℕ) → Set

X ^ 0 = ⊥

X ^ 1 = X

X ^ 2+ n = X ^ suc n × X

注意 X⁰没有定义, 形式化为空类型 ⊥.

定义 给定集合 X，函数 f：ℕ → X 以及自然数 n，递归定义 f〈· · ·〉n：Xⁿ⁺¹ 如下

f〈· · ·〉0＝f(0) f〈· · ·〉(n＋1)＝〈f〈· · ·〉〉n，f(n＋1)〉

也就是说，f〈· · ·〉n＝〈f(0)，f(1)，. . .，f(n)〉.∎

_⟨⋯⟩_ : {X : Set} (f : ℕ → X) (n : ℕ) → X ^ suc n

f ⟨⋯⟩ zero = f 0

f ⟨⋯⟩ (suc n) = f ⟨⋯⟩ n , f (suc n)

命题的表述

再次贴出原命题. 我们只证其中的存在性，不证唯一性.

5.11 Proposition Let X be a nonempty set and α ∈ X. For each n ∈ ℕ×，let Vₙ：Xⁿ → X be a function. Then there is a unique function f：ℕ → X with the following properties：

(i) f(0)＝α.

(ii) f(n＋1)＝Vₙ₊₁(f(0)，f(1)，. . .，f(n))，n ∈ ℕ.

命题 给定非空集合 X，其元素 α：Ⅹ，以及函数 Vₙ：Xⁿ → X，形式化为依赖函数

V：∏(Xⁿ → X).

n：ℕ

module 5-11 (X : Set) (a : X) (V : (n : ℕ) → X ^ n → X) where

存在一个函数f：ℕ → X满足如下性质

(i) f(0)＝α

(ii) ∀n ∈ ℕ，f(n＋1)＝Vₙ₊₁(f〈· · ·〉n)

desired : (f : ℕ → X) → Set

desired f = （i） × （ii）

where

（i） = f 0 ≡ a

（ii） = ∀ n → f (suc n) ≡ V (suc n) (f ⟨⋯⟩ n)

命题的证明

定义 我们使用互递归 (mutual recursion) 来构造所需的函数 f：ℕ → X. 即同时构造以下两个函数.

f：ℕ → X

p：∏ Xⁿ⁺¹

n：ℕ

f : ℕ → X

p : (n : ℕ) → X ^ suc n

使得f 满足

f(0)＝α

f(n＋1)＝Vₙ₊₁(pₙ)

f 0 = a

f (suc n) = V (suc n) (p n)

且p 满足

p₀＝f(0)

pₙ₊₁＝〈pₙ，f(n＋1)〉

p zero = f 0

p (suc n) = p n , f (suc n)

引理 对任意 n，我们有 pₙ＝f〈· · ·〉n.

证明 对 n 归纳.

• 当 n＝0 时，p₀＝f(0)＝f〈· · ·〉0.

• 当 n＝n＋1 时，由归纳假设 pₙ＝f〈· · ·〉n 有

pₙ₊₁＝〈pₙ，f(n＋1)〉

＝〈f〈· · ·〉n，f(n＋1)〉

＝f〈· · ·〉(n＋1)

eq : ∀ n → p n ≡ f ⟨⋯⟩ n

eq zero = refl

eq (suc n) = begin

p (suc n) ≡⟨⟩

(p n , f (suc n)) ≡⟨ cong (_, f (suc n)) (eq n) ⟩

(f ⟨⋯⟩ n , f (suc n)) ≡⟨⟩

f ⟨⋯⟩ (suc n) ∎

定理 以上构造的 f 满足 (i) 和 (ii).

证明 依定义，(i) 显然成立. 对于 (ii)，讨论 n.

• 当 n＝0 时，f(1)＝V₁(f(0)) 显然成立.

• 当 n＝n＋1 时, 由引理 pₙ＝f〈· · ·〉n 有

f(n＋2)＝Vₙ₊₂(pₙ，f(n＋1))

＝Vₙ₊₂(f〈· · ·〉n，f(n＋1))

＝Vₙ₊₂(f〈· · ·〉(n＋1))

desired-f : desired f

desired-f = i , ii

where

i : f 0 ≡ a

i = refl

ii : ∀ n → f (suc n) ≡ V (suc n) (f ⟨⋯⟩ n)

ii zero = refl

ii (suc n) = begin

f (2+ n) ≡⟨⟩

V (2+ n) (p n , f (suc n)) ≡⟨ cong (λ x → V (2+ n) (x , f (suc n))) (eq n) ⟩

V (2+ n) (f ⟨⋯⟩ n , f (suc n)) ≡⟨⟩

V (2+ n) (f ⟨⋯⟩ (suc n)) ∎

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。