Scalaで論理体系を作る話 - 2. 命題論理その2

直観主義論理はカリーハワード対応に見て取れる通り、型付きラムダ計算ほどの単純なモデルが表現できるシンプルな論理ですが、制約も多いのでした。この記事は、より「強い」、つまりより強力な論理である古典論理をどうScalaプログラム内で構築できるのか、について記述します。

Scalaで論理体系を作る話 - 1. 命題論理その1

その前に…

補足 - 証明における禁忌

Scalaプログラム上の証明は、書き方によっては意味を為さなくなります。そのような二つのケースとして、例外を投げることと**自分自身を証明に使ってしまう(循環論法)**ことの二つが挙げられます。

論理式として、$A$を考えます。これはどのような型Aにも値が存在するという主張であり、本来ならば証明はできません。

例外を投げるというのは、例えば

def incompleteProof[A]: A = throw new NotImplementedError()

といったものを指します。throw式は型 Nothing を持つため、結果がthrow式になっていると証明を放棄しているにもかかわらずコンパイルが通ってしまいます。「証明を後に回す」用途で???を置くことはありますが、証明が完了したときにはthrow式が関数定義内に現れてはいけません。

循環論法は、自分自身を右辺にて呼び出すような関数に対応します。例えば、

def selfReferentialProof[A]: A = selfReferentialProof[A]

といったものを指します。また、相互再帰(二つの関数がそれぞれを呼び出す)であってもなりません。
証明内では、すでに実装された関数のみ呼び出すことが許されます。

証明の意味論

直観主義論理の範囲では、証明が上に説明されているような性質を満たすように記述されている場合、関数呼び出しを行った時に例外を投げず必ず停止します(単純型付きラムダ計算の停止性)。正しい証明で評価されない箇所に再帰呼び出しを仕込めるため、逆は真ではありません。

しかし、後述するように、古典論理の体系を考えると正しい証明であっても必ずしもそのような良い性質を持つとは限りません。古典論理のScala上での表現は、どちらかというと純粋に形式的なものと捉えるのが楽であると思います(継続渡しスタイルなどが深く関わっているようですが、理解しきれていませんので疑問として書いておきます)。

疑問：古典論理の証明を表現するコードの妥当性に単純な意味論はあるか？

本題

前回の記事にて、否定演算子￢が、type ￢[A] = A => Nothingのように表されると書きました。また、公理系LIPは公理系LPの二重否定除去則$\neg \neg A \to A$をより弱い否定除去により置き換えていたのでした。つまり、プログラム内で二重否定除去を表現できれば古典論理が表現できたことになります。

二重否定除去をコードで書くと以下のようなシグネチャになります。

def removeDoubleNegation[A]: ((A => Nothing) => Nothing) => A = ???

これは、「「Aを渡すと例外が飛ぶ関数」を受け取ると例外が飛ぶ関数」からAの関数と捉えることができます。本当にこのようなものが実装できるのでしょうか？

公理化か実装か

プログラム上で実装"できそうにない"ような形式体系を考える場合、traitに定義したメソッドを公理として持ちまわす、ということができます。例えば、

trait ClassicalLogic {
  def removeDoubleNegation[A]: ((A => Nothing) => Nothing) => A
}

として、古典論理に依存する体系をすべてClassicalLogicの実装に依存するようにすれば、形式的に証明を行っていくことができます。ここで、ClassicalLogicの実装が真に存在しない場合、体系の意味論的解釈をプログラム上で考えることができなくなります。

しかし、Scalaにはこれを表現する方法が存在します。ですので、traitではなく実装を持つobjectに二重否定除去を書くことができます。

広域脱出による二重否定除去

JavaやScalaは、例外がthrowされると、catch節に捕捉されるまでスタックを一気に抜け続けます。
そこで、「評価されたら例外を投げる」ような関数を引数に渡すことで、「関数が評価されたら瞬時に呼び出し元に戻る」ようなものが表現できます。

Scalazでの実装

抽象構造を提供するライブラリ、Scalazに、大域脱出により二重否定除去を表現するコードがありますので、改変したものを紹介¹します。

def removeDoubleNegation[A](f: ((A => Nothing) => Nothing)): A = {
  // 制御用の例外のクラス
  case class Control(arg: (A => Nothing) => Nothing) extends Throwable(null, null, true, false)

  try {
    f(arg: A => throw new Control(arg))
  } catch {
    case Control(arg) => arg
  }
}

fは返り値の型がNothingであるので、引数を評価するか、評価せずにControl以外の例外を投げるかのどちらかです。

Control以外の例外が投げられた場合は、catchをすり抜けて外部に例外を吐き出します。この時、try式の評価値の型はNothingであるため、型検査に通ります。

そうではなくfの引数が引数argにて評価された場合は、即座にControl(arg)がremoveDoubleNegationのtry節まで投げられ、catchにて捕捉されます(ControlはremoveDoubleNegationでしか定義されないので、他の箇所で捕捉されることが無いことに注意してください)。この時、実体arg: Aが例外とともに呼び出し元に戻されるため、argを返して終わりです。

疑問：
「例外を勝手に投げない」というルールを守っている場合は、最初のケースになることはない。
しかし、後述するようにコンパイルに通るコードが例外を投げる場合がある。なぜ？

糖衣構文

実は先ほどのコードはたった一行で表現できます。

def removeDoubleNegation[A](f: ((A => Nothing) => Nothing)): A = f(a => return a)

xuweiさんに詳細を教えていただきました。

Javaと違って、ラムダを終わりとするreturnではなく、そこから一番内側のメソッドの終わりになります。
(なお、そういうパターンの場合、内部実装としては例外で実装されます)

— Kenji Yoshida (@xuwei_k) July 11, 2018

はい。
-Xprint:jvm
という、途中の抽象構文木をコンパイル時に表示してくれる特殊なコンパイルオプションつけるとこんな感じにhttps://t.co/O2gU8rLGFk

— Kenji Yoshida (@xuwei_k) July 11, 2018

先ほどのコードと全く同じように展開されることがわかります。

True or Falseがなぜわかる？

直観主義論理で証明できず、古典論理で証明できる有名な例の一つとして_排中律_が挙げられます。Twitterで「XXである場合とそうでない場合があるぞい」と主張している排中律博士Botを見かけたことがあるかもしれません。

つまり何が言いたいかっていうとラーメンは神である場合と神でない場合があるぞい

— 排中律博士bot (@dr_haichu_bot) January 10, 2019

排中律とは、どんな命題Aに対しても、Aが真であるか、Aが偽であるかのどちらかであることを主張します。
論理式で書くと、

A \lor \neg A

を主張します。

これは"真偽値"が意味論になる古典論理においては最も自明な定理のうちの一つなのですが、カリーハワード対応との相性はよいものとは言えません。コードでこの主張を記述すると、

def middleExcl[A]: Either[A, A => Nothing] = ???

となります。実際、二重否定除去removeDoubleNegationが与えられていると、次のような実装が存在します。

def middleExclusion[A]: Either[A, A => Nothing] = {
  val negNegProp: (Either[A, A => Nothing] => Nothing) => Nothing = { negProp =>
    val negNegA: (A => Nothing) => Nothing = { notA =>
      val prop: Either[A, A => Nothing] = Right(notA)
      negProp(prop)
    }
    val a: A = removeDoubleNegation(negNegA)
    val prop: Either[A, A => Nothing] = Left(a)
    negProp(prop)
  }
  removeDoubleNegation(negNegProp)
}

このコードは再帰も例外を投げるコードも表面的には含まれていませんが、先ほど言及した「直観主義論理の証明の良い性質」が崩れていることがわかります。

Aに恒偽の型、例えばNothingを入れることを考えましょう。すると、NothingまたはNothing => Nothingのどちらかが入ったEitherが戻されるはずです。前者を評価すると例外が飛ぶので、例外が飛んでほしくなければ後者でなくてはなりません。

今度はAに恒真の型、例えばUnitを入れることを考えましょう。ジェネリックな0引数関数は、型パラメータに依らず同じ値が返ってくるはずです。つまり、例外が飛んでほしくなければUnit => Nothingが返ってきます。ここで、この戻り値にUnitを適用すると、例外が飛びます。

排中律は不自然？

カリーハワード対応によると、型の値の存在が定理と対応するのでした。すなわち、middleExclが証明できるということは、どのような型Aに対しても、AかA => Nothingを返すような実装が存在するということです。これはプログラムの上ではかなりおかしな話であり、例外を発生させないようにするためには「できるだけ」Aを返すべきですが、値が存在しない場合は後者を返さなくてはなりません。しかし、当然コンパイラに事前に値の在住性を知る余地などありません。

型チェッカを納得させるような実装ができるとはいえ、排中律はこのような形式化の中では不自然な結果であると言えると思います²。

述語論理へ

次の記事では、述語論理のScala上での表現を解説します。述語論理の表現はできているもののなかなか難しく、非常に実験的な内容になるとは思います。

1. Copyright (c) 2009-2018 Tony Morris, Runar Bjarnason, Tom Adams, Kristian Domagala, Brad Clow, Ricky Clarkson, Paul Chiusano, Trygve Laugstøl, Nick Partridge, Jason Zaugg, Sam Halliday All rights reserved. ↩

2. ホンマか？ ↩