2021-02-13
軽い気持ちで証明に手を付けたらルーズリーフ2枚くらいになって泣いてしまった
疲れたのでReduceNatExpを書く
ReduceとDReduceまでは簡単に書けたが、MReduceで手が止まった
どちらも「一回しか簡約されない」という制約が付いてるから、木の右と左を見て、違うところを追っていけばいい
複数回簡約が可能、ということは複数回の簡約に分解する処理が必要なのだけれど、分解された簡約は分解元と該当する簡約部分を除いて一致していないといけない
これは手でやる分にはそこまで困らないんだけど、再帰で構造を下っていって処理する場合問題になる
散々考えた結果、部分問題の導出木を元の問題に対して「持ち上げる」操作を実装して対処することにした
n1 + n2 -*-> n3みたいな自明なケースを解いて、e1 + (n1 + n2) -*-> e1 + n3に組み込む
数値で終わる複数回簡約は通るようになった。それ以外はダメ
1+1+1=1+2を示せない
機械に結合法則を教えないとダメらしい
(e1+e2)+e3 -*-> e1+eのときe1+(e2+e3) -*-> e1+e
1+1+1+1=2+2を示せない
((1+1)+1)+1=2+2
結合法則をより正確に教えることで(同値であることを教えた)大筋は解けるようになったが、微妙なチェックで落ちるようになった
演習システムのほうが結合法則を知らない
カッコを正規化すると通るようになるが、その操作によって今まで通っていた導出が間違いになるので、MR-One以下の導出を全部やり直すようにするとたぶん解ける