■

Sparkleで証明できるにもかかわらず、Cleanでは正しくない命題の例。

forall n::Int.(n > 0)=>(n+1 > 0)

何故ならCleanでIntは32ビット整数だから。

うあー

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

・昔のTemplate haskellには、gensymという、そのまんまの関数があったような
http://www.cis.upenn.edu/~bcpierce/courses/advprog/resources/haskell-src/Language.Haskell.THSyntax.html#v%3Agensym
2002年くらいのSimon Peyton Jonesだかの論文読むと普通にgensymを使ってらっしゃる。今はないな〜とか思って、探して見たら、newNameという関数があって、これが代わりを果たすっぽい。gensymのがタイプしやすいんだが

gensym::String->Q String
mkName::String->Name
newName::String-> Q Name

・Template Haskellは、もうちょっとだけ、deSugarしてくれてもいいんじゃないかと思った

Prelude> :set prompt >
> :module + Language.Haskell.TH
> :set -fth
> runQ[| 3:[] |]>>=print
InfixE (Just (LitE (IntegerL 3))) (ConE GHC.Base.:) (Just (ConE GHC.Base.[]))
> runQ[| (:) 3 [] |]>>=print
AppE (AppE (ConE GHC.Base.:) (LitE (IntegerL 3))) (ConE GHC.Base.[])

・declarationのASTを見たいときも

> runQ[d| x=1;f x y=x+n where n=3 |]>>=print
[ValD (VarP x) (NormalB (LitE (IntegerL 1))) [],FunD f [Clause [VarP x_3,VarP y_4] (NormalB (InfixE (Just (VarE x_3)) (VarE GHC.Num.+) (Just (VarE n_5)))) [ValD (VarP n_5) (NormalB (LitE (IntegerL 3))) []]]]

・リストの内包表記。って嫌いだったんだけどなんか好きになれそうな気がした

(\a b -> [(x,y)|x<-a,y<-b,y-x<4]) [1,2,3] [4,5,6]

mapとかだけで書くと、何やってるか分かりづらくなることは多々あるな〜と

abstract reduction

何遍読んでもやっぱわかんね〜。そもそもどこがアルゴリズムで、どこが単なる原理の説明なのかすらよく分からんというダメっぷり。頭わり〜。とりあえず、何故abstract reductionが正しいのかという点はあまり悩まない方がいいかもしれない。abstract reductionが正しいことを証明しましたってだけで論文になってたりするので。というわけで、以下の論文をじーっと読んで
・Nockerの論文:Strictness Analysis using Abstract reduction
忠実にコードに落としていくことにした。Template Haskellを激しく使う

--まだ全部書いてない
{-# OPTIONS -fth #-}
import Language.Haskell.TH
import Data.List
import Data.Maybe(fromJust)

data MatchType 
 = TotalMatch | BotMatch | PartialMatch | NoMatch deriving (Eq,Show)

data AbsExpr
 = AbsTop | AbsBot | AbsVar Name | AbsApp AbsExpr AbsExpr | Union [AbsExpr] deriving Eq
--Union [] is not permitted

instance Ord AbsExpr where
 a <= b|(a==AbsBot) = True
       |(b==AbsTop) = True
       |(a==b) = True
 (AbsApp (AbsVar f) x) <= (AbsApp (AbsVar f') x') = (f==f') && (x<=x')
 (AbsApp e x) <= (AbsApp e' x') = (e<=e') && (x<=x')
 t <= Union xs = (any (t<=) xs)
 _ <= _ = False


--極大元を全て取り出す
supreme::(Ord a)=>[a]->[a]
supreme::(Ord a)=>[a]->[a]
supreme [] = []
supreme (x:xs) = let xs' = filter (not.(<=x)) xs in
  if (any (x<) xs') then (supreme xs') else (x:(supreme xs'))

--simplification of Union expression
simplUnion ::AbsExpr -> AbsExpr
simplUnion (Union [x]) = x
simplUnion (Union ls) = Union (supreme ls)
simplUnion (AbsApp c (Union xs)) = Union (map (AbsApp c) xs)
simplUnion t = t --otherwise

--Nockerの論文table2:A simple matching algorithm
naiveMatch ::AbsExpr -> Exp -> Bool
naiveMatch _ (VarE _) = True
naiveMatch _ (ConE _) = True
naiveMatch AbsTop _ = True
naiveMatch AbsBot _ = False
naiveMatch (AbsApp (AbsVar c) v) (AppE (VarE c') p) = (c==c')&&(naiveMatch v p)
naiveMatch (AbsApp e v) (AppE e' p) = (naiveMatch e e')&&(naiveMatch v p)
naiveMatch (Union es) p = any (\e-> naiveMatch e p) es

--Nockerの論文table3:A matching algorithm for the functional strategy
--使い方が分からないlol
absMatch :: AbsExpr -> Exp -> MatchType
absMatch _ (VarE _) = TotalMatch
absMatch _ (ConE _) = TotalMatch
absMatch AbsTop _ = PartialMatch
absMatch AbsBot _ = BotMatch
absMatch (Union vs) p = combineUnionMatches $ map (\v->absMatch v p) vs 
 where
  combineUnionMatches ms |(all (TotalMatch==) ms)  = TotalMatch
                         |(all (NoMatch==) ms)  = NoMatch
                         |(all (BotMatch==) ms)  = BotMatch
                         |otherwise  = PartialMatch
absMatch e1@(AbsApp _ _) e2@(AppE _ _)
 = let x = (aux e1 e2) in 
      if (fst x) then combineMatches (snd x) else NoMatch
 where
  aux::AbsExpr -> Exp -> (Bool,[MatchType])
  aux (AbsApp (AbsVar c) v) (AppE (VarE c') p) = (c==c',[absMatch v p])
  aux (AbsApp (AbsVar c) v) (AppE (ConE c') p) = (c==c',[absMatch v p])
  aux (AbsApp c1 v) (AppE c2 p) = let x = (aux c1 c2) in (fst x,(snd x)++[absMatch v p])
  combineMatches :: [MatchType] -> MatchType
  combineMatches ms|(all (TotalMatch==) ms) = TotalMatch
                   |(head ms)==TotalMatch = fromJust (find (TotalMatch/=) ms)
                   |otherwise = PartialMatch

そんなに激しくなかった。今のところ、absMatchは使い方がよく分からないのでどうでもいいが、naiveMatchより精密らしい。Union lsは基本的には、lsの最小上界と等価。なんだけど、abstract domainが本質的にinfiniteだとか、上の順序関係は近似だとか、多分そういう事情のせいで、一般にはexactに最小上界を計算することができない。それでも、例えば、[AbsBot , AbsTop]の最小上界はAbsTopに決まってるので、計算できる場合もあって、そのへんの近似計算をやるのが、simplUnion。simplUnion (Union [AbsTop,AbsBot]) = Union [AbsTop],simplUnion (Union [AbsTop])=AbsTop。一発でやらないのは停止判定を挟むのがめんどかっただけで、ほんとは、ちゃんとやらないといけない。ということだと思う。あと、Ordは全順序を想定して作られてるので、今回のように半順序が必要な時に使うのはまずい

で、いくつかの宣言の列(Template Haskellの型だと[Dec])を考える。例えば、

map f [] = []
map f (x:xs) = (f x):(map f xs)

の2つ。case式とかは、いくつかの宣言に分解してしまえばよい

それで、(AbsApp (AbsApp map AbsBot) AbsTop)を計算することを考える(正確には、AbsApp map AbsBotじゃなくて、(AbsApp (AbsVar (mkName "map")) AbsTop)とか書かないとダメだけど、長いので適当に略)。このAbsExprは、naiveMatchを使うと上の宣言の第一式と第二式の両方の左辺にmatchするので、次のように書き換えられる。
(AbsApp (AbsApp map AbsBot) AbsTop)
= Union [AbsTop , (AbsApp (AbsApp (:) (AbsApp AbsBot AbsTop)) (AbsApp (AbsApp map AbsBot) AbsTop))]
Unionのリストの頭がAbsTopなのは、map f [ ]=[ ]から来ている。第一式右辺は、"map Bot Top"にマッチしてるので、左辺のfをBotに[]を、Topに機械的に置換する。一方で、2つ目が謎で、第二式の右辺は、やはりmap Bot Topにマッチしてるので、fをBotに置き換えるというのはいいとして、こっから、xとxsをTopに置換していい理由がよく分からん。勿論、abstract domainに於いて、x:y=Topの解は、x=y=Topしかないんだけど、それは一般の型構成子にも適用できる話なんか?あるいは、なんか根本的に間違ってるんだろうか。とりあえず、今ここが最大の謎

とりあえず、これの右辺にsimplUnionを施していくと、結局
(AbsApp (AbsApp map AbsBot) AbsTop) = AbsTop
を得る。つまり、mapは第一引数について、non-strict。というのがAbstract Reductionの基本的な計算法だと思う。

一方で、(AbsApp (AbsApp map AbsTop) AbsBot)にmatchする式は第一式のみで、
(AbsApp (AbsApp map AbsTop) AbsBot) = AbsBot
となる。多分。というわけで、mapは第二引数については、strict

Abstract Interpretaionの時と違って、高階関数も自然に扱えてる。けど、本当にこれで合ってるのか自信ない。結局、アルゴリズム書いたとしても、何で正しいのか理解しないとダメだよな〜。あー、あと簡約が停止しない場合があるよね、という話(f x = f xとか)は、まあ適当に

妄想とか迷走

さて、Sparkleでsortの正しさを証明しようと思った。めんどいので、isSortedという関数を用意して、"isSorted (sort ls)=True"を証明しようとしたのだけど、オーバーローディングが解決できません！とか怒られる(なお自前の関数を利用するには、.iclファイルに関数書いてProject>Add Moduleでいいのだけど、こんときStart関数がないと何故か怒られる)。型クラス使えないのかよ、Sparkleつかえねー、ということで終わろうと思ったけど、そこらへんは大人なのでぐっとこらえて、Int限定でいいやと思い直した。適当に調べると、型を指定するときには、"[ls::[Int]] isSorted (sort ls)=True"のようにやればいいらしい。が、"Prove topmost theorem"して出てきたGoalを見ると、"forall ls::[a].isSorted(sort ls)"だった。Int指定はどこへ行ってしまったのか。Sparkleは謎が多い。というか、<とかオーバーロードする時、型さえ合ってれば何でも良くて、それが(数学的な意味での)順序関係である必要は全然ないから、x isSorted (sort ls)=True"(これは、"forall ls::Int. not(ls=bottom) => isSorted (sort ls)"という意味)。お前はこれを見たとき帰納法を使うだろ？誰だってそうする。俺だってそうする。んで、Induction Stepまではいくのだけど、そこで更に場合分けが必要になって、めんどくさくなったので諦めた。ていうか、Undoないので、失敗したら1からやり直しというのは辛すぎる。まあ、私がSparkleのtacticをよく理解してないだけなので、多分証明はできるはず。

当初は、Buchbergerアルゴリズムの正しさを証明してやるぜとか思ってたけど、sort程度で挫折してるようじゃ、先は遠い。というか、CoqでBuchbergerアルゴリズムを生成した人たちは、グレブナ基底の存在証明をやったわけだけど、それに一年かかったという話で、一方こっちは最初から関数持ってるから、もっと楽だろうという算段だったんだけど、冷静に考えると正しいかどうか確証が持てない関数を相手取って、正しさを証明しようと試みるのは精神衛生上大変よろしくないよな〜。ていうか、Haskellで適当に書いたBuchbergerアルゴリズム、十中八九まだバグが残ってるはず･･･デバッガの時代は当分続きそうだ

というのはいいんだけど、fixed point promotionによる変換length (map f ls)->length lsと、こないだのSparkleによるlength (map f ls)= length lsの証明とを見比べると、各ステップがよく対応しているように見える。このへんの事情は、shortut fusionでも同じで、まあ融合変換はある種の定理の自動証明になってるというような。ということは、融合変換M->Nがあったら、そのプロセスから、自動的にM=Nの証明@Sparkleを抽出できる(ほんとかよ。hylo-fusionは、本質的にfoldだけでなく、unfoldも含んでるのでSparkleの証明に翻訳できないかも)。そうすると、もし例えばshortcut fusionが間違ってたら、正しくない命題M=Nの証明が得られることになる。というわけで、Sparkleでshortcut fusionを証明するというのは、Sparkleで証明できた命題がCleanで正しいことを部分的に証明するのと同程度の難しさがある。というような、胡散臭いことを考えたのだった。

まあ、Sparkleでshortcut fusionを直接証明するのは無理そうだな〜。CleanでCleanの処理系を書くことはできるので、そういうの経由すれば、証明できなくもないのかもしれず、それが上で「直接証明するのは」って書いた理由。しかし、そもそもCoqではなく、Sparkleを使う理由っていうのは、そういう間接的な証明を避けるというのが、大元にあった気がするので、間接的な証明しかできないのだとすると、Sparkleを使う意義も大分薄れるよな〜とか

こういうクネクネしたことを考えるのは苦手というか、多分基本的な知識が足りてないというか、どうでもええがな、という気分になる

結論:どうでもいい

Higher-Order matching

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 expression syntactically equal modulo alpha conversion. The pattern (rule), but not the expression, is eta-expanded if necessary. (Eta-expanding the epression can lead to laziness bugs.) But not beta conversion (that's called higher-order matching).

ということらしい。とりあえず、右も左も分からんのだけど、Huet-Langのsecond-order matchingというのと、de Moor-Sittampalamによるアルゴリズムというのが有名っぽい。Huetの論文は古いらしいので、Web上では読めないっぽい。de Moore等の論文ってのは多分これ
Higher-order Matching for Program Transformation

自分で思いつくかどうかはともかく、やってること理解するのは難しくないかな。あとまあ、定理証明器書くなら、Higher-Order Unificationとかも必要になるような、ならんような。Higher-Oreder Unificationアルゴリズム最初に考案したのも、Huetらしい。おんなじ人？