以Barendregt的变量约定形式化编程语言研究

来源：计算机工程与科学杂志2024年第10期北京时间：

作者：阿力木江·亚森, 艾合买提·阿不来提, 沙尔旦尔·帕尔哈提, 阿布都克力木·阿布力孜, 哈里旦木·阿布都克里木

单位：1.新疆财经大学信息管理学院，新疆 乌鲁木齐 830000；2.新疆财经大学统计与数据科学学院，新疆 乌鲁木齐 830000

摘要：编程语言、类型系统和逻辑系统中常见的命名绑定，在实践中实现存在困难。在理论中以抽象思考发现并避免即将发生的变量捕获。在实践中变量捕获的检测需要定义笨拙的辅助操作，使形式化和证明变得复杂。现有几种命名绑定技术旨在表达式具有良好的可读性，无变量捕获的代换操作和直观的证明。然而，这些技术的形式化与理论之间存在差别，两者的表达式和证明过程可能有很大的不同。提出一种命名绑定技术，其中在代换操作和推理规则中引入的表达式刷新函数使形式化遵守Barendregt的变量约定，形式系统的形式化与其理论几乎相同。以无类型λ-演算和具有简单数据类型的λ-演算的形式化展示了该技术的优点。

关键词：变量命名,命名绑定,形式系统,Barendregt的变量约定,编程语言理论,

基金资助：国家自然科学基金（62241208，61966033）;新疆维吾尔自治区自然科学基金（2023D01A72）;新疆财经大学校级科研基金（2022XGC049，2022XGC070，2022XGC022）