このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

論理式の集合とは何か?

セミナーで受けた質問ですが、一般的な話なので、応答をこちらに書きます。命題を形式化した構文的対象物が論理式です。この論理式の集合を正確に定義するとどうなるのか? という話です。

内容:

用途と論理を決める

論理式には、絶対的唯一の定義があると思っている方がいるかも知れませんが、それは誤解です。プログラミング言語が何十何百もあるのはご存知でしょう。プログラミング言語ごとにその構文は違います。同様に、論理式(の言語)も人工言語なので、何十何百もあります。論理式の言語と集合は、使用状況と好みに応じてその場その場で作る(定義する)ものだと考えたほうがいいでしょう。

ただし、論理式(の言語と集合)を定義するための、だいたいのガイドラインはあります。このガイドラインも唯一ではなくて、いくつもあります。多様多彩な世界なんです。ここでは、典型的なガイドラインと、そのガイドラインに沿った構文定義の実例をひとつ挙げます。

まず用途が決まらないと、論理式を定義することが出来ないので、ここでは、自然数の計算や、自然数に関わる推論を行うことを目的にします。そして、どんな論理を使うかを決めます。ここでの例では、一番ポピュラーな古典論理を使うことにします。

基本記号を全部挙げる

目的と論理が決まったら、使う記号をすべて列挙します。このとき、記号を分類するガイドラインが役に立ちます。

  1. 定数記号
  2. 変数記号
  3. 演算記号〈関数記号〉
  4. 述語記号〈関係記号〉
  5. 論理記号〈論理結合子記号と限量子記号〉
  6. 補助記号

説明は後にして、各種の記号を並べてしまいます。

  1. 定数記号: '0', '1'
  2. 変数記号: すぐ下で定義する
  3. 演算記号: '+', '*'
  4. 述語記号: '=', '≦'
  5. 論理記号: '∧', '¬', '∀'
  6. 補助記号: '(', ')', ',', '.'

変数記号は無限個あるので、書き並べるわけにいきません。変数記号は次のように決めます。

  • 英字〈ラテン文字〉小文字1文字、またはその後に数字〈digit〉を任意個付けたもの。

例えば、'x', 'a', 'x1', 'k123' などは変数です。'x1'のような複数文字でも、全体としてひとつの記号とみなします。'x'と'1'に分解したりはしません。

上記の基本記号を選んだ方針や理由を述べておきましょう。利便性は考慮せず(実際、不便になります)基本記号を節約する方針です。

  • 定数記号は'0'と'1'だけなので、例えば2を表すには "1 + 1"とする。
  • 演算記号は'+'と'*'だけなので、引き算や割り算は(必要なら)後で定義する。
  • 述語記号も、'≧'や'<'が必要なら後で定義する。
  • 論理記号も通常より少ない。古典論理を使うので、ド・モルガンの法則などを根拠に後から定義できる。
    • A∨B は、¬(¬A∧¬B) と後で定義する。
    • ∃x.A は、 ¬∀x.¬A と後で定義する。
    • A⇒B は、¬A∨B と後で定義する。
  • 自然数しか扱わないので、型の指定はしない。したがって型を表す記号は入ってない。

今までに挙げた記号を基本記号〈{basic | atomic | primitive} symbol〉と呼びます。いくつかの基本記号を、デタラメでもいいので並べたものを記号列〈{string | sequence} of symbols〉と呼びます。複数文字の単一記号もあるので、記号列内の記号をピッタリくっつけるわけにはいきません。空白を挟むことにします。また、記号列全体は二重引用符で囲みます。例えば:

  • "a1 0 ¬ k123 * ≦ ∀ . 1"

こういうデタラメな記号列では、空白(区切り記号)が必要ですが、文法〈構文規則〉で制限した記号列(それが後述する項や論理式)では、空白は必須ではなくなります。例えば、次の記号列は論理式ですが、実際には空白は不要です。

  • "∀ n , m . ¬ ∀ q , r . ( ¬ ( ( n = ( ( q * m ) + r ) ) ∧ ( ( r ≦ m ) ∧ ¬ ( r = n ) ) ) )"

'∃'や'<'を使うことを許して、括弧も適宜省略して書くなら:

  • "∀n,m.∃q,r.(n = q*m + r ∧ r < m)"

構文の定義

記号列のほとんどはデタラメなゴミです。ゴミではない、我々が使うべき記号列をハッキリさせる規則が構文規則〈文法〉です。構文規則の記述には、BNFバッカス/ナウア形式〉が便利であり標準的でもあります。

プログラミング言語に多少の馴染みがあるのなら、次の記事を読むと構文定義(や意味定義)の方法が手っ取り早く分かるでしょう。

BNFに関しては、「UMiToL言語の構文」の節に簡単な例と他の記事への参照があります。

というわけで、構文の定義にはBNFを使うことにします。構文定義の際に、項の定義と論理式の定義の二段階に分けます。〈term〉とは、(今の場合)自然数を表す式のことで、論理式〈formula〉は命題を表す式です。

「項と論理式に分けて定義する」というのもガイドラインのひとつで、「分けないで定義する」というガイドライン(流儀)もあります*1。僕は、分けたほうが分かりやすいと感じています。

項の定義
基本項 ::= '0' | '1' | 変数記号
項 ::= 基本項 | '(' 項 '+' 項 ')' |  '(' 項 '*' 項 ')' | '(' 項 ')'

次は基本項の例です。

  • 0
  • 1
  • x
  • a
  • x1
  • k123

基本項は、記号ひとつからなる記号列なので、"0", "1", "x1" のように書くべきでしょうが、もう二重引用符や空白を律儀に書くのはやめます。

変数記号は無限個あるので、基本項も無限個あります。次は、基本項とは限らない一般の項の例です。

  • ((1 + 0) + 1)
  • ((x*1) + (((1 + 1) + 1)*k123))

上記の構文規則に従えば、演算するごとに括弧で囲むので、括弧が大量に付きます。0, 1, 2, 3, 4 のような定数も次の項で表現します。

  • 0
  • 1
  • (1 + 1)
  • ((1 + 1) + 1)
  • (((1 + 1) + 1) + 1)

人が読み書きするにはひどく不便ですが、機械による処理が単純化されます。

論理式の定義
基本論理式 ::= '(' 項 '=' 項 ')' | '(' 項 '≦' 項 ')'
論理式 ::= 基本論理式 | 論理式 '∧' 論理式 | '¬' 論理式 | '∀' 変数並び '.' '(' 論理式 ')' | '(' 論理式 ')'
変数並び ::= 変数 | 変数並び ',' 変数

この規則から、括弧が相当にうるさい論理式が定義されます。とりあえずは、処理しやすい(構文解析木が作りやすい)構文定義をしました。人間の読み書きのためには、別に略記の規則を導入すればいいでしょう。

もちろん、最初から人間可読性〈human readability〉に優れた構文を定義してもいいですが、構文定義も構文解析処理も複雑になります。ここらへんの兼ね合いは、なかなかに難しいですね。

論理式の集合

最初に決めた基本記号の集合をSymbolとします。

  • Symbol = {'0', '1', '+', '*', '=', '≦', '∧', '¬', '∀', '(', ')', ',', '.', 'x', 'a', 'x1', 'k123', ...}

集合Symbolの要素を並べたものである記号列の集合をSymbol*と書きます。右肩の星はクリーネスターと呼び、「並べたもの」を表す星です。集合Symbol*の要素を幾つか挙げれば:

  • "a1 0 ¬ k123 * ≦ ∀ . 1" ∈ Symbol*
  • "(((1 + 1) + 1) + 1)" ∈ Symbol*
  • "∀ n , m . ¬ ∀ q , r . ( ¬ ( ( n = ( ( q * m ) + r ) ) ∧ ( ( r ≦ m ) ∧ ¬ ( r = n ) ) ) )" ∈ Symbol*

集合Symbol*のなかで、項と認められる記号列の集合をTermとします。もちろん、Term⊆Symbol* です。さらに、論理式と認められる記号列の集合をFormulaとします。Formula⊆Symbol* です。

以上で、集合Formulaがちゃんと定義されました。ここで重要な注意は、集合Formulaは、今ここで「自然数の計算や、自然数に関わる推論を行うこと」を目的に「古典論理を使うこと」を前提に作られたことです。別な目的で別な論理を使うなら、別なFormulaが定義されます。この世に唯一のFormulaが在るわけじゃありません。たくさんのたくさんのFormulaが在り得るのです。

コンテキストに関する注意

集合Formulaの要素、つまり論理式に対してその“意味”を考えます。通常は、論理式の意味は外延(あるいは真理集合)として与えます。例えば、"(x + y = 10)∧(x ≦ y)" の意味なら、{(x, y)∈N2 | (x + y = 10)∧(x ≦ y)} という集合がその意味になります。

しかし、外延(真理集合)が {(x, y, z)∈N3 | (x + y = 10)∧(x ≦ y)} であってもかまいません。「zという変数は入ってないからダメ」とか言うと、「3次元空間R3内で、x2 + y2 = 1 は円筒を表す」といった主張も禁止することになります。何がマズイのかと言うと、変数を含む(含まなくてもいいのだが)論理式と、変数の領域を一緒に考えてないことです。

変数(複数かも知れない)が走る領域に対する指定をコンテキスト〈context〉と呼びます。コンテキストが明示されず、暗黙の前提で済まされることは多いです。そんなときは、「論理式」にコンテキストが暗黙に刷り込まれていると解釈します。

暗黙の前提は、誤解と混乱の原因になるのでやめたほうがいい(あるいは、ほどほどにしたほうがいい)と僕は思いますが、現実には多用されているのでご注意ください。

*1:この例で言えば、型Natと型Boolを導入すれば、項だけで話が済みます。