Viewing Λ-Terms Through Maps

In this paper we introduce the notion of map, which is a notation for the set of occurrences of a symbol in a syntactic expression such as a formula or a lambda term. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable in HOL or Constructive Type Theory) and canonical (one representative per lambda term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic lambda terms and de Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively.The map representation has good properties. Substitution does not require adjustment of binding information: neither alpha conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of lambda calculus that requires no fresh names, or index manipulation.Using the notion of map we study conventional raw lambda syntax. E.g. we give, and prove correct, a decision procedure for alpha equivalence of raw lambda terms that does not require fresh names.We conclude with a definition of beta reduction for map terms, some discussion on the limitations of our current work, and suggestions for future work. (C) 2013 Royal Dutch Mathematical Society (KWG). Published by Elsevier B.V. All rights reserved.