モノイドの左逆元・右逆元(3)
前回のプログラムの動作を確認するため
「以下の Python のコードは、「モノイドの左逆元と右逆元が一致する」ことを示す式の変形を表示するものです。proof_transformation で path を指定して調べる範囲を限定すると停止するのですが、path を指定しない場合は停止するかどうかわかりません。停止するかどうかを調べる方法はありますか」
「アサーションを追加して調べることはできますか」
「すべてのアサーションが成功した場合、停止することを証明できますか」
「現在は step_max は必ず指定してこの回数で終了するようになっていますが、step_max は指定しなくてもよいとして、指定しないときは無限の回数実行されるとしてください(このようにコードが変更されているとしてください)。この状態のコードで無限の回数実行する(step_max を指定しない)とき、path を(正しく)指定したときは停止すると仮定してください。このとき、無限の回数実行するコード(step_max を指定しない)で、path を指定しない場合、停止することが証明できるようにさらにアサーションを追加してください。」
「このプログラムは以前は deque で実装されていました。このとき deque に追加した式の中で読み出されないものがあるため無限に実行される(のではないか)という現象が起こっていました。現在このプログラムはこれをリストで書き換えています。このような現象が起こらないことを確認するため
- リストに追加した式は本当に追加されている
- リストに入っている式はいつか必ず読み出すことができる
ということを確認するためのアサーションを追加してください。」
と入力すると、アサーションを追加してくれたのですが、動作が確認できるようにはなりませんでした。
「証明できる等式を入力したとき停止する」ことを示すためのアサーションはどうすれば良いか、今後検討してみます。
