たまには型のあるSchemeでも

目標

トリック　オア　トリート(Trick or Treat)に因んだ何かを証明してみる！！

と題して

(¬Treat -> Trick) -> (Trick ∨ Treat)
[日本語訳 : お菓子をくれないなら悪戯しちゃうぞ -> 悪戯 か お菓子である!!]

今回はちょっと準備をします

今回はHaskellで証明する事は諦めます。諦めて、本当は型が付いたSchemeでやりたい気分なのですが、私はそれは知らないのでこの記事をなんとか役立ててもらって、型が付いたSchemeが使える人にやってもらいたいです。

HaskellでContinuationを持つ非常に簡単な弱い型の言語を実装する

{-# LANGUAGE Rank2Types , GADTs , FlexibleInstances #-}

instance Show ((Exp -> IO a) -> Exp) where
    show _ = "cont"

data Exp where
    EInt :: Int -> Exp
    EStr :: String -> Exp
    Var  :: String -> Exp
    Lam  :: String -> Exp -> Exp
    App  :: Exp -> Exp -> Exp
    Plus :: Exp -> Exp -> Exp
    Abort :: Exp -> Exp
    Cont :: (Exp -> Return) -> Exp
    CatchCont :: Exp {- ((Exp -> Return) -> Return) -} -> Exp
    -- (Exp -> ⊥) -> ⊥ <=> ¬(¬Exp)
    -- CatchContはもし型があるとすると、¬(¬Exp) -> Expかもー
    CallCC :: Exp -> Exp

data Return where
    Return :: String -> Return

instance Show Exp where
    show (EInt i) = "EInt " ++ show i ++ "\n"
    show (EStr s) = "EStr " ++ s ++ "\n"
    show (Var  v) = "Var " ++ show v ++ "\n"
    show (Lam s body) = "(\\" ++ s ++ " " ++ show body ++ ")\n"
    show (Cont k) = "Cont"

instance Show Return where
    show (Return s) = s

type Env = [(String,Exp)]
    
type Cont = Exp -> Return

binop :: (Int -> Int -> Exp) -> Exp -> Exp -> Env -> Cont -> Return
binop f e1 e2 env k = eval e1 env (\v1 -> case v1 of
                                            EInt v1' -> eval e2 env (\v2 -> case v2 of
                                                                              EInt v2' -> k (f v1' v2')))

eval :: forall a.Exp -> Env -> Cont -> Return
eval (Var s) env k = case lookup s env of
                       Just v -> k v
                       Nothing -> error $ "in eval . NotFound : " ++ s ++ "\n"
eval (App f a) env k = eval f env (\f' -> case f' of
                                            Lam s b -> eval b ((s,a) : env) k
                                            Cont capturedK -> capturedK a
                                            other -> error $ "\nin eval . Apply NotImpl > " ++ show other)
eval self@(Lam _ _) _ k = k self
eval (Plus e1 e2) env k = binop (\a b -> EInt (a + b))  e1 e2 env k
eval self@(EInt _) _ k = k self

eval (Abort e) env k = abort e env
eval (CatchCont (Lam s b)) env k = abort b ((s,Cont k) : env)
{-
eval (CatchCont M) env k は 継続k(kの型はa -> ⊥)の元でeを評価するという事を表す。

これはつまるところ、ケイゾクするか、ケイゾクせずに即座に終了するかのどちらかである。
(下の exp5,exp6,exp7,exp8 をそれぞれ参考にしてみてください...。小さ過ぎて成らないかもですが)

何にせよ最終的には継続に渡るんだから
CatchCont e ∈ aになる必要がある
かつ、e は 継続を受け取るので((a -> ⊥) -> ?)

?の部分は、実は中で継続を使ったならば ⊥ になるし、使わないでおくならば 任意の型b になる。

んですが、今回は簡単の為に、CatchContから継続を受け取る関数は必ず⊥を返すという約束毎にしておきます。(下のexp6参照)

すると
e ∈ (a -> ⊥) -> ⊥
で
CatchCont e ∈ aなわけですから、
CatchCont ∈ ((a -> ⊥) -> ⊥) -> a
となります。成りそうです！！今回のHaskellで作ったものは型付け弱過ぎるのでダメですけど...
-}

eval (CallCC (Lam s b)) env k = eval b ((s,Cont k) : env) k
{-
ケイゾク(k ∈ a -> ⊥)を中で使えば、一気に続きに飛ぶ事が出来る(ショートカット)
使わなくても同じケイゾクに行き着く

CallCC (\s -> b) ∈ aとなる事が分かる。
先と同様に、 s ∈ (a -> ⊥)
(\s -> b) ∈ (a -> ⊥) -> ⊥ (ケイゾクを使った場合)
(\s -> b) ∈ (a -> ⊥) -> a  (ケイゾクを使わなかった場合)

CallCC ∈ ((a -> ⊥) -> a) -> a
これはPierce's Lawと呼ばれるもの(に似てます)
-}

eval a env k = error $ "\nin eval : " ++ show a

exit :: Exp -> Return
exit e = Return (show e)

abort :: Exp -> Env -> Return -- Envは無視して a -> ⊥ と読む
abort e env = eval e env exit

exp1 = Plus (EInt 1) (EInt 2)
exp2 = (App (Lam "x" (Var "x")) (EStr "hoge"))
exp3 = Plus (EInt 1) (Plus (EInt 2) (EInt $ -1))
exp4 = Plus (EInt 1) (Abort (EInt 2))
exp5 = Plus (EInt 1) (CatchCont (Lam "k" (Plus (App (Var "k") (EInt 2)) (EInt 3))))
exp6 = Plus (EInt 1) (CatchCont (Lam "k" (Abort (Plus (EInt 2) (EInt 3)))))
exp7 = Plus (EInt 1) (CallCC (Lam "k" (Plus (App (Var "k") (EInt 2)) (EInt 3))))
exp8 = Plus (EInt 1) (CallCC (Lam "k" (Plus (EInt 2) (EInt 3))))

topeval :: Exp -> Return
topeval e = eval e [] exit

こんなのを実装して何の関係があるのか?という感じです。Expは流石に型が弱過ぎて悲しいのですが・・・。
一応継続を相手にする関数Abort と CatchCont , CallCCに注目してもらえれば良いかな、と思います。

というかこれは本当にそれだけの例なので・・・。

普段継続を相手にする人にしてみれば、CallCCがその名の通りそれかなーという事に気付いてもらえると思います。が、今回はCallCCはちょっと置いておいて・・・。

継続を相手にする関数の中で最も注目して欲しいのはCatchContです。

これは「継続渡しスタイル(CPS)」で書く時のソレだと思ってもらえるんじゃないかなーと思います。

まぁ普通こんなのでピンと来ないと思いますのでググってください。そう、そういう説明はもっと適切な所で探すべきです。

参考までにですが、これまでに見た事無い説明も見てみたいという方は、
http://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf
も参考になるかと思います。

C/C++でラベルを1度でも使った事がある人には楽しめるかなーと。

継続付きのpetitな言語の実装に関しては
http://logic.cs.tsukuba.ac.jp/~kam/courses/jikken2008/cps-prog.txt
http://pllab.is.ocha.ac.jp/lab.html
が参考になるかもしれません。

まぁ上にあるぐらいのモノは非常にシンプルなので問題は無いと思いますが。

ケイゾク周りを型に落とし込む

本当は、GADTsを使ってWell-Typedな継続操りをしたかったのですが環境のあたりで酷く成ったのでパス

先のCatchContをundefined使って型付けしつつ、例のごとく証明に必要な部分を取り揃えたのが次のHaskellのコードです。

{-# LANGUAGE RankNTypes , TypeOperators , EmptyDataDecls , ScopedTypeVariables #-}
data Bot
type Not a = a -> Bot
type a :∨: b = Either a b
type a :⊃: b = a -> b

{-
ケイゾクを使うものを定義するとするならば

contUser :: forall x result.(x -> result) -> result
contUser k = k arg
    where
      arg :: x -- ケイゾクに何が渡るかなんぞ知らんのでundefinedで誤摩化す
      arg = undefined
-}

{-
ContCatcherの型が　そうなるといいよね♪
というのは先に書いておいたので、undefinedです！！

(参考 : http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20060429#p02)
-}
contCatcher :: forall x.((x -> Bot) -> Bot) -> x
contCatcher = undefined

doubleNegElim :: forall x.((x -> Bot) -> Bot) -> x
doubleNegElim contConsumer = contCatcher contConsumer

data Treat
data Trick

or_elim :: forall a b c.(a :∨: b) -> (a -> c) -> (b -> c) -> c
or_elim (Left l) left right = left l
or_elim (Right r) left right = right r

not_intro :: forall a.(a -> Bot) -> Not a
not_intro pr = (\a -> pr a)

not_elim :: forall a.a -> (a -> Bot) -> Bot
not_elim pr1 pr2 = pr2 pr1

excluded :: forall a.a :∨: (Not a)
excluded = goal
    where
      p0 :: ((a :∨: (Not a)) -> Bot) -> Bot
      p0 = not_intro p1

      p1 :: (Not (a :∨: (Not a))) -> Bot
      p1 not_v = not_elim v not_v
          where
            v :: a :∨: (Not a)
            v = Right p2

            p2 :: Not a
            p2 = not_intro p3

            p3 :: a -> Bot
            p3 a = not_elim (Left a) not_v

      goal :: a :∨: (Not a)
      goal = doubleNegElim p0

eq1 :: forall a b.(a :⊃: b) -> ((Not a) :∨: b)
eq1 (aImplb :: (a -> b)) = goal
    where
      goal :: (Not a) :∨: b
      goal = or_elim excluded f g
             
      f :: a -> (Not a) :∨: b
      f = (\a -> Right (aImplb a))
          
      g :: (Not a) -> (Not a) :∨: b
      g = (\nota -> Left nota)

prop1 :: ((Not Treat) :⊃: Trick) -> (Not (Not Treat)) :∨: Trick
prop1 notTreatImplTrick = eq1 notTreatImplTrick

prop2 :: (Not (Not Treat)) :∨: Trick -> Trick :∨: Treat
prop2 pr = or_elim pr left right
    where
      left :: (Not (Not Treat)) -> Trick :∨: Treat
      left pr' = Right $ doubleNegElim pr'

      right :: Trick -> Trick :∨: Treat
      right pr' = Left pr'

trans :: forall a b c.(a -> b) -> (b -> c) -> (a -> c)
trans ab bc = (\a -> bc (ab a))

theorem :: ((Not Treat) :⊃: Trick) -> Trick :∨: Treat
theorem = trans prop1 prop2

で、これは何なの?

なんかShibuya.lispも近いらしい、という事と最近証明証明ばっかりやってるので何か架け橋になる記事書けないかなーみたいな、まぁそれも後付けです。

結果から言うと、今回のTrick or Treatは、「継続を一級オブジェクトで持たない言語」では「全うなスタイル(上のHaskellではundefinedを使ってしまっています)」で証明する事が出来ない、です。

具体的にどの辺がアウトなのかを。
まず、 A -> B ≡ (¬A) ∨ Bが継続がある言語じゃないと言えないよーという事があります。
これはその証明過程において排中律(A ∨ ¬A,どんな命題でも、成り立つか、成り立たないか現時点で白黒付けちゃって良い)を使っている事。

次に¬¬Treat ∨ Trick -> Treat ∨ Trick(証明ではこの過程を飛ばして一気にTrick ∨ Treatとしていますが)を証明するのに、二重否定除去(ある命題の否定を仮定して矛盾が出たならば、その命題は正しいとする)を使っています。二重否定除去は、「背理法」と言った方が馴染みがあるかもしれません。

え、じゃあ、「証明合戦するんだったら」型付きのScheme使ったら大勝利で、Haskellは滅びるべきなんですね、そうなんですね?というHaskell滅ぼしたい派の人も居るんじゃないかと思うんですが、割とHaskellが出来る範囲でどうにか成ったりします。

「Curry-Howard Correspondence」とか「Curry-Howard同型対応」というキーワードで調べると出るのですが、調べると出るので説明しないしうまく説明出来ないので例によって上手く説明してくれている所を探して欲しいのですが、「命題」と「型」を対応させてみちゃおうぜ！！というようなものがあります。
で、天下り的ですが、実は「型付きScheme」は論理学で言う所の「古典論理」で、「Haskell」は「直観主義論理」というのにカテゴリーされます。

「割とHaskellが出来る範囲でどうにか成ったりします」というのは「直観主義論理」がまぁソレなり(とかいうと刺されそうですが)に戦える！！という感じだからです。色々キツいです。

古典論理とか直観主義論理とかまた面倒臭そうな日本語だなぁという感じでタイピングするのも面倒臭い感じなのですが、実は古典論理は日常何気なく使う論理の系です。

じゃあ直観主義論理は何なのか、という事なのですが、

古典論理 = 直観主義論理 + 排中律

という感じになってます。

Haskellの型システム = 直観主義論理なので、今回はundefinedという、ちかたないときにちかたなく使えるHaskellの良心を使ったのでした。

まとめ

たまには型がある言語で遊んでみるのも楽しいかなーと思います。

型付きSchemeでcall/ccとかの型がどうなってるのかは気になるので、この処理系を使え！みたいなモノが在れば是非。

Scalaは限定継続がどうこうという話をみたのだけどあれはどういう形で入れようっていうソレなんだろう...?

参考

知の教科書　論理の哲学 (講談社選書メチエ)

情報科学における論理 (情報数学セミナー)

http://ci.nii.ac.jp/naid/110003743606/
http://ci.nii.ac.jp/naid/110003743618/
http://ci.nii.ac.jp/naid/110003743626/
http://ci.nii.ac.jp/naid/110003743641/ <- λ-cubeとかL-cubeという何がどれに対応するというのを立方体で表したエキサイティングなものが載っていて楽しいです。

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20060429#p02
さかいさんの所の関連リンクが面白いです。

継続とか入れれば古典論理に対応するんじゃね?という話の大元(カモ)
http://portal.acm.org/citation.cfm?id=96714
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.6893
なんかciteseerxは最近良く繋がらなくて悲しい。

継続自体に関しては
"Continuations: A Mathematical Semantics for Handling Full Jumps"
http://www.springerlink.com/content/q0xv4n463623rm84/

"Exceptions, a mathematical semantics for handling full jumps"
http://www.csse.monash.edu.au/~lloyd/tilde/Semantics/1987TR90/
↑のページでも紹介されていますが
"A Practical Introduction to Denotational Semantics"はたまたま昨日借りて読んでいるのですが、くどくない表示的意味論の入門(...?)にも良さげです。個人的には。まぁ英語ですけど・・・。

Practical Denotational Semantics (Cambridge Computer Science Texts)

一応まだ購入可能なのはすごいことだなー

一番大事な事

涼君のCDが11/4発売されましたよ！！

THE IDOLM@STER DREAM SYMPHONY 02 秋月涼