Error al definir Ackermann en Coq

Question

Estoy intentando definir la función de Ackermann-Peters en Coq, y aparece un mensaje de error que no entiendo. Como puede ver, estoy empaquetando los argumentos a, b de Ackermann en un par ab; Proporciono un orden que define una función de orden para los argumentos. Luego utilizo el formulario Function para definir Ackermann en sí, proporcionándole la función de ordenar para el argumento 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. 

Lo que se ve es el siguiente mensaje de error:

Error: No such section variable or assumption: ack .

No estoy seguro de lo que molesta Coq, pero buscando en internet, me encontré con una sugerencia que puede haber un problema con el uso de un recursivo función definida con un orden o una medida, donde la llamada recursiva ocurre dentro de una coincidencia. Sin embargo, al usar las proyecciones fst y snd y if-then-else, se generó un mensaje de error diferente. ¿Puede alguien sugerir cómo definir a Ackermann en Coq?

Answer 1

Parece que Function no puede resolver este problema. Sin embargo, su primo Program Fixpoint puede.

Vamos a definir algunos lemas que tratan bien fundado primero:

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. 

Ahora podemos definir la función de Ackermann-Peter:

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. 

algunas pruebas sencillas que demuestra que podemos calcular con ack:

Example test1 : ack (1, 2) = 4 := eq_refl. 
Example test2 : ack (3, 4) = 125 := eq_refl. (* this may take several seconds *) 

Answer 2

Recibirá este error porque se está refiriendo a la función ack mientras la está definiendo. La autoreferencia solo está permitida en Fixpoint s (es decir, funciones recursivas), pero el problema es, como probablemente sepa, que la función de Ackermann no es una función recursiva primitiva.

Consulte Coq'Art section 4.3.2.2 para obtener más información sobre esto.

De modo que una forma alternativa de definirlo es alinear una segunda función recursiva que es estructuralmente recursiva para el segundo argumento; así que algo como

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

que acaba de intentar su función con Coq 8,4, y el error es ligeramente diferente:

Error: Nested recursive function are not allowed with Function 

supongo que la llamada interior a ACK es el problema, pero no sé por qué.

Espero que esto ayude un poco, V.

PS: La forma habitual defino Ack es lo que escribieron los cables, con un punto fijo interior.