Scalaの型システムには興味深い型が存在します。Scalaの型で述語論理を表現できないか、表現できるとしたら集合論をScalaで書けてしまわないだろうか、という興味から、Scala-proofsというプロジェクトを立ち上げて実験をしています。この記事は、Scala-proofsの中で使用する論理体系の表現手法について解説します。
Scalaのバージョン間で細かい話が変わってくるようですが、この記事はScala 2.12を前提とします。また、後述する理由から、Dotty/Scala3への移植性をできるだけ高めるために、Dottyで廃止される(予定?)の以下の機能を極力縛ることにします：
- 抽象HKT1へのワイルドカード
_の適用- 例えば、
F: * -> *の実装が具体的に与えられていない場合、F[_]は型として違法
- 例えば、
- 存在型
F[A] forSome { type A } - 抽象型
Tからの型投影T#A
私個人の論理学や数学の知識は体系だったものとは言い難いですので、もし記述に誤りや怪しい点があった場合はコメント欄にて指摘を頂けると助かります。
命題論理 - 真偽を扱う論理
命題論理は、
- 命題変数：$A, B, C...$
- 論理結合子：$\to$, $\neg$, $\lor$, $\land$
を持つ体系です。
意味的には、命題変数が命題、すなわち真か偽かが現実に際して決まるような文として、論理結合子は
- $\to$ ... 「ならば」
- $\neg$ ... 「～ではない」
- $\lor$ ... 「または」
- $\land$ ... 「かつ」
といった自然言語の接続詞として、大雑把に捉えることができます。
すべての命題変数にどのような真偽値を代入しても真になるような論理式(例えば、 $A \to A$)を、恒真式と呼びます。
命題論理の公理系
形式的な論理体系では、いくつかの(時たま無限個の)大前提として機能する公理と、これまたいくつかの「推論規則」と呼ばれる、推論を行うために使用する規則を使って、意味抜きされた、つまり具体的な"意味"を必ずしも考えないまま証明を与えていきます。公理系において、公理以外の前提を一つも置かずに推論できる文を「定理」と呼びます。
古典論理 - 完全な命題論理の公理系LP
公理を持たず、次のような導出規則群を持つような公理系$LP$を考えることができます2。これを古典論理の公理系と呼ぶことにします。
| LPの規則 | 別名 | 説明 |
|---|---|---|
| 演繹規則 | $\to I$ | $A$を仮定して$B$が導出できるとき、仮定なしに$A \to B$が導出できる |
| 前件肯定 | $\to E$ | $A$, $A \to B$を仮定して$B$が導出できる |
| 背理法 | $\neg I$ | $A \to (D \land \neg D)$を仮定して$\neg A$が導出できる |
| 二重否定除去 | $\neg E$ | $\neg \neg A$から$A$が導出できる |
| $\land$導入 | $\land I$ | $A, B$から$A \land B$を導出できる |
| $\land$除去 | $\land E$ | $A \land B$から$A$が導出できる。また、$B$も導出できる。 |
| $\lor$導入 | $\lor I$ | $A$から$A \lor B$が導出できる。また、$B \lor A$も導出できる。 |
| $\lor$除去 | $\lor E$ | $A \lor B, A \to C, B \to C$から$C$が導出できる。 |
この体系の特徴として、恒真式はすべて公理系$LP$の定理であり、逆に公理系$LP$の定理はすべて恒真式であることが知られています(自然演繹の完全性・健全性)。言い換えると、論理式に現れる命題変数に具体的な真偽値を代入していって、全体が偽になる組み合わせが一つでもあれば定理ではなく、そうでないならば必ず定理として証明を与えることができます。
直観主義論理 - 二重否定除去を抜いた公理系LIP
$LP$では、完全性と健全性のおかげで、真偽値を代入するだけで$LP$の定理かどうかが判別できました。ここで、$LP$から二重否定除去の規則を取り除き、新たな否定除去規則を加えた体系$LIP$を考えることができます2。つまり、
| LIPの規則 | 別名 | 説明 |
|---|---|---|
| 演繹規則 | $\to I$ | $A$を仮定して$B$が導出できるとき、仮定なしに$A \to B$が導出できる |
| 前件肯定 | $\to E$ | $A$, $A \to B$を仮定して$B$が導出できる |
| 背理法 | $\neg I$ | $A \to (D \land \neg D)$を仮定して$\neg A$が導出できる |
| 否定除去 | $\neg E$ | $(D \land \neg D)$から$A$が導出できる |
| $\land$導入 | $\land I$ | $A, B$から$A \land B$を導出できる |
| $\land$除去 | $\land E$ | $A \land B$から$A$が導出できる。また、$B$も導出できる。 |
| $\lor$導入 | $\lor I$ | $A$から$A \lor B$が導出できる。また、$B \lor A$も導出できる。 |
| $\lor$除去 | $\lor E$ | $A \lor B, A \to C, B \to C$から$C$が導出できる。 |
とします。このような論理体系を、直観主義論理と呼びます。
直観主義論理においては、命題論理で成り立つ定理が成り立たない場合が存在します。主要な例としては、
- 二重否定除去：$\neg \neg A \to A$
- 排中律：$A \lor \neg A$
などがあります。IPC Botに論理式を投げると、直観主義で証明できるかをチェックしてくれます。
定理でない恒真式があることからわかる通り、直観主義論理の「意味」というのは、古典論理のように真偽値を代入して必ずしも確定するものではありません。この体系に「意味」を導入するために、クリピキ意味論などというものが存在するそうです。Scala-proofsでは直接的な利用はしませんが、調べてみるのもよいかもしれません。
カリーハワード対応 - 型と命題の対応
カリーハワード対応と呼ばれる対応が存在し、これは(単純型付けラムダ計算以上の強さの)型システムと直観主義論理の間の対応を与えます。
具体的には、抽象型 A, B, C...を直積型(_, _)、直和型Either[_, _]、関数型_ => _、否定￢[A] := A => ⊥に適用して作った型は、具体的な実装が存在するとき、またその時に限り、直積を$\land$、直和を$\lor$、関数型を$\to$で置き換えた公理系LIPの定理に対応します。メソッド関数の実装が証明と対応し、仮定はラムダ式の引数、結論は具体的な値という置き換えがされます。
ここで、$\perp$は「恒偽」、つまり値が存在しないような型を指します。Scalaにおいては、Nothingがこの役目を担っています。実際、このような対応付けをすると、$LIP$の規則で保障される基礎的な導出規則が証明できることがわかります。例えば、$\lor$除去規則の証明をコードで書くと、
def removeDisjunction[A, B, C]: Either[A, B] => (A => C) => (B => C) => C = {
asm1: Either[A, B] => asm2: (A => C) => asm3: (B => C) => {
asm1 match {
case Left(a) => asm2(a)
case Right(b) => asm3(b)
}
}
}
のようになります。
次の記事では、直観主義論理で証明できないような恒真式をScalaでどのように表現するか、について述べます。
-
正確には、"unreducible"な型コンストラクタ。DottyでのHKT実装に関する論文の6ページ目を参照のこと。 ↩
-
論理学 | 野矢 茂樹 (ISBN-13: 978-4130120531) P.66, 167 を参考 ↩