Lambda Interpreter

语法规则

Term ::= Application| LAMBDA LCID DOT Term

Application ::= Application Atom| Atom

Atom ::= LPAREN Term RPAREN| LCID

Tokens

LPAREN: '('
RPAREN: ')'
LAMBDA: '\' // 为了方便使用 “\”
DOT: '.'
LCID: /[a-z][a-zA-Z]*/ 

Lexer

处理 token 的辅助方法:(可以自行定义)

  • next(Token): 返回下一个 token 是否匹配 Token
  • skip(Token): 和 next 一样, 但如果匹配的话会跳过
  • match(Token): 断言 next 方法返回 true 并 skip
  • token(Token): 断言 next 方法返回 true 并返回 token

Lexer向控制台输出每次检测到的Token类型+换行。

抽象语法树 AST

 抽象语法树 ( AST ) 。lambda 演算的 AST 非常简单,因为我们只有 3 种节点: Abstraction (抽象), Application (应用)以及 Identifier (标识符)
Abstraction 
    Identifier param;//变量
    AST body;//表达式
toString显示为:
\.body.toString()

Application
    AST lhs;左树
    AST rhs;右树
toString显示为:
(lhs.toString()空格rhs.toString())

Indentifier
    String value;//De Bruijn index
toString显示为:
value

De Bruijn index

(\x.\y.x \f.\g.g)
首先转化为:(变量保持不变,数字从0开始代码同层变量,1代表上一层次变量。)
(\x.\y.1 \f.\g.0)
toString显示为:(为了防止alpha变换造成的不一致,去掉变量)
(\.\.1 \.\.0)

求值

首先,我们需要定义,什么是形式(terms)(从语法可以推断),什么是值(values)。

我们的 term 是:


t1 t2   # Application
 
\x. t1  # Abstraction
 
x       # Identifier

value 是最终的形式,也就是说,它们不能再被求值了。在这个例子中,唯一的既是 term 又是 value 的是 abstraction(不能对函数求值,除非它被调用)。

实际的求值规则如下:

  1.   t1 -> t1'
    

    t1 t2 -> t1' t2

  2.   t2 -> t2'
    

    v1 t2 -> v1 t2'

  3. (\x. t12) v2 -> [x -> v2]t12

我们可以这样解读每一条规则:

  • 如果 t1 是值为 t1' 的项, t1 t2 求值为 t1' t2。即一个 application 的左侧先被求值。
  • 如果 t2 是值为 t2' 的项, v1 t2 求值为 v1 t2'。注意这里左侧的是 v1 而非 t1, 这意味着它是 value,不能再一步被求值,也就是说,只有左侧的完成之后,才会对右侧求值。
  • application (\x. t12) v2 的结果,和 t12 中出现的所有 x 被有效替换之后是一样的。注意在对 application 求值之前,两侧必须都是 value。

解释器

规则:

  • 首先检测其是否为 application,如果是,则对其求值:
    • 若 abstraction 的两侧都是值,只要将所有出现的 x 用给出的值替换掉; (3)
    • 否则,若左侧为值,给右侧求值;(2)
    • 如果上面都不行,只对左侧求值;(1)
  • 现在,如果下一个节点是 identifier,我们只需将它替换为它所表示的变量绑定的值。
  • 最后,如果没有规则适用于AST,这意味着它已经是一个 value,我们将它返回。

Main方法

public static void main(String[] args) {

        String source = "(\\x.\\y.x)(\\x.x)(\\y.y)";

        Lexer lexer = new Lexer(source);
        Parser parser = new Parser(lexer);
        AST ast = parser.parse();
        AST result = Interpreter.eval(ast);


}

Test

    @Test
    public void testLexer() {
        Lexer lexer = new Lexer(sources[1]);
        Parser parser = new Parser(lexer);
        AST ast = parser.parse();

        assertEquals("LPAREN" + lineBreak+
                "LPAREN" + lineBreak+
                "LAMBDA" + lineBreak+
                "LCID" + lineBreak+
                "DOT" + lineBreak+
                "LAMBDA" + lineBreak+
                "LCID" + lineBreak+
                "DOT" + lineBreak+
                "LAMBDA" + lineBreak+
                "LCID" + lineBreak+
                "DOT" + lineBreak+
                "LCID" + lineBreak+
                "LPAREN" + lineBreak+
                "LCID" + lineBreak+
                "LCID" + lineBreak+
                "LCID" + lineBreak+
                "RPAREN" + lineBreak+
                "RPAREN" + lineBreak+
                "LPAREN" + lineBreak+
                "LAMBDA" + lineBreak+
                "LCID" + lineBreak+
                "DOT" + lineBreak+
                "LAMBDA" + lineBreak+
                "LCID" + lineBreak+
                "DOT" + lineBreak+
                "LCID" + lineBreak+
                "RPAREN" + lineBreak+
                "RPAREN"+lineBreak+
                "EOF"+lineBreak,bytes.toString());

    }

    @Test
    public void testParser() {
        Lexer lexer = new Lexer(sources[1]);
        Parser parser = new Parser(lexer);
        AST ast = parser.parse();
        assertEquals("(\\.\\.\\.(1 ((2 1) 0)) \\.\\.0)",ast.toString());


    }

    @Test
    public void testInterpreter() {
        Lexer lexer = new Lexer(sources[1]);
        Parser parser = new Parser(lexer);
        interpreter = new Interpreter(parser);

        AST ast = parser.parse();

        AST result = interpreter.eval(ast);

        assertEquals("\\.\\.(1 0)",result.toString());


    }