Ошибка в определении Ackermann в Coq

Question

Я пытаюсь определить функцию Ackermann-Peters в Coq, и я получаю сообщение об ошибке, которое я не понимаю. Как вы можете видеть, я собираю аргументы a, b Ackermann в паре ab; Я предоставляю упорядочение, определяющее функцию упорядочения для аргументов. Затем я использую форму Function для определения самого Аккермана, предоставляя ему функцию упорядочения для аргумента 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 .

Я не уверен, что беспокоит Coq, но поиск в интернете, я нашел предложение может быть проблема с использованием рекурсивного функция, определенная с помощью порядка или меры, где рекурсивный вызов встречается в пределах совпадения. Однако с использованием прогнозов fst и snd и if-then-else сгенерировано другое сообщение об ошибке. Может кто-нибудь предложить, как определить Ackermann в Coq?

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. 

Теперь мы можем определить функцию Аккермана-Петера:

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 s (т. Е. Рекурсивные функции), но проблема, как вы, наверное, знаете, заключается в том, что функция Аккермана не является примитивной рекурсивной функцией.

См. 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 является проблемой, но я не знаю, Зачем.

Надеется, что это помогает немного, В.

PS: Обычный способу я определяю Ack что писали провода с внутренней фиксированной точкой.