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

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

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

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 ответа

Решение

Основное различие между вашим кодом и кодом 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);

может быть написано (в псевдо-Coq) как

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 делает.

Источник

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

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

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

Источник 
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.

см.: coq art's 2004. P167-P168. (Как понять "позитивный" тип в Coq)

Источник
Другие вопросы по тегам