2007-08-08 [長年日記]
λ. Djinn, a theorem prover in Haskell, for Haskell.
今更ながら Djinn を試してみた。 Djinnは「型を入力として受け取り、その型を持つ関数を(もし存在すれば)返す」ようなプログラム。これはカリーハワード対応によって「論理式を受け取って、その証明を(もし存在すれば)返す」ことに対応するので、仕組みは定理証明機で、証明をHaskellプログラムとして書いてくれている考えることもできる。
まずは自明な例を試してみる。
Djinn> id ? a -> a
id :: a -> a
id a = a
Djinn> k ? a -> b -> a
k :: a -> b -> a
k a _ = a
Djinn> s ? (a -> b -> c) -> (a -> b) -> (a -> c)
s :: (a -> b -> c) -> (a -> b) -> a -> c
s a b c = a c (b c)
Djinn> bindMaybe ? Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe :: Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe a b =
case a of
Nothing -> Nothing
Just c -> b c
当然動作する。 これが出来るのは当たり前なのだけど、実際に見ると楽しいな。 それと、bindMaybeで定数関数じゃない方の関数が先に出て来るようになっているのはちょっと賢いかも。
再帰的データ型を試そうとしたが、これは対応していないようだ。
Djinn> data List a = Nil | Cons a (List a) Error: Recursive types are not allowed: List
ついでに少し意地悪な例を試してみる(20060429#p02 より)。
Djinn> dn :: Not (Not a) -> a Djinn> em ? Either a (Not a) -- em cannot be realized.
起動時のメッセージには「If the Djinn says the type is not realizable it is because there is no (total) expression of the given type.」と出てくるが、実際には完全ではない?
どんな決定手続きを使っているのか気になるところ。 LtUにはこう書いてある。
For the curious, Djinn uses a decision procedure for intuitionistic propositional calculus due to Roy Dyckhoff. It's a variation of Gentzen's LJ system. This means that (in theory) Djinn will always find a function if one exists, and if one doesn't exist Djinn will terminate telling you so.
また、ljt.p というPrologのコードがついていて、こっちには「Incorporates the Vorobëv-Hudelmaier etc calculus (I call it LJT). See RD's paper in JSL 1992: "Contraction-free calculi for intuitionistic logic"」と書いてあった。 LJTについては、<URL:http://www.computational-logic.org/iccl/events/WPT-2004/> にある“Normalising Permutations in Sequent Calculus”の概要に以下のように書いてあったので、自然演繹とうまく対応するシーケント計算ということのようだ。
In Prawitz's translation from the sequent calculus LJ to natural deduction, many proofs are mapped to the same one and only differ by the order in which inference rules are applied. One can be transformed into another by simple permutations of these rules. By the use of focusing conditions, a canonical proof can be elected in each permutation class, thus forming Herbelin's permutation-free calculus LJT, which is in bijection with proofs in natural deduction.
そういえば、自然演繹とシーケント計算の対応の問題については、去年のSLACSの A subsystem of sequent calculus isomorphic to natural deduction でも取り上げられていたな。私はあまり理解できていなかったけど。
関連
【2011-07-27 追記】
スタートHaskellの @pi8027 さんのLT「型から項を作る」で思い出して、再度試してみる。 Djinnのバージョンはリリースされたばかりの2011.7.23。
上で上手くいかなかった例は、型を具体化してみたら、うまくいった。
Welcome to Djinn version 2011-07-23.
Type :h to get help.
Djinn> dn :: Not (Not (Either a (Not a))) -> Either a (Not a)
Djinn> em ? Either a (Not a)
em :: Either a (Not a)
em =
case dn (\ a -> void (a (Right (\ b -> a (Left b))))) of
Left c -> Left c
Right d -> Right d
ただし、型変数名が違うとダメ。
Djinn> :clear Djinn> dn :: Not (Not (Either b (Not b))) -> Either b (Not b) Djinn> em ? Either a (Not a) -- em cannot be realized.
要は多相型には対応していないということね。 そりゃそうかと納得した。
