带 letrec 的 Lambda 演算中的最大共享

增加程序中的共享有利于压缩代码，并避免运行时归约工作的重复，从而加速执行。我们展示了如何为表示为带 letrec 的 lambda 演算项的程序获得最大程度的共享。我们在具有相同无限展开的所有项中，为 lambda-letrec-项引入了“最大紧凑性”的概念。该概念并非纯粹基于语法定义，而是基于图语义。lambda-letrec-项被解释为一阶项图，使得项之间的展开等价性通过项图解释的互模拟得以保持和反映。随后可以通过函数互模拟来比较项图的紧凑性。我们描述了针对以下两个问题的实用且高效的方法：将 lambda-letrec-项转换为最大紧凑形式；以及判定两个 lambda-letrec-项是否展开等价。将 lambda-letrec-项 $L$ 转换为最大紧凑形式 $L_0$ 的过程分为三步：(i) 将 $L$ 翻译为其项图 $G = [[ L ]]$；(ii) 计算 $G$ 的最大共享形式，即其互模拟坍缩 $G_0$；(iii) 从项图 $G_0$ 回读出一个具有性质 $[[ L_0 ]] = G_0$ 的 lambda-letrec-项 $L_0$。这保证了 $L_0$ 和 $L$ 具有相同的展开，且 $L_0$ 表现出最大共享。判定两个给定 lambda-letrec-项 $L_1$ 和 $L_2$ 是否展开等价的程序会计算它们的项图解释 $[[ L_1 ]]$ 和 $[[ L_2 ]]$，并检查这些项图是否互模拟。为便于说明，我们还提供了一个可直接使用的实现。