### Alpha-structural recursion and inductionAlpha-structural recursion and induction

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

Source: ACM Digital Library