我如何证明以下算法？答案

【问题标题】：how can i prove the following algorithm?我如何证明以下算法？
【发布时间】：2021-01-09 17:19:42
【问题描述】：

Exp(n)
  If n = 0
    Return 1
  End If
  
  If n%2==0
    temp = Exp(n/2)
    Return temp × temp
  Else //n is odd
    temp = Exp((n−1)/2)
    Return temp × temp × 2
  End if

我如何通过 n 中的强归纳证明对于所有 n ≥ 1，乘以的次数为 Exp (n) ≤ 2 log2 n。

ps: Exp(n) = 2^n

【问题讨论】：

Exp(n) 应该计算 Power(2, n)?
我会在cs.stackexchange.com回答这个问题。

标签： algorithm math logic theorem-proving inductive-logic-programming

【解决方案1】：

一个简单的方法是使用strong induction。

首先，证明Exp(0)终止并返回2^0。
令 N 为任意偶数非负数。
假设函数 Exp 正确计算并返回 [0, N] 中每个 n 的 2^n。
在此假设下，证明Exp(N+1) 和Exp(N+2) 都终止并正确返回2^(N+1) 和2^(N+2)。

你已经完成了！通过归纳可知，对于 any 非负 N，Exp(N) 正确返回 2^N。

PS：请注意，在这篇文章中，2^N 的意思是“2 的 N 次方”，而不是“2 和 N 的二进制表示的按位异或”。

【讨论】：

【解决方案2】：

该程序完全应用以下重复：

P[0] = 1
n even -> P[n] -> P[n/2]²
n odd  -> P[n] -> P[(n-1)/2]².2

程序总是终止，因为对于n>0、n/2和(n-1)/2 < n，递归调用的参数总是减小。

P[n] = 2^n 是递归的解。确实，

n = 0 -> 2^0 = 1
n = 2m -> 2^n = (2^m)²
n = 2m+1 -> 2^n = 2.(2^n)²

这涵盖了所有情况。

由于每次调用都会将n 的有效位数减一并执行一两次乘法，因此总数不超过有效位数的两倍。

【讨论】：