-2

以下是我已经做过的作业，但做错了。我不明白为什么解决方案就足够了。（经过一周的阅读和谷歌搜索后，我转而询问。）

该示例类似于 Hutton 关于 Haskell 的书中使用的示例。

Base case:

add Zero m
=   { applying add }
m
=   { property of add }
add m Zero

Inductive case:

add (Succ n) m
=   { applying add }
Succ (add n m)
=   { induction hypothesis }
Succ (add m n)
=   { property of add }
add m (Succ n)



-- Hypothesis:
add n m = add m n

-- Method:
by induction on n

-- Using:
add n (Succ m) = Succ (add n m)
add n Zero = n

data Nat = Zero
         | Succ Nat


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

我看不到的是为什么允许感应箱在它停止的地方停止。它使用假设，然后取消应用添加以生成作为归纳案例假设版本的东西。

add n m = add m n -- hypothesis
add m (Succ n)  -- hypthesis applied to the induction case add (Succ n) m

换句话说，另一个版本的假设是通过假设假设成立而产生的。

足够了？当我找到一个可行的假设时，我是否总是将假设视为有效？对于归纳案例，如果我可以通过假设假设本身已经被证明来生成应用于归纳案例的假设版本就足够了？

我很难将感应从数字转移到功能。请不要让我愚蠢地死去。谢谢。

4

3 回答 3

4

足够了？当我找到一个可行的假设时，我是否总是将假设视为有效？

不，您需要：

  1. 证明它适用于所有基本（非递归）案例。在这里你只有一个：Zero。所以你需要展示

add Zero m = add m Zero持有。

  1. 证明对于所有递归情况，假设参数的假设足以证明构造结果。同样，这里唯一的递归情况是Succ; 所以你需要证明

给定 add n m = add m n，add (Succ n) m = add m (Succ n)持有。

于 2015-12-11T14:44:52.203 回答
3

如果您更正式地说明问题，包括 forall 量词，也许会有所帮助：

forall (n m : Nat), add n m = add m n

对 n 的归纳

应用归纳原理：

forall m, add 0 m = add m 0 
          -> (forall n m, add n m = add m n -> add (S n) m = add m (S n)) 
          -> forall n m, add n m = add m n

现在我们需要证明基本情况add Z m = add m Z和归纳情况forall n m, add n m = add m n -> add (S n) m = add m (S n)

基本情况：forall m, add Z m = add m Z

Let mbe any Nat（这称为介绍）。

  • 申请addLHS，您将获得m = add m Z.
  • 申请forall m, add m Z = m（如果你愿意，你可以证明这一点）重写 RHS 并且你得到m = m.

这通过平等的反身性成立。

归纳案例forall n m, add n m = add m n -> add (S n) m = add m (S n)

Let n, mbe anyNat并引入假设add n m = add m n（即假设它成立）

目标：add (S n) m = add m (S n)

  • 适用add于 LHS：S (add n m) = add m (S n)
  • 使用假设重写：S (add m n) = add m (S n)
  • 向 LHS申请forall x y, S (add x y) = add (S x) y（同样，如果您愿意，您可以证明这一点）以获得add m (S n) = add m (S n).

这适用于反身性。

我们完成了。

于 2015-12-11T14:50:49.770 回答
-2

尝试一个例子。

3 = 1 + 1 + 1 + 0

所以在 中Nat，3表示为Succ (Succ (Succ Zero))。现在对于任何m :: Nat, （考虑两种情况：Zero和Succ (Succ (... (Succ Zero) ...)）

我们有

add (Succ (Succ (Succ Zero))) m = 
Succ (add (Succ (Succ Zero)) m) = -- we took 1 from 3 and added it to the overall answer
Succ (Succ (add (Succ Zero) m)) = -- ditto
Succ (Succ (Succ (add Zero m))) = -- ditto
Succ (Succ (Succ m)) -- by applying the base case for `add`

所以我们看到结果是“无论m是什么（0 或其他），再加上三个”，或者m+3如你所料。

于 2015-12-11T13:33:28.053 回答