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

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

有帮助吗?

解决方案

此处是来自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在后来的章节上就应该有类似的东西。

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

其他提示

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

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

许可以下: CC-BY-SA归因
不隶属于 cs.stackexchange
scroll top