评估扩展欧几里得算法的实现

Question

经过一些实验和搜索，我得出了以下定义：

emcd' :: Integer -> Integer -> (Integer,Integer,Integer)
emcd' a 0 = (a, 1, 0)
emcd' a b = 
  let (g, t, s) = emcd' b r
  in (g, s, t - (q * s))
    where
      (q, r) = divMod a b

我会评估 emcd' 56 15 直到最内层，例如：

  emcd' 56 15 
= let (g, t, s) = emcd' 15 11 in (
    let (g, t, s) = emcd' 11 4 in (
      let (g, t, s) = emcd' 4 3 in (
          let (g, t, s) = emcd' 3 1 in (
            let (g, t, s) = emcd' 1 0 in (
              (1, 1, 0)
            ) in (g, s, t - (3 * s))
          ) in (g, s, t - (1 * s))
        ) in (g, s, t - (2 * s))
      ) in (g, s, t - (1 * s))
  ) in (g, s, t - (3 * s))

我的评估方向正确吗？

编辑：

根据Will Ness的评论，我正在更新评价。

Answer 1

大方向是正确的，但它包含已经执行的递归调用，因此不应该存在。相反，它是

  emcd' 56 15 
= let (g, t, s) = (
    let (g, t, s) = (
      let (g, t, s) = (
          let (g, t, s) = (
            let (g, t, s) = (
              (1, 1, 0)
            ) in (g, s, t - (3 * s))
          ) in (g, s, t - (1 * s))
        ) in (g, s, t - (2 * s))
      ) in (g, s, t - (1 * s))
  ) in (g, s, t - (3 * s))

接下来我推导出以下伪代码（其中 a where { ... } 代表 let { ... } in a）：

= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(3*s))
              where { (g, t, s) = (1, 1, 0) } } } } }

这两个确实是等价的，但我认为 where 伪代码更具可读性。

稍微重构一下定义，就变成了

foo a 0 = (a, 1, 0)
foo a b = (g, s, t-(q*s))
          where { (q, r) = divMod a b 
                ; (g, t, s) = foo b r }

然后我们用 where 而不是 let 的伪代码编写，使用基本的剪切和粘贴替换，

foo 56 15
= (g, s, t-(q*s))
  where { (a, b) = (56, 15)      --
        ; (q, r) = divMod a b
        ; (g, t, s) = foo b r }
= (g, s, t-(q*s))
  where { (q, r) = divMod 56 15    --
        ; (g, t, s) = foo 15 r }
= (g, s, t-(q*s))
  where { (q, r) = (3, 11)           --
        ; (g, t, s) = foo 15 r }
= (g, s, t-(3*s))
  where { (g, t, s) = foo 15 11 }      --
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(q*s))
     where { (a, b) = (15, 11)             --
           ; (q, r) = divMod a b
           ; (g, t, s) = foo b r } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(q*s))
     where { (q, r) = divMod 15 11
           ; (g, t, s) = foo 11 r } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(q*s))
     where { (q, r) = (1, 4)
           ; (g, t, s) = foo 11 r } }  
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = foo 11 4 } }  
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(q*s))
        where { (a, b) = (11, 4)
              ; (q, r) = divMod a b
              ; (g, t, s) = foo b r } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(q*s))
        where { (q, r) = divMod 11 4
              ; (g, t, s) = foo 4 r } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(q*s))
        where { (q, r) = (2, 3)
              ; (g, t, s) = foo 4 r } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = foo 4 3 } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(q*s))
           where { (a, b) = (4, 3)
                 ; (q, r) = divMod a b
                 ; (g, t, s) = foo b r } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(q*s))
           where { (q, r) = divMod 4 3
                 ; (g, t, s) = foo 3 r } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(q*s))
           where { (q, r) = (1, 1)
                 ; (g, t, s) = foo 3 r } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = foo 3 1 } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(q*s))
              where { (a, b) = (3, 1)
                    ; (q, r) = divMod a b
                    ; (g, t, s) = foo b r } } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(q*s))
              where { (q, r) = divMod 3 1
                    ; (g, t, s) = foo 1 r } } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(q*s))
              where { (q, r) = (3, 0)
                    ; (g, t, s) = foo 1 r } } } } } 
= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(3*s))
              where { (g, t, s) = foo 1 0 } } } } }

现在我们已经达到基本情况：

= (g, s, t-(3*s))
  where { (g, t, s) = (g, s, t-(1*s))
     where { (g, t, s) = (g, s, t-(2*s))
        where { (g, t, s) = (g, s, t-(1*s))
           where { (g, t, s) = (g, s, t-(3*s))
              where { (g, t, s) = (1, 1, 0) } } } } } 
= (1, s, t-(3*s))
  where { (t, s) = (s, t-(1*s))
     where { (t, s) = (s, t-(2*s))
        where { (t, s) = (s, t-(1*s))
           where { (t, s) = (0, 1-(3*0)) } } } } 
= (1, s, t-(3*s))
  where { (t, s) = (s, t-(1*s))
     where { (t, s) = (s, t-(2*s))
        where { (t, s) = (1, 0-(1*1)) } } } 
= (1, s, t-(3*s))
  where { (t, s) = (s, t-(1*s))
     where { (t, s) = (-1, 1-(2*(-1))) } } 
= (1, s, t-(3*s))
  where { (t, s) = (3, (-1)-(1*3)) } 
= (1, (-4), 3-(3*(-4)))
= (1, (-4), 15)

希望这里没有剪切和粘贴错误。总体思路只是以纯机械的方式进行简单的替换。

_{旁注：(g,t,s)=foo a b === g==gcd a b && g==t*a+s*b.}

评估扩展欧几里得算法的实现

Evaluating implementation of Extended Euclidean algorithm

evaluation

haskell

euclidean-algorithm