Математически, почему этот алгоритм SICP для экспоненты числа по модулю другого числа работает?

Это определение fast-exp из 1.2.4, которое относится к:

(define (fast-expt b n)
  (cond ((= n 0) 1)
        ((even? n) (square (fast-expt b (/ n 2))))
        (else (* b (fast-expt b (- n 1))))))

Если мы переименуем вещи, чтобы они больше соответствовали expmod, это будет выглядеть так:

(define (expt base exp)
  (cond ((= exp 0) 1)
        ((even? exp)
         (square (expt base (/ exp 2))))
        (else
         (* base (expt base (- exp 1))))))

Чтобы получить наивное expmod, мы можем пока просто вычислить остаток от каждого предложения:

(define (expmod base exp m)
  (cond ((= exp 0) 1)
        ((even? exp)
         (remainder (square (expt base (/ exp 2))) m))
        (else
         (remainder (* base (expt base (- exp 1))) m))

До сих пор мы не использовали сноску (ab) mod m = ((a mod m)(b mod m) mod m). Конечно, это частный случай (aa) mod m = ((a mod m)(a mod m) mod m), который дает (remainder (square a) m) = (remainder (sqaure (remainder a m)) m). Мы можем использовать это с предложением even, чтобы

         (remainder (square (expt base (/ exp 2))) m)

становится:

         (remainder (square (remainder (expt base (/ exp 2)) m))
                    m)

В середине у нас есть остаток от экспоненты, так что это эквивалентно:

         (remainder (square (expmod base (/ exp 2) m)) m)

Используя новое предложение even, мы имеем

(define (expmod base exp m)
  (cond ((= exp 0) 1)
        ((even? exp)
         (remainder (square (expmod base (/ exp 2) m)) 
                    m))
        (else
         (remainder (* base (expt base (- exp 1))) m))

Чтобы упростить нечетное предложение, давайте пока используем E вместо (expt base (- exp 1)).

Используя определяющие свойства числа mod, мы можем сказать для любого числа a:

         a = (+ (* (quotient a m) m) (remainder a m))

Так что верно и то, что:

         E = (+ (* (quotient E m) m) (remainder E m))

подставив это в наше предложение odd:

         (remainder (* base E) m)

дает:

         (remainder (* base (+ (* (quotient E m) m) (remainder E m))) m)

Мы можем игнорировать (* (quotient E m) m), потому что любой терм, содержащий это, делится на m и поэтому будет оцениваться как 0 при выполнении внешнего remainder, так что это эквивалентно:

         (remainder (* base (remainder E m)) m)

расширение E до исходного значения:

         (remainder (* base (remainder (expt base (- exp 1)) m)) m)

еще раз, в середине у нас есть остаток от экспоненты, так что это становится:

         (remainder (* base (expmod base (- exp 1) m)) m)

И наш expmod теперь:

(define (expmod base exp m)
  (cond ((= exp 0) 1)
        ((even? exp)
         (remainder (square (expmod base (/ exp 2) m)) 
                    m))
        (else
         (remainder (* base (expmod base (- exp 1) m))
                    m))))

(ab) mod n = [a (b mod n)] mod n

также верно.

Вот доказательство по индукции по a.

Базовый случай: когда a = 0, (0b) mod n = 0 mod n = [0 (b mod n)] mod n.

Индуктивный случай:

По предположению индукции предположим, что (ab) mod n = [a (b mod n)] mod n верно. Нам нужно доказать, что ((a+1) b) mod n = [(a + 1) (b mod n)] mod n.

((a+1) b) mod n
= (ab + b) mod n
= (ab mod n) + (b mod n)
= [a (b mod n)] mod n + (b mod n)             by induction hypothesis
= [a (b mod n)] mod n + (b mod n) mod n
= [a (b mod n) + (b mod n)] mod n
= [(a + 1) (b mod n)] mod n

по желанию.

На этом заканчивается доказательство того, что

(ab) mod n = [a (b mod n)] mod n

На самом деле, вы можете видеть, что

(ab) mod n = [(a mod n) (b mod n)] mod n

является следствием, вытекающим из него. Вот доказательство:

(ab) mod n 
= [a (b mod n)] mod n            by what we just proved
= [(b mod n) a] mod n
= [(b mod n) (a mod n)] mod n    by what we just proved
= [(a mod n) (b mod n)] mod n