Próbuję zdefiniować funkcję Ackermanna-Petersa w Coq i otrzymuję komunikat o błędzie, którego nie rozumiem. Jak widać, pakuję argumentya, b Ackermanna w parzeab; Zapewniam porządek definiujący funkcję porządkowania argumentów. Następnie używamFunction formularz do zdefiniowania samego Ackermanna, udostępniając mu funkcję zamawianiaab argument.

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

Otrzymuję następujący komunikat o błędzie:

Błąd: brak takiej zmiennej sekcji lub założenia:ack.

Nie jestem pewien, co przeszkadza Coq, ale przeszukiwanie Internetu, znalazłem sugestię, że może istnieć problem z użyciem funkcji rekurencyjnej zdefiniowanej za pomocą porządku lub miary, gdzie wywołanie rekurencyjne występuje w dopasowaniu. Jednak używając projekcjifst isnd i anif-then-else wygenerował inny komunikat o błędzie. Czy ktoś może zasugerować, jak zdefiniować Ackermanna w Coq?