Kontroli

Kontroli（世界语中“verify”的词）是 Dedukti 逻辑框架的另一种实现，专注于证明的验证。

Kontroli 的用例是验证由自动化推理工具（如证明辅助工具和自动定理证明器）生成的证明。它通过提供“第二意见”来验证 Dedukti 的输出，并使用户更容易理解和从实现中学习。它也是一个并行化类型检查的测试平台。

用法

Kontroli 至少需要 Rust 1.64。安装说明可在 https://rustup.rs/ 获取。

在 Isabelle/Pure 生成的输出上运行 Kontroli

cargo run --release examples/pure.dk

命令行选项 -j 启用并发检查，-c 启用并发解析。

安装 Kontroli

cargo install --path kocheck

Kontroli 提供了一个命令行程序 kocheck 和一个库。这意味着您可以将 Kontroli 用作您自己的应用程序的一部分。鉴于 Kontroli 库不依赖于 Rust 的标准库，您还可以在网页等环境中使用它，提供类型检查作为服务。

目标

Kontroli 力求成为以下内容

• 小巧：尽可能少写代码 ...
• 正确：... 因为你没有写的代码中不包含错误
• 高效：至少在主要用例中与 Dedukti 一样快
• 兼容：尽可能遵守 Dedukti 的语法/语义
• 保守：使用经过验证和充分测试的技术

差异

与 Dedukti 相比，有几个不同之处

• Kontroli 具有模块系统，允许嵌套模块。
• Kontroli 不支持高阶重写规则，因为这会使整个程序变得更加复杂，从而与小型类型检查器的理念相矛盾。
• Kontroli 仅在所有自由模式变量都有类型注解的情况下，才确保重写规则的类型安全性。
• Kontroli 不使用决策树进行重写。
• Kontroli 没有任何像 #EVAL 或 #ASSERT 这样的命令，这些命令在 Dedukti 测试中特别有用。相反，代码库中的测试更受欢迎。

语法

Kontroli 实现了 Dedukti 语法的子集。语法示例可以在 examples/nat.dk 或 examples/pure.dk 中看到。

Kontroli 规定，在具有子项 (t) 的项中，t 必须本身是有效的项。这排除了一种 Dedukti 允许的语法形式，即 (a: A) -> b，因为 a: A 本身不是一个合适的项。然而，这样的项可以等价地写成 a: A -> b。

开发

一些用于开发 Kontroli 的有用命令

• 生成文档：cargo doc --open
• 运行测试：cargo test
• 运行基准测试：cargo bench -p kontroli -- --sample-size 10