AI 中文总结
研究为带显式替换的演算定义新项展开，以此关联带显式替换的lambda演算与Boudol的带多重性的资源感知lambda演算，函数参数可用性或受限，核心方法是新项展开，主要贡献是建立了这种关联。
AI 中文摘要
项展开最初于2004年被引入，作为一种关联交集类型系统中类型化项与线性项的方式。近期，项展开有了新应用，如关联lambda项与其他子结构类型系统中类型化项，以及用定量类型关联强规范化lambda项与具有相同范式的弱线性项。本文为带显式替换的演算定义了新的项展开，用于关联带显式替换的lambda演算与Boudol的带多重性的资源感知lambda演算，其中函数参数可用性可能受限。
英文摘要
Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 19-35
