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

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

扫码查看
原文链接
  • 万方数据
  • 维普
编程语言、类型系统和逻辑系统中常见的命名绑定,在实践中实现存在困难.在理论中以抽象思考发现并避免即将发生的变量捕获.在实践中变量捕获的检测需要定义笨拙的辅助操作,使形式化和证明变得复杂.现有几种命名绑定技术旨在表达式具有良好的可读性,无变量捕获的代换操作和直观的证明.然而,这些技术的形式化与理论之间存在差别,两者的表达式和证明过程可能有很大的不同.提出一种命名绑定技术,其中在代换操作和推理规则中引入的表达式刷新函数使形式化遵守Barendregt的变量约定,形式系统的形式化与其理论几乎相同.以无类型λ-演算和具有简单数据类型的λ-演算的形式化展示了该技术的优点.
A study of formalizing programming languages with Barendregt's variable convention
Implementing name bindings occurring in programming languages,types,and logical sys-tems is not easy.In theory,the abstract thinking of the human mind can detect and avoid a possible var-iable capture.In implementation though,detecting variable capture requires clumsy auxiliary opera-tions,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 Barendregt's 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.

variable namename bindingformal systemBarendregt's variable conventionprogram-ming language theory

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

展开 >

新疆财经大学信息管理学院,新疆乌鲁木齐 830000

新疆财经大学统计与数据科学学院,新疆乌鲁木齐 830000

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

国家自然科学基金国家自然科学基金新疆维吾尔自治区自然科学基金新疆财经大学校级科研基金新疆财经大学校级科研基金新疆财经大学校级科研基金

62241208619660332023D01A722022XGC0492022XGC0702022XGC022

2024

10.3969/j.issn.1007-130X.2024.10.009

计算机工程与科学
国防科学技术大学计算机学院

计算机工程与科学

CSTPCD北大核心
影响因子：0.787
ISSN：1007-130X
年,卷(期)：2024.46(10)