Основы coq: функция bin_to_nat - PullRequest
Новая
       75

Основы coq: функция bin_to_nat

0 голосов
/ 20 января 2019

Я прохожу курс «Основы логики» и застрял на последнем упражнении с Основами:

Имея двоичное число записать преобразователь в его унарное представление: 

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

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

Я решил проблему с рекурсивной функцией в C. Единственное, я использовал «0» вместо «A» и «1» вместо «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;
}

Моя проблема сейчас заключается в том, как написать этот код в coq: 

unsigned int n = pow2(i);

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

Ответы [ 2 ]

0 голосов
/ 24 января 2019

Для вопроса о вычислительных мощностях 2, вы должны посмотреть на следующий файл, предоставленный в библиотеках Coq (по крайней мере, до версии 8.9):

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

Этот файл содержит множество функций вокруг натуральных чисел, все они могут быть использованы в качестве иллюстрации о том, как программировать с помощью Coq и этого типа данных.

0 голосов
/ 20 января 2019

Основное различие между вашим кодом и кодом Coq состоит в том, что код Coq должен возвращать натуральное число, а не печатать его. Это означает, что нам нужно отслеживать все, что печатает ваше решение, и возвращать результат сразу.

Поскольку печать S означает, что ответ является преемником того, что еще напечатано, нам понадобится функция, которая может взять 2 ^ (n) -й преемник натурального числа. Существуют различные способы сделать это, но я бы предложил рекурсию по n и отметить, что 2 ^ (n + 1) -й преемник x является 2 ^ (n) -ым преемником 2 ^ (n) -го преемника х.

Этого должно быть достаточно, чтобы получить то, что вы хотите. 

unsigned int n = pow2(i);

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

можно записать (в псевдококке) как 

pow2_succ i (rec_converter str (S i)).

Однако следует отметить еще одну вещь: вы не сможете напрямую получить доступ к i-му «символу» ввода, но это не должно быть проблемой. Когда вы пишете свою функцию как Fixpoint

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

первый «символ» m будет вторым «символом» исходного ввода. Так что вам просто нужно получить доступ к первому «персонажу», что и делает Fixpoint.

...