[kisoron-ml] Prof. Jean-Pierre Jouannaud at NII Logic Seminar

[Makoto Tatsuta]

	   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 at nii.ac.jp
http://research.nii.ac.jp/~tatsuta