Coq에서 Ackermann을 정의하는 중 오류가 발생했습니다.

Question

Coq에서 Ackermann-Peters 함수를 정의하려고하는데 이해가 안되는 오류 메시지가 나타납니다. 보시다시피, 저는 Ackermann의 인수 a, b을 한 켤레에 포장합니다. ab; 인수에 대한 순서 지정 함수를 정의하는 순서를 제공합니다. 그런 다음 Function 양식을 사용하여 Ackermann 자체를 정의하고 ab 인수에 대한 정렬 함수를 제공합니다.

Error: No such section variable or assumption: ack .

내가 COQ 귀찮게하지만, 인터넷 검색, 내가 제안 재귀를 사용하여 문제가있을 수 있습니다 찾았는지 확실하지 않다 :

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. 

내가 도착하면 다음과 같은 오류 메시지입니다 함수는 순서 부 또는 측정 값으로 정의되며 재귀 호출은 일치 항목 내에서 발생합니다. 그러나 투영 fst 및 snd 및 if-then-else을 사용하면 다른 오류 메시지가 생성됩니다. 누군가가 Coq에서 Ackermann을 정의하는 방법을 제안 할 수 있습니까?

Answer 1

Function은이 문제를 해결할 수 없습니다. 그러나 그 사촌은 Program Fixpoint 수 있습니다.

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으로 계산할 수 있음을 입증 :

이

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 - 피터 함수를 정의 할 수 있습니다

이의 첫 잘 foundedness을 치료하는 몇 가지 보조 정리를 정의 할 수

을

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을 참조하십시오.

이렇게 정의하는 또 다른 방법은 두 번째 인수에 대해 구조적으로 재귀적인 두 번째 재귀 함수를 인라인하는 것입니다.

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 : 나는 긍정 전선은 내부 fixpoint으로 쓴 것입니다 정의하는 일반적인 방법.