从基于归约到无归约的规范化与识别

### 从基于归约到无归约的规范化与识别 #### 1. 规范化函数的转换 在规范化函数的转换过程中，我们首先看到了一些关键的步骤和优化。 ##### 1.1 归约压缩的推论 - **死子句**：“iterate4 (VAL v)” 子句是死子句，可以实现为抛出 “DEAD CLAUSE” 异常。 - **不变式**：所有到 iterate4 的有效转换现在都是针对 DEC (PR_OPR (v1, r, v2), C) 进行的。 ##### 1.2 重命名转换函数和扁平化配置 将简化后的机器转换为熟悉的 ‘eval/apply/continue’ 抽象机器。具体重命名如下： - refocus4_term 重命名为 eval5 - refocus4_context 重命名为 continue5 - iterate4 重命名为 apply5 同时，将配置 iterate4 (DEC (PR_OPR (v1, r, v2), C)) 扁平化为 apply5 (v1, r, v2, C)。代码如下： ```ml (* eval5 : term * context -> result *) fun eval5 (LIT n, C) = continue5 (C, INT n) | eval5 (OPR (t1, r, t2), C) = eval5 (t1, CTX_LEFT (C, r, t2)) (* continue5 : context * value -> result *) and continue5 (CTX_MT, v) = RESULT v | continue5 (CTX_LEFT (C, r, t2), v1) = eval5 (t2, CTX_RIGHT (v1, r, C)) | continue5 (CTX_RIGHT (v1, r, C), v2) = apply5 (v1, r, v2, C) (* apply5 : value * operator * value * context -> result *) and apply5 (INT n1, ADD, INT n2, C) = continue5 (C, INT (n1 + n2)) | apply5 (INT n1, SUB, INT n2, C) = continue5 (C, INT (n1 - n2)) (* normalize5 : term -> result *) fun normalize5 t = eval5 (t, CTX_MT) ``` ##### 1.3 重新函数化 抽象机器处于去函数化形式，其高阶对应形式如下： ```ml (* eval6 : term * (value -> ’a) -> ’a *) fun eval6 (LIT n, k) = k (INT n) | eval6 (OPR (t1, r, t2), k) = eval6 (t1, fn v1 => eval6 (t2, fn v2 => apply6 (v1, r, v2, k))) (* apply6 : value * operator * value * (value -> ’a) -> ’a *) and apply6 (INT n1, ADD, INT n2, k) = k (INT (n1 + n2)) | apply6 (INT n1, SUB, INT n2, k) = k (INT (n1 - n2)) (* normalize6 : term -> result *) fun normalize6 t = eval6 (t, fn v => RESULT v) ``` 得到的重新函数化程序是一个熟悉的 CPS 形式的 eval/apply 评估函数。 ##### 1.4 回到直接风格 将 CPS 形式转换为直接风格，代码如下： ```ml (* eval7 : term -> value *) fun eval7 (LIT n) = INT n | eval7 (OPR (t1, r, t2)) = apply7 (eval7 t1, r, eval7 t2) (* apply7 : value * operator * value -> value *) and apply7 (INT n1, ADD, INT n2) = INT (n1 + n2) | apply7 (INT n1, SUB, INT n2) = INT (n1 - n2) (* normalize7 : term -> result *) fun normalize7 t = RESULT (eval7 t) ``` 得到的程序是一个传统的直接风格的 eval/apply 评估函数，即通常手工编写的无归约规范化函数。 #### 2. 识别 Dyck 单词的归约语义 目标是定义一个一步归约函数来识别格式良好的括号单词（Dyck 单词），并构建相应的基于归约的识别函数。 ##### 2.1 抽象语法：项和值 - **预项**：从字符字符串解析为单词，即 ML 括号列表。 ```ml datatype parenthesis = L of int | R of int type word = parenthesis list (* smurf : string -> word option *) fun smurf s = let fun loop (~1, ps) = SOME ps | loop (i, ps) = (case String.sub (s, i) of #"(" => loop (i - 1, (L 0) :: ps) | #"[" => loop (i - 1, (L 1) :: ps) | #"{" => loop (i - 1, (L 2) :: ps) | #"}" => loop (i - 1, (R 2) :: ps) | #"]" => loop (i - 1, (R 1) :: ps) | #")" => loop (i - 1, (R 0) :: ps) | _ => NONE) in loop ((String.size s) - 1, nil) end ``` - **项**：项是一个单词。 - **值**：值是一个空单词，即空括号列表。 ##### 2.2 收缩概念 收缩概念是在上下文中移除匹配的括号对。 ```ml datatype potential_redex = PR_MATCH of int * int type contractum_or_error = bool (* contract : potential_redex -> contractum_or_error *) fun contract (PR_MATCH (l, r)) = l = ```