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とか)は、まあ適当に