如何在Isabelle/HOL中伪造存在类型？

Question

考虑以下简单过程语言的Isabelle/HOL定义：

typedecl channel

datatype process = Put channel char process | Get "char ⇒ process" | Stop

该语言支持通过通道发送和接收字符。

现在，我想要输入通道。channel类型应该具有它可以作为参数传输的值的类型：

typedecl 'a channel

Put和Get数据构造函数应具有以下(多态)类型：

Put :: "['a channel, 'a, process] ⇒ process"
Get :: "['a channel, 'a ⇒ process] ⇒ process"

然而，这需要支持数据类型中的存在量化，而这是Isabelle/HOL所没有的。

我试图伪造存在量词，并提出了以下尝试：

typedecl put
axiomatization put :: "['a channel, 'a] ⇒ put" where
  put_inject: "put a x = put b y ⟷ a = b ∧ x = y"

bnf_axiomatization 'r get
axiomatization get :: "['a channel, 'a ⇒ 'r] ⇒ 'r get" where
  get_inject: "get a f = get b g ⟷ a = b ∧ f = g"

datatype process = Put put process | Get "process get" | Stop

不幸的是，这将导致以下错误消息：

Type definition with open dependencies, use "typedef (overloaded)" or enable configuration option "typedef_overloaded" in the context.
  Type:  process
  Deps:
  map_get(process.process_IITN_process
          ⇒ (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool,
           (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool),
  bd_get,
  set_get(process.process_IITN_process
          ⇒ (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool)
The error(s) above occurred in typedef "process"

我的尝试是否合理，如果是，我如何解决这个问题？有没有更好的解决方案？

Answer 1

实际上，get的公理与bnf_axiomatization不一致。但是，如果您将自己限制为可计数类型'a，则这种类型是存在的。一旦你确定了这样一个基数界限，你甚至不需要恢复到公理化。然后，可以在HOL中使用编码和解码功能在通用域中模拟存在类型。

例如，对于可数类型，自然数可以用作通用域。这已经被使用了，例如，在Imperative_HOL中建模可以存储类型值的堆，参见the paper from 2008。赫夫曼为伊莎贝尔的领域理论库HOLCF做了类似的事情。

有了这样的编码，您可以使用无类型通道构造进程的数据类型，然后根据需要使用编码和解码函数在数据类型上创建类型安全视图。