A Canonical Locally Named Representation of Binding
A Canonical Locally Named Representation of Binding
复制标题
绑定的规范本地命名表示
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
W. Ricciotti
中科院分区：
文献类型：
--
作者：
R. Pollack;M. Sato;W. Ricciotti
本文研究具有约束的语言的完全形式化表示。我们之前已经写过一种表示，它遵循一种可以追溯到Frege的方法，基于一阶语法，针对局部绑定变量与全局或自由变量使用不同的语法类（Sato和Pollack，J SymbComput 45：598-616，2010）。本文不同于我们以前的工作，是更抽象。鉴于我们以前给出了一个特定的具体功能，规范选择的名称绑定器，在这里，我们抽象地描述了这样一个选择功能，以保证规范表示所需的属性，并专注于元理论的表示，证明它是在替代保持同构与名义伊莎贝尔表示纯lambda条款。这个元理论在Isabelle/HOL中正式化。最后一节概述了Matita中具有多重绑定和同时替换的具有挑战性的语言的形式化。Isabelle和Matita的证明文件可以在网上找到。
This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables (Sato and Pollack, J Symb Comput 45:598–616, 2010). The present paper differs from our previous work by being more abstract. Whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal Isabelle representation of pure lambda terms. This metatheory is formalized in Isabelle/HOL. The final section outlines a formalization in Matita of a challenging language with multiple binding and simultaneous substitution. The Isabelle and Matita proof files are available online.