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