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

Я пытаюсь определить функцию Акерманна-Петерса в 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?


coq totality ackermann
person Mayer Goldberg    schedule 24.04.2012    source источник
comment
Сегодня я столкнулся с той же проблемой. Вы нашли решение?   -  person Abhishek Anand    schedule 27.06.2013
comment
@AbhishekAnand Прошло какое-то время ... Я предоставил решение с Program Fixpoint ниже. Вы нашли решение с Function?   -  person Anton Trunov    schedule 30.06.2017
comment
Нет, не знал. Спасибо за Ваш ответ.   -  person Abhishek Anand    schedule 01.07.2017

Ответы (3)


arrow_upward
8
arrow_downward

Кажется, что 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 М. Созо и К. Манжена, можно определить эту функцию способ:

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 < / а>.

person Anton Trunov    schedule 29.06.2017

arrow_upward
3
arrow_downward

Вы получаете эту ошибку, потому что вы ссылаетесь на функцию ack при ее определении. Самостоятельная ссылка разрешена только в Fixpoints (т.е. рекурсивных функциях), но проблема, как вы, вероятно, знаете, что функция Аккермана не является примитивной рекурсивной функцией.

Дополнительную информацию см. В разделе 4.3.2.2 Coq'Art.

Таким образом, один альтернативный способ определить это - встраивать вторую рекурсивную функцию, которая структурно рекурсивна для второго аргумента; так что-то вроде

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.
person wires    schedule 24.04.2012
comment
Я не использовал Fixpoint, а Function. Это должно работать с полными функциями, которые имеют убывающий аргумент, и я должен иметь возможность сделать это, используя либо меру, либо сравнение, за которым следует теорема о том, что аргументы в рекурсивных вызовах либо имеют меньшую меру, либо меньше исходной аргументы в соответствии с компаратором. Я знаю, что Аккерманн - это PR 2-го порядка, но очевидно, что PR-статус функции не помешал вам каким-то образом его кодировать. Что меня интересует, так это то, что не так с кодировкой, которую я дал, которая, кажется, соответствует описанию в руководстве. - person Mayer Goldberg; 24.04.2012

arrow_upward
1
arrow_downward

Я только что попробовал вашу функцию с Coq 8.4, и ошибка немного отличается:

Error: Nested recursive function are not allowed with Function

Я предполагаю, что проблема заключается во внутреннем вызове подтверждения, но я не знаю почему.

Надеюсь, это немного поможет, В.

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

person Vinz    schedule 21.05.2012