数学联邦政治世界观
超小超大

Amann分析中recursion theorem的证明 (3-2)

(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)) 显然成立.

数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。

相关小说

修仙那几年 连载中
修仙那几年
吴凡 13071928971
一个沙雕爽文的诞生,爽就够了
0.1万字8个月前
(不羡仙) 连载中
(不羡仙)
柑橘不是橘
本文五个男主,所以不知道女主到底会跟哪一个男主在一起反正现在还不知道,进入小说世界其实是一个迷主要不知道到底是谁写的这本小说,女主是成长型,......
50.2万字8个月前
刺客伍六七之忆失还情 连载中
刺客伍六七之忆失还情
血卿酒颜辞
回忆?凭什么我不能拥有?首领?迟早要了你的人头!暗影刺客?昔日往友还会帮我吗……白……曾经害我,我怎可能放过,我会让你血债血偿!梅小姐,若不......
1.8万字8个月前
仙域世界 连载中
仙域世界
无尽深海
陆思瑶是一个极限运动爱好者,蹦极,低空跳伞,跳伞,徒手攀岩,高空跑酷和泅渡长江,一次机缘巧合或者说是祸不单行在太平洋百慕大附近进行跳伞并根据......
31.1万字8个月前
山海吃货联萌 连载中
山海吃货联萌
映双双
【皮卡丘文社】新书《岌岌扶唧唧》求眼熟~吃了吗?吃饱了吗?下顿想吃什么?想美容养颜还是延年益寿?或者,过目不忘?来吃饭吧!山河海私房菜欢迎您......
18.9万字8个月前
大海会奔向哪里 连载中
大海会奔向哪里
I格瑞叶辉清明
abo文,幼儿园文笔主cp:心海每篇的字都挺少的可怜,我不是太有空更文会尽量一日两更
0.7万字8个月前