はじめに
本記事では、命題論理の定理であるド・モルガンの法則を、TypeScript を用いて証明することを目指します。
ド・モルガンの法則とは、任意の命題
が成り立つことを言います。
さて証明です。命題の真偽のみに興味があるので、p: boolean, q: boolean で表現し、全パターン試してみればいいわけです。!、&&、||、 === と対応づけることができます。
const booleans = [true, false]
booleans.forEach(
p =>
booleans.forEach(
q => {
console.assert(!(p || q) === !p && !q)
console.assert(!(p && q) === !p || !q)
}
)
)
上記のコードは何も出力せずに終了します。!(p || q) も !p && !q も、p, q が false, false のときだけ true になり、それ以外の場合は false になります。同様に、!(p && q) も !p || !q も、p, q が true, true のときだけ false になり、それ以外の場合は true になります。
これにてド・モルガンの法則を TypeScript で証明することができました。
……で、終わりでは味気ないと思います。
実は、
- プログラムを実行せずとも型検査を通過した段階で証明終了とでき、
- 命題論理より広範な数学の定理証明にまで拡張でき、
- 命題に必ず真偽があるという公理の使用を最小限にできる
方法があります。(3 つ目は少し解りにくいかと思います。後ほどちゃんと説明します。)
そもそも、型システムの下でのプログラムの記述は、数学の定理証明と本質的に等価であることが知られています。このことはカリー＝ハワード同型対応と呼ばれます。ここでいう定理証明とは、いくつかの決まった推論規則のみから所望の命題を導く、自然演繹という枠組みに則ったものです。
これを利用したのが Lean や Coq のような定理証明支援系と呼ばれる言語たちです。このような言語たちが定理証明のための特有の機能を持っていることは事実ですが、一方で、我々エンジニアが普段ソフトウェア開発の現場で使っている言語でも、ある程度の証明記述ができるということを見ていきたいと思います。
コードはこちらの Playground にまとめてあるので、適宜手を動かして遊びながら読んでみてください。
型システムと命題論理の対応づけ
命題論理では、
| 記法 | 名称 |
|---|---|
| 矛盾 | |
| 否定 | |
| 連言 | |
| 選言 | |
| 含意 | |
| 同値 |
これらの型システムとの対応づけにおいて、重要なのは以下の二点です。
- 命題を型で表現する。
- 命題に対応する型の値が存在することは、その命題を事実たらしめる。
したがって証明に相当するのは、型エラーを出すことなく、また any へのキャストのようなズルをせずに、命題に対応する型の値を構成することです。
以下では、当該文脈で命題
含意
type Imp<P, Q> = (_: P) => Q
即ち、ジェネリクス <P, Q> について、引数が P 型で戻り値が Q 型であるような関数型です。P 型の値があれば Q 型の値が構成できるとき、それを関数化すれば Imp<P, Q> 型の値が得られます。また、Imp<P, Q> 型の値と P 型の値があれば、関数適用によって Q 型の値が得られます。
使用例として、
const exampleImp = <P, Q>(): Imp<Imp<P, Imp<P, Q>>, Imp<P, Q>> =>
impPImpPQ => // `Imp<P, Imp<P, Q>>` 型の値 `impPImpPQ` を受け取る。
// `Imp<P, Q>` 型の値を構成する。
p => // `P` 型の値 `p` を受け取る。
// `Q` 型の値を構成する。
impPImpPQ(p)(p)
連言
class And<P, Q> {
private left: P
private right: Q
private constructor(left: P, right: Q) {
this.left = left
this.right = right
}
static intro<P, Q>(left: P, right: Q): And<P, Q> {
return new And(left, right)
}
elimLeft(): P {
return this.left
}
elimRight(): Q {
return this.right
}
}
即ち、ジェネリクス <P, Q> について、P 型と Q 型の直積型です。P 型の値と Q 型の値が揃っていれば、intro メソッドによって And<P, Q> 型の値が得られます。また、And<P, Q> 型の値があれば、elimLeft メソッドによって P 型の値が得られ、elimRight メソッドによって Q 型の値が得られます。
使用例として、
const exampleAnd = <P, Q>(): Imp<And<P, Q>, And<Q, P>> =>
andPQ => // `And<P, Q> 型の値 `andPQ` を受け取る。
// `And<Q, P>` 型の値を構成する。
And.intro(
// `Q` 型の値を構成する。
andPQ.elimRight(),
// `P` 型の値を構成する。
andPQ.elimLeft()
)
選言
class Or<P, Q> {
private body: {tag: "left", payload: P} | {tag: "right", payload: Q}
private constructor(body: typeof this.body) {
this.body = body
}
static introLeft<P, Q>(left: P): Or<P, Q> {
return new Or<P, Q>({tag: "left", payload: left})
}
static introRight<P, Q>(right: Q): Or<P, Q> {
return new Or<P, Q>({tag: "right", payload: right})
}
elim<R>(left: Imp<P, R>, right: Imp<Q, R>): R {
switch(this.body.tag) {
case "left":
return left(this.body.payload)
case "right":
return right(this.body.payload)
}
}
}
即ち、ジェネリクス <P, Q> について、P 型と Q 型の直和型です。P 型の値があれば introLeft メソッドによって、Q 型の値があれば introRight メソッドによって Or<P, Q> 型の値が得られます。また、ジェネリクス <R> について、Or<P, Q> 型の値と Imp<P, R> 型の値と Imp<Q, R> 型の値が揃っていれば、elim メソッドによって R 型の値が得られます。
使用例として、
const exampleOr = <P, Q>(): Imp<Or<P, Q>, Or<Q, P>> =>
orPQ => // `Or<P, Q>` 型の値 `orPQ` を受け取る。
// `Or<Q, P>` 型の値を構成する。
orPQ.elim(
// `Imp<P, Or<Q, P>>` 型の値を構成する。
p => // `P` 型の値 `p` を受け取る。
// `Or<Q, P>` 型の値を構成する。
Or.introRight(p),
// `Imp<Q, Or<Q, P>>` 型の値を構成する。
q => // `Q` 型の値 `q` を受け取る。
// `Or<Q, P>` 型の値を構成する。
Or.introLeft(q)
)
矛盾
type Bot = never
TypeScript では、never は全ての型の部分型です。したがって Bot 型の値があれば、それを任意の型の値と見做すことができます。
使用例として、
const exampleBot = <P>(): Imp<Or<P, Bot>, P> =>
orPBot => // `Or<P, Bot>` 型の値 `orPBot` を受け取る。
// `P` 型の値を構成する。
orPBot.elim(
// `Imp<P, P>` 型の値を構成する。
p => // `P` 型の引数 `p` を受け取る。
// `P` 型の値を構成する。
p,
// `Imp<Bot, P>` 型の値を構成する。
bot => // `Bot` 型の値 `bot` を受け取る。
// `P` 型の値を構成する。
bot
)
否定
type Not<P> = Imp<P, Bot>
同値
type Iff<P, Q> = And<Imp<P, Q>, Imp<Q, P>>
ド・モルガンの法則の証明
ここまでに定義した型を使って、実際に証明を行いましょう。
\neg (P \lor Q) \leftrightarrow \neg P \land \neg Q
まず、
const deMorgan1Left = <P, Q>(): Imp<Not<Or<P, Q>>, And<Not<P>, Not<Q>>> =>
notOrPQ => // `Not<Or<P, Q>>` 型の値 `notOrPQ` を受け取る。
// `And<Not<P>, Not<Q>>` 型の値を構成する。
And.intro(
// `Not<P>` 型の値を構成する。
p => // `P` 型の値 `p` を受け取る。
// `Bot` 型の値を構成する。
notOrPQ(Or.introLeft(p)),
// `Not<Q>` 型の値を構成する。
q => // `Q` 型の値 `q` を受け取る。
// `Bot` 型の値を構成する。
notOrPQ(Or.introRight(q))
)
次に、
const deMorgan1Right = <P, Q>(): Imp<And<Not<P>, Not<Q>>, Not<Or<P, Q>>> =>
andNotPNotQ => // `And<Not<P>, Not<Q>` 型の値 `andNotPNotQ` を受け取る。
// `Not<Or<P, Q>>` 型の値を構成する。
orPQ => // `Or<P, Q>` 型の値 `orPQ` を受け取る。
// `Bot` 型の値を構成する。
orPQ.elim(
// `Imp<P, Bot>` 型の値を構成する。
p => // `P` 型の値 `p` を受け取る。
// `Bot` 型の値を構成する。
andNotPNotQ.elimLeft()(p),
// `Imp<Q, Bot>` 型の値を構成する。
q => // `Q` 型の値 `q` を受け取る。
// `Bot` 型の値を構成する。
andNotPNotQ.elimRight()(q)
)
これらをまとめることで
const deMorgan1 = <P, Q>(): Iff<Not<Or<P, Q>>, And<Not<P>, Not<Q>>> =>
And.intro(
// `Imp<Not<Or<P, Q>>, And<Not<P>, Not<Q>>>` 型の値を構成する。
deMorgan1Left(),
// `Imp<And<Not<P>, Not<Q>>, Not<Or<P, Q>>>` 型の値を構成する。
deMorgan1Right()
)
\neg (P \land Q) \leftrightarrow \neg P \lor \neg Q
const deMorgan2Right = <P, Q>(): Imp<Or<Not<P>, Not<Q>>, Not<And<P, Q>>> =>
orNotPNotQ => // `Or<Not<P>, Not<Q>>` 型の値 `orNotPNotQ` を受け取る。
// `Not<And<P, Q>>>` 型の値を構成する。
orNotPNotQ.elim(
// `Imp<Not<P>, Not<And<P, Q>>>` 型の値を構成する。
notP => // `Not<P>` 型の値 `notP` を受け取る。
// `Not<And<P, Q>>` 型の値を構成する。
andPQ => // `And<P, Q>` 型の値 `andPQ` を受け取る。
// `Bot` 型の値を構成する。
notP(andPQ.elimLeft()),
// `Imp<Not<Q>, Not<And<P, Q>>>` 型の値を構成する。
notQ => // `Not<Q>` 型の値 `notQ` を受け取る。
// Not<And<P, Q>>` 型の値を構成する。
andPQ => // `And<P, Q>` 型の値 `andPQ` を受け取る。
// `Bot` 型の値を構成する。
notQ(andPQ.elimRight())
)
次に
排中律を以下のように定義します。
const excludedMiddle = <P>(): Or<P, Not<P>> =>
undefined as any
公理は証明ができないので、any へのキャストを使って無理やり型検査を通すことになります。
これを使うことで、以下のように証明ができます。
const deMorgan2Left = <P, Q>(): Imp<Not<And<P, Q>>, Or<Not<P>, Not<Q>>> =>
notAndPQ => // `Not<And<P, Q>>` 型の値 `notAndPQ` を受け取る。
// `Or<Not<P>, Not<Q>>` 型の値を構成する。
excludedMiddle<P>().elim(
// `Imp<P, Or<Not<P>, Not<Q>>>` 型の値を構成する。
p => // `P` 型の値 `p` を受け取る。
// `Or<Not<P>, Not<Q>>` 型の値を構成する。
Or.introRight(
// `Not<Q>` 型の値を構成する。
q => // `Q` 型の値 `q` を受け取る。
// `Bot` 型の値を構成する。
notAndPQ(And.intro(p, q))
),
// `Imp<Not<P>, Or<Not<P>, Not<Q>>>` 型の値を構成する。
notP => // `Not<P>` 型の値 `p` を受け取る。
// `Bot` 型の値を構成する。
Or.introLeft(notP)
)
const deMorgan2 = <P, Q>(): Iff<Not<And<P, Q>>, Or<Not<P>, Not<Q>>> =>
And.intro(
// `Imp<Not<And<P, Q>>, Or<Not<P>, Not<Q>>>` 型の値を構成する。
deMorgan2Left(),
// `Imp<Or<Not<P>, Not<Q>>, Not<And<P, Q>>>` 型の値を構成する。
deMorgan2Right()
)
まとめ
これにてド・モルガンの法則を TypeScript で証明することができました。
ちなみに、定理証明支援系とそうでない言語の本質的な違いは、依存型と呼ばれる機能にあります。依存型とは値に依存する型のことで、これを導入すると全称量化
Discussion