如何在Pyret中基于给定Nat加法函数实现递归乘法函数

先巩固nat-plus的运行逻辑 #

你需要先完全搞懂给出的加法函数的递归逻辑，才能顺利复用它实现乘法：
皮亚诺体系中自然数的加法规则是：

• 0加任意数m等于m
• 「n的后继」加m，等于「n加m」的后继
  给出的代码完全贴合这个规则：

fun nat-plus(n :: Nat, m :: Nat) -> Nat:
  cases (Nat) n:
    | O => m # 边界条件：n是0，直接返回m
    | S(nn) => S(nat-plus(nn, m)) # 递归：把n拆解为前继nn，加完后补一个后继
  end

举个实际运行示例：计算2+1也就是nat-plus(S(S(O)), S(O))的执行过程：

1. n是S(S(O))，匹配到S(nn)分支，nn为S(O)，返回S(nat-plus(S(O), S(O)))
2. 内层调用n是S(O)，匹配到S(nn)分支，nn为O，返回S(nat-plus(O, S(O)))
3. 最内层调用n是O，返回S(O)
4. 逐层往外返回结果，最终得到S(S(S(O)))也就是3，和预期一致。

乘法函数的实现思路 #

皮亚诺体系里的乘法规则刚好可以直接复用加法函数，规则如下：

• 边界条件：0乘任意数m都等于0
• 递归条件：「n的后继」乘m，等于m加上「n乘m」的结果（本质就是累加m共n次）
  对应可以直接写出如下结构的乘法函数：

fun nat-mult(n :: Nat, m :: Nat) -> Nat:
  cases (Nat) n:
    | O => O # 边界条件匹配
    | S(nn) => nat-plus(m, nat-mult(nn, m)) # 递归调用加法和自身
  end

逻辑验证 #

你可以用2*3的例子自行验证执行过程：
nat-mult(S(S(O)), S(S(S(O)))) 会拆解为 nat-plus(S(S(S(O))), nat-mult(S(O), S(S(S(O)))))，再逐层递归最终得到S(S(S(S(S(S(O))))))也就是6，符合预期。

内容的提问来源于stack exchange，提问作者bobaloogie