Ich habe den Kurs "Logische Grundlagen" bestanden und bin bei der letzten Übung der Grundlagen festgefahren:

Wenn eine Binärzahl einen Konverter in seine unäre Darstellung schreibt:

Inductive bin : Type :=
  | Z
  | A (n : bin)
  | B (n : bin).

Fixpoint bin_to_nat (m:bin) : nat :=
  (* What to do here? *)

Ich habe das Problem mit einer rekursiven Funktion in C gelöst. Das einzige, was ich verwendet habe, ist "0" anstelle von "A" und "1" anstelle von "B".

#include <stdio.h>

unsigned int pow2(unsigned int power)
{
    if(power != 0)
        return 2 << (power - 1);
    else
        return 1;
}

void rec_converter(char str[], size_t i)
{
    if(str[i] == 'Z')
        printf("%c", 'Z');
    else if(str[i] == '0')
        rec_converter(str, ++i);
    else if(str[i] == '1')
    {
        unsigned int n = pow2(i);

        for (size_t j = 0; j < n; j++)
        {
            printf("%c", 'S');
        }
        rec_converter(str, ++i);
    }
}

int main(void)
{
    char str[] = "11Z";

    rec_converter(str, 0);
    printf("\n");

    return 0;
}

Mein Problem ist jetzt, wie man diesen Code in coq schreibt:

unsigned int n = pow2(i);

for (size_t j = 0; j < n; j++)
{
    printf("%c", 'S');
}
rec_converter(str, ++i);
2
user4035 20 Jän. 2019 im 00:02

3 Antworten

Beste Antwort

Der Hauptunterschied zwischen Ihrem Code und dem Coq-Code besteht darin, dass der Coq-Code die natürliche Zahl zurückgeben sollte, anstatt sie zu drucken. Das heißt, wir müssen den Überblick über alles behalten, was Ihre Lösung gedruckt hat, und das Ergebnis auf einmal zurückgeben.

Da das Drucken eines S bedeutet, dass die Antwort der Nachfolger von allem ist, was sonst gedruckt wird, benötigen wir eine Funktion, die den 2 ^ (n) -ten Nachfolger einer natürlichen Zahl annehmen kann. Es gibt verschiedene Möglichkeiten, dies zu tun, aber ich würde eine Rekursion auf n vorschlagen und feststellen, dass der 2 ^ (n + 1) -te Nachfolger von x der 2 ^ (n) -te Nachfolger des 2 ^ (n) -ten Nachfolgers von x ist x.

Das sollte ausreichen, um das zu bekommen, was Sie wollen.

unsigned int n = pow2(i);

for (size_t j = 0; j < n; j++)
{
    printf("%c", 'S');
}
rec_converter(str, ++i);

Kann geschrieben werden (in Pseudo-Coq) als

pow2_succ i (rec_converter str (S i)).

Beachten Sie jedoch Folgendes: Möglicherweise können Sie nicht direkt auf das i-te "Zeichen" der Eingabe zugreifen, dies sollte jedoch kein Problem darstellen. Wenn Sie Ihre Funktion als Fixpoint schreiben

Fixpoint rec_converter (n: bin) (i: nat): nat :=
match n with
| Z => 0
| A m => ...
| B m => ...
end.

Das erste "Zeichen" von m ist das zweite "Zeichen" der ursprünglichen Eingabe. Sie müssen also nur auf das erste "Zeichen" zugreifen, genau das, was ein Fixpoint tut.

4
SCappella 24 Jän. 2019 im 02:56

Bei der Frage zu Rechenleistungen von 2 sollten Sie sich die folgende Datei ansehen, die in den Coq-Bibliotheken bereitgestellt wird (mindestens bis Version 8.9):

https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Nat.html

Diese Datei enthält eine Vielzahl von Funktionen rund um die natürlichen Zahlen. Sie können alle als Illustrationen zum Programmieren mit Coq und diesem Datentyp verwendet werden.

2
Yves 24 Jän. 2019 im 09:11
Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | Z => O
  | A n =>2 * (bin_to_nat n)
  | B n =>2 * (bin_to_nat n) + 1
  end.

Siehe: coq art's 2004. P167-P168. (Wie man 'positiven' Typ in Coq versteht)

0
user13130175 26 März 2020 im 16:27