コンピュータサイエンス研究会

2011.02.07

研究会名：コンピュータサイエンス研究会
開催日：2011年2月7日（月）13:30～15:30
題目：“Labelings for Decreasing Diagrams”
講師：Harald Zankl氏(University of Innsbruck)
開催場所：電気通信研究所2号館W410号室

コンピュータサイエンス研究会　講演会の御案内

コンピュータサイエンス研究会
主査篠原　歩

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので，ご案内申し上げます．

日時：2011年2月7日（月）13:30～15:30
場所：電気通信研究所2号館W410号室
題目：“Labelings for Decreasing Diagrams”
講師：Harald Zankl (University of Innsbruck)
概要：This talk is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We build on recent work (van Oostrom 2008), (Aoto 2010), and (Hirokawa and Middeldorp 2010) and study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the paper have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.