http://www.reed.edu/~carlislp/ghc6-doc/users_guide/rewrite-rules.html より GHC currently uses a very simple, syntactic, matching algorithm for matching a rule LHS with an expression. It seeks a substitution which makes the LHS and expressi…

さて、Sparkleでsortの正しさを証明しようと思った。めんどいので、isSortedという関数を用意して、"isSorted (sort ls)=True"を証明しようとしたのだけど、オーバーローディングが解決できません！とか怒られる(なお自前の関数を利用するには、.iclファイル…

何遍読んでもやっぱわかんね〜。そもそもどこがアルゴリズムで、どこが単なる原理の説明なのかすらよく分からんというダメっぷり。頭わり〜。とりあえず、何故abstract reductionが正しいのかという点はあまり悩まない方がいいかもしれない。abstract reduct…

・Preludeには変な関数がはいってるよな〜とか http://www.zvon.org/other/haskell/Outputprelude/index.html recipとか、(1/n)の方が短いし、いらないじゃんと思うけど、なんであるんだろう。readParenとか何する関数なのかもよくわからん ・昔のTemplate h…

Sparkleで証明できるにもかかわらず、Cleanでは正しくない命題の例。 forall n::Int.(n > 0)=>(n+1 > 0)何故ならCleanでIntは32ビット整数だから。