排中律と二重否定除去をSMLで実装する

「排中律は型付きプログラミング言語すべてで実装できない」という旨のツイートを目撃したので、静的型をもつプログラミング言語Standard MLで排中律を実装してみたいと思います。

まず、call/ccがあれば古典論理の諸々（パースの法則とか）が実装できるみたいな話があります。そして、SMLの一部の処理系（SML/NJやMLton）にはcall/ccがあるので、古典論理特有の命題を実装できます。（素のSMLでは多分無理です）

（世間ではcall/ccと言ったらSchemeッ！という風潮^[要出典]で、Schemeには静的型がない[^typed racket]ので、静的型があると古典論理特有のアレが実装できない、みたいな誤解が生じるのかもしれません）

[^typed racket]: Schemeの一種であるRacketにはTyped Racketという静的型のあるやつがあるみたい（？）なので、Typed Racketでもこの記事と同じようなことができるかもしれません。誰かやってみて。

準備・直観主義論理

まずはいくつか型を定義します。

datatype ('a, 'b) either = Left of 'a | Right of 'b

(* uninhabited type *)
datatype void = Void of void

(* absurd : void -> 'b *)
fun absurd (Void v : void) : 'b = absurd v

type 'a not = 'a -> void

('a, 'b) either はよくある直和型です。他の多くの言語と異なり、SMLやOCamlでは型構築子は後置です。また、型変数の名前はプライムから始まります。

void は値を持たない型、論理学でいう矛盾、ボトム $\bot$ です。SMLでは型構築子が0個の型を書けないので、こういう書き方になります。

absurd は「矛盾からはなんでも導ける」爆発律に対応する関数です。

'a not は、論理学でいう命題 'a の否定です。直観主義論理の $\lnot A \equiv A\rightarrow \bot$ みたいな感じで定義しています。y : 'a not と x : 'a があった時に矛盾、あるいは任意の命題を導くやつ（否定の除去則）は absurd (y x) と書けます。

ここまでは普通の直観主義論理っぽいですね。

call/ccで実装する排中律

では本題です。call/ccを使って、古典論理の範囲に踏み込んでみましょう。

筆者の手元で使えるのがMLtonなのでMLtonのcall/ccを使うことにします。使い方は以下を見れば良さそうです。

• http://www.mlton.org/MLtonCont

まずは排中律を実装してみましょう。排中律は unit -> ('a, 'a not) either という型の関数 excludedMiddle として実装します。

実装の前に方針を立てます。excludedMiddle は 'a か 'a not のどちらかの値を返す必要がありますが、いきなり任意の型 'a の値を返せるわけがないですよね。

対するもう一方の候補は 'a not で、こちらは 'a -> void という関数ですので、頑張ればなんらかの値を返せそうです。というわけで、最初は 'a not の方を Right に包んで返すことにしましょう。（「最初は」って、あたかも複数回制御を返すように聞こえますね。その通りです。）

この際に返す関数は、 'a という型の値を受け取ったら void を返さないといけません。しかし void は値がないので、どうしたものでしょうか。

ここでcall/ccの出番です。excludedMiddle が呼ばれた段階で継続を保存しておき、 'a の値が渡された瞬間に時間を巻き戻して（比喩です） excludedMiddle から Left に包まれた値として返せば良いのです。「いきなり 'a の値を返せるわけがない」と書きましたが、最初は無理でも、このタイミングなら可能なのです。

MLtonでの排中律の実装は次のようになります：

(* excludedMiddle : unit -> ('a, 'a not) either *)
fun excludedMiddle () : ('a, 'a not) either
    = MLton.Cont.callcc (fn cont : (('a, 'a not) either) MLton.Cont.t => Right (fn (x : 'a) => MLton.Cont.throw (cont, Left x)))

これを使って何かプログラムを書いてみましょう。ん〜〜、

1. 文字列型について排中律を呼び出して、
   1. Left に包まれた文字列が返ってきたらその文字列を印字、
   2. Right に包まれた「文字列の否定」 string -> void が返ってきたら
      1. まず Hello と印字してから
      2. world!\n という文字列について「文字列の否定」を呼び出す

という処理はどうでしょうか。

val () = case excludedMiddle () of
             Left (x : string) => print x
           | Right (y : string not) =>
                 (print "Hello "; absurd (y "world!\n"))

実行結果：

Hello world!

call/ccを使って実装する二重否定除去

excludedMiddle を使うと ('a not) not -> 'a という型の関数も実装できます。この際に追加でcall/ccを使う必要はありません（直観主義論理の上で排中律と二重否定除去は同値なので）。

あるいは、先に二重否定除去をcall/ccを使って実装し、それを使って排中律を実装することも考えられます。

この辺は読者への演習問題とします。

---

ところで「古典論理の推論規則をプログラミング言語で実装する」って何なんですかね？そういう型を持った関数を書くだけなら無限ループなり例外送出なりでできてしまうので、少なくともそういうやつは除外しないと意味のある話にならなさそうな気がします。