LFCS Seminar: Randy Pollack
Viewing Lambda Terms Through Maps
What 


When 
Apr 18, 2013 from 02:00 PM to 03:00 PM 
Where  IF 4.3133 
Add event to calendar 
vCal iCal 
Abstract:
In this paper we introduce the notion of map, which is a notation for occurrences of a symbol in a syntactic expression such as a formula or a lambdaterm. 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 lambdaterm). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic lambdaterms 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 alphaconversion 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 alphaequivalence of raw lambda terms that does not require fresh names.
We conclude with a definition of betareduction of map terms, some discussion on the limitations of our current work, and suggestions for future work.
[Joint work with Sato, Schwichtenberg, and Sakurai]