名词性抽象
Nominal Abstraction
摘要：
递归关系规范通常用于描述形式系统的计算结构。最近的研究证明理论已经确定了两个功能，促进直接的，基于逻辑的推理这样的描述：通过递归定义的原子判断的解释和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑目前不允许定义体现与绑定相关的动态方面的关系，这是许多推理任务所需的能力。我们提出了一个新的术语之间的关系称为名义抽象作为克服这一缺陷的一种手段。我们将名义抽象到一个丰富的逻辑，也包括定义，通用量化，归纳，并共同归纳，然后我们证明是一致的。我们提出的例子表明，这种逻辑可以提供优雅的治疗绑定的情况下，出现在许多证明，如那些建立属性的类型演算和任意级联替代，在reductionalarguments中发挥作用。
英文摘要：
Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
