如何手动评估我的多功能功能？答案

【问题标题】：How to manually evaluate my mult function?如何手动评估我的多功能功能？
【发布时间】：2021-12-29 10:45:57
【问题描述】：

这是我的第一个 Stack Overflow 问题，如果我忘记了任何重要信息，请告诉我，我会补充！

所以我是 Haskell 的新手，只是学习类型和类。现在我声明了 1 个类型和 2 个函数：

data Nat   = Zero   | Succ Nat  

add :: Nat -> Nat -> Nat 
add Zero n = n 
add (Succ m) n = Succ (add m n)

mult :: Nat -> Nat -> Nat 
mult Zero _ = Zero 
mult (Succ m) n = add n (mult m n);

当调用第一个函数时，我可以完全评估它并了解 Haskell 是如何处理它的。像这样：

> 2 + 1 = 3 
>
> add (Succ (Succ Zero)) (Succ Zero)
> 
> Succ (add (Succ zero)) (Succ Zero)) 
>
> Succ (Succ (add Zero (Succ Zero))
>
> Succ (Succ (Succ Zero))

但我无法理解mult 函数的情况。对我来说，这看起来将是一个无限循环的添加。谁能解释我如何评估mult 函数？

【问题讨论】：

标签： haskell types

【解决方案1】：

对于mult，您可以使用与add 相同的方式进行评估——通过重复替换名称的定义。只是需要更长的时间。

> 2 * 2 = 4

mult (Succ (Succ Zero)) (Succ (Succ Zero))

-- Substituting second case of mult. m = Succ Zero, n = Succ (Succ Zero)
add (Succ (Succ Zero)) (mult (Succ Zero) (Succ (Succ Zero))

-- Substituting second case of mult. m = Zero, n = Succ (Succ Zero)
add (Succ (Succ Zero)) (add (Succ (Succ Zero)) (mult Zero (Succ (Succ Zero))))

-- Substituting FIRST case of mult, because the first parameter is now Zero. 
add (Succ (Succ Zero)) (add (Succ (Succ Zero)) Zero)

-- And now we have nothing but addition left.

-- Substituting the inner add:
add (Succ (Succ Zero)) (Succ (add (Succ Zero) Zero))
add (Succ (Succ Zero)) (Succ (Succ (add Zero Zero)))
add (Succ (Succ Zero)) (Succ (Succ Zero))

-- Substituting the outer add:
Succ (add (Succ Zero) (Succ (Succ Zero)))
Succ (Succ (add Zero (Succ (Succ Zero))))
Succ (Succ (Succ (Succ Zero)))

Q.E.D

证明mult递归最终会结束的关键在于，每个递归调用都比前一个“小”——通过“移除”一层Succ。

【讨论】：

非常感谢您的解释！正如你所提到的，它会因为一层 Succ 被删除而结束，是因为 Mult 定义“mult (Succ m)”吗？ Succ 的元素“m”在哪里？
是的，没错
知道了，谢谢回答

【解决方案2】：

该模式与add 几乎完全相同，但使用add n 而不是Succ 作为前面慢慢积累的东西。他们在这里并排；我已在 add 缩减中将您的第一个 Succ Zero 替换为 n，以使相似之处更加明显：

add (Succ (Succ Zero)) n    mult (Succ (Succ Zero)) n
Succ (add (Succ zero) n)    add n (mult (Succ Zero) n)
Succ (Succ (add Zero n))    add n (add n (mult Zero n))
Succ (Succ n)               add n (add n Zero)

【讨论】：