coq 基础：bin_to_nat 函数

Question

我正在通过逻辑基础课程，但在基础的最后一个练习题上卡住了：

将二进制数写入其一元表示形式的转换器：

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

Answer 1

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

由于打印 S 意味着答案是打印的任何其他内容的后继，我们需要一个函数来获取自然数的第 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 个 "character"，但这应该不是问题。当您将函数编写为 Fixpoint

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

m 的第一个 "character" 将是原始输入的第二个 "character"。所以你只需要访问第一个 "character"，这正是 Fixpoint 所做的。

Answer 2

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

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

此文件包含大量与自然数相关的函数，它们都可以用作说明如何使用 Coq 和此数据类型进行编程。

Answer 3

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。（如何理解 'positive' Coq 中的类型）

coq 基础：bin_to_nat 函数

coq Basics: bin_to_nat function

coq

logical-foundations