2006-04-29 昭和節 [長年日記]
λ. javascriptでRDFをパース
やっぱし、やっている人はいるもんだな。 何かに使えそうな気がするのでメモ。
λ. (forall x. ((x->r)->r)->x) -> Either a (a->r)
今日ちょっと混乱したことを元にクイズにしてみた。多分その手の人にはピンとくる問題。表記はHaskellのものを使ったが、実際には多相ラムダ計算の問題と考えていい。
問題
- 「(forall x. ((x->r)->r)->x) -> Either a (a->r)」という型を持つ関数を定義せよ。(ただし⊥が途中で現れたりする定義は禁止)
- この関数は何を表しているのだろうか?
解答編
問題の関数はこんな感じで定義できる。
notNotEM :: ((Either a (a->r)) -> r) -> r notNotEM k = k (Right (\a -> k (Left a))) dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r) dn2EM dn = dn notNotEM
で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易いかも*1。
data Absurd type Not p = p -> Absurd type Or = Either notNotEM :: Not (Not (p `Or` Not p)) dn2EM :: (forall x. Not (Not x) -> x) -> p `Or` Not p
で、面倒なので詳しい説明は省略するが、例えばNK(自然演繹の体系NJに二重否定除去規則を追加した体系)で排中律を証明すると、この関数の構造を反映した証明図が得られる*2。
[1: P]
------------- (∨I左)
P ∨ ¬P [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
⊥
------------- (¬I{1})
¬P
------------- (∨I右)
P ∨ ¬ P [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
⊥
------------------ (¬I{2})
¬¬(P ∨ ¬P)
------------------ (¬¬E)
P ∨ ¬P
他の体系での証明は誰かにまかせた。あろはさんはこの証明をCoqで表現してみると良い勉強になるかも。ついでに古典論理のうさんくささをもっと感じられるかもw
余談
ちなみに、色々と細かいことを抜きにすれば、否定は継続に対応し、二重否定除去規則に対応するものはcall/ccで実現できる。Haskellにはそれらは存在しないので多少回りくどい表現になっているが、一級継続とcall/ccが存在する言語では直接それらを使って排中律に相当するものを表現することが出来る。例えばSchemeだと以下のような感じだろうか*3。
(define (left x) (list #t x)) (define (right x) (list #f x)) (call-with-current-continuation (lambda (k) (k (right (lambda (a) (k (left a)))))))
しかし、それにしても奇妙な定義と振る舞いである。これに関係して、Philip Wadler, Call-by-value is dual to call-by-name. Proc. ICFP 2003, pp. 189-201. <URL:http://homepages.inf.ed.ac.uk/wadler/topics/dual.html> に載っていたお伽噺が面白かったので、引用する。
Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”
The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.
The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?
“I accept,” said the man at last. “Do I get (a) or (b)?”
The devil paused. “I choose (b).”
The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.
“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”
The devil took possession of the valise. Then he said,“Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.” And the devil handed back to the man the same valise that the man had just handed to him.
さっぱりわからないので、そろそろ答えを発表していただけるとうれしいです。。。
りょーかい。じゃ発表します。
同僚というか先輩が以下のを発見したのですが。<br>(ここインデント大丈夫かな)<br>f xrrx = case (f xrrx) of<br> Left a -> Right ar<br> where<br> ar _ = xrr (\_ -> ar a)<br> xrr xr = xr (xrrx xrr)<br> Right ar -> Right ar<br>推論させると(((t -> t1) -> t1) -> t) -> Either a (a -> t1)になります。
はじめまして、mputさんの同僚（or先輩？）です。<br>くだんの回答は、<br>「型理論も証明の世界もなーんも知らん人間」が<br>「ただひたすら ghci -fglasgow-exts に型推論させて一致させてみる」<br>ことだけを目的に書いたもんです。<br>が、やっぱ forall x. は出てきませんし、<br>そもそも正解を型推論させてもあの型にはならないので、<br>こんなアプローチでがんばっても無駄でしたねえ…^^;
koyama41さん、はじめまして。<br>この定義だとfの再帰呼び出しが停止せず⊥になる点がまずいです。ただ、期待した答えでこそなかったですが、これはこれで面白い定義だと思いますし、結構惜しかったんじゃないかと思いますよ。<br>それと、推論した型にforallが出てこない点については、明示的に型を書けば型チェックが通るので問題ないです。GHCではそのような型を使う場合には明示的に書かなくてはならないことになっているので。