Agda のメモリ超過

別に Agda の限界を試しているつもりはないのだが

　　Agda interaction error: agda: Heap exhausted;
　　agda: Current maximum heap size is 3758096384 bytes (3584 MB).

3.5GBくらいごみだが、増やしてもおそらくは意味がない。なんかループしてるんだな。

この前、Model Checking 書いた時にも、別な無限ループくらってた。

型検査は基本的には Unification なんだけど、

　　NP Hard

だっていう論文を昔みたっけ。とりあえず、

　　なだめすかしながら

みたいな感じでやり過ごす予定です。結果は、プロシンで発表するはず。