证明 Haskell 中乘法对加法函数的分配律

Question

我目前正在学习 haskell 和 lambda 演算的初学者课程，我不确定如何进行以下练习：

使用haskell中的(+)和(*)操作的以下定义，证明：

1)(*)对(+)的分配律

(∀m⇓,n⇓,k⇓::N) (m+n) * k = m * k + n * k

定义：

(+) :: N -> N -> N
(+) = \m n -> case m of { 0 -> n; S(y) -> S(y+n)}

(*) :: N -> N -> N
(*) = \m n -> case m of { 0 -> 0; S y -> n + (y*n)}

我的想法是做我在之前练习中所做的事情，证明 m 的每个可能情况。不同的是，我做的练习是针对布尔类型的，它只能是真或假，这是很自然的，所以我的猜测是对 m = 0 和 m = S(y)[=15 的情况进行证明=]

我很容易地证明了 m = 0 的等式，但在 m = S(y) 时被卡住了

案例 m = 0

(0 + n) * k =? 0 * k + n * k
Left side:
(0 + n) * k = (case 0 of {0->n;Sy->...}) * k
= n * k
Right side:
0 * k + n * k = (case 0 of {0->0;Sy->...}) + (n * k)
= 0 + (n * k) = (case 0 of {0->(n*k);Sy->...}) = n * k (equal to the left side)

案例 m = S(y)

(Sy + n) * k =? Sy * k + n * k
Left side:
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k
= case Sx of {0->...;Sx-> k + k * (y+n)
Right side:
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k
= k + k*y + n * k (Point at which I got stuck)

(...) 代表无关代码

附带一问，∀m⇓上的向下箭头⇓到底是什么意思？提前致谢！

Answer 1

好吧，您只是忘记应用归纳假设：

(Sy + n) * k =? Sy * k + n * k
Left side:
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k
= case Sx of {0->...;Sx-> k + k * (y+n)
( inductive hypothesis; we know that k * (y+n) = k*y + k*n)
= k + k*y + k*n
Right side:
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k
= k + k*y + n * k

记住：您是通过归纳法对 + 的第一个参数提供 (m+n)*k == m*k + n*k。您证明了基本情况 (0+n)*k，因此在证明归纳情况时，您假设知道 (y+n)*k == y*k + n*k 达到某个特定值 y，并且您想证明 (S(y) + n)*k == S(y)*k + n*k。

证明 Haskell 中乘法对加法函数的分配律

Prove distributive law of multiplication over addition functions in Haskell

haskell

functional-programming

lambda-calculus