Lib.rs

Lambdascript

Lambdascript 在λ演算项上执行beta归约步骤，在归约前可以推断多态类型。它不是一个高性能的λ演算实现。相反，该工具主要服务于三个目的，这些目的都是说明性或教育性的。

1. 它展示了如何使用 rustlr 解析器生成器。Lambdascript的LALR(1)语法在rustlr格式中给出 这里。

2. 对于编程语言课程的初学者，该工具展示了将项归约到正常形式的每一步，包括必要的alpha转换。它包括使用正常顺序（按名调用）策略进行的完整beta-归一化，以及使用按值调用的弱归一化。可以为S、K、I等项给出定义。

3. 对于更高级的学生，该程序源代码展示了λ项如何在抽象语法中表示，以及如何实现归约。类型模块展示了如何使用统一算法推断类型。

使用方法

该程序是用Rust编写的，应该作为一个可执行文件安装：cargo install lambdascript。您必须安装Rust（从 http://rust-lang.net.cn）才能执行cargo命令。

程序可以读取脚本，或者从stdin交互式读取。默认情况下，项以无类型模式评估。给定一个包含以下内容的文件 simple.ls

define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.x z (y z);
define lazy INFINITY = (lambda x.x x) (lambda x.x x);
lambda y.K y INFINITY;

lambdascript untyped simple.ls 将输入作为脚本评估。'untyped'指令是可选的，因为它是默认值。然后它进入交互模式，同时加载定义。如果没有可选的文件名，λ脚本将直接以交互模式启动。以下是执行 simple.ls 的示例会话

λy.K y INFINITY
= λy.(λxλy.x) y INFINITY
 < alpha conversion of y to y1 >
 =>  λy.(λy1.y) INFINITY
= λy.(λy1.y) ((λx.x x) (λx.x x))
 =>  λy.y

Entering interactive mode, enter 'exit' to quit...
<<< typed
TERMS DEFINED IN THE UNTYPED MODE WILL NOW BE TYPE-CHECKED BEFORE EVALUATION    
<<< K I INFINITY
TYPE INFERENCE FOR <K I INFINITY> FAILED : UNTYPABLE
EVALUATION CANCELED
<<< I I
THE INFERRED TYPE OF <I I> IS e -> e
I I
= (λx.x) I
 =>  I
= λx.x

由于默认采用按名调用（call-by-name）求值，因此在不带类型的模式下终止了减少。如果将文件的最后一条语句替换为 weak (K I INFINITY x)，则将使用按值调用进行弱减少，导致无限循环。如果 lazy 未包含在 INFINITY 的定义中，也会有同样的无限循环。在 lambdascript 中，只有完整求值和弱按值调用是实现的减少策略。

可以使用 typed 指令从带类型模式切换到不带类型模式。在 terms 中没有类型的语法。大多数通用类型总是被推断出来。未定义的自由变量不被视为可类型化。注意，I I 是良好类型的，因为为 I 推断出的类型方案可以实例化两次。也可以在带类型模式下直接执行脚本。 lambdascript typed simple.ls 将显示所有定义的类型。

THE INFERRED TYPE OF I IS: Π(a -> a)
THE INFERRED TYPE OF K IS: Π(a -> b -> a)
THE INFERRED TYPE OF S IS: Π((h -> f -> g) -> (h -> f) -> h -> g)
TYPE INFERENCE FOR <(λx.x x) (λx.x x)> FAILED : UNTYPABLE
DEFINITION OF INFINITY NOT ACCEPTED
In the typed mode, the undefined free variable INFINITY cannot be typed
TYPE INFERENCE FOR <λy.K y INFINITY> FAILED : e -> UNTYPABLE
EVALUATION CANCELED

在这里，Π 量化其作用域内的所有类型变量。

类型总是在 beta-减少之前推断，因此可以称为静态类型。

Lambdascript 使用 lambda 项的标准语法：应用从左到右结合，应用比抽象绑定更紧密，这意味着 λ 的作用域尽可能地向右扩展，除非被括号限定。然而，应用内的 lambda 表达式必须始终由括号限定：因此 x lambda y.y 应该替换为 x (lambda y.y)。脚本中要评估的定义和项必须用分号（;）分隔。所有变量和标识符的长度限制为 15 个字符。

文件 pure.ls 包含了众所周知（不带类型）的 lambda-演算结合子的完整定义列表。

交互式解释器指令

在 <<< 提示符下，可以给出以下特殊指令

• exit 或 quit：退出程序
• typed：切换到带类型模式：将推断类型，不可类型化的项将不会减少。
• untyped：切换到不带类型模式
• use lambda 或 use lam 或 use Lam 或 use \：在某些系统中，希腊字母 λ（unicode 0x03BB）可能无法正确显示。要更改 lambda 显示的符号，可以选择以下四种替代方案之一（选择限于这四种，因为符号必须是一个静态分配的字符串）。
• use greek 或 use unicode：恢复显示 λ，这是默认设置
• trace off：关闭显示中间减少步骤：只显示初始项和最终范式
• trace medium：显示 beta-减少步骤，但不显示定义的展开或 alpha-转换
• trace on 或 trace max：恢复显示所有步骤：这是默认设置