如何使用类或区域设置？

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.f在现场每个定义flanguage专门到foo_big_step和foo_typing和每一个定理thmlanguage变得专门到foo.thm。参数和语言环境中的所有常量的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的语义和类型判断常数即席与句法常数big_step和typing再次超载foo_big_step和foo_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" 

后，伊莎贝尔的解析器将通过此指foo_big_step类型找出和场景Language内，term "(x :: 'exp, E) ⇒ v"解析为区域设置参数big_step。

这应该也适用于区域设置Language的多种解释，只要类型足以唯一地解决超载问题。如果没有，你会得到错误信息，这并不总是很容易理解。