このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

命題のリストの扱い方 (A9P7)

RSS練習問題

※この記事は「記事9 問題集7」

単一の論理式〈形式化された命題〉だけではなくて、論理式のリストを徹底的に使い倒した最初の人はおそらくゲンツェンだろう。プログラミングで言えば、単一タプル引数（パックされた多引数）、単一タプル戻り値（パックされた多値戻り値）ではなくて、“ほんとの多引数”、“ほんとの多値戻り値”を使うことになる。

ほんとの多引数は普通だが、ほんとの（パックされない）多値戻り値はあまり使われていない。が、データフロー＆ポイントフリースタイルなら、複数のチャンネルに出力データを同時に流す多値も自然だろう。選言的リストだと、「複数チャンネルに同時に流す」ではなくて、「複数チャンネルのうちのどれかを選択して流す」になる -- このような引数受け渡し方式は一般的ではない。カリー／ハワード対応が示唆するデータ構造／制御構造が、必ずしも利用されてはいないわけだ。… てなことを考えながらこの問題をやるのも面白いかも知れない（面白くないかも知れない）。

これより前に行うべき練習は：

内容：

  1. 論理式のリストの書き方
  2. 題材に使う論理式
  3. 論理式のリストのスコット・ブラケット
  4. 論理式のリストの連接

論理式のリストの書き方

すべての論理式はコンテキスト付き〈コンテキスト内にある〉と考える。閉論理式が空なコンテキストをもつとき、空なコンテキストは省略することがある。

  • (x∈R| x ≧ 0 ) ←… コンテキストを省略はできない。
  • (| 1 ≧ 0) ←… コンテキストを省略して単に 1 ≧ 0 と書いてもよい。だが、コンテキストは存在し、コンテキスト領域は1である。
  • (x, y∈R| 1 ≧ 0) ←… 閉論理式だが、コンテキストが空ではないので、コンテキストを省略できない。

本来、論理結合子（∧, ∨, ¬, ⇒）による演算は、同じコンテキストを持つ論理式に対してだけ定義される。現実には、コンテキストを暗黙に水増ししてから論理演算を行っている。ここでは、暗黙の水増しは許さない。水増しは明示的に行う。

[補足]
f:R→R と g:R→R に対して、関数fと関数gの足し算 f + g は意味を持つ、しかし、h:N→R に対して、f + h は意味を持たない。また、k:R2→R に対して、f + k も意味を持たない。

域〈domain | 始域〉が異なる2つの関数に対して、足し算が無意味なのと同様に、コンテキストが異なる論理式の論理演算も無意味である。本来意味がないことが現実に行われている場合は、なにかしら暗黙のトリックが存在する。形式化の際には、そのようなトリックを明示化する必要がある。
[/補足]

論理式のリストの構成と書き方は次の約束に従う。

  1. 異なるコンテキストの論理式をリストにすることは出来ない。コンテキストの水増しやリネームを明示的にして、コンテキストを揃える必要がある。絵では、ワイヤーをボックス／ケーブルシース／ストライプ内に入れるか、ボックス／ケーブルシース／ストライプを拡大する。あるいは、代入〈substitution〉で変換する。（この節最後を参照。）
  2. 論理式（＝コンテキスト付き論理式）(α| A), (α| B) の連言的リストは、∧((α| A), (α| B)) となるが、コンテキストをまとめて ∧(α| A, B) のように書く。絵では、∧(α| … ) は、連言的なボックス／ケーブルシース／ストライプとなる。
  3. 同様に、論理式の選言的リストは、∨(α| A, B) のように書く。絵では、∨(α| … ) は、選言的なボックス／ケーブルシース／ストライプとなる。
  4. 連言的リストを∧-リスト、選言的リストを∨-リストともいう。
  5. sを '∧' または '∨' の値を取る変数、αをコンテキスト、A1, ..., An をコンテキストなしの論理式の並びとして、リストは s(α| A1, ..., An) の形に書ける。
  6. 連言的リスト ∧(α| A1, ..., An) を、[α| A1, ..., An] と書いてもよい。
  7. 選言的リスト ∨(α| A1, ..., An) を、[α| A1 | ... | An] と書いてもよい。縦棒記号が2つの意味で使われているが、最初の縦棒の左はコンテキスト。
  8. 単一の論理式からなるリストは、論理式そのものと同一視する。∧((α| A)) = ∨((α| A)) = (α| A)
  9. 空なリスト [α|] は使わない。∧(α|), ∨(α|) は使ってもよい。通常、∧(α|) は (α|T) に、∨(α|) は (α|⊥) に置き換える。
  10. 論理式のリストをスコット・ブラケットのなかに入れるときは、外側の角括弧は書かなくてもよい。〚[α| A, B]〛 = 〚α| A, B〛, 〚[α| A | B]〛 = 〚α| A | B〛
  11. したがって、スコット・ブラケット内に現れるカンマは連言と解釈し、リスト区切りとしての縦棒は選言と解釈する。
  12. 左上付きマーカーを使った 〚∧(α| A, B)〛, 〚∨(α| A, B)〛 でも、もちろん構わない。この場合は、連言的か選言的かの区別は左上付きマーカー '∧', '∨'で明確に分かる。
  13. [α| A1, ..., An], [α| A1 | ... | An] という書き方は、実用性を考慮した略記で、理論上は s(α| A1, ..., An) という書き方のほうが好ましい。

具体的な記法として選言的リスト／連言的リストをどう書くか（それは容易に変更され得る）より、概念としての選言的リスト／連言的リストを把握することが大事。

「ボックス／ケーブルシース／ストライプ」に付いては、次の記事の図・画像を眺めれば見当は付くだろう。（見当が付かなきゃ付かないで別にかまわんが。）

題材に使う論理式

次の40個のコンテキストなしの論理式は、「命題と、そのコンテキスト／真理集合」で使ったコンテキスト付き論理式からコンテキストを外したものである。これらのコンテキストなし論理式を参照するときは、P1, P2, ..., P40 とする。例えば、P1 は 1 + 2 = 3 のことであり、P30 は x2 + y2 = 4 ∧ x + y ≧0 のことである。

  1. 1 + 2 = 3
  2. 1 + 2 < 3
  3. 12 = 22
  4. 3 ≦ 5 ∧ 3 ≦ 3
  5. 1 + 2 < 3 ⇒ 12 = 22
  6. 1 + 2 < 3 ∨ 12 = 22 ∨ 3 ≦ 3
  7. (3 ≦ 5 ∧ 3 ≦ 3) ⇒ 1 + 2 < 3
  8. (3 ≦ 5 ∨ 3 ≦ 3) ⇒ ¬(1 + 2 < 3)
  9. ¬(1 + 2 < 3) ⇒ (1 + 2 = 2)
  10. 1 + 2 = 3 ⇒ (1 + 2 < 3 ⇒ 12 = 22)
  11. ∀n∈N.(n ≧ 0)
  12. ∃n∈N.(n < 0)
  13. ∀n∈N.∃m∈N.(m ≧ n)
  14. ∀n∈N.∃m∈N.(m < n)
  15. ∀x∈R.∃y∈R.(y2 = x)
  16. ∀x∈R.∃y∈R.(x ≧ 0 ⇒ y2 = x)
  17. ∃y∈R.∀x∈R.(x ≧ 0 ⇒ y2 = x)
  18. ∀x∈R.∀y∈R.∃n∈N.((x ≧ 0 ∧ y > 0) ⇒ yn ≧ x)
  19. x < 0 ∨ 1 < x
  20. 0 < x ∧ x < 1
  21. 0 < x ∧ 1 < x
  22. x < 0 ⇒ x2 = 1
  23. x2 = 1 ⇒ x < 0
  24. x2 = 1 ⇒ x = 0
  25. x2 = 1 ⇒ x = 1
  26. x2 = 1 ⇒ (x = 1 ∨ x = -1)
  27. (x2 = 1 ∧ x ≧ 0) ⇒ x = 1
  28. (x2 = 1 ∧ x ≧ 0) ⇒ (x = 1 ∨ x = -1)
  29. x2 + y2 = 1
  30. x2 + y2 = 4 ∧ x + y ≧0
  31. x2 + y2 = 4 ∧ x + y ≧ -1
  32. x2 + y2 = 1 ∨ x + y = 0
  33. x2 + y2 = 1 ⇒ x = 1
  34. x = 1 ⇒ x2 + y2 = 1
  35. (x = 1 ∧ y = 0) ⇒ x2 + y2 = 1
  36. x2 + y2 = 1 ⇒ x + y ≦ 2
  37. x2 + y2 = 1 ⇒ x + y ≦ 1
  38. x2 + y2 ≦ 1 ⇒ x + y ≦ 2
  39. x2 + y2 ≦ 1 ⇒ x + y ≦ 1
  40. (x2 + y2 ≦ 1 ∧ x + y ≦ 0) ⇒ x + y ≦ 1

リストとして、∧(x, y∈R| P1, P30) と書いた場合、

  • ∧(x, y∈R| 1 + 2 = 3, x2 + y2 = 4 ∧ x + y ≧0)

のことであり、その意味は、

  • ∧((x, y∈R| 1 + 2 = 3), (x, y∈R| x2 + y2 = 4 ∧ x + y ≧0))

である。そのスコット・ブラケットは次のように計算できる。



    〚∧(x, y∈R| P1, P30)〛

  = 〚∧((x, y∈R| 1 + 2 = 3), (x, y∈R| x2 + y2 = 4 ∧ x + y ≧0))〛

  = 〚x, y∈R| 1 + 2 = 3〛∩〚x, y∈R| x2 + y2 = 4 ∧ x + y ≧0)〛

  = 〚x, y∈R| x2 + y2 = 4 ∧ x + y ≧0〛

コンテキストを変更して ∧(x, y∈N| P1, P30) とすると、そのスコット・ブラケット 〚∧(x, y∈N| P1, P30)〛 は違った値になる。

論理式のリストのスコット・ブラケット

次の論理式のリストのスコット・ブラケット（の値）を求めよ（図示せよ）。

  1. ∧(x∈R| P1, P11, P19)
  2. ∧(x∈R| P1, P22)
  3. ∧(x∈R, y∈R| P5, P20, P29, P40)
  4. ∨(x∈R| P1, P11, P19)
  5. ∨(x∈R| P1, P22)
  6. ∨(x∈R, y∈R| P5, P20, P29, P40)

問題が少数しかないが、このタイプの練習問題は、自分でいくらでも作れる。

  1. 40個の命題から、複数の（いくつでもよい）命題を選んで並べる。A1, A2, ..., An とする。
  2. コンテキストαを選ぶ。αは次のいずれかの形を使う； (), (x∈X), (y∈Y), (x∈X, y∈Y) 。ここで、X, Y には N, Z, Q, R のいずれかを選ぶ。i = 1, 2, ..., n のすべてに対して、Aiに現れる変数が、コンテキストαにも現れるように注意する（そうでないと、変数の型〈変域〉が不明になる）。
  3. sとして、'∧', '∨' のどちらかを選ぶ。
  4. 論理式のリスト s(α| A1, A2, ..., An) を作る。
  5. 出来たリストのスコット・ブラケット 〚s(α| A1, A2, ..., An)〛 を求める。スコット・ブラケット（の値）は、コンテキストαの領域 Dom(α) の部分集合である。

問題を作る過程自体が、理解を促すのにとても有効だから、上記の手順を実行してみることをオススメする。

論理式のリストの連接

以下、s, t を '∧', '∨' のどちらかを表す変数、α, β をコンテキストとして、論理式のリストを s(α| A1, ..., An), t(β| B1, ..., Bm) のように書く。この書き方が一番紛れがない。

2つのコンテキスト α, β がコンフリクトするとは、

  1. αとβに同じ名前の変数が出現する。
  2. 同じ名前の変数に対する型〈変域〉が、αとβでは異なる。

例えば、(x∈R, y∈R) と (n∈N, x∈R, y∈Z) は変数名yにおいてコンフリクトする。しかし、(x∈R, y∈R) と (n∈N, x∈R) はコンフリクトしてない。

コンテキストαとβがコンフリクトしてないとき、αとβの連接〈concatenation〉α#β は、単にリストとしての連接である。

  • 例： (x∈R, y∈R)#(n∈N, x∈R) = (x∈R, y∈R, n∈N, x∈R)

同じ変数宣言が繰り返されることは問題ではない（許される）。なお、次の操作を施してもコンテキストは同値である。

  • 変数宣言の並び順を変える（交換）。
  • 変数宣言を重複させる（複製）、または重複した変数宣言をまとめる（縮約）。

2つの論理式のリスト s(α| A1, ..., An), t(β| B1, ..., Bm) の連接も定義したいが、いつでも連接できるわけではない。次の条件を満たすとき連接可能である。

  1. sとtが等しい。つまり、両方とも連言的リストであるか、両方とも選言的リストであるとき。
  2. αとβが連接可能である。つまり、αとβがコンフリクトしてない。

この条件を満たすとき、連接は次のように定義する。

  • s(α| A1, ..., An) # s(β| B1, ..., Bm) := s(α#β| A1, ..., An, B1, ..., Bm)

連接演算は、常に定義されるわけではないが、定義される範囲内において結合的かつ単位的である。単位元は空なリスト ∧(ε|) と ∨(ε|) である。ここで、εは空なコンテキスト () を表す。

単位元が2つあることから分かるように、連接演算の記号'#'は、連言的連接演算と選言的連接演算を一緒に表現した演算子記号である。連言的連接演算の記号と選言的連接演算の記号を別にするときは、新しい記号を導入せずに、区切り記号（カンマと縦棒）を流用する（オーバーロードする）。

  • ∧(α| A1, ..., An), ∧(β| B1, ..., Bm) := ∧(α#β| A1, ..., An, B1, ..., Bm)
  • ∨(α| A1, ..., An) | ∨(β| B1, ..., Bm) := ∨(α#β| A1, ..., An, B1, ..., Bm)

あるいは、

  • [α| A1, ..., An], [β| B1, ..., Bm] := [α#β| A1, ..., An, B1, ..., Bm]
  • [α| A1 | ... | An] | [β| B1 | ... | Bm] := [α#β| A1 | ... | An | B1 | ... | Bm]

このテの流用（オーバーロード）は頻繁に行われるが、学習者を混乱させる要因になっている。

一時的に違う記号、例えば && と ‖ で表しておいて、慣れたら、, と | に切り替える、という方法もあるだろう。

  • ∧(α| A1, ..., An) && ∧(β| B1, ..., Bm) := ∧(α#β| A1, ..., An, B1, ..., Bm)
  • ∨(α| A1, ..., An) ‖ ∨(β| B1, ..., Bm) := ∨(α#β| A1, ..., An, B1, ..., Bm)

が、二段階になると余計な手間が増える、ということもある。なかなか難しいね。

論理式のリストの連接のスコット・ブラケット

先の問題で使った論理式のリストを再掲する。

  1. ∧(x∈R| P1, P11, P19)
  2. ∧(x∈R| P1, P22)
  3. ∧(x∈R, y∈R| P5, P20, P29, P40)
  4. ∨(x∈R| P1, P11, P19)
  5. ∨(x∈R| P1, P22)
  6. ∨(x∈R, y∈R| P5, P20, P29, P40)

論理式のリストは大文字ギリシャ文字で表すのが習慣なので、それぞれを Γ1, Γ2, ..., Γ6 とする。2つのリストが連接可能かどうかは：

↓1st＼2nd→ Γ1 Γ2 Γ3 Γ4 Γ5 Γ6
Γ1 Γ1#Γ1 Γ1#Γ2 Γ1#Γ3 - - -
Γ2 Γ2#Γ1 Γ2#Γ2 Γ2#Γ3 - - -
Γ3 Γ3#Γ1 Γ3#Γ2 Γ3#Γ3 - - -
Γ4 - - - Γ4#Γ4 Γ4#Γ5 Γ4#Γ6
Γ5 - - - Γ5#Γ4 Γ5#Γ5 Γ5#Γ6
Γ6 - - - Γ6#Γ4 Γ6#Γ5 Γ6#Γ6

連接可能な組み合わせを取り出すと：

  1. Γ1#Γ1 = Γ1, Γ1
  2. Γ1#Γ2 = Γ1, Γ2
  3. Γ1#Γ3 = Γ1, Γ3
  4. Γ2#Γ1 = Γ2, Γ1
  5. Γ2#Γ2 = Γ2, Γ2
  6. Γ2#Γ3 = Γ2, Γ3
  7. Γ3#Γ1 = Γ3, Γ1
  8. Γ3#Γ2 = Γ3, Γ2
  9. Γ3#Γ3 = Γ3, Γ3
  10. Γ4#Γ4 = Γ4 | Γ4
  11. Γ4#Γ5 = Γ4 | Γ5
  12. Γ4#Γ6 = Γ4 | Γ6
  13. Γ5#Γ4 = Γ5 | Γ4
  14. Γ5#Γ5 = Γ5 | Γ5
  15. Γ5#Γ6 = Γ5 | Γ6
  16. Γ6#Γ4 = Γ6 | Γ4
  17. Γ6#Γ5 = Γ6 | Γ5
  18. Γ6#Γ6 = Γ6 | Γ6

問題： これらの連接を実際に計算し、そのスコット・ブラケット（の値＝真理集合）を求めよ（図示せよ）。

このタイプの練習問題は、自分でいくらでも作れる。

論理式のリストと連接に関する法則

2つのリスト Γ = s(α| A1, ..., An), Δ = t(β| B1, ..., Bm) があるとき、ΓとΔが同値だとは：

  1. s = t である。つまり、両方とも連言的リストであるか、両方とも選言的リストであるとき。
  2. αとβが同値である。（並び順の交換、複製、縮約の操作で同じコンテキストになる）
  3. (A1, ..., An) と (B1, ..., Bm) が、並び順の交換、複製、縮約の操作で同じになる。

2つのリストΓとΔが同値なとき、Γ 〜 Δ と書くことにする。関係 〜 は、実際に同値関係である。

  1. Γ 〜 Γ
  2. Γ 〜 Δ ならば、Δ 〜 Γ
  3. Γ 〜 Δ, Δ 〜 Σ ならば、Γ 〜 Σ

連言的リストの連言的連接（演算子記号はカンマ）と、選言的リストの選言的連接（演算子記号は縦棒）は次の法則を満たす。

  1. (Γ, Δ), Σ = Γ, (Δ, Σ)
  2. ∧(ε|), Γ = Γ
  3. Γ, ∧(ε|) = Γ
  4. (Γ | Δ) | Σ = Γ | (Δ | Σ)
  5. ∨(ε|) | Γ = Γ
  6. Γ | ∨(ε|) = Γ

同値関係で考えると：

  1. Γ 〜 Γ' かつ Δ 〜 Δ' ならば、Γ, Δ 〜 Γ', Δ'
  2. Γ 〜 Γ' かつ Δ 〜 Δ' ならば、Γ | Δ 〜 Γ' | Δ'
  3. Γ, Δ 〜 Δ, Γ
  4. Γ, Γ 〜 Γ
  5. Γ | Δ 〜 Δ | Γ
  6. Γ | Γ 〜 Γ

結局、イコールではなくて同値関係で考えると、連言的連接演算も選言的連接演算も、ベキ等可換なモノイドになる。今出てきた言葉に関しては：

[補足]
コンテキストに関して同様な同値関係 α 〜 β が定義できて：

  1. (α#β)#γ = α#(β#γ)
  2. ε#α = α
  3. α#ε = α
  4. α 〜 α' かつ β 〜 β' ならば、α#β 〜 α'#β'
  5. α#β 〜 β#α
  6. α#α 〜 α

ΓとΔが同値なら、それらのコンテキストどうしも同値である。
[/補足]

連接とスコット・ブラケットとの関係は：

  1. 〚∧(ε|)〛 = 〚(ε|T)〛 = 1
  2. 〚∨(ε|)〛 = 〚(ε|⊥)〛 = 0
  3. Γ 〜 Δ ならば、〚Γ〛 \stackrel{\sim}{=} 〚Δ〛 （\stackrel{\sim}{=} は集合としての同型）

〚Γ, Δ〛や〚Γ | Δ〛を〚Γ〛と〚Δ〛で記述しようとすると、単純に 〚Γ〛∩〚Δ〛, 〚Γ〛∪〚Δ〛 では済まず、けっこう複雑な記述になる。ので割愛（興味ある人は頑張って記述してみて）。

ΓとΔが同じコンテキストを持つときなら、

  1. 〚Γ, Δ〛 = 〚Γ〛∩〚Δ〛
  2. 〚Γ | Δ〛= 〚Γ〛∪〚Δ〛

が成立する。