プログラマのための述語論理

たまにやっている「プログラマのための××○○」モノでがんす。これは一回読み切り。

表題どおり、述語論理の入り口を説明する目的があります。それと、ラムダ式もクロージャも高階の型／関数もないようなプログラミング言語（具体例にはJavaを使いますが）で、述語論理のような形式体系をどの程度表現できるかを試してみるのが、もうひとつの目的。それで、「やっぱりJavaみたいな言語はダメだ」と思うか、「けっこう、なんとかなるもんだ」と思うか、… さー、どちらでしょう。

[追記]変なJavaのコードでワケワカになってしまうときは、「述語論理はJavaScripを使うべきだった」のJavaScriptコードを参照してください（面倒で、すみません）。[/追記]

※長いよ。印刷の時はサイドバー消えます。

内容：

最初に命題論理を一瞥＜いちべつ＞

命題論理ってのは、真偽（boolean）値に関する計算のことです。それだけ？ 言い出すと色々あるんだけど、とりあえずそれだけでいいと思います。僕の印象では、命題論理をやり過ぎなんだよな。いきなり述語論理をやったほうが実用的だし、かえって理解しやすいと思うよ。命題論理で息切れしてはバカバカしい。

命題論理の値はtrueとfalseの2つだけで、演算記号は次：

記号	意味	プログラミング言語での記号
∧	かつ（連言）	&&
∨	または（選言）	||
¬	ではない（否定）	!
⇒	ならば（含意）	あまり見かけない

プログラミング言語で「⇒」に対応する記号がない（「==>」とか「implies」を使う例があるけど）のは、p ⇒ qがif (p) q else trueで表現できるからでしょう。ちなみに、次の3つの式は同じ結果になります。

1. p ⇒ q
2. ¬p ∨ q
3. if (p) q else true

p, qが取る値の組み合わせは4種しかないので、すべての場合をチェックすれば確認できます。

述語とは

述語（predicate）とは、ある集合X上で定義されて真偽値を値とする関数です。真偽値の集合{true, false}をBで表現すると、X上の述語は、X→B という関数型を持つ対象物だといえます。

Javaでは、X→Bのような型や対象（関数そのもの）を直接表現するのは難しいので、型パラメータX付きのインターフェースで代用しましょう。

public interface Predicate<X> {
 boolean isTrueFor(X x);
}

述語の例：

/* nullな引数は考えない */

class Positive implements Predicate<Integer> {
 public boolean isTrueFor(Integer n) {
  return n > 0;
 }
}

class Zero implements Predicate<Integer> {
 public boolean isTrueFor(Integer n) {
  return n == 0;
 }
}

class Empty implements Predicate<String> {
 public boolean isTrueFor(String s) {
  return s.equals("");
 }
}

引数が2つとか3つの述語（ときに関係とも呼ばれる）もありますが、今回は1引数の述語だけを考えます。

述語の論理計算

述語に対しても、真偽値と同じような論理計算を行うのが述語論理（predicate logic）です。ですから、∧、∨などを述語に対しても定義します。論理の教科書では、述語p, qに対するp∧qは次のように定義します。

 (p∧q)(x) = p(x)∧q(x)

同じ記号∧が使われていますが、左側の∧は述語に対する演算、右側の∧は真偽値に対する演算です。なにげなく自然に定義されちゃうのですが、左側の∧は“高階の演算”なので、プログラミング言語に直すと、そう簡単ではありません。

次のようにでもしましょうか。

/** 述語論理の演算 */
public class Predicative {
 public static <X> Predicate<X>
  and(final Predicate<X> p, final Predicate<X> q) {
   return new Predicate<X>() {
     public boolean isTrueFor(X x) {
      return p.isTrueFor(x) && q.isTrueFor(x);
     }
   };
  }

 // ...

}

なんだかJavaのソースじゃないみたい。Predicative.and というstaticメソッドを定義しているんですが、これは意味的には p:X→Bとq:X→Bを引数に取って、新しい述語（B値の関数）X→Bを返すものです。つまり、関数引数で関数戻り値の高階関数です。しかも、述語の定義域であるXはパラメータ（事前に固定されてない）ので、総称の高階関数です。そんなものをJavaで無理繰り書こうとするからこんなことに、、、、

∨（or）、¬（not）、⇒（implication, implies）も同様です。（⇒は、∨と¬から作れるので別に定義しなくてもかまいませんけど。）んで、述語に対する論理演算を確かめてみるコードを書いてみましょう：

public class PredicateLogicDemo_01 {
 public static void main(String[] args) {
  Predicate<Integer> PositiveOrZero =
    Predicative.or(new Positive(), new Zero());
  Predicate<String> NotEmpty = Predicative.not(new Empty());

  int[] intData = {1, 0, -2, 3, -1};
  String[] strData = {"Hello", "", "World"};

  for (int n : intData) {
    boolean truth = PositiveOrZero.isTrueFor(n);
    System.out.println("PositiveOrZero " + n + " = " + truth);
  }
  for (String s : strData) {
    boolean truth = NotEmpty.isTrueFor(s);
    System.out.println("NotEmpty " + s + " = " + truth);
  }
 }
}

C:\tmp>java PredicateLogicDemo_01

PositiveOrZero 1 = true

PositiveOrZero 0 = true

PositiveOrZero -2 = false

PositiveOrZero 3 = true

PositiveOrZero -1 = false

NotEmpty Hello = true

NotEmpty  = false

NotEmpty World = true

これが述語論理のキモ：限量子

論理演算子∧、∨、¬、⇒を述語に対して定義しただけでは、述語論理とは呼べませんよ。「∀」、「∃」って変わった記号を見たことありますか？ これが述語論理のキモなんです。

記号∀は「任意の」とか「すべての」と読みます。∀x.(x*x ≧ 0) は∀の使い方の例です。この例は、「任意の（すべての）xに対して、(x*x ≧ 0) だ」という意味です。

一方、記号∃は「ある…に対して」とか「…が存在する」と読みます。∃x.(x*x = 2) なら、「あるxに対して（xが存在して）、(x*x = 2) だ」ということです。これは、2の平方根の存在を主張しています。

さてところで、「任意の」とか「存在する」とか言っても、どの範囲で考えているかで意味や結果が変わってきます。∀x.(x*x ≧ 0) はいつでも正しいようですが、xに複素数を許すと正しくなくなります。∃x.(x*x = 2)は、xを整数の範囲で考えたら偽ですが、実数の範囲なら真ですね。そこで、∀x∈Z.(x*x ≧ 0) とか ∃x∈R.(x*x = 2) のように変数が動く範囲（領域、集合）を添えます。ここでZは整数全体、Rは実数全体を（習慣として）表します。

今出てきた∀と∃を限量子とか限量記号と呼びます（減量じゃないよ）。∀は全称限量子（全称記号）と呼び、∃は存在限量子（存在記号）です。用語が難しげですが、気にしないでください。

述語pがあると、∀x∈X.(p(x)) とか ∃x∈X.(p(x)) として限量子付き論理式を作れます。この論理式の真偽は原理的に定まるはずです。なぜなら、集合Xのメンバーを取り出してはpに適用する（真偽を調べる）作業を、しらみつぶしに実行すればいいからです。

限量子のプログラミング

いまさっき「しらみつぶしに実行すればいい」と言いましたが、普通それはできません。本来、∀や∃を使うのは、集合Xが無限集合のときだからです。Xが無限ならコンピュータにやらせても無限走行するだけで埒＜らち＞があきません。

それじゃ困るのでXが有限の場合を考えましょう。Xが有限の場合でも、まったく無意味ってわけではありませんからね。こんな感じでどうでしょう：

public class Predicative {

 // ...

 public static <X> boolean forAll(Iterable<X> domain, Predicate<X> pred) {
  for (X x : domain) {
    if (! pred.isTrueFor(x)) {
     return false;
    }
  }
  return true;
 }

 // ...
}

Predicative.forSomeも同様ですね。

集合リテラルもどき

限量子Predicative.forAllとPredicative.forSomeのデモサンプルを書こうとすると、有限集合の領域が必要なのですが、Javaだと{3, -1, 5, 0}のようなリテラルで書けないのでヤッカイです。それで、リテラルに近い表現ができるように、Ordered.Setというメソッドを定義しましょう。newは不要で、Ordered.Set(3, -1, 5, 0) と書けます。Ordered.Set(0, 3, -1, 3, 5, 0)のように書いても重複は除かれます（集合なので）。そして、書いた順番で要素が記憶されます（orderedなので）。実は、ordered setはリストです（よってiterable）。

import java.util.*;

public class Ordered {
 public static <X> List<X> Set(X... elements) {
  List<X> list = new ArrayList<X>();
  Map<X, Boolean> map = new HashMap<X, Boolean>();
  for (X x : elements) {
    if (map.get(x) == null) {
     list.add(x);
     map.put(x, true);
    }
  }
  return list;
 }
}

public class OrderedSetDemo {
 public static void main(String[] args) {
  for (int n : Ordered.Set(0, 3, -1, 3, 5, 0)) {
    System.out.println(n);
  }
  for (String s : Ordered.Set("Hello", "", "Hello", "World")) {
    System.out.println(s);
  }
 }
}

C:\tmp>java OrderedSetDemo

0

3

-1

5

Hello
World

Ordered.Setを使って、限量子のデモを書いてみます。

public class PredicateLogicDemo_02 {
 public static void main(String[] args) {
  Predicate<Integer> PositiveOrZero = Predicative.or(new Positive(), new Zero());
  Predicate<String> NotEmpty = Predicative.not(new Empty());

  String formula;
  boolean truth;

  formula ="∀s∈{\"Hello\", \"\", \"World\"}.(¬empty(s))";
  truth = Predicative.forAll(Ordered.Set("Hello", "", "World"), NotEmpty);
  System.out.println(formula + " ==> " + truth);

  formula = "∀s∈{\"Hello\", \"Hello\", \"World\"}.(¬empty(s))";
  truth = Predicative.forAll(Ordered.Set("Hello", "Hello", "World"), NotEmpty);
  System.out.println(formula + " ==> " + truth);

  formula = "∃x∈{-1, -2, 0, 3}.(positive(x)∨zero(x))";
  truth = Predicative.forSome(Ordered.Set(-1, -2, 0, 3), PositiveOrZero);
  System.out.println(formula + " ==> " + truth);

  formula = "∃x∈{-1, -2, -3}.(positive(x)∨zero(x))";
  truth = Predicative.forSome(Ordered.Set(-1, -2, -3), PositiveOrZero);
  System.out.println(formula + " ==> " + truth);
 }
}

C:\tmp>java PredicateLogicDemo_02

∀s∈{"Hello", "", "World"}.(¬empty(s)) ==> false

∀s∈{"Hello", "Hello", "World"}.(¬empty(s)) ==> true

∃x∈{-1, -2, 0, 3}.(positive(x)∨zero(x)) ==> true

∃x∈{-1, -2, -3}.(positive(x)∨zero(x)) ==> false

とまー、少しは述語論理に親しみを持てましたでしょうか？