A New Approach to Abstract Syntax with Variable Binding |
| |
Authors: | Murdoch J Gabbay Andrew M Pitts |
| |
Affiliation: | (1) Cambridge University Computer Laboratory, Cambridge, UK, GB |
| |
Abstract: | The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions
of ‘name-abstraction’ and ‘fresh name’ that provide a new way to represent, compute with, and reason about the syntax of formal
systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together
with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the
standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular,
there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding
substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly
close to informal practice in computer science.
Received October 2000 / Accepted in revised form April 2001 |
| |
Keywords: | : Abstract syntax Alpha-conversion Permutation actions Set theory Structural induction |
本文献已被 SpringerLink 等数据库收录! |
|