isabelle - 什么样的类型定义在本地环境中是合法的？

Question

在伊莎贝尔的NEWS文件，我发现

Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure/HOL. Note that the logical environment may contain multiple interpretations of local typedefs (with different non-emptiness proofs), even in a global theory context.

(可追溯到 Isabelle2009-2)。这是关于 typedef 的最新消息吗？和本地的理论背景？此外，“不引入对参数或假设的依赖”的限制实际上意味着什么？

如果这意味着我不能在 typedef 的定义集中使用语言环境参数，那么我不会考虑typedef完全本地化(因为唯一允许的实例可以很容易地移到本地上下文之外，或者我错过了什么？)。

是否(或者应该，或者将永远)有可能做一些事情(其中用于 typedef 的集合取决于语言环境参数 V ):

datatype ('a, 'b) "term" = Var 'b | Fun 'a "('a, 'b) term list"

locale term_algebra =
  fixes F :: "'a set"
    and V :: "'b set"
begin

definition "domain α = {x : V. α x ~= Var x}"

typedef ('a, 'b) subst =
  "{α :: 'b => ('a, 'b) term. finite (domain α)}"

end

我目前为此获得:

Locally fixed type arguments "'a", "'b" in type declaration "subst"

Answer 1

对此还有几点说明:

局部理论基础结构仅组织现有的模块概念(locale，class 等)，以便定义机制(definition，theorem，inductive，function 等)可以在各种上下文。这不会改变逻辑基础，因此不能依赖于术语参数 ( fixes ) 或前提 ( assumes ) 的规范元素不会从根本上变得更好。它们只是被 retrofit 到更大的框架中，这已经是一个额外的逻辑好处。

典型的局部理论目标是 locale及其衍生物，如 class .这些根据上面概述的原则在逻辑内工作:通过 fixes 的某些上下文进行 lambda-lifting和 assumes .其他野心更大的目标可想而知，但需要一些勇敢和英勇的家伙来实现。例如，可以结束 AWE理论解释机制作为另一个局部理论目标，然后获取类型/常量/公理的参数化——通常以通过显式证明术语在 LCF 证明者中实现可接受的推论为代价(或以放弃 LCF 为代价- ness 并通过一些神谕来做到这一点)。

平原 typedef如上所示(及其衍生产品，如最近的 HOL-BNF 的本地化 codatatype 和 datatype)可以稍微改进其依赖类型参数，但这意味着一些实现工作不能证明现在的微薄结果是合理的.它只允许使用如下隐式参数编写多态类型构造:

context fixes type 'a
begin
datatype list = Nil | Cons 'a list
end

导出后你会得到 'a list照常。

更多并发症:fixes type 'a不存在。 Isabelle/Pure 通过 Hindley-Milner 隐式处理类型参数。