如果你正在做一个需要规则推理的程序比如写一个编译器原型、类型检查器、程序分析工具甚至是证明助手里的自定义策略大概率会遇到同一个问题传统的规则引擎写起来很笨尤其是在处理“变量绑定”“作用域”“高阶函数”这些概念时几乎要把整个环境、替换、去重逻辑手写一遍。我第一次在项目里尝试用 Prolog 处理 lambda 表达式的类型推断时最痛苦的部分不是规则本身而是如何表示λx. x这样的绑定结构。用字符串变量名会撞名用 de Bruijn 索引要写一堆位移逻辑用显式环境又让规则失去可读性。后来接触到 ELPI 这个“可嵌入的 Lambda Prolog 解释器”发现它在设计上就是为了解决这类问题。这篇文章会从 ELPI 的概念讲起一步一步带你安装环境、理解核心语法并实现一个简单的类型化 lambda 演算类型检查器最后梳理嵌入到宿主程序时的思路和常见问题。文章适合对逻辑编程有一定了解但没深入使用过 Lambda Prolog 的开发者也适合想在 OCaml、Coq 等环境中嵌入推理能力的读者。1. 什么是 ELPI从 Prolog 到 Lambda Prolog1.1 传统 Prolog 能做什么Prolog 是一种基于一阶逻辑的声明式编程语言。你不需要告诉计算机“怎么做”而是描述“什么是真的”然后由解释器通过合一和回溯寻找答案。一个经典的例子是家族关系% family.pl parent(tom, bob). parent(bob, alice). ancestor(X, Y) :- parent(X, Y). ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).查询ancestor(tom, alice)时Prolog 会先匹配第一条规则发现parent(tom, alice)不成立再匹配第二条规则尝试找到Z使得parent(tom, Z)和ancestor(Z, alice)同时成立最终返回true。这种机制非常适合写规则、做搜索、做约束求解比如八皇后、图搜索、语法分析等。但传统 Prolog 在处理“程序本身也是数据”的场景时非常吃力。以 lambda 演算为例项可以表示为% 一阶表示方式 term(var(x)). term(app(M, N)). term(lam(x, M)).这里lam(x, M)只是“带有一个字符串变量名的结构体”并不是真正的λx. M。你没有办法直接表达“把 M 中的 x 替换成 N”这个操作必须自己写替换函数还要处理 alpha 等价λx. x和λy. y虽然形式不同但应当视为同一个函数。传统 Prolog 的合一不会帮你做这些。1.2 Lambda Prolog 增加了什么Lambda Prolog 是在 Prolog 基础上引入高阶逻辑机制的一种逻辑编程语言。它的核心改进有三个第一项中可以使用高阶抽象语法也就是用函数本身表示绑定。λx. x可以写成lam (x\ x)其中x\ ...是 ELPI 中表示“以 x 为参数的函数”的语法。lam (x\ x)就是一个lam构造器里面保存了一个函数而不是字符串。这样一来绑定变量不再需要命名也不会发生命名冲突替换由 λ 演算的 beta 归约自然完成逻辑层不需要维护环境。第二引入了pi和sigma量化。pi x\ P表示“对于任意 xP 成立”sigma x\ P表示“存在某个 x使得 P 成立”。当你需要在规则里引入“任意新变量”时pi非常自然。第三引入了直觉主义蕴含符。它允许在推导过程中临时添加假设适合表示“在当前上下文中可证明”这类场景。1.3 ELPI 项目定位ELPI 的全称是 Embeddable Lambda Prolog Interpreter也就是“可嵌入的 Lambda Prolog 解释器”。它基于 OCaml 实现既提供了命令行解释器也提供了 OCaml API方便你把逻辑推理能力嵌入到自己的程序中。ELPI 最知名的使用场景之一是在 Coq 证明助手中。Coq 生态里的coq-elpi项目允许开发者用 ELPI 编写自定义策略把高阶逻辑规则直接写成 ELPI 程序。除此之外ELPI 也适合用来做类型推断、程序转换、规则匹配、领域特定语言解释器等任务。可以说ELPI 是面向“编程语言和形式化工具开发”的一把专用工具理解它之后你会在很多需要规则推理的项目里多一个十分趁手的选项。2. 环境准备与安装2.1 准备依赖在开始安装 ELPI 之前电脑上需要有 OCaml 环境。推荐使用 opam 作为包管理器它是 OCaml 生态里最常用的工具用来管理编译器版本和第三方库。本文示例以常见环境为例重点演示配置思路具体版本需要根据你的项目实际情况调整。你需要先确认几个基础工具已经安装OCaml 编译器opam 包管理器dune 构建工具后续嵌入 OCaml 项目时需要make、gcc 等基础编译工具如果你还没有 opam可以优先安装 opam再用它安装 OCaml。安装完成后先初始化 opam 环境opam init eval $(opam env)2.2 通过 opam 安装 ELPI安装 ELPI 的命令很简单opam update opam install elpi安装完成后可以在终端里验证是否成功elpi --version如果输出版本信息说明命令行解释器已经就绪。不同版本的输出格式可能不同不要纠结具体数字能打印出来即可。2.3 运行第一个 ELPI 文件创建一个hello.elpi文件% hello.elpi main :- print Hello, ELPI!.这里定义了一个main谓词表示程序入口。用下面的命令运行elpi hello.elpi终端会输出Hello, ELPI!如果你不想创建文件也可以在 REPL 里直接输入查询。在终端执行elpi进入交互模式输入type p prop. p.type p prop.声明p是一个命题p.是一个事实。接着输入p.作为查询解释器会回答成功。2.4 建议的工程目录ELPI 文件通常和宿主项目放在一起但逻辑代码与宿主代码建议保持分离。一个典型的目录结构如下project/ dune-project src/ main.ml logic/ typechecker.elpi stdlib.elpi把.elpi文件单独放在logic目录里有助于复用、测试和维护。如果规则文件很多还可以在 ELPI 内使用accumulate机制加载其他文件而不是把所有代码堆到一个大文件里。3. 核心语法拆解从 Prolog 到 Lambda Prolog3.1 类型化谓词声明ELPI 和许多现代逻辑编程语言一样要求谓词带类型声明。你可以把类型声明看作是一门轻量级类型系统它能在运行前发现很多低级错误。例如定义一个判断“某个元素是否在列表中”的谓词type mem A - list A - prop. mem X [X|_]. mem X [_|L] :- mem X L.这里type mem A - list A - prop.表示mem接收两个参数第一个是任意类型A第二个是A的列表结果是一个命题。第一条子句mem X [X|_].表示如果元素就是列表头那么成立第二条子句表示否则继续在尾列表中查找。列表语法和 Prolog 保持一致[X|_]表示“以 X 开头剩余部分不关心”的列表。在 REPL 中查询mem 2 [1,2,3].会输出成功。类型声明的意义不只是做静态检查它还能帮助解释器生成更清晰的错误信息尤其是在使用高阶语法时类型信息几乎必不可少。3.2 高阶抽象语法HOAS高阶抽象语法Higher-Order Abstract Syntax简称 HOAS是 Lambda Prolog 最核心的设计思想。先定义一种简单的项类型kind tm type. type app tm - tm - tm. type lam (tm - tm) - tm.kind tm type.引入一个新的类型族tm。app是两个tm组合成一个tm的构造器。关键是lam它的类型是(tm - tm) - tm也就是说它接收一个“从 tm 到 tm 的函数”返回一个tm。于是恒等函数λx. x可以写成lam (x\ x)注意x\ x是 ELPI 的 lambda 抽象语法。这里的x不是字符串也不是全局变量而是这个函数自己的形参。整个lam (x\ x)就是一个闭项不需要为它准备一个“变量名集合”。对比传统 Prolog 的lam(x, var(x))ELPI 的写法避免了绑定性变量的命名冲突也避免了替换函数。当你想对一个lam做 beta 规约时直接应用函数即可type beta tm - tm - tm - prop. beta (lam F) M (F M).beta (lam F) M (F M)这条规则的意思是(λx. F x)应用到M结果就是F M。同样的逻辑用一阶表示法写需要几十行环境操作和替换代码用高阶抽象表示一行就完成了。3.3 pi 与 sigma 量化pi和sigma是 Lambda Prolog 中非常有用的量化工具。pi x\ Goal表示“对于任意 xGoal 成立”。sigma x\ Goal表示“存在某个 x使得 Goal 成立”。在类型检查规则里我们经常需要引入一个“新的局部变量”也就是一个尚未被实例化的变量。例如判断某个项是否是封闭项可以这样写type closed tm - prop. closed cnst. closed (app M N) :- closed M, closed N. closed (lam F) :- pi x\ closed (F x).这里pi x\ closed (F x)的含义是对于任意新的局部常量xF x都是封闭的。如果F内部引用了某个全局自由变量那么closed (F x)会因为找不到匹配的子句而失败因此整体规则能正确判断“项是否没有自由变量”。sigma则常用于“生成一个新名字”或“找出某个未知项”的场景。比如type find_name tm - prop. find_name N :- sigma N\ (N lam (x\ x)).这只是一个简单示意但你可以看到sigma的本质它允许规则中引入一个不固定的未知量再由后续条件逐步约束。3.4 蕴含在推导中添加临时假设是 ELPI 的一个非常有特色的操作符它相当于在证明过程中临时向子句库中添加假设。例如要判断“在已知of x A的前提下M的类型为B”可以把这个前提写到规则右侧of (lam F) (arr A B) :- pi x\ (of x A of (F x) B).这里的逻辑含义是对于任意新变量x如果临时假设of x A成立那么可以推导出of (F x) B。这个能力对实现类型检查器至关重要因为它天然对应了“把变量加入类型环境”这一步。在传统 Prolog 里你需要自己维护一个环境列表并在子句之间传递在 ELPI 里环境信息通过上下文假设自动传播代码简洁很多。3.5 内置类型与常用设施ELPI 内置了不少常用类型和谓词。列表、整数、字符串都是可以直接使用的。一个简单的打印例子type main prop. main :- L [1, 2, 3], print L.运行后的输出就是[1, 2, 3]。字符串在 ELPI 中用双引号表示例如hello。也可以用{{ ... }}来引用 ELPI 自身的源码片段这在实现“元编程”或自举工具时非常方便。4. 完整实战案例用 ELPI 实现类型检查器下面我们做一个真正能运行的类型检查器目标是对一个简单的 lambda 演算进行类型推断。这个案例能完整展示pi、、HOAS 和类型化谓词声明这几个核心特性。4.1 语法和类型规则我们定义一个只有一种基本类型num和函数类型arr的类型系统。项的语法包括常量cnst我们规定它的类型是num应用app M N抽象lam F其中F是一个高阶函数表示带绑定的项类型规则如下cnst : num如果M : A - B且N : A那么app M N : B如果假设x : A时F x : B成立那么lam F : A - B4.2 定义类型和项第一步定义类型和项的类型族% typechecker.elpi % 类型定义 kind ty type. type num ty. type arr ty - ty - ty. % 项定义 kind tm type. type cnst tm. type app tm - tm - tm. type lam (tm - tm) - tm.kind ty type.引入新类型族ty。type num ty.定义类型常量num。type arr ty - ty - ty.定义函数类型构造器。kind tm type.引入tm类型族。type app tm - tm - tm.表示应用type lam (tm - tm) - tm.表示用高阶函数来保存抽象体。4.3 编写类型判断谓词接下来是核心的类型判断谓词type of tm - ty - prop. of cnst num. of (app M N) B :- of M (arr A B), of N A. of (lam F) (arr A B) :- pi x\ (of x A of (F x) B).逐行解释type of tm - ty - prop.声明of接收一个项和一个类型返回命题。of cnst num.表示常量的类型就是num。应用规则先检查函数类型是否为arr A B再检查参数类型是否为A。抽象规则引入新变量x假设of x A成立然后检查F x的类型是B。这里最值得体会的是第三条规则它没有像传统实现那样维护一个“符号表”而是用pi引入新局部变量用把它加入上下文。整个类型环境是隐式传递的。4.4 编写测试谓词为了让程序运行后能直接看到结果我们再加一个测试谓词type test_of_term tm - prop. test_of_term T :- of T Ty, print Term: T, print Type: Ty. main :- print Test 1: id , test_of_term (lam (x\ x)), print Test 2: const , test_of_term (lam (x\ cnst)), print Test 3: application , test_of_term (lam (x\ app (lam (y\ y)) x)).test_of_term接收一个项调用of得到类型然后打印项和类型。三个测试分别对应lam (x\ x)恒等函数期望类型为arr A A。lam (x\ cnst)忽略输入返回常量期望类型为arr A num。lam (x\ app (lam (y\ y)) x)λx. (λy.y) x期望类型为arr A A。4.5 运行与验证保存文件后运行elpi typechecker.elpi预期输出类似 Test 1: id Term: lam (c0 \ c0) Type: arr X0 X0 Test 2: const Term: lam (c0 \ cnst) Type: arr X0 num Test 3: application Term: lam (c0 \ app (lam (c1 \ c1)) c0) Type: arr X0 X0注意 ELPI实战：用Lambda Prolog轻松实现类型检查器
如果你正在做一个需要规则推理的程序比如写一个编译器原型、类型检查器、程序分析工具甚至是证明助手里的自定义策略大概率会遇到同一个问题传统的规则引擎写起来很笨尤其是在处理“变量绑定”“作用域”“高阶函数”这些概念时几乎要把整个环境、替换、去重逻辑手写一遍。我第一次在项目里尝试用 Prolog 处理 lambda 表达式的类型推断时最痛苦的部分不是规则本身而是如何表示λx. x这样的绑定结构。用字符串变量名会撞名用 de Bruijn 索引要写一堆位移逻辑用显式环境又让规则失去可读性。后来接触到 ELPI 这个“可嵌入的 Lambda Prolog 解释器”发现它在设计上就是为了解决这类问题。这篇文章会从 ELPI 的概念讲起一步一步带你安装环境、理解核心语法并实现一个简单的类型化 lambda 演算类型检查器最后梳理嵌入到宿主程序时的思路和常见问题。文章适合对逻辑编程有一定了解但没深入使用过 Lambda Prolog 的开发者也适合想在 OCaml、Coq 等环境中嵌入推理能力的读者。1. 什么是 ELPI从 Prolog 到 Lambda Prolog1.1 传统 Prolog 能做什么Prolog 是一种基于一阶逻辑的声明式编程语言。你不需要告诉计算机“怎么做”而是描述“什么是真的”然后由解释器通过合一和回溯寻找答案。一个经典的例子是家族关系% family.pl parent(tom, bob). parent(bob, alice). ancestor(X, Y) :- parent(X, Y). ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).查询ancestor(tom, alice)时Prolog 会先匹配第一条规则发现parent(tom, alice)不成立再匹配第二条规则尝试找到Z使得parent(tom, Z)和ancestor(Z, alice)同时成立最终返回true。这种机制非常适合写规则、做搜索、做约束求解比如八皇后、图搜索、语法分析等。但传统 Prolog 在处理“程序本身也是数据”的场景时非常吃力。以 lambda 演算为例项可以表示为% 一阶表示方式 term(var(x)). term(app(M, N)). term(lam(x, M)).这里lam(x, M)只是“带有一个字符串变量名的结构体”并不是真正的λx. M。你没有办法直接表达“把 M 中的 x 替换成 N”这个操作必须自己写替换函数还要处理 alpha 等价λx. x和λy. y虽然形式不同但应当视为同一个函数。传统 Prolog 的合一不会帮你做这些。1.2 Lambda Prolog 增加了什么Lambda Prolog 是在 Prolog 基础上引入高阶逻辑机制的一种逻辑编程语言。它的核心改进有三个第一项中可以使用高阶抽象语法也就是用函数本身表示绑定。λx. x可以写成lam (x\ x)其中x\ ...是 ELPI 中表示“以 x 为参数的函数”的语法。lam (x\ x)就是一个lam构造器里面保存了一个函数而不是字符串。这样一来绑定变量不再需要命名也不会发生命名冲突替换由 λ 演算的 beta 归约自然完成逻辑层不需要维护环境。第二引入了pi和sigma量化。pi x\ P表示“对于任意 xP 成立”sigma x\ P表示“存在某个 x使得 P 成立”。当你需要在规则里引入“任意新变量”时pi非常自然。第三引入了直觉主义蕴含符。它允许在推导过程中临时添加假设适合表示“在当前上下文中可证明”这类场景。1.3 ELPI 项目定位ELPI 的全称是 Embeddable Lambda Prolog Interpreter也就是“可嵌入的 Lambda Prolog 解释器”。它基于 OCaml 实现既提供了命令行解释器也提供了 OCaml API方便你把逻辑推理能力嵌入到自己的程序中。ELPI 最知名的使用场景之一是在 Coq 证明助手中。Coq 生态里的coq-elpi项目允许开发者用 ELPI 编写自定义策略把高阶逻辑规则直接写成 ELPI 程序。除此之外ELPI 也适合用来做类型推断、程序转换、规则匹配、领域特定语言解释器等任务。可以说ELPI 是面向“编程语言和形式化工具开发”的一把专用工具理解它之后你会在很多需要规则推理的项目里多一个十分趁手的选项。2. 环境准备与安装2.1 准备依赖在开始安装 ELPI 之前电脑上需要有 OCaml 环境。推荐使用 opam 作为包管理器它是 OCaml 生态里最常用的工具用来管理编译器版本和第三方库。本文示例以常见环境为例重点演示配置思路具体版本需要根据你的项目实际情况调整。你需要先确认几个基础工具已经安装OCaml 编译器opam 包管理器dune 构建工具后续嵌入 OCaml 项目时需要make、gcc 等基础编译工具如果你还没有 opam可以优先安装 opam再用它安装 OCaml。安装完成后先初始化 opam 环境opam init eval $(opam env)2.2 通过 opam 安装 ELPI安装 ELPI 的命令很简单opam update opam install elpi安装完成后可以在终端里验证是否成功elpi --version如果输出版本信息说明命令行解释器已经就绪。不同版本的输出格式可能不同不要纠结具体数字能打印出来即可。2.3 运行第一个 ELPI 文件创建一个hello.elpi文件% hello.elpi main :- print Hello, ELPI!.这里定义了一个main谓词表示程序入口。用下面的命令运行elpi hello.elpi终端会输出Hello, ELPI!如果你不想创建文件也可以在 REPL 里直接输入查询。在终端执行elpi进入交互模式输入type p prop. p.type p prop.声明p是一个命题p.是一个事实。接着输入p.作为查询解释器会回答成功。2.4 建议的工程目录ELPI 文件通常和宿主项目放在一起但逻辑代码与宿主代码建议保持分离。一个典型的目录结构如下project/ dune-project src/ main.ml logic/ typechecker.elpi stdlib.elpi把.elpi文件单独放在logic目录里有助于复用、测试和维护。如果规则文件很多还可以在 ELPI 内使用accumulate机制加载其他文件而不是把所有代码堆到一个大文件里。3. 核心语法拆解从 Prolog 到 Lambda Prolog3.1 类型化谓词声明ELPI 和许多现代逻辑编程语言一样要求谓词带类型声明。你可以把类型声明看作是一门轻量级类型系统它能在运行前发现很多低级错误。例如定义一个判断“某个元素是否在列表中”的谓词type mem A - list A - prop. mem X [X|_]. mem X [_|L] :- mem X L.这里type mem A - list A - prop.表示mem接收两个参数第一个是任意类型A第二个是A的列表结果是一个命题。第一条子句mem X [X|_].表示如果元素就是列表头那么成立第二条子句表示否则继续在尾列表中查找。列表语法和 Prolog 保持一致[X|_]表示“以 X 开头剩余部分不关心”的列表。在 REPL 中查询mem 2 [1,2,3].会输出成功。类型声明的意义不只是做静态检查它还能帮助解释器生成更清晰的错误信息尤其是在使用高阶语法时类型信息几乎必不可少。3.2 高阶抽象语法HOAS高阶抽象语法Higher-Order Abstract Syntax简称 HOAS是 Lambda Prolog 最核心的设计思想。先定义一种简单的项类型kind tm type. type app tm - tm - tm. type lam (tm - tm) - tm.kind tm type.引入一个新的类型族tm。app是两个tm组合成一个tm的构造器。关键是lam它的类型是(tm - tm) - tm也就是说它接收一个“从 tm 到 tm 的函数”返回一个tm。于是恒等函数λx. x可以写成lam (x\ x)注意x\ x是 ELPI 的 lambda 抽象语法。这里的x不是字符串也不是全局变量而是这个函数自己的形参。整个lam (x\ x)就是一个闭项不需要为它准备一个“变量名集合”。对比传统 Prolog 的lam(x, var(x))ELPI 的写法避免了绑定性变量的命名冲突也避免了替换函数。当你想对一个lam做 beta 规约时直接应用函数即可type beta tm - tm - tm - prop. beta (lam F) M (F M).beta (lam F) M (F M)这条规则的意思是(λx. F x)应用到M结果就是F M。同样的逻辑用一阶表示法写需要几十行环境操作和替换代码用高阶抽象表示一行就完成了。3.3 pi 与 sigma 量化pi和sigma是 Lambda Prolog 中非常有用的量化工具。pi x\ Goal表示“对于任意 xGoal 成立”。sigma x\ Goal表示“存在某个 x使得 Goal 成立”。在类型检查规则里我们经常需要引入一个“新的局部变量”也就是一个尚未被实例化的变量。例如判断某个项是否是封闭项可以这样写type closed tm - prop. closed cnst. closed (app M N) :- closed M, closed N. closed (lam F) :- pi x\ closed (F x).这里pi x\ closed (F x)的含义是对于任意新的局部常量xF x都是封闭的。如果F内部引用了某个全局自由变量那么closed (F x)会因为找不到匹配的子句而失败因此整体规则能正确判断“项是否没有自由变量”。sigma则常用于“生成一个新名字”或“找出某个未知项”的场景。比如type find_name tm - prop. find_name N :- sigma N\ (N lam (x\ x)).这只是一个简单示意但你可以看到sigma的本质它允许规则中引入一个不固定的未知量再由后续条件逐步约束。3.4 蕴含在推导中添加临时假设是 ELPI 的一个非常有特色的操作符它相当于在证明过程中临时向子句库中添加假设。例如要判断“在已知of x A的前提下M的类型为B”可以把这个前提写到规则右侧of (lam F) (arr A B) :- pi x\ (of x A of (F x) B).这里的逻辑含义是对于任意新变量x如果临时假设of x A成立那么可以推导出of (F x) B。这个能力对实现类型检查器至关重要因为它天然对应了“把变量加入类型环境”这一步。在传统 Prolog 里你需要自己维护一个环境列表并在子句之间传递在 ELPI 里环境信息通过上下文假设自动传播代码简洁很多。3.5 内置类型与常用设施ELPI 内置了不少常用类型和谓词。列表、整数、字符串都是可以直接使用的。一个简单的打印例子type main prop. main :- L [1, 2, 3], print L.运行后的输出就是[1, 2, 3]。字符串在 ELPI 中用双引号表示例如hello。也可以用{{ ... }}来引用 ELPI 自身的源码片段这在实现“元编程”或自举工具时非常方便。4. 完整实战案例用 ELPI 实现类型检查器下面我们做一个真正能运行的类型检查器目标是对一个简单的 lambda 演算进行类型推断。这个案例能完整展示pi、、HOAS 和类型化谓词声明这几个核心特性。4.1 语法和类型规则我们定义一个只有一种基本类型num和函数类型arr的类型系统。项的语法包括常量cnst我们规定它的类型是num应用app M N抽象lam F其中F是一个高阶函数表示带绑定的项类型规则如下cnst : num如果M : A - B且N : A那么app M N : B如果假设x : A时F x : B成立那么lam F : A - B4.2 定义类型和项第一步定义类型和项的类型族% typechecker.elpi % 类型定义 kind ty type. type num ty. type arr ty - ty - ty. % 项定义 kind tm type. type cnst tm. type app tm - tm - tm. type lam (tm - tm) - tm.kind ty type.引入新类型族ty。type num ty.定义类型常量num。type arr ty - ty - ty.定义函数类型构造器。kind tm type.引入tm类型族。type app tm - tm - tm.表示应用type lam (tm - tm) - tm.表示用高阶函数来保存抽象体。4.3 编写类型判断谓词接下来是核心的类型判断谓词type of tm - ty - prop. of cnst num. of (app M N) B :- of M (arr A B), of N A. of (lam F) (arr A B) :- pi x\ (of x A of (F x) B).逐行解释type of tm - ty - prop.声明of接收一个项和一个类型返回命题。of cnst num.表示常量的类型就是num。应用规则先检查函数类型是否为arr A B再检查参数类型是否为A。抽象规则引入新变量x假设of x A成立然后检查F x的类型是B。这里最值得体会的是第三条规则它没有像传统实现那样维护一个“符号表”而是用pi引入新局部变量用把它加入上下文。整个类型环境是隐式传递的。4.4 编写测试谓词为了让程序运行后能直接看到结果我们再加一个测试谓词type test_of_term tm - prop. test_of_term T :- of T Ty, print Term: T, print Type: Ty. main :- print Test 1: id , test_of_term (lam (x\ x)), print Test 2: const , test_of_term (lam (x\ cnst)), print Test 3: application , test_of_term (lam (x\ app (lam (y\ y)) x)).test_of_term接收一个项调用of得到类型然后打印项和类型。三个测试分别对应lam (x\ x)恒等函数期望类型为arr A A。lam (x\ cnst)忽略输入返回常量期望类型为arr A num。lam (x\ app (lam (y\ y)) x)λx. (λy.y) x期望类型为arr A A。4.5 运行与验证保存文件后运行elpi typechecker.elpi预期输出类似 Test 1: id Term: lam (c0 \ c0) Type: arr X0 X0 Test 2: const Term: lam (c0 \ cnst) Type: arr X0 num Test 3: application Term: lam (c0 \ app (lam (c1 \ c1)) c0) Type: arr X0 X0注意