根据产品类型定义递归函数

mark 发表于 Dev

标记

我正在尝试将每个整数形式化为自然数对的等价类，其中第一个成分是正数部分，第二个成分是负数部分。

Definition integer : Type := prod nat nat.

我想定义一个规范化函数，在该函数中，正数和负数会尽可能抵消。

Fixpoint normalize (i : integer) : integer :=
let (a, b) := i in
match a with
| 0 => (0, b)
| S a' => match b with
        | 0 => (S a', 0)
        | S b' => normalize (a', b')
        end
end.

但是Coq说：

错误：规范化的递归定义格式错误。在环境中normalize：integer-> integer i：integer a：nat b：nat a'：nat b'：nat递归调用归一化具有等于“（a'，b'）”的主参数，而不是“ i”的子项”。

我认为这可能与有充分根据的递归有关？

无伴奏合唱

递归调用必须在原始参数的“子项”上进行。归纳类型的术语的子术语本质上是与用于创建原始术语的类型相同的术语。例如，自然数的子项S a'是a'。

不幸的是，对于您的定义（按书面规定），一对i: prod nat nat在这种意义上没有任何子术语。这是因为prod不是递归类型。它的构造pair: A -> B -> prod A B函数不接受任何类型prod A B的参数。

为了解决这个问题，我建议先在两个单独的自然数上定义您的函数。

Fixpoint normalize_helper (a b : nat) : integer :=
match a with
| 0 => (0, b)
| S a' => match b with
        | 0 => (S a', 0)
        | S b' => normalize a' b'
        end
end.

然后normalize可以很容易地用定义normalize_helper。

本文收集自互联网，转载请注明来源。

如有侵权，请联系 [email protected] 删除。