12

Coq で Ackermann-Peters 関数を定義しようとしていますが、理解できないエラー メッセージが表示されます。ご覧のとおりa, b、Ackermann の引数をペアでパッケージ化しています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 を定義する方法を提案できますか?

4

3 に答える 3

3

ack関数の定義中に関数を参照しているため、このエラーが発生します。自己参照は s (つまり、再帰関数) でのみ許可されFixpointますが、問題は、おそらくご存知のように、アッカーマン関数が原始的な再帰関数ではないことです。

詳細については、 Coq'Art セクション 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.
于 2012-04-24T18:04:02.300 に答える
1

あなたの関数を Coq 8.4 で試してみましたが、エラーは少し異なります。

Error: Nested recursive function are not allowed with Function

ack への内部呼び出しが問題だと思いますが、理由はわかりません。

これが少し役立つことを願っています、V.

PS: 私が Ack を定義する通常の方法は、wires が書いたもので、内側に固定点があります。

于 2012-05-21T07:57:44.517 に答える