无法确定终止答案

【问题标题】：Cannot determine termination无法确定终止
【发布时间】：2018-06-25 14:59:27
【问题描述】：

判断一个集合是否是另一个集合的子集的函数：

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“无法猜测修复的递减参数。”鉴于递归是在 t 的子集（s1 的尾部）上完成的，为什么不能保证终止？

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

【问题讨论】：

标签： coq termination totality

【解决方案1】：

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

这是一个例子：

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

接受的解释是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 的定义，您会发现它经过精心设计，始终返回递归调用的结果或第一个输入，此外，在递归调用中，第一个参数确实是一个变量通过第一个输入的模式匹配获得。这种递减性质是公认的。

【讨论】：

【解决方案2】：

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

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

【讨论】：