如何使用类或语言环境？

Question

我正在尝试为编程语言定义通用操作：

type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"

locale language =
  fixes big_step :: "'exp × 'val env ⇒ 'val ⇒ bool" (infix "⇒" 55)
  fixes typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50)

例如这是一种特定的语言：

datatype foo_exp =
  FooBConst bool |
  FooLet vname foo_exp foo_exp |
  FooVar vname |
  FooAnd foo_exp foo_exp

datatype foo_val = FooBValue bool | FooIValue int
type_synonym foo_env = "foo_val env"
datatype foo_type = FooBType | FooIType
type_synonym foo_tenv = "foo_type env"

inductive foo_big_step :: "foo_exp × foo_env ⇒ foo_val ⇒ bool"
inductive foo_typing :: "foo_tenv ⇒ foo_exp ⇒ foo_type ⇒ bool"

如何使其成为 language 语言环境的实例？

是否可以在一种理论中对不同的语言使用相同的符号（⇒ 和 _ ⊢ _ : _）？这个符号可以是多态的吗？

Answer 1

要专门化语言环境的参数，您需要像

那样进行解释

interpretation foo: language foo_big_step foo_typing .

这将为专门用于 foo_big_step 和 foo_typing 的语言环境 f 中的每个定义 f 以及每个定理 [=19] 生成一个缩写 foo.f =] 的 language 专门用于 foo.thm。 locale中参数和所有常量的mixfix语法注解不会被继承

类型类不能在此上下文中使用，因为您的语言环境取决于多个类型变量，而 Isabelle 中的类型类仅支持一种类型变量。

如果您想对大步语义和类型判断使用某种多态表示法，Adhoc_Overloading 可能会起作用，前提是 Isabelle 的解析器可以静态地唯一地解析重载。这可能是这样工作的：

 theory Language imports Main "~~/src/Tools/Adhoc_Overloading" begin

 type_synonym 'a env = "vname ⇒ 'a option"

 consts
   big_step :: "'exp × 'val env ⇒ 'val ⇒ bool" (infix "⇒" 55)
   typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50)

  locale language = 
    fixes big_step :: "'exp × 'val env ⇒ 'val ⇒ bool"
    fixes typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool"
  begin

  adhoc_overloading Language.big_step big_step
  adhoc_overloading Language.typing typing

  end

解释完成后，需要注册foo的语义和类型判断常量foo_big_step和foo_typing，用句法常量big_step和typing 再一次。

interpretation foo: language foo_big_step foo_typing .
adhoc_overloading Language.big_step foo_big_step
adhoc_overloading Language.typing foo_typing

所以当你写

term "(x :: foo_exp, E) ⇒ v"

此后，Isabelle 的解析器将根据 this 引用的类型找出 foo_big_step，并在语言环境 Language 内，将 term "(x :: 'exp, E) ⇒ v" 解析为语言环境参数 big_step.

只要类型足以唯一地解析重载，这也适用于语言环境的多种解释 Language。否则，您会收到错误消息，这些消息并不总是容易理解。

如何使用类或语言环境？

How to use classes or locales?

isabelle

如何使用 类 或语言环境？

How to use classes or locales?

isabelle

如何使用类或语言环境？