Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Randy Pollack

LFCS Seminar: Randy Pollack

— filed under:

Viewing Lambda Terms Through Maps

  • LFCS Seminar
When Apr 18, 2013
from 02:00 PM to 03:00 PM
Where IF 4.31-33
Add event to calendar vCal


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 lambda-term. 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 of map terms, some discussion on the limitations of our current work, and suggestions for future work.


[Joint work with Sato, Schwichtenberg, and Sakurai]

Document Actions