ソフトウェア概要
Term Rewriting System (TRS)のなかで主要なアルゴリズム（多分）である， Unification，Critical Pair，CompletionをFlashで実装したものです． 私はTRSの専門家ではないので，本当に正しく実装されているかどうかはアレです．
デモ
使い方
画面は３つあります．Unificationのデモ，Critical Pairのデモ，Completionのデモです． 画面上のバーの名前をクリックすることで，それぞれの画面に遷移することができます．
右側には，関数入力フィールドと，各種コマンドがあります． 関数入力フィールドには，関数名とその引数の数をコンマ区切りで記述します． "+,2"という行は，+関数は2つの引数を取ると言う意味です． コマンドは，update，next，exec, clearの４つあります． updateは，画面状態を更新するときに用います． nextは，サンプルがあれば次のサンプルを入力します． execは，各アルゴリズムを実行します． clearは，画面を初期化します． なお，execコマンドを実行する前は，かならずupdateコマンドを実行してください．
なお，各関数式は，前置記法を取っています．
Unification
Unificationを実行する画面です． 左，右，下と３つのパートに分かれています． 左と右は，Unificationを行う二つの関数式および木が表示されます． 下は，Unificationの結果が表示されます．
木のノードをクリックすることで，対応する部分木がオレンジ色で表示されます．
Critical Pair
Critical Pairを求める画面です． 左，右，下の３つのパートに分かれています． 左はCritical Pairの元のペアです． 右は結果です． 下は，選択されているRewriting Ruleの木を表示します．
なお，現状では式の編集はできません．
Completion
Completionを実行する画面です． 左，右，下の３つのパートに分かれています． 左は元のRewriting Rule群です． 右はCompletionされたRewriting Rule群です． 下は，選択されているRewriting Ruleの木を表示します．
なお，現状では式の編集はできません．
動作環境
- Flash Player 7以上がインストールされている環境
ダウンロード
swfファイル単体と，ソースコード一式を置いておいたので，欲しい方は適当にダウンロードしてください． なお，FlashMX 2004で開発しましたので，それ以外で読み込めるかどうかは分かりません．
既知のバグ
Cricical Pair内の，関数合成が怪しい動作をします． そのため，ときどき変な結果を返します． よって，Completionも変な結果が混ざっています． ようするに，バグ．
注意事項
本ページで配布しているプログラムにより発生したいかなる損害も，私は責任を負いません． swfファイルの再配布は自由とします． ソースコード一式をダウンロードし，改変した後に，公開することも自由とします． ただし，先の行為により発生したいかなる問題や損害も，私は責任を負いません．