4

In Isabelle's NEWS file, I found

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.

(which dates back to Isabelle2009-2). Is this the latest news with respect to typedef and local theory contexts? Further, what does the restriction "without introducing dependencies on parameters or assumptions" actually mean?

If it would mean that I cannot use locale parameters in the defining set of a typedef, then I would not consider typedef to be localized at all (since the only allowed instances can easily be moved outside the local context, or am I missing something?).

Is it (or should it, or will it ever be) possible to do something along the lines (where the set used for a typedef depends on the locale parameter 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

for which I currently obtain:

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

2 回答 2

3

对此还有几点说明：

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

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

  • 简单typedef如上所示（及其衍生产品，如本地化codatatype和datatype最近的 HOL-BNF）可以在其依赖类型参数方面略有改进，但这意味着一些实施工作不能证明目前微薄的结果是合理的。它只允许使用如下隐式参数编写多态类型构造：

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

    导出后，您将'a list照常获得。

    进一步的并发症：fixes type 'a不存在。Isabelle/Pure 通过 Hindley-Milner 隐式处理类型参数。

于 2013-10-09T20:17:04.393 回答
2

与此同时，这个问题在 Isabelle 邮件列表中得到了解答。简短的版本是我试图做的事情根本不可能。以下是@makarius 的解释：

[不引入对参数或假设的依赖项] 意味着您不能在类型规范中引用上下文的fixes/ assumes——这在 Isabelle/Pure/HOL 中在逻辑上是不可能的。只有非空性证明存在于上下文中，并且由此产生的定理是局部的。（不过，在实践中很难实现证明对上下文逻辑内容的实际依赖。）

'typedef' 正式本地化在可能的范围内。本地化意味着以通常的方式使用本地理论基础设施和上下文。对于 typedef，这意味着额外的逻辑事物，例如名称空间、语法、派生声明等。

从历史上看，由于不可能使 typedef 依赖于上下文的逻辑部分，它根本没有本地化，直到今天许多工具实现都受此影响。

至于我的具体例子：

您必须通过对 type 的参数使用不同的名称来规避范围冲突 [...] subst。尽管如此，这从逻辑的角度来看是行不通的：对术语参数 V 的依赖不能在 HOL 中使用typedef。局部理论概念并没有提供增强逻辑的神奇方法——它只是现有逻辑框架的基础设施。

于 2013-05-17T07:49:59.940 回答