A Canonical Local Representation of Binding
A Canonical Local Representation of Binding
复制标题
绑定的规范局部表示
DOI：
10.1007/s10817-011-9229-y
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Randy Pollack
中科院分区：
文献类型：
--
作者：
藤浦祥雅;大久保弘崇;粕谷英人;山本晋一郎;Randy Pollack
本文研究了带绑定的语言的完全形式化表示。我们之前已经写过一种可以追溯到弗雷格的表示，基于一阶语法，对局部绑定变量与全局变量或自由变量使用不同的语法类（Sato和Pollack， J Symb computer 45:598-616, 2010）。这篇论文与我们以前的工作不同，它更抽象。鉴于我们之前给出了一个特定的具体函数来规范地选择绑定器的名称，这里我们抽象地描述了这种选择函数保证规范表示所需的属性，并关注该表示的元理论，证明它与纯lambda项的名义伊莎贝尔表示保持替换同构。这个元理论在Isabelle/HOL中被形式化了。最后一节概述了一种具有多重绑定和同时替换的具有挑战性的语言在matta中的形式化。伊莎贝尔和玛蒂塔的证明文件可以在网上找到。
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.