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

A study of formalizing programming languages with Barendregt’s variable convention

作　　者：阿力木江·亚森 艾合买提·阿不来提 沙尔旦尔·帕尔哈提 阿布都克力木·阿布力孜 哈里旦木·阿布都克里木 ALIMUJIANG Yasen;AIHEMAITI Abulaiti;SHAERDANER Paerhati;ABUDUKELIMU Abulizi;HALIDANMU Abudukelimu(College of Information Management,Xinjiang University of Finance&Economics,Urumqi 830000;Institute of Statistics and Data Science,Xinjiang University of Finance&Economics,Urumqi 830000,China)

机构地区：[1]新疆财经大学信息管理学院,新疆乌鲁木齐830000 [2]新疆财经大学统计与数据科学学院,新疆乌鲁木齐830000

出　　处：《计算机工程与科学》2024年第10期1807-1814,共8页Computer Engineering & Science

基　　金：国家自然科学基金(62241208,61966033);新疆维吾尔自治区自然科学基金(2023D01A72);新疆财经大学校级科研基金(2022XGC049,2022XGC070,2022XGC022)。

摘　　要：编程语言、类型系统和逻辑系统中常见的命名绑定,在实践中实现存在困难。在理论中以抽象思考发现并避免即将发生的变量捕获。在实践中变量捕获的检测需要定义笨拙的辅助操作,使形式化和证明变得复杂。现有几种命名绑定技术旨在表达式具有良好的可读性,无变量捕获的代换操作和直观的证明。然而,这些技术的形式化与理论之间存在差别,两者的表达式和证明过程可能有很大的不同。提出一种命名绑定技术,其中在代换操作和推理规则中引入的表达式刷新函数使形式化遵守Barendregt的变量约定,形式系统的形式化与其理论几乎相同。以无类型λ-演算和具有简单数据类型的λ-演算的形式化展示了该技术的优点。Implementing name bindings occurring in programming languages,types,and logical systems is not easy.In theory,the abstract thinking of the human mind can detect and avoid a possible variable capture.In implementation though,detecting variable capture requires clumsy auxiliary operations,which complicates formalization and proofs.Several name binding techniques have been proposed to have readable representations,capture-free substitutions,and intuitive proofs.However,their formalizations are quite different from theory:terms and proofs do not look like of theory.This paper proposes a name binding technique,substitutions and inference rules incorporating a term refreshing function comply with Barendregts variable convention,thus the formalization of formal systems almost identical to their theory.Untypedλ-calculus and simply typedλ-calculus are formalized to demonstrate the merits of this technique.

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

分 类 号：TP313[自动化与计算机技术—计算机软件与理论]