0

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

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）的子集上完成的，为什么不能保证终止？

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

4

2 回答 2

5

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

这是一个例子：

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

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

于 2018-01-17T16:22:28.560 回答
2

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

如果您希望 Coq 接受这一点，您可能需要使用有根据的递归重写您的函数。Adam Chipala 的书 CPDT 对此有一个很好的章节。

于 2018-01-16T21:48:06.957 回答