[logic-ml] Talk by Masahiko Sato, 14 Nov. Thu 11:00-

[Shinya Katsumata]

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

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.