haskell - 如何手动评估我的多功能功能？

Question

这是我的第一个 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 函数？

Answer 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。