解开 Landin 结的一个奇技
编程语言
2025-07-30 v1
摘要
在本文中,我们探讨 Landin 结——它被理解为一种编码一般递归(包括非终止性)的模式,该模式可在原本终止的语言中加入高阶引用后实现。我们观察到这并不总是成立——高阶引用本身并不会导致非终止性。其关键洞见在于:Landin 结主要并非依赖于存储函数的引用,而是依赖于对函数环境的非限制性量化。我们通过一个经闭包转换的语言展示了这一点:在该语言中,函数的环境被显式化,并通过非直谓量化隐藏了环境的类型。一旦加入引用,这种非直谓量化就可被利用来编码递归。我们猜想,通过限制对环境的量化,可以将高阶引用安全地加入终止语言中,既无需诉诸线性性等更复杂的类型系统,也不必限制引用存储函数的能力。
引用
@article{arxiv.2507.21317,
title = {One Weird Trick to Untie Landin's Knot},
author = {Paulette Koronkevich and William J. Bowman},
journal= {arXiv preprint arXiv:2507.21317},
year = {2025}
}