无法确定终止

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"不能猜测减少修正的论点." 鉴于递归是在t(尾部s1)的子集上完成的,为什么不能保证终止？

注意:此问题来自此网站,其作者要求解决方案不公开发布.此外,我已经解决了这个问题,因此不需要解决方案.解释为什么coq不能确定终止将非常感激.

Answer 1

作为第一近似,用于接受一个递归调用的规则是,在递归调用的参数之一应该是一个变量通过获得模式匹配从所述输入变量在同一等级中的输入.实际上,规则略微放松,但并不多.

这是一个实例:

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你将看到它经过精心设计,总是返回递归调用的结果,或者第一个输入,而且,在递归调用中,第一个参数确实是通过模式匹配从第一个输入.这种减少的属性被认可.