名称的生成解除绑定
Generative Unbinding of Names
摘要：
本文关注的是FreshML语言家族使用的类型化名称绑定的形式。它的典型特征是名称绑定由一个抽象的（名称，值）对表示，该抽象的（名称，值）对只能通过生成新的绑定名称来解构。本文证明了一个新的结果，什么操作的名称可以共存的这一结构。在FreshML中，人们对名称的唯一观察就是测试它们是否相等。这种有限的观察量被认为是必要的，以确保在α-等效名称粘合剂之间没有可观察到的差异。然而，从算法的角度来看，允许对名称的其他操作和关系是可取的，例如全排序。本文表明，与预期相反，人们可以添加不只是排序，但几乎任何关系或数值函数的名称，而不会干扰基本的正确性结果，这种形式的类型化名称绑定（即对象级阿尔法等价精确对应于上下文等价的编程元级），只要一个考虑到动态创建的名称的状态。
英文摘要：
This paper is concerned with the form of typed name binding used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation of fresh bound names. The paper proves a new result about what operations on names can co-exist with this construct. In FreshML the only observation one can make of names is to test whether or not they are equal. This restricted amount of observation was thought necessary to ensure that there is no observable difference between alpha-equivalent name binders. Yet from an algorithmic point of view it would be desirable to allow other operations and relations on names, such as a total ordering. This paper shows that, contrary to expectations, one may add not just ordering, but almost any relation or numerical function on names without disturbing the fundamental correctness result about this form of typed name binding (that object-level alpha-equivalence precisely corresponds to contextual equivalence at the programming meta-level), so long as one takes the state of dynamically created names into account.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
