Ошибка в определении Аккермана в Coq
Я пытаюсь определить функцию Ackermann-Peters в Coq, и я получаю сообщение об ошибке, которое я не понимаю. Как видите, я собираю аргументы a, b
Аккермана в паре 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.
Я получаю следующее сообщение об ошибке:
Ошибка: нет такой переменной раздела или допущение:
ack
,
Я не уверен, что беспокоит Coq, но, просматривая Интернет, я обнаружил предположение, что может быть проблема с использованием рекурсивной функции, определенной с помощью порядка или меры, когда рекурсивный вызов происходит внутри совпадения. Однако, используя прогнозы fst
а также snd
и if-then-else
генерируется другое сообщение об ошибке. Может кто-нибудь подсказать, как определить Аккермана в Coq?
3 ответа
Это похоже на 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 *)
Используя плагин Equations от M. Sozeau и C. Mangin, можно определить функцию следующим образом:
From Equations Require Import Equations Subterm.
Equations ack (p : nat * nat) : nat :=
ack p by rec p (lexprod _ _ lt lt) :=
ack (pair 0 n) := n + 1;
ack (pair (S m) 0) := ack (m, 1);
ack (pair (S m) (S n)) := ack (m, ack (S m, n)).
К сожалению, невозможно использовать ( , )
обозначение для пар из-за проблемы № 81. Код взят из набора тестов Equation: ack.v.
Вы получаете эту ошибку, потому что вы ссылаетесь на ack
функционировать, пока вы его определяете. Самостоятельная ссылка разрешена только в Fixpoint
s (т.е. рекурсивные функции), но проблема, как вы, наверное, знаете, в том, что функция Аккермана не является примитивной рекурсивной функцией.
Смотрите Coq'Art раздел 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.
Я только что попробовал вашу функцию с Coq 8.4, и ошибка немного отличается:
Error: Nested recursive function are not allowed with Function
Я предполагаю, что внутренний вызов ack - проблема, но я не знаю почему.
Надеюсь, это немного поможет, В.
PS: Обычный способ, которым я определяю Ack - это то, что написали провода, с внутренней точкой фиксации.