0

为什么以下是自然数的正确实现?

mod PEANO-NAT is
  sort Nat .
  op zero : -> Nat .
  op succ : Nat -> Nat .
  op plus : Nat Nat -> Nat .
  vars N M : Nat .
  eq plus(zero, M) = M .
  eq plus(succ(N), M) = succ(plus(N, M)) .
endm

特别是我很难理解最后两行以及它们如何确保正确定义自然数。任何帮助

4

1 回答 1

1

一个更好的问题可能是:为什么这个自然数加法的定义是正确的?

要回答这个问题,我们必须证明通过这两个方程,加法是一个可交换的 Monoid。这意味着:a + b = b + a

对于基本情况和归纳步骤,您可以尝试使用归纳来做到这一点。

试试看。我很乐意提供帮助。

于 2019-02-06T23:39:18.807 回答