nat_to_bin的递归定义是病态的

Question

我目前正在阅读软件基础系列的第一卷。在其中一个练习中，我应该写一个函数，将自然数(一元形式)转化为等效的二进制数。

这是我的代码/方法:

Inductive bin : Type := 
| Z
| B0 (n : bin)
| B1 (n : bin).
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Fixpoint nat_to_bin (n:nat) : bin := 
match n with
| 0 => Z
| 1 => B1 Z
| 2 => B0 (B1 Z)
| m => match evenb(m) with 
| true => B0 (nat_to_bin (Nat.div m 2))
| false => B1 (nat_to_bin (Nat.modulo m 2)) 
end
end.

我正在使用https://jscoq.github.io/scratchpad.html做这些练习。现在我得到这个错误信息:

nat_to_bin的递归定义是病态的。在环境Nat_to_bin: NAT ->本

n: nat

n0: nat

n1: nat

n2: nat

递归调用nat_to_bin的主参数等于"Nat.divN 2 "而不是以下变量之一:" no0 "n1"n2"．递归定义为:"fun n: nat =>用

匹配n| 0 =>Z

| 1 =>B1 Z

| 2 =>B0 (B1 Z)

| S (S (S _)) =>

if evenb n then B0 (nat_to_bin (Nat.div n 2))

else B1 (nat_to_bin (Nat.modulo n 2))

结束".

Answer 1

为了保持良好的逻辑属性，Coq中所有可定义的函数都是终止的。为了加强这一点，对固定点定义有一个限制，就像您正在尝试做的那样，称为保护条件。这个限制大致是递归调用只能在函数实参的子项上进行。

在您的定义中并非如此，您将nat_to_bin应用于术语(Nat.div n 2)和(Nat.modulo n 2)，这是应用于n的函数。虽然你可以在数学上证明它们总是小于n，但它们不是n的子项，所以你的函数不遵守保护条件。

如果你想用你现在所做的方式定义nat_to_bin，你需要求助于良基础归纳，这将使用nat上的良基础顺序，允许你在任何你能证明比n小的项上调用你的函数。然而，这个解决方案是相当复杂的，因为它会迫使你做一些不那么容易的证明。

相反，我建议采用另一种方式:就在书中，建议定义一个函数incr : bin -> bin，将二进制数加1。您可以使用它在n上通过简单的递归来定义nat_to_bin，如下所示:

Fixpoint nat_to_bin (n:nat) : bin := 
match n with
| 0 => Z
| S n' => incr (nat_to_bin n')
end.

对于incr本身，您也应该能够在二进制数上使用简单的递归写出它，因为它们在外面写的是低阶位。