■
証明からプログラムを抽出するという研究は、そこそこ昔からあるらしい(し、Coqなんかで実際に実装されてもいる)けど、逆はないのかな。あんまし原理的なことが理解できてないんで、あれなんだけども、formal proof書くのは、プログラム書くのの500倍(当社比)大変なので、やっぱ証明からプログラムを生成するという方向は、何か根本的にダメな気がする。まあ、今のproof assistantがしょぼすぎるという側面はあるのかもしれないが
■
http://alohakun.blog7.fc2.com/blog-entry-614.html
この日記のタイトルは、半角スペースかなんかだった記憶が。こことかで、ソース見ると、ちゃんと半角スペースになってるような。というわけで、ノータイトルじゃないんです＞＜
>L.L. Ring
そ･･･それくらいはすけるも一行で
import Data.Char;main=readFile "bloglist.dat">>=print.(\l->[x|x<-take 50 l,elem x$drop 50 l]).map(takeWhile(not.isDigit).snd.head.lex).lines
無理すぎるorz
型
主にSparkleのソースを読むときに、型の表記がよくわからんのがキモイということで調べた。他はまあ、Haskell分かれば、(書けるかどうかは知らんが)とりあえず、読めるかな〜と
・基本型
Int,Bool,Char,Real
・一意型
型の前に、*を付けると一意型。一意型はよーわからんが、線形型に於けるexponentialの逆みたいなもん。一意型の変数は一回しか使えないらしい
・属性変数
id:: u:a -> u:aみたいなやつ。よく分からんが、idの引数の型が一意型(つまり、*a)の場合は、返り値も一意型*aで、非一意型(普通の型)aの場合は、返り値も、非一意型aだというのを表すのに使うらしい。idの場合は、別に、引数の型と返り値の型は一緒なので、id:a->aでいい気もするけどダメなのかな。hoge:: u:pnya -> u:pnyiみたいなケースだと、こういうのないと困るよね〜と
・無名属性変数
名前の通り。u:aと書く代わりに、型の前にドットを付けた.aとかいうやつ。可読性をあげるとか書いてあるが、却ってややこしい気が
・正格性注釈
!を付けると、その引数について、正格に評価するようにコンパイラに指示できるらしい。Libraries/StdEnv/StdList.iclより例
hd::![.a] -> .a hd [a:x] = a hd [] = abort "hd of []"
・型クラス
Libraries/StdEnv/StdList.iclより例
sum:: !.[a] -> a | + , zero a sum xs = accsum xs zero where accsum [x:xs] n = accsum xs (n + x) accsum [] n = n
zeroと+は型クラス名で、型aがこの二つの型クラスのinstanceであるという制約を表している。Haskell風に書くと、"sum::(+ a , zero a)=>!.[a]->a"みたいな感じかな。
参考にしたサイト
http://www.geocities.jp/lethevert/clean/gettingStarted15.html
http://sky.zero.ad.jp/~zaa54437/programming/clean/LanguageReport21/Chap9.html#sc1
http://www.geocities.jp/lethevert/clean/gettingStarted12.html
http://d.hatena.ne.jp/m-a-o/20070106#p3で、sumはstrictness analysis外しても問題なく動くな〜って書いたけど、正格性注釈のおかげっぽい。にしても、一意型とか属性変数とかが、複雑に絡んでくると、頭が混乱するんだけど、これは慣れなのか
まとめ:CleanのコードをHaskellに移植するときは、型クラス以外はどうでもいい
レッスン2
Coqとかに比べて、Sparkleユーザって、世界に10人くらいしかいなそうなので(いや知らんけどね)、なんかもうナンバー1よりオンリー1って感じだよな〜(何が
一応マニュアルっぽいものはあった。マニュアルというには、アレだが
http://www.cs.kun.nl/~marko/research/sparkle/sparklesheet.pdf
Property language syntaxが、定理を入力する時に重要。このへんもCoqっぽい
http://www.possibly.me.uk/notes/sparkle.shtml
私の中でよくある疑問
・整数型とか、実数型とかはinductiveなデータ構造でないので、帰納法は使えないんでないの？まあ、整数の方はどうとでもなるか。でも、自然数型はないので、そのへん色々あれだよな〜→実数は不明。てかまあ無理だろ、常識的に考えて。整数型に対して、induction使うと、n=0,n<0,n>0,n=bottomの4つの場合のサブゴールが作られるらしい。自然数に限定したい場合は、普通に"n>=0 => prop"みたいにやればよいっぽい
・inductiveなデータ構造に対しては、(Coqでそうであるように)inductionがちゃんと使えるんだろうか→よくわからん。使えるっぽい?
・Sparkleで証明した命題が、Cleanで正しいことを保証するもの(原理的に保証するって意味で、実装にバグがあるとかいうのは別の話)って何?当然、Cleanの意味論と結びつく何かがどっかにないとダメなような→謎。いや、グラフ書換えがどうとかって書いてあるけど、それがなんやねんと
・こないだの、"ls++[ ]=[ ]"について。lsがbottomだったら、左辺はbottomで、右辺は、[ ]だから、成り立ってないじゃん、という。一方で、reverse (reverse xs)=xsは、xsがbottomの時でさえ厳密に成り立つので、この落とし前はどうつければええねん→謎。definedness tacticが何なのかという話
とりあえず、いつもの如く"length (map f ls) = length ls"はやっとこう。もう、length.(map f)に足向けて寝れないよ
length (map f ls) = length ls Induction ls. 1.Reduce NF All. Reflexive. 2.Reduce NF All. Reflexive. 3.Introduce l ls IH f. Reduce NF All. Rewrite -> All IH. Reflexive. Q.E.D
普通に、lsに関して帰納法を使って、個々のサブゴールについては、Reduceするだけで、ほぼ終わり。
あと何気に感心したのは、reverse (reverse xs)=xsは証明できなくて(多分)、証明できるのはfinite xs=>reverse (reverse xs)=xsという点。まあ、当たり前と言えば当たり前なんだけど、証明を追っていくと、結局、帰納法でbottomに対しても証明しないといけないというのが効いてるんだな〜と分かる。このへんは、Coq(や普通の数学)とはちょっと違うところでもあり、微妙な議論をするときに、きちんとやる自信がない
まあ、やってることは至極単純で、Expr(HaskellとかCleanの式),Prop(命題),Goal(という名前はよくない気がするけど。A1,...,An|-Bみたいな形の図式),Tactic(GoalをGoalに変換)の4つくらいのデータ定義して、単一化書いて適当にごにょごにょしてやればよいかな〜とか、そんな感じ(多分)。実装はやる気になればすぐだと思う。Tacticをきちんと全部書くのがだるそうだけど。
問題として、
・どの程度のことが証明できるのか(shortcut fusionが証明できるとかならディモールトベネ)
・Sparkleで証明した命題が、Cleanで正しいことを保証するものが何なのか分からなくてキモイ
単純に考えれば、Coqでできるくらいのことはできそうだが。上の2点がすっきりすれば、実際に書いてみるのもいいかもしれない。
あと何気にUndoが未実装。やる気ないぜ(褒め言葉)!
mixi鑑定書
http://kantei.rw.to/mixi
他人の結果を覗き見するためにプロフィール経由せず、id指定して、鑑定結果を見れるようにしてみた
--to compile,ghc -package network main.hs
import Network.Socket
import Network.BSD
import IO(catch)
hoge :: Integer -> IO String
hoge id =
do{sock<-(socket AF_INET Stream 0);
addr <- (inet_addr host)>>=(\h -> return (SockAddrInet port h)) ;
connect sock addr ;
send sock "GET /mixi/ HTTP/1.1\n" ;
send sock "Host: kantei.rw.to\n" ;
send sock referer ;
send sock "Connection: close\n\n" ;
recvAll sock}
where
port = 80
host = "210.189.253.145"
referer = "Referer: http://mixi.jp/show_friend.pl?id="++(show id)++"\n"
recvAll s = recvAux s ""
recvAux s t =
catch ( (recv s 512)>>=(\u -> (recvAux s (t++u))) )
(\e -> (sClose s)>>(return t))
--Network.Socket.recv raises an EOF error when it gets back 0 bytes of data
main =
do{num <- getLine ;
text <- hoge ((read num)::Integer) ;
putStrLn text }
なんかCleanの話ばっかだ
