无法确定终止

Question

确定一个集合是否是另一个集合的子集的函数：

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil => true
  | h :: t => match (beq_nat (count h s1) (count h s2)) with
    | true => subset (remove_all h t) (remove_all h s2)
    | false => false
    end
  end.

为清楚起见

beq_nat判断两个自然数是否相等
count统计给定自然数在集合中出现的次数
remove_all 从集合中删除给定自然数的每个实例

CoqIDE "Cannot guess decreasing argument of fix." 鉴于递归是在 t 的子集（s1 的尾部）上进行的，为什么不能保证终止？

注意：此问题来自this website，其作者要求解决方案不要公开发布。此外，我已经解决了这个练习，因此 不需要解决方案。非常感谢解释为什么 coq 无法确定终止。

Answer 1

您的终止参数是正确的，但 Coq 不够聪明，无法自行解决这个问题。粗略地说，Coq 只接受对其主要参数的句法子项执行的递归调用。这是一个非常严格的概念：例如，[1; 3] 是 [0; 1; 2; 3] 的子列表，但不是句法子项。

如果您希望 Coq 接受这一点，您可能需要使用有根据的递归重写您的函数。 Adam Chipala 的书 CPDT 有 nice chapter on this.

Answer 2

作为第一个近似值，接受递归调用的规则是，在递归调用中，参数之一应该是通过模式获得的变量-从输入变量 相同等级 匹配 。实际上，规则稍微宽松一些，但幅度不大。

这是一个例子：

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

acceptance的解释是p是rank 1的参数，它是从n作为模式匹配变量得到的，它是rank 1的初始参数。所以函数在结构上是递归的，在第一个参数上递减。应该总是有一个减少的论点。不接受多个参数之间的合并减少。

如果你不想被细节淹没，你应该停止阅读这里。

规则的第一个放松是递减递归参数可以是模式匹配构造，只要所有分支中的值确实是一个小于第一个的变量即可。这是一个利用这个想法的笨拙函数的例子：

Require Import List Arith.

Fixpoint awk1 (l : list nat) :=
  match l with
  | a :: ((b :: l'') as l') => 
    b :: awk1 (if Nat.even a then l' else l'')
  | _ => l
  end.

所以在函数awk1中递归调用的不是一个变量，而是一个模式匹配表达式，但是没关系，因为这个递归调用的所有可能值确实都是通过模式匹配得到的变量.这也说明了终止检查器有多挑剔，因为表达式 (if Nat.even a then (b :: l'') else l'') 不会被接受：(b :: l'') 不是变量。

规则的第二个放宽是递归参数可以是函数调用，只要这个函数调用可以转换为可接受的表达式。这是一个示例，是上一个示例的后续。

Definition arg n (l : list nat) :=
  if Nat.even n then
    l 
  else
    match l with _ :: l' => l' | _ => l end.

Fixpoint awk2 (l : list nat) :=
match l with
  a :: l' => a :: awk2 (arg a l')
| _ => l
end.

规则的第三个放松是，用于计算递归参数的函数甚至可以是递归的，只要它可以递归地传递递减的属性。这是一个例子：

Fixpoint mydiv (n : nat) (m : nat) :=
   match n, m with
     S n', S m' => S (mydiv (Nat.sub n' m') m)
   | _, _ => n
   end.

如果打印 Nat.sub 的定义，您会发现它经过精心设计，始终 return 要么是递归调用的结果，要么是第一个输入，此外，在递归调用中，第一个参数确实是通过模式匹配从第一个输入获得的变量。这种递减属性是公认的

无法确定终止

Cannot determine termination

termination

coq

totality