Thumbnail
Access Restriction
Subscribed

Author Pitts, Andrew M.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2006
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Abstract syntax ♦ Binders ♦ Induction ♦ Names ♦ Recursion
Abstract The $\textit{nominal}$ approach to abstract syntax deals with the issues of bound names and α-equivalence by considering constructions and properties that are invariant with respect to permuting names. The use of permutations gives rise to an attractively simple formalization of common, but often technically incorrect uses of structural recursion and induction for abstract syntax modulo α-equivalence. At the heart of this approach is the notion of finitely supported mathematical objects. This article explains the idea in as concrete a way as possible and gives a new derivation within higher-order classical logic of principles of $α-\textit{structural}$ recursion and induction for α-equivalence classes from the ordinary versions of these principles for abstract syntax trees.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2006-05-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 53
Issue Number 3
Page Count 48
Starting Page 459
Ending Page 506


Open content in new tab

   Open content in new tab
Source: ACM Digital Library