京都大学数理解析研究所の勝股です。

11月14日11:00から、佐藤雅彦 京都大学名誉教授に 以下の講演をしていただくことになりましたので、 ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 14 Nov, 2013 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/main.htm (See 34) 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)

Speaker: Professor Emeritus Masahiko Sato

Title: Viewing lambda terms through maps (Joint work with Randy Pollack, Helmut Schwichtenberg and Takafumi Sakurai)

Abstract: In this talk 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) 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.