我想在勒柯克定义阿克曼彼得斯功能,我得到的是我不明白的错误消息。 正如你所看到的,我包装参数a, b
阿克曼的一对ab
; 我提供定义的参数排序功能的排序。 然后我用Function
的形式来定义阿克曼本身,为它提供了排序功能, ab
的说法。
Require Import Recdef.
Definition ack_ordering (ab1 ab2 : nat * nat) :=
match (ab1, ab2) with
|((a1, b1), (a2, b2)) =>
(a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))
end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, ack (a, b-1))
end.
我得到的是下面的错误信息:
错误:没有这样的部分变量或假设: ack
。
我不知道是什么困扰勒柯克,但搜索互联网,我发现了一个建议,有可能是使用与排序或措施,其中递归调用比赛中发生定义的递归函数的问题。 然而,使用突起fst
和snd
和if-then-else
产生一个不同的错误消息。 有人可以请建议如何在勒柯克定义阿克曼?
看起来Function
也解决不了这个问题。 然而,其表弟Program Fixpoint
即可。
让我们来定义一些引理第一治疗精心foundedness:
Require Import Coq.Program.Wf.
Require Import Coq.Arith.Arith.
Definition lexicographic_ordering (ab1 ab2 : nat * nat) : Prop :=
match ab1, ab2 with
| (a1, b1), (a2, b2) =>
(a1 < a2) \/ ((a1 = a2) /\ (b1 < b2))
end.
(* this is defined in stdlib, but unfortunately it is opaque *)
Lemma lt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof. intro p; intros; elim (lt_wf p); auto with arith. Defined.
(* this is defined in stdlib, but unfortunately it is opaque too *)
Lemma lt_wf_double_ind :
forall P:nat -> nat -> Prop,
(forall n m,
(forall p (q:nat), p < n -> P p q) ->
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
intros P Hrec p. pattern p. apply lt_wf_ind.
intros n H q. pattern q. apply lt_wf_ind. auto.
Defined.
Lemma lexicographic_ordering_wf : well_founded lexicographic_ordering.
Proof.
intros (a, b); pattern a, b; apply lt_wf_double_ind.
intros m n H1 H2.
constructor; intros (m', n') [G | [-> G]].
- now apply H1.
- now apply H2.
Defined.
现在,我们可以定义阿克曼彼得功能:
Program Fixpoint ack (ab : nat * nat) {wf lexicographic_ordering ab} : nat :=
match ab with
| (0, b) => b + 1
| (S a, 0) => ack (a, 1)
| (S a, S b) => ack (a, ack (S a, b))
end.
Next Obligation.
inversion Heq_ab; subst. left; auto. Defined.
Next Obligation.
apply lexicographic_ordering_wf. Defined.
一些简单的测试证明了我们可以计算ack
:
Example test1 : ack (1, 2) = 4 := eq_refl.
Example test2 : ack (3, 4) = 125 := eq_refl. (* this may take several seconds *)
使用方程由M. Sozeau和C.曼金插件有可能定义函数是这样的:
From Equations Require Import Equations Subterm.
Equations ack (p : nat * nat) : nat :=
ack p by rec p (lexprod _ _ lt lt) :=
ack (pair 0 n) := n + 1;
ack (pair (S m) 0) := ack (m, 1);
ack (pair (S m) (S n)) := ack (m, ack (S m, n)).
不幸的是,它不是可以使用( , )
符号来表示,由于对问题#81 。 该代码是从等式的测试套件采取: ack.v 。
因为你引用的您得到这个错误ack
功能,而你定义它。 自基准仅在允许Fixpoint
S(即递归函数),但问题是,正如你可能知道,阿克曼函数不是原始递归函数。
见Coq'Art节4.3.2.2对于一些这方面的更多信息。
所以一个替代的方式来定义它是通过内联一个第二递归函数,是用于第二个参数结构递归; 所以像
Fixpoint ack (n m : nat) : nat :=
match n with
| O => S m
| S p => let fix ackn (m : nat) :=
match m with
| O => ack p 1
| S q => ack p (ackn q)
end
in ackn m
end.
我只是想你的函数勒柯克8.4,并且错误略有不同:
Error: Nested recursive function are not allowed with Function
我想内心的召唤,以确认是问题,但我不知道为什么。
希望这有助于一点,V.
PS:通常的方法我定义确认是什么电线写的,带有内部固定点。