我正在尝试使用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.
发布于 2019-05-15 07:29:33
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 ...
特别是,不允许对通过某个任意函数(在本例中为copy2 a ((i-1) / 2)
中的div
和sub
)获得的值进行递归调用。
这里有三个选项:
n
限定的事实,所以我们可以使用n
作为“燃料”,我们知道在我们进行递减参数的子项之前,n
实际上不会耗尽。这个解决方案比以前的解决方案不那么通用和健壮;它与终止检查器的斗争要困难得多。另一种表示
我们有三种情况:零、偶数和奇数。幸运的是,标准库有一个结构几乎相同的类型,即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
中。我们只能在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
,这是n
中的一个线性值。
不管是好是坏,Coq的终止标准实际上比这更聪明:可以将递减参数传递给嵌套固定点,“子项”关系将通过它进行跟踪。
Cons-free除法
实际上,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.
我们的想法是编写一个包含两个参数的代码解决方案(有点像燃料解决方案),它们以相等(d2 n n
)开头,并且我们从其中一个(n2
)中删除两个 S
构造函数(n2
),为我们从另一个(<>D54>)中删除一个代码( S
)。重要细节:
n1
(在任何情况下都不是0
),然后保证它是最上面的n2
(我们返回的项)中递减,而不是(Coq只跟踪递减参数的子项)。
所有这些都确保了div2 n
是n
的子术语(而不是严格的子术语(或专有的子术语),因为n
可以是O
)。
这与以前的基于燃料的解决方案有相似之处,但在这里,递减的论点比欺骗类型检查器的设备更相关。
这种技术是cons-free编程的一种变体。(但请注意,这些约束与文献中讨论的约束并不完全相同,例如,当重点放在避免内存分配而不是通过结构良好来确保终止时。)
结论: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.
https://stackoverflow.com/questions/56132183
复制相似问题