CoqでAckermannを定義する際にエラーが発生しました。

Question

CoqでAckermann-Peters関数を定義しようとしていますが、わからないエラーメッセージが表示されています。ご覧のとおり、私はAckermannの引数a, bを1組でパッケージ化しています。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. 

次のエラーメッセージです：

Error: No such section variable or assumption: ack .

私はコックを気にかわからないんだけど、インターネットを検索、私は提案は、再帰を使用してに問題がある可能性があり見つから関数は、順序付けまたはメジャーで定義され、再帰呼び出しは一致内で発生します。しかし、投影fstとsndとif-then-elseを使用すると、異なるエラーメッセージが生成されました。誰かがCoqでAckermannを定義する方法をお勧めしますか？

Answer 1

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 *) 

Answer 2

定義中にack関数を参照しているため、このエラーが発生します。自己参照はFixpoint（すなわち再帰関数）でのみ許可されていますが、問題は、おそらく知っているように、Ackermann関数は基本的な再帰関数ではないということです。

詳細については、Coq'Art section 4.3.2.2を参照してください。

それを定義するもう1つの方法は、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. 

Answer 3

のようなものは、私はちょうどCoqの8.4を使用して機能を試してみましたが、エラーが若干異なります。

Error: Nested recursive function are not allowed with Function 

私はACKへの内部呼び出しが問題だと思いますが、私は知りませんなぜ。

希望これはビットを助け、 V.

PS：私はACKを定義する通常の方法は、ワイヤは、内側固定点で、書いたものです。