根据产品类型定义递归函数 [英] Defining recursive function over product type

问题描述

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

I'm trying to formalize each integer as an equivalence class of pairs of natural numbers, where the first component is the positive part, and the second component is the negative part.

定义整数:类型:= prod nat nat.

我想定义一个归一化函数，使正负尽可能多地抵消.

I want to define a normalization function where positives and negatives cancel as much as possible.

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说:

错误:归一化的递归定义格式不正确.在环境中规范化:整数->整数i:整数a:自然b:自然a':自然b':自然递归调用以规范化为主要参数等于(a'，b')"，而不是"i"的子项.

Error: Recursive definition of normalize is ill-formed. In environment normalize : integer -> integer i : integer a : nat b : nat a' : nat b' : nat Recursive call to normalize has principal argument equal to "(a', b')" instead of a subterm of "i".

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

I think this might have to do with well-founded recursion?

推荐答案

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

Recursive calls must be made on a "subterm" of the original argument. A subterm for a term in an inductive type is essentially a term of the same type that was used to create the original term. For example, a subterm of a natural number like S a' is a'.

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

Unfortunately for your definition (as written), a pair i: prod nat nat doesn't have any subterms in this sense. This is because prod isn't a recursive type. Its constructor pair: A -> B -> prod A B doesn't take anything of type prod A B as an argument.

要解决此问题，建议您先在两个单独的自然数上定义函数.

To fix this, I'd suggest defining your function on two separate natural numbers first.

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_helper 定义 normalize .

Then normalize can easily be defined in terms of normalize_helper.

这篇关于根据产品类型定义递归函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！