2

我正在通过逻辑基础课程并被困在基础知识的最后一个练习中：

让二进制数将转换器写入它的一元表示：

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);
4

3 回答 3

4

您的代码和 Coq 代码之间的主要区别在于 Coq 代码应该返回自然数，而不是打印它。这意味着我们需要跟踪您的解决方案打印的所有内容并立即返回所有结果。

由于打印 anS意味着答案是打印的任何其他内容的后继，因此我们需要一个可以获取自然数的第 2^(n) 个后继的函数。有多种方法可以做到这一点，但我建议对 n 进行递归，并注意 x 的第 2^(n + 1) 个后继者是第 2^(n) 个后继者的第 2^(n) 个后继X。

这应该足以得到你想要的。

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 的第一个“字符”将是原始输入的第二个“字符”。所以你只需要访问第一个“字符”，这正是 aFixpoint所做的。

于 2019-01-20T01:45:53.230 回答
2

关于计算能力 2 的问题，您应该查看 Coq 库中提供的以下文件（至少到 8.9 版）：

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

该文件包含许多围绕自然数的函数，它们都可以用作说明如何使用 Coq 和这种数据类型进行编程的说明。

于 2019-01-24T09:11:40.103 回答
0 
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 的 2004。P167-P168。（如何理解 Coq 中的“积极”类型）

于 2020-03-26T16:27:35.377 回答