Ich versuche, die Ackermann-Peters-Funktion in Coq zu definieren, und ich bekomme eine Fehlermeldung, die ich nicht verstehe. Wie Sie sehen können, verpacke ich die Argumente a, b von Ackermann in ein Paar ab ; Ich stelle eine Ordnung bereit, die eine Ordnungsfunktion für die Argumente definiert. Dann benutze ich das Formular Function , um Ackermann selbst zu definieren und es mit der Sortierfunktion für das Argument ab zu versehen.
Was ich bekomme, ist die folgende Fehlermeldung:
Fehler: Keine solche Abschnittsvariable oder -annahme:
ack.
Ich bin nicht sicher, was Coq stört, aber als ich im Internet suchte, fand ich einen Vorschlag, dass es ein Problem mit der Verwendung einer rekursiven Funktion gibt, die mit einer Ordnung oder einem Maß definiert ist, wobei der rekursive Aufruf innerhalb einer Übereinstimmung erfolgt. Bei Verwendung der Projektionen fst und snd und if-then-else wurde jedoch eine andere Fehlermeldung generiert. Kann jemand bitte vorschlagen, wie man Ackermann in Coq definiert?
Es scheint, als ob Function dieses Problem nicht lösen kann. Allerdings kann sein Cousin Program Fixpoint .
Lassen Sie uns zuerst einige Lemmas definieren, die die Begründetheit behandeln:
%Vor%Jetzt können wir die Ackermann-Péter-Funktion definieren:
%Vor% Einige einfache Tests, die zeigen, dass wir mit ack :
Sie erhalten diesen Fehler, weil Sie auf die Funktion ack verweisen, während Sie sie definieren. Selbstreferenz ist nur in Fixpoint s erlaubt (dh rekursive Funktionen), aber das Problem ist, wie Sie wahrscheinlich wissen, dass die Ackermann-Funktion keine primitive rekursive Funktion ist.
Siehe Coq'Art Abschnitt 4.3.2.2 für weitere Informationen hierzu.
Eine andere Möglichkeit, sie zu definieren, besteht darin, eine zweite rekursive Funktion einzufügen, die für das zweite Argument strukturell rekursiv ist; so etwas wie
%Vor%Ich habe gerade Ihre Funktion mit Coq 8.4 versucht, und der Fehler ist etwas anders:
%Vor%Ich schätze, der innere Ruf nach ack ist das Problem, aber ich weiß nicht warum.
Hoffe das hilft ein bisschen, V.
PS: Die übliche Art, wie ich Ack definiere, ist, was Drähte mit einem inneren Fixpunkt geschrieben haben.