sicp 1.17 尾递归解法的证明

sicp_1.17.scm

; ref: http://community.schemewiki.org/?sicp-ex-1.17
(define (fast-mult-by-add a b) 
   (define (double x) (+ x x)) 
   (define (halve x) (/ x 2)) 
    
   (define (helper a b product) ;; "add a" b times 
     (cond ((= b 0) product) 
           ((even? b) (helper (double a) (halve b) product)) 
           (else (helper a (- b 1) (+ a product))))) 
   (helper a b 0)) 
  

背景

尾递归需要引入一个新的 "不变量" 来定义一种新的 状态 表示方法.
所以, 将递归,转换为 尾递归的第一步是: 先定义出一种新的 状态等价表示方法.
而实现之后, 就需要证明 实现方法与预定义的 状态表示法是等价的, 即可证明 新的尾递归实现的正确性(相对于想要实现的 状态转换关系 而言).

这种,纯数学的,函数正确性的证明方法, 很新奇.所以试着模仿 http://community.schemewiki.org/?sicp-ex-1.16 证明下:

证明

尾递归使用的状态转换关系:

(helper a b product) = a * b + product.

证明过程:

• Case 1: b = 0.

(helper a b product)
= (helper a 0 product)
= product
= a*0 + product
= a*b + product

• Case 2: b > 0 and b is even.

(helper a b product)
= (helper 2*a b/2 product)
= (2 * a) * (b/2) + product
= a * b + product.

• Case 3: b > 0 and b is odd.

(helper a b product)
= (helper a b-1 a+product)
= a*(b-1) + (a + product)
= a*b + product