在Coq中定義Ackermann的錯誤

我想在Coq中定義Ackermann-Peters函數，並且收到一條我不明白的錯誤消息。正如你所看到的，我將Ackermann的參數a, b包裝成一對ab;我提供了一個爲參數定義排序函數的順序。然後，我使用Function表格來定義Ackermann本身，爲它提供ab參數的排序功能。在Coq中定義Ackermann的錯誤

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嗎？

來源

2012-04-24 Mayer Goldberg

今天我遇到了同樣的問題。你找到解決方案嗎？ – 2013-06-27 06:33:35

@AbhishekAnand這已經有一段時間了......我在下面提供了一個帶有「程序修復點」的解決方案。你有沒有用'Function'找到解決方案？ – 2017-06-30 10:40:37

不，我沒有。感謝您的回答。 – 2017-06-30 21:12:30

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

來源

2017-06-29 18:53:14

由於在定義它時引用ack函數，您會收到此錯誤。自我引用只允許在Fixpoint s（即遞歸函數）中使用，但問題是，正如您可能知道的那樣，Ackermann函數不是原始的遞歸函數。

有關更多信息，請參見Coq'Art section 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.

來源

2012-04-24 18:04:02 wires

我沒有使用Fixpoint，而是使用Function。這應該適用於具有遞減參數的全部函數，並且我應該能夠使用度量或比較來做到這一點，接下來是一個定理，即遞歸調用中的參數要麼具有較小的度量，要麼小於原始的論據，根據比較。我知道Ackermann是二階PR，但顯然這個函數的PR狀態並不妨礙你以某種方式對它進行編碼。我想知道的是我給出的編碼有什麼問題，它似乎遵循手冊中的描述。 – 2012-04-24 18:30:41

我只是想你的函數勒柯克8.4，並且錯誤略有不同：

Error: Nested recursive function are not allowed with Function

我猜內心的召喚，以確認是問題，但我不知道爲什麼。

希望這有助於一點，五

PS：通常的方法我定義確認是什麼電線寫的，帶有內部固定點。

來源

2012-05-21 07:57:44 Vinz

在Coq中定義Ackermann的錯誤

回答

相關問題