Prof. Jean-Pierre Jouannaud at NII Logic Seminar
Date: April 7, 2014, 14:00--16:00
Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Jean-Pierre Jouannaud (Tsinghua University and Ecole Polytechnique)
Title: Confluence by critical pair analysis
Abstract: Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. In this paper, we show that this is still true of a rewrite system RT union RNT such that RT is terminating and RNT is a left-linear, rank non-increasing, possibly non-terminating, rewrite system: confluence can then be reduced to the joinability of the critical pairs of RT and to the existence of decreasing diagrams for the critical pairs of RT inside RNT, as well as for the parallel critical pairs of RNT. Since left-linearity and rank non-increasingness are easily decided in linear time, implementing our test in a system like CSI (Innsbruck) should require little effort for a wide benefit. We believe that this applies to higher-order systems as well. Further, we shall discuss an old open problem of Huet in the form of a non-terminating, non-confluent, critical pair free rewrite system, and will show that it has a "hidden critical pair" which joinability (if it were joinable) would imply its confluence. This is a joint work with Jiaxiang Liu.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: tatsuta@nii.ac.jp http://research.nii.ac.jp/~tatsuta