菜单

λ演算解释器

2019年5月30日 - 日志类记录

中文版本

注意:这是之前帖子的重要重构。当我意识到首先我必须对这个初始帖子进行一些改进以获得更好的结构时,我正计划将其变成一个系列。嗯,这是结果,我希望你喜欢。或者,可以在此处找到原始版本。

事实上,它是一种如此简单的语言,它的完整实现适用于一篇文章,这使得学习/教授解释基础变得很好。

但在我们开始之前,什么是lambda演算呢?这是维基百科的描述:

Lambda演算(也称为λ演算)是数学逻辑中的一种形式系统,用于表示基于函数抽象的计算和使用变量绑定和替换的应用。它是一种通用的计算模型,可用于模拟任何单一的图灵机,并且是数学家Alonzo Church在20世纪30年代首次引入的,作为对数学基础的调查的一部分。

为了说明,这是一个非常简单的λ演算程序可能是这样的:

(λx. λy. x) (λy. y) (λx. x)

在λ演算中只有两个构造:函数抽象(即lambda表达式)和应用程序(即函数调用),然而,您可以使用它执行任何计算!

1.结构

解释器获取程序的源代码并执行它。为了将程序字符串转换为可执行格式,解释器必须完成大量工作,并且这项工作通常分为几个阶段。编译器和口译员可能有很多阶段,我们将有两个阶段:

另外,有很多种解释器,我们会编写一个AST解释器,因为我们可以将词法分析的结果直接输入解释器。其他类型的解释器将需要额外的阶段来将AST转换为解释器的输入格式。

2.语法

在编写解析器之前,我们需要定义的第一件事是我们将要解析的语言的语法,这里是λ演算的BNF语法:

term ::= application
       | LAMBDA LCID DOT term

application ::= application atom
              | atom

atom ::= LPAREN term RPAREN
       | LCID

2.1. 语法结构

一个production是一个替换规则:它表明我们能够取代它的左侧,其右侧

制作的left-hand由单个非终结点组成

生产的right-hand包括一个或多个由管道()分隔的替代替代|

一种alternative是零级或更多的任何序列terminalsnonterminals

nonterminal以小写字母显示,用于表示定义它的生产的right-hand

terminals以大写字母显示,表示实际文本输入中的某些模式。

2.2. 语法解析

语法以a开头term,因为它是语法的第一条规则。

term可能由一个application或一个abstraction(定义内联)组成。

一个application可以由任一另一个的application后面的atom或可替代地由单个atom。这是一个左递归规则(递归,因为它引用自身,左递归,因为重复的术语出现在第一个位置),这意味着它是左关联的(即具有表单的应用程序a b c,应该被分组为(a b) c而不是a (b c))。

atoms可以是小写标识符(LCID)或term括在括号中(用于消除歧义)。

3.Tokens

语法中的终端正是我们词法分析器必须生成的标记(后来我们的解析将消耗)。以下是创建每个令牌的规则:

LPAREN: '('
RPAREN: ')'
LAMBDA: 'λ' /* we'll also allow `\` for convenience */
DOT: '.'
// lowercase identifier: lowercase letter followed by any letters
LCID: /[a-z][a-zA-Z]*/

为了表示标记,我们将创建Token类来保存type(上面的一个)和一个可选的语义值(例如匹配的字符串LCID)。

class Token {
  constructor(type, value) {
    this.type = type;
    this.value = value;
  }
};

4.Lexer

现在我们可以使用上面的定义来编写一个Lexer,为解析器提供一些便于使用的的API来进行操作。

Lexer的LCID模块的创建是比较无聊的:它是一个大的switch语句,它检查源代码中的下一个char:

_nextToken() {
  switch (c) {
    case 'λ':
    case '\\':
      this._token = new Token(Token.LAMBDA);
      break;

    case '.':
      this._token = new Token(Token.DOT);
      break;

    case '(':
      this._token = new Token(Token.LPAREN);
      break;

    /* ... */
  }
}

词法分析器将为解析器提供以下API:

好的,现在就可以开始写Parser

5.语法解析器(Parser)

在我们开始编写解析器之前,关于这个语法只有一个棘手的问题:我们手写解析器通常是递归下降(我们写出来也是这样的),但是它们不能处理左递归

但幸运的是,可以通过一个简单的技巧避免左递归带来的问题:

我们先看看原始结构……

application ::= application atom
              | atom

……并把它分成两部分:

application ::= atom application'

application' ::= atom application'
               | ε  /* empty */

现在我们有一个右递归规则,只有application'在另一个atom下一个时才能扩展,否则我们选择不ε匹配的替代右边(),即我们停止。

在实现解析器时,我们必须小心保持应用程序规则为左关联,否则它将改变应用程序执行的顺序,并且我们的解释器将是不正确的。

5.1. 抽象语法树AST

根据我们的语法,我们还可以导出AST的节点:具有多个非终结符或具有任何终端的右侧备选方案将在大多数情况下需要新节点。(在我们的例子中的例外是LPAREN term RPAREN替代,它只是term括在括号中,所以我们只需要term。)

然后我们为三个备选方案创建三个节点:

这是一个简单的AST程序:

(λx. x) (λy. y)

Application {
  lhs: Abstraction {
    param: 'x',
    body: Identifier { name: 'x' }
  },
  rhs: Abstraction {
    param: 'y',
    body: Identifier { name: 'y' }
  }
}

5.2. 解析器实现

现在我们有了AST节点,我们可以使用它们构建实际的树。

我们还可以使用以下步骤从语法派生我们的解析器实现:

这是实际的代码:

term() {
  // term ::= LAMBDA LCID DOT term
  //        | application
  if (this.lexer.skip(Token.LAMBDA)) {
    const id = this.lexer.token(Token.LCID);
    this.lexer.match(Token.DOT);
    const term = this.term();
    return new AST.Abstraction(id, term);
  }  else {
    return this.application();
  }
}

application() {
  // application ::= atom application'
  let lhs = this.atom();
  while (true) {
    // application' ::= atom application'
    //                | ε
    const rhs = this.atom();
    if (!rhs) {
      return lhs;
    } else {
      lhs = new AST.Application(lhs, rhs);
    }
  }
}

atom() {
  // atom ::= LPAREN term RPAREN
  //        | LCID
  if (this.lexer.skip(Token.LPAREN)) {
    const term = this.term(Token.RPAREN);
    this.lexer.match(Token.RPAREN);
    return term;
  } else if (this.lexer.next(Token.LCID)) {
    const id = new AST.Identifier(this.lexer.token(Token.LCID));
    return id;
  }
}

6.计算

现在我们有了AST,我们可以用它来评估程序。

为了知道我们的解释器应该如何评估每个构造,我们首先需要查看λ演算的评估规则。

6.1. 计算法则

首先,我们需要定义什么是我们的术语,哪些是值。

我们也可以从语法中推导出我们的术语:

t1 t2   # Application

λx. t1  # Abstraction

x       # Identifier

是的,这些与我们AST的节点完全相同!但哪些是价值观?

值是最终形式的术语,即无法进一步评估它们。在这种情况下,唯一的值是抽象。(除非被调用,否则无法评估函数。)

实际评估规则如下:

1)       t1 → t1'
     —————————————————
      t1 t2 → t1' t2


2)       t2 → t2'
     —————————————————
      v1 t2 → v1 t2'


3)    (λx. t12) v2 → [x ↦ v2]t12

以下是我们如何阅读每条规则:

  1. 如果t1是一个评估的术语t1't1 t2将评估为t1' t2。即首先评估应用程序的左侧。
  2. 如果t2是一个评估的术语t2'v1 t2将评估为v1 t2'。请注意,左侧v1不是t1,这意味着它是一个值,因此无法进一步评估。也就是说,只有当我们完成对应用程序左侧的评估时,我们才会开始评估正确的应用程序。
  3. 应用的结果(λx. t12) v2是一样有效地取代所有出现xt12v2。请注意,在评估应用程序之前,双方都必须是值。

6.2. 计算程序(Interpreter)

解释器遵循评估规则将程序减少到一个值。

我们现在要做的就是将上面的规则翻译成JavaScript:

const eval = ast => {
  while (true) {
    if (ast instanceof AST.Application) {
      if (isValue(ast.lhs) && isValue(ast.rhs)) {
        ast = substitute(ast.rhs, ast.lhs.body);
      } else if (isValue(ast.lhs)) {
        ast.rhs = eval(ast.rhs);
      } else {
        ast.lhs = eval(ast.lhs);
      }
    } else {
      return ast;
    }
  }
};

注意:本文的原始版本提供了一个稍微不同的eval函数版本,它将变量绑定存储在上下文映射中。该函数有点大,不太清楚,但需要更少的代码,使一般项目更简单。但是,实现中存在一个错误,我决定切换到上面的版本,它更符合评估规则(以及TaPL中提供的版本)

我希望评估规则和评估功能之间的对应关系是明确的,但无论如何,这里是书面形式:

6.3 De Bruijn值

substitute函数的实现使用De Bruijn索引,该索引为每个变量分配其出现与其定义之间的距离。

例如,以下的实现truefalse(参见Church Encoding以供参考):

(λx. (λy. x)) (λf. (λg. g))

变为:

(λx. (λy. 1)) (λf. (λg. 0))

请注意,参数名称不再是必需的,但我会保留它们以突出显示索引,保持其他所有内容相同。

我们可以在解析期间通过使用上下文扩充解析器来生成索引,该上下文将作为一组变量名称使用。为了找到变量的De Bruijn索引,我们在上下文堆栈中得到它的偏移量。

以下是受影响的主要规则(其他规则将简单地管理上下文变量):

term(ctx) {
  if (this.lexer.skip(Token.LAMBDA)) {
    const id = this.lexer.token(Token.LCID);
    this.lexer.match(Token.DOT);
    /* Push the parameter into the context stack when parsing the
     * abstraction's body (without mutating the current context)
     */
    const term = this.term([id].concat(ctx));
    return new AST.Abstraction(id, term);
  }
  /* ... */
}

atom(ctx) {
  /* ... */
  if (this.lexer.next(Token.LCID)) {
    const id = this.lexer.token(Token.LCID)
    // Use the builtin indexOf to get the distance in the stack
    return new AST.Identifier(ctx.indexOf(id), ctx.length);
  }
  /* ... */
}

6.4替换方案

我个人觉得替换算法有点令人困惑,这就是为什么我没有把它包含在文章的原始版本中,但我会尽力解释它。

替代实际上建立在2个操作之上:shift实际subst

让我们看看步骤详解

  1. 如果我们从以下来源开始:(λx. (λy. y x)) (λt. a)
  2. 假设这a是一个高于上一级的自由变量,它将与De Bruijn索引类似:(λx. (λy. 0 1)) (λt. 1)
  3. 现在,我们评估使用规则3:我们替换每个变量指向x(λt. 1)(λy. 0 (λt. 1)))
  4. 你能发现问题吗?(λt. 1)最初是指a,但在替换之后它指的是y。那是因为我们(λt. 1)比之前更深一层,但没有更新自由变量。因此,替换定义如下:↓([x ↦ ↑value] node) 这意味着:下移替换的所有出现的结果xnodevalue移。
  5. 打破它:5.1。首先,我们将值中的自由变量向上移动一个:(λx. (λy. 0 1)) (λt. 2) 5.2。然后我们用x新值替换出现的事件:(λx. (λy. 0 (λt. 3))) 请注意,我们碰到的是指指数a23。之所以发生这种情况,是因为每次我们增加节点的深度(通过将其置于闭包内),我们需要将其移动深度差,在这种情况下是一个(它只在一个额外的闭包内)。5.3然后我们删除封闭的抽象:(λy. 0 (λt. 3)) 5.4。并将所有自由变量向下移动一个:(λy. 0 (λt. 2))
  6. 最后,我们只需要在正确的偏移处查找参数的名称,我们得到一个合适的输出:(λy. y (λt. a))

6.5。关于替代的说明

替换逻辑是递归的,因此它需要实现以递归方式访问AST的函数。完整的实现包括用于编写AST访问者和两个访问者的实用程序功能:shiftsubst。这个代码很长而且不是很有趣,所以我在这里跳过它,但最后会有完整的实现。

7.结果打印

我们现在差不多完成了:我们已经可以将程序减少到一个值,我们现在剩下的就是实现逻辑来打印这个值。

一种简单的方法是通过向toString每个AST节点添加一个方法,我们唯一需要注意的是我们必须将De Bruijn索引映射回原始变量名,如上面第6项所示。

这是代码:

/* Abstraction */ toString(ctx=[]) {
  return `(λ${this.param}. ${this.body.toString([this.param].concat(ctx))})`;
}

/* Application */ toString(ctx) {
  return `${this.lhs.toString(ctx)} ${this.rhs.toString(ctx)}`;
}

/* Identifier */ toString(ctx) {
  return ctx[this.value];
}

我们知道解释器会将程序减少到一个值,我们也知道这个值将是一个AST节点,并且根据评估规则,λ演算中唯一的值是抽象。然后我们可以得出结论,评估结果将是一个抽象,因此是Abstraction.toString方法中context参数的默认值,因此我们可以从外部调用它而不提供上下文。

现在我们可以调用toString结果节点,并且它将递归地打印它的所有子节点(传递上下文)以生成它的字符串表示。

8.把所有的结合

我们需要一个将所有这些部分连接在一起的转轮脚本,代码应该类似于:

// assuming you have some source
const source = '(λx. λy. x) (λx. x) (λy. y)';

// wire all the pieces together
const lexer = new Lexer(source);
const parser = new Parser(lexer);
const ast = parser.parse();
const result = Interpreter.eval(ast);

// stringify the resulting node and print it
console.log(result.toString());

发表评论

电子邮件地址不会被公开。 必填项已用*标注