名称的生成式解绑
编程语言
2015-07-01 v2 计算机科学中的逻辑
摘要
本文关注 FreshML 系列语言所使用的类型化名称绑定形式。其特征是名称绑定由抽象的 (名称，值) 对表示，且仅能通过生成新鲜绑定名称进行解构。本文证明了关于哪些名称操作可以与该构造共存的新结果。在 FreshML 中，对名称唯一的观察是测试它们是否相等。这种受限的观察量被认为对于确保 alpha 等价名称绑定之间没有可观察差异是必要的。然而，从算法角度来看，允许对名称进行其他操作和关系（如全序关系）是可取的。本文表明，与预期相反，只要考虑到动态创建名称的状态，不仅可以添加序关系，还可以添加几乎任何关于名称的关系或数值函数，而不会破坏这种类型化名称绑定形式的基本正确性结果（即对象级 alpha 等价精确对应于编程元级的上下文等价）。
引用
@article{arxiv.0801.1251,
title = {Generative Unbinding of Names},
author = {Andrew M. Pitts and Mark R. Shinwell},
journal= {arXiv preprint arXiv:0801.1251},
year = {2015}
}