Term Rewriting Based On Set Automaton Matching

要約

タイトル：セットオートマトンマッチングに基づく用語書き換え
要約：
– サブタームパターンマッチングアルゴリズムを使用して、効率的な用語書き換え手順を実装する方法を調査しています。
– 書き換えシステムの左辺から、セットオートマトンを構築し、用語内のすべてのredexes（再帰的な部分式）を効率的に見つけることができます。
– 書き換え戦略が与えられた場合、パターンマッチングステップと書き換えステップを交互に挿入して、redexの発見とサブタームの置換をスムーズに統合する手順を形式的に説明します。
– 外部最上位の書き換えにこの手順を具体化した効率的な実装を提示し、いくつかの実験の結果を示します。
– 私たちの実装は、同様のツールと競争力があることが示されています。

要約(オリジナル)

In this article we investigate how a subterm pattern matching algorithm can be exploited to implement efficient term rewriting procedures. From the left-hand sides of the rewrite system we construct a set automaton, which can be used to find all redexes in a term efficiently. We formally describe a procedure that, given a rewrite strategy, interleaves pattern matching steps and rewriting steps and thus smoothly integrates redex discovery and subterm replacement. We then present an efficient implementation that instantiates this procedure with outermost rewriting, and present the results of some experiments. Our implementation shows to be competitive with comparable tools.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI