[kisoron-ml] Dr. Sylvain Salvati Lecture at NII Logic Seminar

[Makoto Tatsuta]

	 Dr. Sylvain Salvati Lecture at NII Logic Seminar

Date: October 31, 2012, 13:30--15:30

Place: National Institute of Informatics, Lecture Room 1208 (12th floor)
場所: 国立情報学研究所 12階 1208室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/introduce/access1-j.shtml)

Speaker: Dr. Sylvain Salvati (INRIA Bordeaux Sud-Ouest)

Title: Myhill-Nerode, Loader, Urzyczyn and logical relations

Abstract: 
When trying to define a notion of recognizability on languages over a
particular class of structures, it is customary to prove an
equivalence between a class of machines and congruences of finite
index on those structures.  Such equivalences can be coined as
"Myhill-Nerode theorems". This talk is going to be centered on such an
equivalence concerning languages of simply typed lambda-terms. Here
machines are type-checkers based on "uniform intersection types" and
finite index congruences are "extensional finite models" of the
lambda-calculus. The use of logical relations give a nice way of
proving that uniform intersection types and extensional finite models
allow to define exactly the same sets of lambda-terms. This result
relates two important results of the literature on lambda-calculus:
the undecidability of lambda-definability in finite standard models by
Loader (2001) and the undecidability of the inhabitation problem for
intersection types by Urzyczyn (1999). It shows in particular that
these two problems are turing-equivalent, and provides a refinement of
Urzyczyn's result. (Joint work with Giulio Mazonetto, Mai Gehrke and
Henk Barendregt)

問合せ先:
金沢 誠 (国立情報学研究所)
e-mail: kanazawa at nii.ac.jp