著者

高橋 祐多 中野 圭介

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.4, pp.52-71, 2018-10-25 (Released:2018-12-26)

---

一般に関数の等価性判定問題は決定不能であるが,関数の定義に構文的な制約を加えることで決定可能にすることができる. そのような制約の 1 つとして,木から文字列への決定性トップダウン変換(deterministic top-down tree-to-string transducer,yDT)が存在し, 等価性判定が決定可能な関数としては,比較的広い範囲のものを扱うことができる. この yDT の等価性判定の決定可能性は 2015 年に Seidl らによって示されたが,2 つの半アルゴリズムを組み合わせることによって証明されており, 計算量が特定できず,実用性が確認されていない. そこで,本論文では yDT の等価性判定を行うプログラムを実装し,Seidl らの等価性判定アルゴリズムが実用に堪えうるものか検証する.