建立树并减少修正论点

Question

我正在尝试在Coq中使用以下函数来实现使用n个元素构建Braun树的功能，但是Coq给了我一个错误，它无法猜测到fix参数的降低：

Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
  fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) := 
    match i with
    | 0 => (T a E E,E) 
    | _ => match Nat.odd i with
           | true => let m := ((i - 1) / 2) in 
                     let (s,t) := copy2 a m in
                     ((T a s t),(T a t t)) 
           | false => let m := ((i - 2) / 2) in
                      let (s,t) := copy2 a m in
                     ((T a s s),(T a s t)) 
           end
    end
in
match copy2 x n with
|(_,snd) => snd
end.

我知道不是问题出现在偶数和奇数情况下，因为当我删除偶数/奇数情况时，它给出了相同的错误：

Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
  fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) := 
    match i with
    | 0 => (T a E E,E) 
    | _ => let m := ((i - 1) / 2) in 
                     let (s,t) := copy2 a m in
                     ((T a s t),(T a t t)) 
    end
in
match copy2 x n with
|(_,snd) => snd
end.

我怎样才能说服Coq我实际上是在减少争论？

编辑BraunTree的类型：

Inductive BraunTree : Type :=
| E : BraunTree
| T: V -> BraunTree -> BraunTree -> BraunTree.

Answer 1

Fixpoint/ fix仅允许在语法上较小的参数上进行递归调用。

Fixpoint example (n : nat) :=
  ... (* There must be a match on [n] somewhere *)
    ... match n with
        | O => base_case (* no recursive call allowed *)
        | S m =>
          ... (example m)
          (* We can only call [example] on [m], or some even smaller value obtained by matching on [m] *)
         end ...

特别是，它不能就通过某种任意函数得到的值递归调用（在这种情况下，div并sub在copy2 a ((i-1) / 2)）。

这是三个选项：

1. 选择自然数的另一种表示形式，以便其上的模式匹配自然分解为所需定义的不同分支（基本情况（零），偶数，奇数）。

2. 利用递归深度实际上受限制的事实n，因此我们可以将其n用作“燃料”，我们知道在完成之前实际上不会耗尽它。

3. 狡猾地提取出递减参数的子项以进行递归调用。与以前的解决方案相比，此解决方案的通用性和鲁棒性较低。与终止检查器的斗争更加艰巨。

替代代表

我们有三种情况：零，偶数和奇数。幸运的是，标准库的类型具有几乎相同的结构positive：

Inductive positive :=    (* p > 0 *)
| xH                     (* 1 *)
| xI (p : positive)      (* 2p + 1 *)
| xO (p : positive)      (* 2p     *)
.

positive用一个额外的零指向类型，我们得到N：

Inductive N :=
| N0                      (* 0 *)
| Npos (p : positive)     (* p > 0 *)
.

还有一个转换函数N.of_nat : nat -> N，尽管如果转换变得很烦人，最好在N各处使用而不是nat。

最终定义以对的案例分析开始N，显示positive数字的案例使用fix-point 处理，其中基本案例是1而不是0。我们必须转移一些细节，因为偶数情况是2p而不是2p + 2 ，所以我们必须做（i-1，i）而不是一对大小为（i + 1，i）的树。但是总的来说，递归案例仍然很自然地符合非正式规范：

Require Import NArith PArith.

Parameter V : Type.

Inductive BraunTree : Type :=
| E : BraunTree
| T: V -> BraunTree -> BraunTree -> BraunTree.

Definition copy (x : V) (n : N) : BraunTree :=
  match n with
  | N0 => E
  | Npos p =>
    let
      (* copy2 a i : a tree of (i-1) copies of a, and another of i copies of a *)
      fix copy2 (a : V) (i : positive) : (BraunTree * BraunTree) := 
        match i with

        | xH => (* i = 1 *)
          (E, T a E E)

        | xI p => (* i = 2p + 1 *)
          let (s,t) := copy2 a p in
          ((T a t s),(T a t t))

        | xO p => (* i = 2p *)
          let (s,t) := copy2 a p in
          ((T a s s),(T a t s))

        end
    in
    match copy2 x p with
    |(_,snd) => snd
    end
  end.

足够的燃料

我们在上添加燃料fix作为递减参数。我们只能用if结束n = i = 0，所以我们知道结果应该是什么。

(* note: This doesn't need to be a Fixpoint *)
Definition copy (x : V) (n : nat) : BraunTree :=
let
  fix copy2 (a : V) (n : nat) (i : nat) : (BraunTree * BraunTree)  := 
    match n with
    | O => (T a E E,E)
    | S n' =>
      match i with
      | O => (T a E E,E) 
      | _ =>
        if Nat.odd i then
          let m := div2 ((i - 1) / 2) in 
          let (s,t) := copy2 a n' m in
          ((T a s t),(T a t t)) 
        else
          let m := div2 ((i - 2) / 2) in 
          let (s,t) := copy2 a n' m in
          ((T a s s),(T a s t)) 
      end
    end
in
match copy2 x n n with
|(_,snd) => snd
end.

在以下情况下可以很好地工作：

• 我们可以计算所需的燃料量；
• 当我们用完燃料时，有一个可以预见的答案。

如果这些假设中的任何一个都不成立，则需要使用来填充代码option。

嵌套递归

如前所述，Coq对于减少参数有严格的规定。通常的解释是，我们只能对递减调用，该递归调用是通过对递减参数（或传递式，其子术语之一）进行模式匹配而获得的。

一个明显的限制是，由于条件是句法的（即，Coq着眼于定义以跟踪递减论证的出处），因此论证n最多只能减少一个常数（相对于，为常数n）。match定义中的数量有限。特别是，没有办法对除以2的结果进行递归调用，因为这表示n/2线性减少in的值n。

不管好坏，Coq的终止标准实际上比这要聪明一些：可以将递减的参数传递给嵌套的固定点，然后通过它跟踪“子项”关系。

无缺点部门

的确，Peano的除法nat可以这样定义：Coq可以判断结果是股息的子项：

Definition div2 (n : nat) :=
  let fix d2 (n1 : nat) (n2 : nat) {struct n1} :=
    match n2 with
    | S (S n2') =>
      match n1 with
      | O => n1
      | S n1' => d2 n1' n2'
      end
    | _ => n1
    end
  in d2 n n.

我们的想法是写fix的两个参数（有点像燃料解决方案），这等于（开始了-点d2 n n），我们去掉2个 S从一个构造函数（n2他们的），每一个 S我们从其他的删除（n1）。重要说明：

• 在所有非递归情况下，我们都会返回n1（无论如何都不会 返回0），然后保证它是topmost的子项n。

• 并且该函数必须在n1（我们返回的术语）中递减，而不是n2（Coq仅跟踪递减参数的子项）。

所有确保这div2 n是的子项n（不是严格的子项（或适当的子项），因为n可能是O）。

这与以前的基于燃料的解决方案有相似之处，但是在这里，减少的论点比欺骗类型检查器的设备更为重要。

此技术是无缺点编程的一种变体。（请注意，尽管约束条件与文献中讨论的约束条件并不完全相同，例如，当重点是避免内存分配而不是通过结构良好的基础来确保终止时）。

结论：的定义 copy

一旦有了div2，我们就可以copy进行一些调整，再次通过模式匹配来获得i-1和i-2作为的适当子项i。下面的i'和i''是i（通过视觉检查）的适当子项，div2 i'和div2 i''是i'和i''（根据的定义div2）的子项。通过传递性，它们是的适当子项i，因此终止检查器接受。

Definition copy (x : V) (n : nat) : BraunTree :=
let
  fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree)  := 
    match i with
    | 0 => (T a E E,E) 
    | S i' => (* i' = i-1 *)
      if Nat.odd i then
        let m := div2 i' in 
        let (s,t) := copy2 a m in
        ((T a s t),(T a t t)) 
      else
        match i' with
        | O => (* Unreachable *) (E, E)
        | S i'' => (* i'' = i-2 *)
          let m := div2 i'' in 
          let (s,t) := copy2 a m in
          ((T a s s),(T a s t)) 
        end
    end
in
match copy2 x n with
|(_,snd) => snd
end.