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

Question

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

typedecl channel

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

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

现在我想打字 channel 。 channel type 应该具有它可以作为参数传输的值的类型:

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 做了类似的事情, Isabelle 的领域理论库。

有了这样的编码，您就可以使用无类型 channel 构造进程的数据类型，然后根据需要使用编码和解码函数创建数据类型的类型安全 View 。