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: [email protected]