在 Coq 中定义 Ackermann 函数时出现错误

Question

我正在尝试在Coq中定义Ackermann-Peters函数，但是我收到了一个我不理解的错误消息。正如您所见，我正在将Ackermann的参数a、b打包成一对ab；我提供了一个用于定义参数排序的排序函数。然后，我使用Function表单来定义Ackermann本身，并为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。

我不确定是什么困扰了Coq，但在搜索互联网时，我发现建议使用具有排序或度量的递归函数定义可能存在问题，其中递归调用出现在匹配内部。然而，使用投影fst和snd以及一个if-then-else生成了不同的错误消息。请问有人可以建议如何在Coq中定义Ackermann函数吗？

- Mayer Goldberg

---

我今天遇到了同样的问题。你找到解决方案了吗？ - Abhishek Anand

@AbhishekAnand 好久不见了... 我在下面提供了一个使用 Program Fixpoint 的解决方案。你找到了使用 Function 的解决方案吗？ - Anton Trunov

不，我没有。谢谢你的回答。 - Abhishek Anand

Answer 1

似乎 Function 无法解决这个问题。然而，它的近亲 Program Fixpoint 可以。

首先，让我们定义一些关于良基性的引理：

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.

现在我们可以定义Ackermann-Péter函数：

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. Mangin开发的Equations插件，可以这样定义函数：

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，无法使用(,)符号表示一对。这段代码取自Equation的测试套件：ack.v。

- Anton Trunov

Answer 2

您之所以会出现这个错误，是因为您在定义ack函数时引用了它。自我引用只允许在Fixpoint中（即递归函数），但问题是，正如您可能知道的那样，阿克曼函数不是原始递归函数。

有关此问题的更多信息，请参见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.

- wires

---

我使用的不是Fixpoint，而是Function。这应该适用于拥有递减参数的全函数，并且我应该能够使用度量或比较来实现，接着使用一个定理，指出递归调用中的参数要么具有更小的度量，要么小于原始参数，按照比较器的规则。我知道Ackermann是2阶PR，但显然函数的PR状态并没有阻止您以某种方式对其进行编码。我想知道的是，我给出的编码方式有什么问题，它似乎遵循手册中的描述。 - Mayer Goldberg

Answer 3

我刚刚在 Coq 8.4 中尝试了您的函数，错误略有不同：

Error: Nested recursive function are not allowed with Function

我猜内部调用ack的问题出在哪里，但我不知道为什么。

希望这能有所帮助， V。

附注：我通常定义Ack的方式是wires写的，使用内部不动点。

- Vinz