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.
关键词
变量命名/命名绑定/形式系统/Barendregt的变量约定/编程语言理论
Key words
variable name/name binding/formal system/Barendregt's variable convention/program-ming language theory
维普
万方数据