娱乐性 λ 演算的玩具解析器

[geelaw]

因为 这篇 blog 里面记载的原因 突然就对 λ 演算有一点点兴趣，于是写了一个 λ 项的解析器。

作为一个理论计算机科学学生，我比较喜欢 neat 的设定，为了最简化问题，采用 de Bruijn 下标记法，使用无类型的 λ 演算，并且不允许自由变量。

词法：

• 空白只有分割单词的作用；
• lambda 单词是 lambda 这个串，或者 .（句点）；
• var 单词是一个不超过 65536 的正整数；
• const 单词是一个标识符（选的字符集比较怪，细节没什么可说的）；
• ( 单词和 ) 单词就是 ( 和 )。

语法：

• 一个 λ 项从开始符号 Term 产生；
• Term 可以变成 List Abs 或者 List App；
• List 可以变成 List App 或者 空白；
• Abs 可以变成 lambda Term；
• App 可以变成 var、const 或者 ( Term )。

语义（如何联系到普通的记法）：

• 任何 var 都不能超过它具有的 Abs 祖先的个数。（不允许自由变量）
• var 的面值决定了它表示的变量是被它祖上第 面值 近的 Abs 祖先捕获的变量。
• const 的字面量通常来说是一个字典里面的 entry，这样在书写的时候会简单一些，和文字替换是一样的效果（外面可能需要加括号），具体字典有哪些 entry 由 parser 的消费者决定。
• 举例来说 λx.λy.xy 的写法是 lambda lambda 2 1 或者更简单的是 ..2 1。

目前只写了解析器（从头开始手写的~包括自己的内存池、引用计数指针、CRTP 模板、自己的词法器、语法器，这个语法太简单了，所以手写比较容易），

GitHub 的地址是 GeeLaw/pure-lambda-calculus-playground。