mutex Tech BlogPublicationへの投稿
🧑‍⚖

ド・モルガンの法則を TypeScript で証明してみた

tony
に公開
TypeScript
型
math
logic
Tech blog
tech

はじめに

本記事では、命題論理の定理であるド・モルガンの法則を、TypeScript を用いて証明することを目指します。

ド・モルガンの法則とは、任意の命題 P, Q について、

\neg (P \lor Q) \leftrightarrow \neg P \land \neg Q \\ \neg (P \land Q) \leftrightarrow \neg P \lor \neg Q

が成り立つことを言います。

さて証明です。命題の真偽のみに興味があるので、P, Q を p: boolean, q: boolean で表現し、全パターン試してみればいいわけです。\neg は !、\land は &&、\lor は ||、 \leftrightarrow は === と対応づけることができます。

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 にまとめてあるので、適宜手を動かして遊びながら読んでみてください。

型システムと命題論理の対応づけ

命題論理では、P, Q, R のようなアルファベットで表される命題変数と、以下の結合子の組み合わせによって命題を表します。

記法 名称
\bot 矛盾
\neg P 否定
P \land Q 連言
P \lor Q 選言
P \to Q 含意
P \leftrightarrow Q 同値

これらの型システムとの対応づけにおいて、重要なのは以下の二点です。

  • 命題を型で表現する。
  • 命題に対応する型の値が存在することは、その命題を事実たらしめる。

したがって証明に相当するのは、型エラーを出すことなく、また any へのキャストのようなズルをせずに、命題に対応する型の値を構成することです。

以下では、当該文脈で命題 P を事実と定めることを P を仮定すると言い、当該文脈で命題 P を事実と結論づけることを P を導くと言います。

含意

P を仮定すると Q が導けるとき、それを以て P \to Q が導けます。また、P \to Q および P を仮定すると、Q が導けます。対応する型は以下のようになります。

type Imp<P, Q> = (_: P) => Q

即ち、ジェネリクス <P, Q> について、引数が P 型で戻り値が Q 型であるような関数型です。P 型の値があれば Q 型の値が構成できるとき、それを関数化すれば Imp<P, Q> 型の値が得られます。また、Imp<P, Q> 型の値と P 型の値があれば、関数適用によって Q 型の値が得られます。

使用例として、(P \to (P \to Q)) \to (P \to 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)

連言

P および Q を仮定すると、P \land Q が導けます。また、P \land Q を仮定すると、P ないし Q が導けます。対応する型は以下のようになります。

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 型の値が得られます。

使用例として、P \land Q \to Q \land P の証明を載せておきます。

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()
    )

選言

P ないし Q を仮定すると、P \lor Q が導けます。また、P \lor Q および P \to R および Q \to R を仮定すると、R が導けます。対応する型は以下のようになります。

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 型の値が得られます。

使用例として、P \lor Q \to Q \lor P の証明を載せておきます。

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)
    )

矛盾

\bot を仮定すると、任意の命題が導けます。対応する型は以下のようになります。

type Bot = never

TypeScript では、never は全ての型の部分型です。したがって Bot 型の値があれば、それを任意の型の値と見做すことができます。

使用例として、P \lor \bot \to P の証明を載せておきます。

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
    )

否定

\neg P は P \to \bot を略記したものです。

type Not<P> = Imp<P, Bot>

同値

P \leftrightarrow Q は (P \to Q) \land (Q \to P) を略記したものです。

type Iff<P, Q> = And<Imp<P, Q>, Imp<Q, P>>

ド・モルガンの法則の証明

ここまでに定義した型を使って、実際に証明を行いましょう。

\neg (P \lor Q) \leftrightarrow \neg P \land \neg Q の証明

まず、\to を証明します。

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))
    )

次に、\gets を証明します。

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)
      )

これらをまとめることで \leftrightarrow の証明とできます。

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 の証明

\gets の方が簡単なのでそちらから行きます。

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())
    )

次に \to ですが、実はここまでに定義した型だけでは証明ができません。ここまでの体系は直観主義論理と呼ばれ、排中律、即ち P \lor \neg P という公理を認めていないものになります。「はじめに」で述べた「命題に必ず真偽があるという公理」とはこれのことです。排中律を認めた体系は古典論理と呼ばれます。

排中律を以下のように定義します。

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 で証明することができました。

ちなみに、定理証明支援系とそうでない言語の本質的な違いは、依存型と呼ばれる機能にあります。依存型とは値に依存する型のことで、これを導入すると全称量化 \forall や存在量化 \exists を表現できるようになり、一気に適用先が広がります。詳しくは Lean 4 のテキストをご参照ください。

mutex Tech Blog
mutex Tech BlogPublication

東京大学発のスタートアップ 株式会社mutex の Tech Blogです！

Discussion