关于 Lambda 项的唯一可闭与唯一可类型化骨架
编程语言
2017-09-14 v1
摘要
Lambda 项的唯一可闭骨架是 Motzkin 树，其通过用 de Bruijn 索引标记叶子预先确定可获得的唯一闭 Lambda 项。类似地，闭 Lambda 项的唯一可类型化骨架通过用 de Bruijn 索引标记叶子预先确定可获得的唯一简单类型化 Lambda 项。我们通过一系列逻辑程序变换，推导出用于其组合生成的高效代码，并研究其统计性质。结果，我们获得了描述 Lambda 项可闭和唯一可闭骨架的上下文无关文法，为使用解析组合学工具进行深入研究打开了大门。我们对更困难的（唯一）可类型化项案例的经验研究揭示了关于其密度和渐近行为的一些有趣开放问题。作为两类项之间的联系，我们还展示了大小为 的唯一可类型化闭 Lambda 项骨架与大小为 的二叉树之间存在双射。
引用
@article{arxiv.1709.04302,
title = {On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms},
author = {Olivier Bodini and Paul Tarau},
journal= {arXiv preprint arXiv:1709.04302},
year = {2017}
}
备注
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)