带De Bruijn指标的Beta范式在限制交型系统中的主类型
Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
摘要：
带有de Bruijn索引的Alzida演算将Alzida项的每个alpha类集合到一个唯一项中，使用索引而不是变量名。交集类型提供有限类型多态性，并且可以通过当且仅当一个项是可类型化的时才可规范化的属性来规范化可规范化的交集项。为了更接近计算，并简化beta压缩中原子操作的形式化，几个显式替换演算主要是用de Bruijn指数开发的。没有类型和简单类型系统的显式替换演算的版本与更复杂的类型系统（如交集类型）的版本相比，得到了很好的研究。在以前的工作中，我们介绍了一个de Bruijn版本的交叉类型系统的Adjuda演算，并证明了它保持主题约简，类型系统的基本属性。本文提出了一个具有de Bruijn指标的交型系统，它最初被引入到Beta-范式的主类型化中。我们提出了在这个新的系统和相应的版本的类型推断和重建的范式从主要类型算法的特点。我们简要讨论了主体归约性质的失效和可能的解决方案。
英文摘要：
The lambda-calculus with de Bruijn indices assembles each alpha-class of lambda-terms in a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism and can characterise normalisable lambda-terms through the property that a term is normalisable if and only if it is typeable. To be closer to computations and to simplify the formalisation of the atomic operations involved in beta-contractions, several calculi of explicit substitution were developed mostly with de Bruijn indices. Versions of explicit substitutions calculi without types and with simple type systems are well investigated in contrast to versions with more elaborate type systems such as intersection types. In previous work, we introduced a de Bruijn version of the lambda-calculus with an intersection type system and proved that it preserves subject reduction, a basic property of type systems. In this paper a version with de Bruijn indices of an intersection type system originally introduced to characterise principal typings for beta-normal forms is presented. We present the characterisation in this new system and the corresponding versions for the type inference and the reconstruction of normal forms from principal typings algorithms. We briefly discuss the failure of the subject reduction property and some possible solutions for it.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
