Tim*_*ess 8 recursion type-theory induction
递归和归纳证明之间的关系是什么?
比方说fn(n),
递归就是fn(n)调用本身直到相遇base condition;
归纳是在base condition遇到的时候,试着证明(base case + 1)也是正确的.
似乎递归和归纳在不同的方向.从一开始n到base case,另一种是从开始base case到infinite.
有人可以详细解释这个想法吗?
Rot*_*sor 11
递归和归纳是非常相同的事情!如果您使用具有依赖类型的编程语言(例如Agda),这一点就变得很明显,但是在没有它们的情况下可以在某种程度上进行演示.
请记住,由于库里 - 霍华德的对应关系,类型是命题,程序是证明.当你编写一个类型的函数Nat -> Nat(我将使用Haskell表示法)时,你试图证明,给定一个自然数,你的程序将终止并产生另一个自然数.现在我们可能有这样的定义:
f 0 = 1
f (1 + n) = n * f n
Run Code Online (Sandbox Code Playgroud)
这既是递归定义,也是同时f终止的归纳证明!
您可以通过以下方式将其作为证据阅读:
让我们证明fx终止于任何x.
f 0根据定义保持不变,因此终止.f n终止,也f (1 + n)终止(因为它调用的所有函数都终止).注意,由于递归不限于递减其计数器的函数,因此归纳也不限于自然数.还存在结构归纳,对应于结构递归,这两者在数学/编程中都非常流行.当试图在更复杂的数据结构(列表/树/等)上证明事物/定义函数时,将使用这些.
现在,解决您对递归/归纳的"方向"的关注.在这里考虑"需求方向"和"供给方向"是有帮助的,这是相反的.
定义递归函数时,需求(方法调用)从较大的值流向基本情况.另一方面,供应(返回值)从基础情况流向较大的参数值."定义"是另一种思考供给的方式.它从基本情况开始,并通过递归情况传播到无穷大.
现在,当您进行归纳证明时,定理就是您的供应,而目标是您的需求.您可以从基本情况中得出一个定理T 0,然后使用感应情况改进到大到很大的T n:您的电源从0流向无穷大.现在,如果你有一个目标G n,你可以使用归纳步骤制作一个较小的目标G(nk)直到你达到零.这样你的需求从n变为0.
正如您所看到的,两种情况下供应方向都是"无限",两种情况下需求方向都"为零".
您还可以在不改变其含义的情况下反转归纳和递归描述中的明显顺序:
归纳是指何时证明P n持有你需要首先通过重复应用归纳案例将目标减少到P 0,然后使用基本案例证明最终目标.
类似地,递归是指您首先定义基本案例,然后根据先前的案例定义其他值.看,方向很容易交换!
| 归档时间: |
|
| 查看次数: |
6024 次 |
| 最近记录: |