无法确定终止 [英] Cannot determine termination

问题描述

确定一个集合是否是另一个集合的子集的功能:

Function for determining if a set is a subset of another:

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从集合中删除给定自然数的每个实例

• beq_nat determines equality of two natural numbers
• count counts the number of times a given natural number occurs in a set
• remove_all removes each instance of a given natural number from a set

CoqIDE无法猜测Fix的递减参数.鉴于递归是在t的子集(s1的尾部)上进行的，为什么不能保证终止?

CoqIDE "Cannot guess decreasing argument of fix." Given that the recursion is being done on a subset of t (the tail of s1) why is this not guaranteed to terminate?

注意:该问题来自于此网站，其作者要求解决方案不公开发布.此外，我已经解决了此练习，因此不需要解决方案.解释为什么coq无法确定终止的原因.

Note: This problem is from this website whose authors request solutions not to be posted publicly. Furthermore I have already solved this exercise so a solution is not desired. An explanation of why coq can't determine termination would be much appreciated.

推荐答案

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

As a first approximation, the rule for accepting a recursive call is that in the recursive call one of the arguments should be a variable obtained through pattern-matching from the input variable at the same rank in the inputs. In reality, the rule is slightly more relaxed, but not much.

这是一个实例:

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

接受的解释是p是等级1的参数，它是从n的模式匹配变量获得的，它是等级1的初始参数.因此该函数在结构上是递归的，递减关于第一个论点.总应该有一个减少的论点.几个参数之间的总和减少是不可接受的.

The explanation for acceptance is that p is the argument at rank 1, it is obtained as a pattern-matching variable from n, which is the initial argument at rank 1. So the function is structurally recursive, decreasing on the first argument. There should always be an argument that decreases. Combined decrease between several arguments is not accepted.

如果您不想淹没在细节中，应该在这里停止阅读.

You should stop reading here if you do not want to be drowned in details.

该规则的第一个松弛之处是，递归递减参数可以是模式匹配构造，只要所有分支中的值确实是小于第一个的变量即可.这是一个利用这种想法的笨拙函数的示例:

The first relaxation of the rule is that the decreasing recursive argument may be a pattern matching construct, as long as the value in all branches is indeed a variable that is smaller than the first one. Here is an example of an awkward function that exploits this idea:

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'')不是变量.

So in the function awk1 the recursive call is not on a variable, but on a pattern-matching expression, but it is okay because all possible values of this recursive call are indeed variables obtained through pattern matching. This also illustrates how picky the termination checker can be, because the expression (if Nat.even a then (b :: l'') else l'') would not be accepted: (b :: l'') is not a variable.

该规则的第二个放松之处是，递归参数可以是一个函数调用，只要该函数调用可以转换为可以接受的表达式即可.这是一个示例，是对上一个示例的补充.

The second relaxation of the rule is that the recursive argument can be a function call, as long as this function call is convertible to an expression that is accepted. Here is an example, following up on the previous one.

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.

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

The third relaxation of the rule is that the function used to compute the recursive argument can even be recursive, as long as it can transmit the decreasing property recursively. Here is an illustration:

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的定义，您会发现它经过精心设计，总是返回递归调用的结果或第一个输入，而且在递归调用中，第一个参数确实是一个变量从第一个输入通过模式匹配获得.这种减少的性质被认识到.

If you print the definition of Nat.sub you will see that it is carefully crafted to always return either the result of a recursive call, or the first input, and moreover, in recursive calls, the first argument is indeed a variable obtained through pattern-matching from the first input. This kind of decreasing property is recognized.

这篇关于无法确定终止的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！