HOL Light 语法

C* 分三个阶段读取源文件中反引号之间的内容。词法分析器把字符流切分为词法单元，采用贪婪策略，每次匹配尽可能长的字母数字或符号词法单元。语法分析器根据一张记录中缀运算符、绑定子与前缀运算符的表，把词法单元转换为预类型或预项；理论可以在运行时扩展这张表。随后的类型检查把预类型转换为 hol_typehol_type，把预项转换为 termterm，同时解析重载常量，并通过类型推断补全隐式类型。

本页说明这三个阶段的规范，它们均继承自 HOL Light；C* 增补的常量、字面量与约定见 C* 的扩展。

词法分析器读入 ASCII 输入流，并把它切分为词法单元。它的处理方式大体遵循通行规则：在每个位置先跳过空白，再取出同一字符类中尽可能长的一段连续字符。

• 空白：空格、制表符（\t\t）、换行符（\n\n）、回车符（\r\r）。空白用于分隔词法单元，除此之外没有意义。
• 分隔符：逗号 ,, 与分号 ;;。二者各自构成一个词法单元，不会与相邻字符合并。
• 括号：( ) [ ] { }( ) [ ] { }。每个括号都单独构成一个词法单元。
• 符号字符：\ ! @ # $ % ^ & * - + | < = > / ? ~ . :\ ! @ # $ % ^ & * - + | < = > / ? ~ . :
• 字母数字字符：AA–ZZ、aa–zz、00–99、下划线 __ 与单引号 ''。
• 数字：00–99。

注意单引号 '' 属于字母数字字符，而非字符串定界符：HOL Light 没有字符字面量，'a'a 是一个普通标识符（按惯例用作类型变量）。

不属于括号、分隔符或保留字的词法单元都是标识符，分为两类：

1. 字母数字标识符是尽可能长的一段连续字母数字字符：xx、ListList、appendappend、x1x1、Is_ZeroIs_Zero、_foo_foo、__init__init。
2. 符号标识符是尽可能长的一段连续符号字符：++、==>==>、!!!!、|->|->、****。

由于采用最长匹配，相邻的符号字符会合并为一个词法单元：x**yx**y 的词法分析结果是 xx、****、yy，而 x* *yx* *y 的结果是 xx、**、**、yy。因此空白只在符号运算符之间才具有意义，别处则无关紧要。

保留字是不能用作标识符的词法单元。默认的集合为：

(  )  [  ]  {  }
:  ;  .  |
let  in  and  if  then  else
match  with  function  ->  when

(  )  [  ]  {  }
:  ;  .  |
let  in  and  if  then  else
match  with  function  ->  when

语言并未固定这个集合：理论可以添加更多保留字，HOL Light 自身的库在引入新语法时就会这样做。其余词法单元，包括下面优先级表中的各个运算符，都只是附带了语法分析状态的普通标识符。

字符串字面量是词法分析器唯一特殊处理的字面量。它们用双引号 "" 括起，并支持常见的转义：\n\n、\t\t、\"\"、\\\\，以及形如 \031\031 的十进制字符编码。字符串字面量在项的语法分析阶段展开为 char listchar list（参见 §项的形式）。

类型先被解析为预类型，再经检查并转换为逻辑类型。类型写在冒号之后，既可以作为项的类型标注（t:tyt:ty），也可以作为独立的类型引述（`:ty``:ty`）。

类型的核心抽象语法，即 HOL Light 的 hol_typehol_type，恰好有两个构造子：

• Tyvar of stringTyvar of string —— 类型变量，如 'a'a 或 AA。
• Tyapp of string * hol_type listTyapp of string * hol_type list —— 应用于一组参数的类型构造子，如 boolbool（Tyapp("bool", [])Tyapp("bool", [])）、num listnum list 或 A -> BA -> B。

下面的各种语法形式都是这两个构造子之一的语法糖。

当且仅当标识符不是已声明的类型构造子时，它才被解析为类型变量。因此，AA 是变量，boolbool 是常量；新增类型定义也就可能改变已有类型表达式的解析结果。后缀应用只接受一个参数；对于元数更高的构造子，需要将参数用逗号分隔并用括号括起，组成元组，写在构造子名字之前。有限类型 :1:1、:2:2、…… 是类型层面的数值，用作 cartcart 构造子的索引类型，以表示定长向量。

由紧到松依次为：

1. 原子类型——标识符、有限类型、带括号的类型以及元组前缀；
2. 后缀类型应用 ty conty con；
3. 笛卡尔幂 ^^，左结合；
4. 积 ##，右结合；
5. 和 ++，右结合；
6. 函数 ->->，右结合。

:(int)list -> hprop

:(int)list -> hprop

Tyapp("fun", [Tyapp("list", [Tyapp("int", [])]); Tyapp("hprop", [])])

Tyapp("fun", [Tyapp("list", [Tyapp("int", [])]); Tyapp("hprop", [])])

类型常量 hprophprop、ctypectype、struct_namestruct_name、fieldfield，以及缩写 addraddr 与 bytebyte，由 C* 而非 HOL Light 引入；参见 C* 的扩展。

项先被解析为预项，再经过类型推断与检查，转换为逻辑项。

项的核心抽象语法，即 HOL Light 的 termterm，恰好有四个构造子：

• Var of string * hol_typeVar of string * hol_type —— 变量及其类型。
• Const of string * hol_typeConst of string * hol_type —— 常量及其类型。
• Comb of term * termComb of term * term —— 一个项对另一个项的应用（组合）。
• Abs of term * termAbs of term * term —— λ-抽象，其第一个分量是一个变量。

标识符最终成为 VarVar 还是 ConstConst，由类型推断与检查阶段决定，不在词法分析阶段决定；具体取决于该名字是否为当前理论中已声明的常量。

语法分析器根据一张表解析中缀运算符，这张表会随着理论的扩充而扩展。优先级数字越大，结合力越强。没有优先级数字的行沿用上一行的层级。

还有两种形式未列入表中。函数应用的结合力强于所有中缀运算符：f x + yf x + y 即 (f x) + y(f x) + y，f x yf x y 即 (f x) y(f x) y。类型标注 t:tyt:ty 的结合力强于所有中缀运算符，但弱于应用，因此 f x:intf x:int 标注的是应用 f xf x；若只想标注参数本身，必须加括号写成 f (x:int)f (x:int)。

按结合力由紧到松排列，项可以有以下形式。

原子项。

• 变量与常量：任何未被解析为关键字、绑定子或运算符的标识符。它成为 VarVar 还是 ConstConst，在类型推断阶段确定。
• 字面量：双引号括起的字符串字面量，会转换为 char listchar list；十进制、十六进制（0x1f0x1f）或二进制（0b10110b1011）形式的数值字面量，类型为 :num:num；以及 C* 中带 ii 后缀的整数字面量（123i123i），类型为 :int:int。
• 带括号的项：( t )( t )。
• 列表字面量：[ t1; t2; ... ][ t1; t2; ... ]，是 CONSCONS 与 NILNIL 的语法糖。注意分隔符是分号；若用逗号，构造出的则是元组。
• 集合枚举：{ t1, t2, ... }{ t1, t2, ... }，是 INSERTINSERT 与 EMPTYEMPTY 的语法糖。
• 集合概括：标准形式 { x | P }{ x | P }，以及广义形式 { f x | x | P }{ f x | x | P }，后者的中间分量显式列出被绑定的变量。
• 模式匹配：match t with p -> e | ...match t with p -> e | ...，也可以带守卫，写成 match t with p when c -> e | ...match t with p when c -> e | ...。functionfunction 形式则对被匹配的项做抽象：function p -> e | ...function p -> e | ...，同样支持 whenwhen 守卫。
• 条件式：if p then t else eif p then t else e。
• let 绑定：let x = t in bodylet x = t in body、函数形式 let f x = t in bodylet f x = t in body，以及并行绑定 let x = t and y = u in bodylet x = t and y = u in body。
• 全域：(:ty)(:ty)，某个类型的全集。

其后依次是绑定子、前缀运算符、应用与中缀运算，分别见下文；中缀运算按§运算符优先级解析。

绑定子的写法为

binder v1 ... vn. body

binder v1 ... vn. body

它在主体（bodybody）中依次绑定 v1v1 到 vnvn，主体的范围尽可能向右延伸。标准的绑定子如下：

例如 \x y. x + y\x y. x + y 是柯里化的加法函数，!n. n > 0!n. n > 0 对所有 nn 做全称量化。由于主体尽可能向右延伸，!n. P n /\ Q n!n. P n /\ Q n 即 !n. (P n /\ Q n)!n. (P n /\ Q n)；若希望量词的作用域提前结束，必须加括号。 forallforall 与 existsexists 是重载记号，也用作堆量词。

有三个前缀运算符，其结合力强于所有中缀运算符，但弱于应用：

• ~~ —— 逻辑否定，如 ~(x = y)~(x = y)。
• ---- —— 整数取负，如 --1i--1i。它是前缀运算符，而非中缀的 --；x - --1ix - --1i 中的空格不可省略，否则 - --- -- 会合并为一个符号词法单元。
• modmod —— 同余的模，从不单独书写：它出现在同余式末尾的 (mod n)(mod n) 中，如 (x == y) (mod n)(x == y) (mod n)。

一些运算符是重载的：语法分析器先给出一个通用常量，类型检查器再依据类型上下文把它解析为具体的常量。作用于 :int:int 类型的项时，++ 与 -- 成为 int_addint_add 与 int_subint_sub；作用于 :num:num 时，它们成为自然数上的相应运算。同样的机制也确定了 <<、<=<=、** 等运算符的含义，并让 &&&&、||||、truetrue、falsefalse、forallforall 与 existsexists 既可以表示逻辑常量，也可以表示堆命题常量。当上下文无法确定类型时，显式的类型标注或带后缀的字面量（写 0i0i 而非 00）可以消除歧义。

变量还可以带有隐式类型：理论可以声明，除非另有说明，使用特定名字的变量都具有指定的类型。 C* 利用这一机制，让变量 hphp、hp1hp1、hp2hp2、hp3hp3、hp1'hp1'、hp2'hp2'、hp3'hp3' 无需标注就是 :hprop:hprop 类型的堆命题，hpAhpA、hpA'hpA' 则为 :A->hprop:A->hprop；证明库中的规则也使用这些名字来陈述。

• 反引号内的内容按最长匹配原则切分为词法单元，涉及三类字符：字母数字（含 __ 与 ''）、符号，以及单字符的括号与分隔符；//// 表示注释的开始，不能用作运算符。
• 完全由数字构成的词法单元、0x0x/0b0b 形式以及 123i123i 都先被词法分析为普通标识符，只有在项的语法分析阶段才成为数值字面量。
• 类型只有 TyvarTyvar 与 TyappTyapp 两种；应用是后缀形式且结合力最强，其后按结合力递减依次是 ^^（左结合），以及 ##、++、->->（均为右结合）。
• 项只有 VarVar、ConstConst、CombComb、AbsAbs 四种；应用的结合力强于所有中缀运算符，类型标注 t:tyt:ty 介于二者之间；中缀运算按优先级表解析，其中分离逻辑运算符与对应的逻辑运算符处于同一优先级。
• 绑定子的形式为 binder v1 ... vn. bodybinder v1 ... vn. body，主体尽可能向右延伸；前缀运算符是 ~~、---- 与 modmod。
• 重载运算符与带隐式类型的变量由类型推断解析，而非由语法分析器解析。