第 34 回 NUEセミナーのお知らせ
東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています。
テーマはプログラム理論や定理自動証明を中心に、情報科学の理論的なさまざ
まな話題をとりあげています。興味をおもちの方はどなたでもフラリと気楽に
おたちより下さい。
*********************************************
日時: 10月29日(火) 13:30 -- 14:30
場所: 東北大学・電気通信研究所・2号館・2階 セミナー室 (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(a)nue.riec.tohoku.ac.jp