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 λλ 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 λλ term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic λλ 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 αα 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 λλ calculus that requires no fresh names, or index manipulation.Using the notion of map we study conventional raw λλ syntax. E.g. we give, and prove correct, a decision procedure for αα equivalence of raw λλ terms that does not require fresh names.We conclude with a definition of ββ reduction for map terms, some discussion on the limitations of our current work, and suggestions for future work.