[logic-ml] NUE seminar (34)

[Yoshihito Toyama]

                   第 34 回 NUEセミナーのお知らせ

東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています。
テーマはプログラム理論や定理自動証明を中心に、情報科学の理論的なさまざ
まな話題をとりあげています。興味をおもちの方はどなたでもフラリと気楽に
おたちより下さい。
 
      *********************************************
 
 日時： 　１０月２９日（火） １３：３０ -- １４：３０
  
 場所：   東北大学・電気通信研究所・２号館・２階 セミナー室 (W214)
 
      *********************************************

講演 

話題提供者： Vincent van Oostrom (Utrecht University)

題目：   Z   Syntax-Free Developments

概要： We introduce the Z-property for abstract rewriting systems, and
 show that it can be used to prove confluence of several well-known
 term rewrite systems (terminating or not, and overlapping or not), in
 particular:

 - the applicative TRS for associativity: (xy)z -> x(yz);

 - the applicative TRS for self-distributivity: (xy)z -> xz(yz);

 - lambda-calculus with beta-reduction: (\x.M)N -> M[x:=N].

 Turning to meta-theoretical properties, we first show that the
 Z-propery allows to recover the traditionally syntactically defined
 notion of (super)development/multistep in a syntax-free way. To that
 end, we show the equivalence between the Z-property and Takahashi's
 angle-property.  Next, we showing that the Z-property not only
 entails confluence, but also the existence of a hyper-cofinal
 strategy.
 
 We conclude by presenting further (non-)examples of rewrite systems
 having the Z-property, and some open questions.

 (joint work with Patrick Dehornoy)

==============================================

 NUEセミナーに関する問い合わせは以下にどうぞ。

    外山 芳人

    〒980-8577 仙台市 青葉区 片平 2-1-1
               東北大学 電気通信研究所

        TEL  022 217 5449
        FAX  022 217 5452
        MAIL toyama at nue.riec.tohoku.ac.jp