Stack Over Flow

[ken.coba]

小林です。

毎度毎度でほんとに申し訳ないです・・・

"Programming Language Theory
and its Implementation"
Michael J.C. Gordon

を読んで、Chapter10にある
Simple Theorem Prover
をClojureで実装してみました。

https://gist.github.com/823632

だいたい動いたなーと思ったんですが、
prove関数でちょっとした証明を入力すると
StackOverFlowが出てしまいます。
; ソースコード中、最後のテストケースtest-proveでも出ます。

もし原因が分かる方いらっしゃいましたら
お教えいただけるとありがたいです。

あと、毎度のことですが「これはイケてない」
という箇所のご指摘いただけるとありがたいです。

[Takahiro]

こんばんは。
rewrite1内のprewalk-replaceでツリーがどんどん膨らんでスタックオーバーフローしてるみたいです。
(cw/prewalk-replace '{Z ((X + N) = ((((N + 1) - 1) * (N + 1)) DIV 2)),
Y ((1 <= N) and (N <= M)),
X (X = (((N - 1) * N) DIV 2))}
'(((X and Y) implies Z) = (X implies (Y
implies Z))))

2011年2月12日21:43 ken.coba <ken....@gmail.com>:

[ken.coba]

Takahiroさん
小林です。

ありがとうございます。そっちのほうでしたか・・・
私はてっきり、matchfnの後ろの再帰のせいかと。
また調べてみます。しかしprewalk内でオーバーフローされるのでは、
別の方法を考えるしかないのか。

この手のプログラムを作っていて思うのは、
1.matchfnのように枝分かれする再帰を再帰なしにする方法はないのか
(matchfnは再帰の引数に再帰呼び出しが入っているのです)
2.スタックオーバーフローの原因がここだ！って分かる上手い方法はないのか
ってことです。

どなたか、ヒントとか資料へのポインタでもご存じでしたら
お教えいただけるとありがたいです。

On 2月12日, 午後11:31, Takahiro <fat...@googlemail.com> wrote:
> こんばんは。
> rewrite1内のprewalk-replaceでツリーがどんどん膨らんでスタックオーバーフローしてるみたいです。
> (cw/prewalk-replace '{Z ((X + N) = ((((N + 1) - 1) * (N + 1)) DIV 2)),
> Y ((1 <= N) and (N <= M)),
> X (X = (((N - 1) * N) DIV 2))}
> '(((X and Y) implies Z) = (X implies (Y
> implies Z))))
>

> 2011年2月12日21:43 ken.coba <ken.c...@gmail.com>:

[Takahiro]

こんばんは。
>しかしprewalk内でオーバーフローされるのでは、別の方法を考えるしかないのか。
prewalk-replace はトップダウンに根から置換が走り、置換後の要素に対しても置換が走るみたいなので
X を (X = (((N - 1) * N) DIV 2)) に置き換えると無限ループになってしまいます。
postwalk-replace はボトムアップな置換で葉から置換していくのでこっちでいいのではないでしょうか。
prewalk/postwalkの動作はかなり分かりにくいですね。

> 2.スタックオーバーフローの原因がここだ！って分かる上手い方法はないのかってことです。
(require '[clojure.contrib.trace :as trace])
(eval `(trace/dotrace ~(keys (ns-interns 'prover)) デバッグしたい式))
がなかなかいい感じです。
今回の場合だと
(eval `(trace/dotrace ~(keys (ns-interns 'prover)) (test-prove)))
ですね。
https://gist.github.com/825982

2011年2月14日21:51 ken.coba <ken....@gmail.com>:

[ken.coba]

Takahiroさん
小林です。

ありがとうございますー。
とりあえずStackoverflowは回避できました。
本当のところ、この変換で正しいかは検算します。

デバッグ技法もマスターせねば・・・。
ありがとうございました。

On 2月15日, 午前12:00, Takahiro <fat...@googlemail.com> wrote:
> こんばんは。>しかしprewalk内でオーバーフローされるのでは、別の方法を考えるしかないのか。
>
> prewalk-replace はトップダウンに根から置換が走り、置換後の要素に対しても置換が走るみたいなので
> X を (X = (((N - 1) * N) DIV 2)) に置き換えると無限ループになってしまいます。
> postwalk-replace はボトムアップな置換で葉から置換していくのでこっちでいいのではないでしょうか。
> prewalk/postwalkの動作はかなり分かりにくいですね。
>
> > 2.スタックオーバーフローの原因がここだ！って分かる上手い方法はないのかってことです。
>
> (require '[clojure.contrib.trace :as trace])
> (eval `(trace/dotrace ~(keys (ns-interns 'prover)) デバッグしたい式))
> がなかなかいい感じです。
> 今回の場合だと
> (eval `(trace/dotrace ~(keys (ns-interns 'prover)) (test-prove)))
> ですね。https://gist.github.com/825982
>

> 2011年2月14日21:51 ken.coba <ken.c...@gmail.com>: