Preface
这是我关于program language semantic学习的一些笔记和实现。本文将以丘奇编码化的lambda calculis 为toy例子, 讨论一个简单的CC Machine 模型的抽象解析器的在racket语言实现。此外，这里的实现将采用谓词式的声明定义风格而非类型系统.
丘奇编码(church encoding)的话我写了一个比较简陋的
core scheme丘奇编码器
why we need abstract interepetor?
抽象的虚拟机可以作为我们进行语义分析的一种cook book, 并且是一种比较好的进行程序静态分析的起始点来帮助我们抽象程序的执行(编译)过程，
what is not here?
暂时我们不会讨论抽象解析器相关的证明过程， 这个我会放在proof的笔记中。估计是没时间了。。。
0x00 表达式规则
在定义抽象解析器之前先我们定义下我们的抽象机能够接受什么样子的输入吧
aexp(atomic expression)即程序中不能够拆分的最基本的表达式， 我们可以用它来表示值。
(define (aexp? e)
(match e
[(? symbol?) #t]
[`(λ (,(? symbol?)) ,body) #t]
[else #f]))
因为我们的程序已经被丘奇编码，所以所有的东西应该都已经被编码为了变量或者闭包.
此外我们还需要处理函数作用的compound expression情况，根据lambda演算的性质这种情况显然还没有到达normal form, 我们可以在上面不断的作用求值规则来最后归约到值。
(define (cexp? e)
(match e
[(? aexp?) #t]
[`(,(? cexp? f) ,(? cexp?)) #t]
[else #f]
))
这里我把值类型也归到了复合表达式里面，主要是为了后面在写步进规则的时候能够避免处理过多的派生规则。
0x01 在一切开始之前。。。。。
由于cc machine 还是一个基于文本替换而不是真正的使用值的模型，我们其实只是规定了值的形式（其实是只规定了不能再拆分的原子表达式），所以我们自然需要文本替换的规则
(define (subst e x t)
(match e
;; var
[(? symbol? y) (if (equal? x y) t y)]
;; fun
[`(λ (,(? symbol? y)) ,body)
(if (equal? x y)
e
`(λ (,y) ,(subst body x t)))]
;; app
[`(,(? cexp? e1) ,(? cexp? e2))
`(,(subst e1 x t) ,(subst e2 x t))]))
0x02 定义CC Machine
ok 准备工作已经完成了， 简单的介绍一下什么是CC Machine 。
首先，总的来说 CC Machine 是一个状态机， 它的状态由一个二元组<M, E>来表示， 其中M代表控制字符串，E代表当前程序上下文。从我个人的理解来说， 这里的控制字符串其实说的就是一个redex， 而这里的context其实就是一个带洞的抽象栈结构。 所以CC machine 其实是一种context-redex语义的模型。而我们状态转移的过程， 也就是我们的步进函数step其实就是在需要求值的地方加上一个洞， 之后在求值完成之后把洞重新填满再求值的这么一个过程。比如说如下的规则
<(M N), E> --> <M, E[(HOLE N)>
其中M 是一个作用再N上的复合表达式， 我们的步进函数就把当前的M设置成当前的redex 而我们在栈上增加上一个带洞的表达式以便于我们完成对M的求值之后重新填回。
是一个典型的small step 语义。
具体的状态转移规则直接看code吧， racket还是比较ad hoc的
;; fill in the hole of e1 with e2
(define (fill e1 e2)
;; there should be only one hole, although the efficiency is low here
(match e1
['HOLE
e2]
[`(,l ,r)
`(,(fill l e2) ,(fill r e2))]
[else e1]))
;; small step state transition
;; greek aplhabet varsigma is usually used as "state"
(define (step-cc ς)
(match ς
;; if both value, do beta reduce
[`(((λ (,x) ,em) ,(? aexp? v)) ,k)
`(,(subst em x v) ,k)]
;; if redex is evaled, take out the application which contain hole
;; v in left
;; hole with nothing left
[`(,(? aexp? v) (HOLE ,en))
`((,v ,en) HOLE)]
;; hole in left
[`(,(? aexp? v) ((HOLE ,en) ,k))
`((,v ,en) ,k)]
;; hole in right
[`(,(? aexp? v) (,k (HOLE ,en)))
`((,v ,en) ,k)]
;; v in right
;; hole with nothing left
[`(,(? aexp? v) (,eu HOLE))
`((,eu ,v) HOLE)]
;; hole in left
[`(,(? aexp? v) ((,eu HOLE) ,k))
`((,eu ,v) ,k)]
;; hole in right
[`(,(? aexp? v) (,k (,eu HOLE)))
`((,eu ,v) ,k)]
;; if left is value, then set right as redex
[`((,(? aexp? v1) ,(? cexp? em)) ,k)
`(,em ,(fill k `(,v1 HOLE)))]
;; if m and n both not evaled, create a redex
[`((,(? cexp? em) ,(? cexp? en)) ,k)
`(,em ,(fill k `(HOLE ,en)))]
[else
(displayln "reach end")
#f]))
注：习惯上我们使用希腊字符ς来表示状态,这个是希腊字母中出现在句尾上的sigma
为了我们的状态机能够真正的接受表达式作为输入，我们需要把输入的表达式注入我们的抽象机作为初始状态，这个不难，我们只需要给表达式一个洞作为起始的context就可以啦
(define (inject-cc e)
`(,e HOLE))
0x03 求值规则
为了让我们的抽象机真正的run起来，我们需要一个函数来模拟一次一次的step(一个自反传递闭包)，这样就可以解释执行我们的表达式
;; reflexive transitive closure
(define (multistep-cc ς)
(let ([next (step-cc ς)])
(displayln (format " --> ~s" next))
(if next
(multistep-cc next)
ς)))
;; specify valid value
(define (eval-cc ς)
(displayln (format "the init state is ~s" ς))
(let ([norm (multistep-cc ς)])
(match norm
[`(,(? aexp? b) HOLE) b]
[else (error (format "stuck at ill form ~s" norm))])))
0x04 简化CC Machine
CC Machine 其实有简化版本Simplified CC Machine(SCC Machine)。
通过观察我们不难发现， CC Machine 的规则有些是可以合并的。比如：
这种情况下面其实U 肯定是lambda, 而且这个时候其实已经可以求值了， 不需要先pull出来再写回去， 而对于
这个时候我们只需要调换redex就可以应用上面一条rule了
还有一个地方，我的代码中不是很明显， 但是其实在函数作用的rule中除了求值的那一条是要求N（也就是被作用的项）不能是值的， 我的racket代码使用的是调换rule的顺序来实现这一点的。 再简化rule之后，其实我们现在可以把这个限制拿掉了。
(define (step-scc ς)
(match ς
;; in scc machine we should't exclude value case
[`((,(? cexp? em) ,(? cexp? en)) ,k)
`(,em ,(fill k `(HOLE ,en)))]
;; if redex is evaled, switch redex from v n to make it form can be evaled
;; v in left
;; hole with nothing left
[`(,(? aexp? v) (HOLE ,en))
`(,en (,v HOLE))]
;; hole in left
[`(,(? aexp? v) ((HOLE ,en) ,k))
`(,en ((,v HOLE) ,k))]
;; hole in right
[`(,(? aexp? v) (,k (HOLE ,en)))
`(,en (,k (,v HOLE)))]
;; v in right, leftside should only be lambda with HOLE
;; hole with nothing left
[`(,(? aexp? v) ((λ (,x) ,em) HOLE))
`(,(subst em x v) HOLE)]
;; hole in left
[`(,(? aexp? v) (((λ (,x) ,em) HOLE) ,k))
`(,(subst em x v) (HOLE ,k))]
;; hole in right
[`(,(? aexp? v) (,k ((λ (,x) ,em) HOLE)))
`(,(subst em x v) (,k HOLE))]
[else
(displayln "reach end")
#f]
))
参考资料
犹他大学note of Programming Languages and Lambda Calculi by Matthew Flatt
网友评论