0x00 Preface
我们如果想要使用抽象机来进行程序分析，我们之前提到的CC Machine显然是不够的，虽然这已经能反映一部分语言的语义模型，我们来简单的回顾一下CC Machine(这里我直接用了简化版本的rule )。
SCC Machine
之前都是code这里简单说明一下这里的几个符号 [] 代表程序中的洞，即当前程序控制字（或者说redex）的占位符, E[ some ]， 代表将E中的洞使用some来填入.
这个模型有个显而易见的问题我们虽然说是模拟了栈的结构，或者说是函数式编程中continuation，看规则2规则3, 我们希望对程序中的洞进行操作，比如取出或者是填入的操作但是，有个问题：我们不知道洞在哪里！
如果我们的目标语言是最简单的lambda演算,那么我们可以分别对一个S表达式的左侧和右侧都去搜索一下看看洞是不是在里面，在我们成功定位了洞之后就可以进行对应的语义分析了。
0x01 CK Machine
为了解决上面的问题我们可以通过洞对函数作用位置和洞在参数位置打上不一样的标记来解决。这里让我们把continuation的部分记作K：
taged continuation
这里mt代表只剩下一个洞了，fn tag代表洞在函数作用的位置， ar tag代表洞在参数的位置
ok, 然后我们refine之前的SCC Machine就可以得到新的模型：CK Machine
ck machine
这样一来其实填洞的操作就变得容易多了，我们只需要模式匹配我们之前定义的k这个数据结构就可以了，如果有类型语言自然是定义类型模式匹配没啥好说的，我个人比较喜欢用racket, 也差不多，用 quasi pattern 可以轻松的解决
(define (step-ck ς)
(match ς
[`((,(? cexp? em) ,(? cexp? en)) ,(? kont? k))
`(,em (arg ,en ,k))]
;; if fun is evaled, switch redex to argument
[`(,(? aexp? v) (arg ,en ,k))
`(,en (fun ,v ,k))]
;; arg and fun are both evaled, perform application
[`(,(? aexp? v) (fun (λ (,x) ,em) ,k))
`(,(subst em x v) ,k)]
[else
(displayln "reach end")
#f]
))
0x02 CEK Machine
CK Machine本质上来说还是为了让我们在写rule的时候更加简单，本质还是一个基于文本替换(textual repalcement)的一种模型，现实中的编程语言许多都不是通过这种文本替换的方式来进行语义分析的。现实中的大多数语言我们都希望我们变量都是一个指向堆栈上内存空间的一个指针。顺着这个思路我们可以修改我们的CK Machine,首先我们需要引入一个新的对象到我们的状态数据结构上，我们用这个新加入的环境（env）来模拟堆。这里假设在我们当前解析的语言中，所有的变量都在堆上。 此时我们的状态可以描述为一个三元组：
同时在这里我们可以refine我们的值语义来达到延迟替换的效果。 或者说真正定义我们的值语义，因为在纯的文本计算中我们是没有像我们在大多数语言中遇到的一样的值的。为了保证我们的值是定义良好的， 我们不希望我们的表达式中出现自由变量，换句话说，我们的符号要不是被 captured，就是在env对应了一个值。使用一个开放表达式(open term)加上一个环境的闭包就可以很好的满足我们的需求。
state definition
NOTE：一般的使用希腊字符来表示env
状态转移的过程其实和CK machine没有什么太大的区别，只是原来的直接替换变成了更新环境,这里为了看起来更加清楚我直接把闭包的定义展开了。这样就是标准三元组的状态转移。
cek machine
Ref
class note of Kris Micinski
2017 class note of UMD's CMCS430
Abstracting Abstract Machine
我的实现代码
https://github.com/StarGazerM/my-foolish-code/blob/master/pla/cek.rkt
网友评论