内核如何在LCF定理箴言中工作

Question

我听说基于LCF的定理传记中存在一些机制，只允许一些功能来创建类型定理的值。我相信这些是基于抽象数据类型。

有人可以在伪代码中绘制这项工作吗？（如果上述正确是正确的）

Answer 1

此处是来自isabelle的内核（Isabelle / pure中的文件Thm.ml）的一些想法和代码：

abstype thm = Thm of
 deriv *                        (*derivation*)
 {cert: Context.certificate,    (*background theory certificate*)
  tags: Properties.T,           (*additional annotations/comments*)
  maxidx: int,                  (*maximum index of any Var or TVar*)
  shyps: sort Ord_List.T,       (*sort hypotheses*)
  hyps: term Ord_List.T,        (*hypotheses*)
  tpairs: (term * term) list,   (*flex-flex pairs*)
  prop: term}                   (*conclusion*)
and deriv = Deriv of
 {promises: (serial * thm future) Ord_List.T,
  body: Proofterm.proof_body}
with

.

此处是ML上的Paulson Book的报价。关于抽象数据类型，他说：

模块化结构使程序更易于理解。更好， 模块应该作为可互换的部件：用一个模块替换一个模块 改进的版本不应要求更改其余部分。程序。标准 ML的抽象类型和仿函数可以帮助我们达到这个目标。 模块可以揭示其内部细节。当模块被替换时，其他 依赖此类细节的部分部分将失败。 ML提供了几个 宣布抽象类型和相关操作的方式，同时隐藏类型 表示。

因此您无法实例化您可以使用它的抽象数据类型（其字段+函数）。如何实现如何实现此功能的依赖性。如果你想在Lambda微积分中做到这一点，那么在Benjamin Pierce的Tapl在后来的章节上就应该有类似的东西。

这是一个很好的参考，也是这里

Answer 2

如果我回忆起来，这是John Harrison的实际逻辑手册和自动推理的手册。

jon sterling写了一些 notes 用于叙述每年或两次背部，特别是使用序列微积分的LCF证据。