檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-12-01 (金)

有限集合とは何だろう への補足

| 13:09 | 有限集合とは何だろう への補足を含むブックマーク

有限集合とは何だろう(ストーリー付き練習問題集)」にちょっと補足します。Xが有限のとき、S⊆X である集合Sは有限集合ですが、このことを示すストーリーに触れます。

内容:

  1. 余談:宇都宮市民の髪の毛の本数
  2. [m]の部分集合に関する補題
  3. 証明要求とその書き換え
  4. 集合のあいだの同型の構成
  5. おわりに

余談:宇都宮市民の髪の毛の本数

Wikipeiaの「鳩の巣原理」の項目に、「ロンドンには、同じ本数の髪の毛を持った少なくとも2人の人間が存在する」の証明が載っています。

この証明の根拠になっているのは次の(現実世界の)事実です。

  • 人の髪の毛の本数は15万本ほどである。
  • ロンドンの人口は100万人以上である。
  • 100万本以上の髪の毛を持つ人はいない。

これらの事実に鳩の巣原理を適用して結論を得ます。

人口100万はかなり安全にみた数で、人口50万でも大丈夫でしょう。つまり、50万本以上の髪の毛を持つ人はいないとします。餃子しか思い浮かばない宇都宮市*1でも50万以上の人口があるので、次の命題は成立します。

  • 宇都宮市には、同じ本数の髪の毛を持った少なくとも2人の人間が存在する

[m]の部分集合に関する補題

有限集合とは何だろう(ストーリー付き練習問題集)」で話題にした中心的な命題は次でした。

  • 集合Xは有限 :⇔ ∃n∈N.( X ¥stackrel{¥sim}{=} [n] ) ---(有限集合の定義)
  • ∀X:Set.∀n, m∈N.( (X ¥stackrel{¥sim}{=} [n] ∧ X ¥stackrel{¥sim}{=} m) ⊃ n = m ) ---(基数の一意性)

この2つをまとめて書くために、一意存在を意味する'∃!'を使うと便利です。∃!x.P(x) の意味は、∃x.P(x) ∧ ( P(x)∧P(y) ⊃ x = y ) です。単なる存在命題より強い命題(きつい条件)になります。

  • ∀X:Set.( Xは有限集合 ⊃ ∃!n∈N.( X ¥stackrel{¥sim}{=} [n] ) ) ---(有限集合に対する基数の一意存在)

これから、「集合として同型」と「基数が同じ」が同値であることが分かります。つまり、次が成立します。

  • ∀X, Y:Set.( X, Yは有限 ⊃ ( X ¥stackrel{¥sim}{=} Y ⇔ ∃n∈N.( X ¥stackrel{¥sim}{=} [n] ∧ Y ¥stackrel{¥sim}{=} [n]) ) )

含意を記号'⊃'で表しているのに、同値は'⇔'でバランス悪いんだけど勘弁してね(バランスをとるなら、'⊂⊃'かな?)。

さて、集合として同型でない状況を分析するときは、次の命題がキーになります。

  • ∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ m ) )

自然言語で書くならば:

  • Sは集合だとして、自然数mに対して S⊆[m] ならば、S ¥stackrel{¥sim}{=} [n] かつ n ≦ m であるような自然数nが存在する。

これが正しいなら、[m]の部分集合は有限集合であり、その基数はm以下であることがわかります。

これから、基数の大小に関する次の命題も導けます。

  • X, Yが有限集合のとき、X⊆Y ならば、Xの基数はYの基数以下である。

もっと一般化すれば:

  • X, Yが有限集合のとき、XからYへの単射が存在するならば、Xの基数はYの基数以下である。

証明要求とその書き換え

前節で提示した命題 ∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ m ) ) を証明しましょう。数学的帰納法を使うと、当たり前すぎる命題でも証明できることが多いので、数学的帰納法でやっつける方針で。

まず、今問題にしている命題をターゲット命題とする証明要求を次の形に書ます。

 Γ/ S:Set |-? ∀m∈N.(
                  S⊆[m]
                  ⊃
                  ∃n∈N.(
                      S ¥stackrel{¥sim}{=} [n] ∧ n ≦ m
                  )
                )

変数mに注目して、ターゲット命題を ∀m∈N.P(m) の形だと読みます。すると、数学的帰納法のベースとステップは次のようになります。

  • ベース: S⊆[0] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ 0)
  • ステップの前件: S⊆[k] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k )
  • ステップの後件: S⊆[k + 1] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k + 1 )

ベースのほうは、n = 0 として示せます。すると、課題(=証明要求)はステップだけになります。ステップの前件を前提('|-?'の左側)に、ステップの後件をターゲットにすれば、次の証明要求となります。

 Γ/ S:Set, k:N,
     S⊆[k] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k )
  |-?
     S⊆[k + 1] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k + 1 )

“ステップの後件の前件”も証明要求の前提側に移動すれば:

 Γ/ S:Set, k:N,
     S⊆[k] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k ),
     S⊆[k + 1]
  |-?
     ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k + 1 )

ターゲットは存在命題なので、条件にみあう自然数nを構成または検索すればいいことになります。

集合のあいだの同型の構成

前節で、∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ m ) ) に対する証明要求を書き換えて、ターゲットは次の命題としました。

  • ∃n∈N.( S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k + 1 )

S ¥stackrel{¥sim}{=} [n] を定義に従って展開すれば:

  • ∃f:S→[n], g:[n]→S.(f;g = idS ∧ g;f = id[n] )

したがって、整数nと共に、上記を満たす写像f, gも構成しなくてはなりません。

証明要求の前提に S⊆[k + 1] が入っています。つまり、S ⊆ {0, 1, ..., k} です。k∈S か ¬(k∈S) のどちらかは常に成立します(排中律)。¬(k∈S) ならば、S⊆[k] となります。つまり、次は必ず成立します。

  • S⊆[k] ∨ k∈S

S⊆[k] のときは、前提に入っている帰納法のステップの前件から S ¥stackrel{¥sim}{=} [n] ∧ n ≦ k であるnの存在がいえます。残りは、k∈S のときにターゲットを示すことだけです。

S' = S\{k} ('\'は集合の差)と置くと、S'⊆[k] となるので、再び帰納法のステップの前件から S' ¥stackrel{¥sim}{=} [n'] ∧ n' ≦ k となるn'があります。となると、ターゲットはさらに絞れて、次の証明要求として書けます。

  • Γ'/ ¬(k∈S'), S' ¥stackrel{¥sim}{=} [n'], S = S'∪{k} |-? S ¥stackrel{¥sim}{=} [n' + 1]

ここで、Γ'は適当に調整した文脈(背景知識となる前提)です。前提にある S' ¥stackrel{¥sim}{=} [n'] から次のような f', g' の存在は保証されています。

  • f':S'→[n'], g':[n']→S', f';g' = idS', g';f' = id[n']

これらをもとに、次のような f, g を作れば要求は満たせます。S = S'∪{k}, n = n' + 1 である点に注意してください。

  • f:S'∪{k}→[n' + 1], g:[n' + 1]→S'∪{k}, f;g = idS, g;f = id[n]

f, gは次のように構成(定義)します。

  • f(i) := if (i < k) then f'(i) else n'
  • g(j) := if (j < n') then g'(j) else k

elseの部分を分かりやすく書くと、f(k) = n', g(n') = k です。こうして作った(構成した)f, gが、f;g = idS, g;f = id[n] を満たすのはすぐに分かるでしょう。

おわりに

やってみたことは、我々が直感的に当たり前だと思っていることを、適当な演繹系〈証明系 | 論理系〉のなかで証明できることを示す(実際の証明を構成する)ことです。得られる結果は「当たり前」なので、あんまり面白くないです。

「結果が面白くない」以外に、このテの話の問題点は、前提とターゲットの区別が付きにくいことです。まだ証明されてないターゲットも、内容的には当たり前なので、前提だと勘違いしがちです。

証明支援系を使うと勘違いは防げますが、お気軽に使える証明支援系がないのがまた困った話です。うーむ。

*1:宇都宮市を選んだのは僕が栃木県出身だから。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171201

2017-11-30 (木)

麺類の具・トッピングの提供形態について

| 11:57 | 麺類の具・トッピングの提供形態についてを含むブックマーク

結論を先に書くと; 麺類の具・トッピングは「載せ」と「別皿」が選べるといいな。


有澤誠先生は、コンピュータやプログラミングの先生ですが、以前(今は見つからない)エッセイのようなブログ記事のようなテキストをWebで公開していました。そのなかに天ぷらうどんの話があったと記憶してます。

「天ぷらうどんの天ぷらは、うどんに載せないほうがいい」という趣旨でした。天ぷら(かき揚げも含む)はサクサクしているのがおいしいのだから、うどんつゆに浸したら台無しだ、と。しかし、天ぷらとうどんを一緒に食べるのを否定しているわけではなくて、天ぷらをオカズにうどんを食べるのがよい、と。

僕も有澤先生の意見に同意です。しかし、ウチの長男は、つゆが滲みて柔らかくなった天ぷら衣や、つゆに油が混じるのがいいと言います。まー、好みは色々だってことです。

同様な問題は、ラーメンの具である海苔でも発生します。よく行く百麺〈ぱいめん〉だと、大きめの海苔が載っているんですが、僕は最初に取り出して食べてしまいます。海苔はパリパリのほうがおいしいと思っているからです。

海苔をスープに溶かすように混ぜたい人もいるでしょう。俺流塩ラーメンだと、海苔は載ってないのですが、無料トッピングに岩海苔があります。スープに磯の香りを付けたいなら岩海苔のほうが向いているでしょう。

*1

というわけで、有望としては、麺類の具・トッピングのたぐいは、「載せ」と「別皿」が選べるといいな。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171130

2017-11-28 (火)

有限集合とは何だろう(ストーリー付き練習問題集)

| 12:56 | 有限集合とは何だろう(ストーリー付き練習問題集)を含むブックマーク

「Xは有限集合である」とか「Xは有限集合でない」とかの表現はよく出てきますが、この有限性ってのはいったい何なんでしょう? 少しマジメに考えてみることにします。これといった予備知識を要求しませんが、マジメに考える態度は必要です。

実は、有限性を調べるのは目的じゃなくて手段です。証明の“お膳立て”シリーズとか、自然演繹ダメじゃんシリーズ(って、そんなシリーズねえけど、「存在記号の除去規則について考える」とか)に対して、例題を提供するのが、この記事の主たる目的です。この記事を読みながら、ハッキリとは書いてない証明を全部書いていくことが練習問題になります。内容的には超カンタン(当たり前)なので、明示的な証明は逆にハードです。

内容:

  1. 自然数についてよく知っているとする
  2. 論理記号など
  3. 有限性の定義
  4. 個数勘定の原理
  5. 個数勘定の補題と鳩の巣原理
  6. 個数勘定の補題数学的帰納法
  7. もう少し数学的帰納法のためのお膳立て
  8. 証明要求を順方向に並べてみる
  9. 自然数の部分集合で有限なもの

自然数についてよく知っているとする

公理的集合論では、集合ありき/集合しかない世界で考えるので、自然数集合論のなかで組み立てたりします。しかし我々は、集合を習うはるか前に自然数を習います。集合についてあまり知らなくても、自然数についてはけっこうよく知っています。

という事情から、自然数についてはよく知っているとします。「よく知っている」とは次のような事だとします。

  1. 0, 1, 2などの個々の自然数を知っている。
  2. 自然数の全体が集合Nを形成することを知っている。
  3. 自然数の加減乗除について知っている。引き算は部分演算(n ≦ m のときだけ m - n を定義)、割り算は整除を使う。
  4. 自然数の大小関係について知っている。また、加減乗除と大小関係の“関係”についても知っている。例えば、n ≦ n', m ≦ m' ならば n + m ≦ n' + m' など。

これらの知識は、だいたい小学校で習います(集合概念は小学校で習わないかな)。小学校では習わない重要な事として、数学的帰納法の原理があります。

  • 自然数の変数(集合N上を走る変数)を含む命題Pに対して、P(0) と ∀k∈N.P(k)⊃P(k + 1) が成立するなら、∀n∈N.P(n) が成立する。

記号'⊃'は「ならば」です。'⇒'を使う人が多いかも知れませんが、僕は'⊃'を使う('⇒'や'→'は他の意味で使う)ことが多いので、今回は'⊃'にします(気分によって使う記号は変わるんだけどね)。

数学的帰納法の原理は、しばしばドミノ倒しに喩えられます。最初の(0番目の)ドミノが確実に倒れ、k番目のドミノが倒れたなら(k + 1)番目も倒れることが保証されているなら、全部のドミノが倒れるはずだ、ってことです。P(0) を数学的帰納法ベース〈the base case〉、∀k∈N.P(k)⊃P(k + 1) を数学的帰納法ステップ〈the inductive/induction step〉と呼ぶことがあります。

*1

論理記号など

既に前節で論理記号を使っています。ここで使う論理記号を列挙すると:

  1. ∧ :論理AND、連言〈れんげん〉
  2. ∨ :論理OR、選言〈せんげん〉
  3. ⊃ :含意〈がんい〉
  4. ¬ :論理NOT、否定
  5. ∀ :全称限量子〈ぜんしょう・げんりょうし〉
  6. ∃ :存在限量子〈そんざい・げんりょうし〉

変数の型宣言は x:X の形にします。ここでの型は集合のことなので、Xは集合です。例えば、n:N と宣言されていれば、それ以降nは自然数の変数です。原則としては(サボらないならば)、宣言されてない変数は使えません。ただし、文脈から暗黙に宣言される(とみなす)変数を使うことはしばしばあります。

限量子∀, ∃の直後に書く変数(束縛変数)には、その場で型を指定します。∀n:N.P のような形です。ただし、∀n∈N.P のように、所属記号'∈'を使うこともあります。'∈'より':'が望ましいと思うのですが、僕はついつい'∈'で書いてしまいます。

型の指定には'∈'より':'が望ましいと書いたのは、'∈'は命題(述語論理の論理式)のなかで述語記号(関係記号)として使われるものだからです。もちろん'∈'は本来の意味 -- 要素と集合のあいだの所属関係として使います。

'∈'が出てくるってことは、常識的な集合概念は仮定するってことです。公理的集合論ではなくて、素朴集合論です。素朴集合論って何だ? ってことは、次の記事で扱っています。

有限性の定義

自然数nに対して、

  • [n] = {k∈N | k < n}

と定義します。特に、

  • [0] = {}
  • [1] = {0}

準備が出来たので、Xが有限集合であることを定義します。基本的に論理式で書きますが、すぐ下に自然言語の記述も併記します。

  • 論理式: Xは有限集合 :⇔ ∃n∈N.( X ¥stackrel{¥sim}{=} [n] ) ---(有限集合の定義)
  • 自然言語: Xは有限集合だとは、自然数nが存在して、X ¥stackrel{¥sim}{=} [n] となること。

ここで使った'¥stackrel{¥sim}{=}'は、集合として同型という意味です。その定義は:

  • 論理式: X ¥stackrel{¥sim}{=} Y :⇔ ∃f:X→Y, g:Y→X.(f;g = idX ∧ g;f = idY ) ---(集合として同型の定義)
  • 自然言語: X ¥stackrel{¥sim}{=} Y だとは、写像 f:X→Y と 写像 g:Y→X があって、f;g = idX かつ g;f = idY が成立すること。

';'は写像の図式順結合〈diagrammatic order composition〉記号、idXはXの恒等写像です。論理式の後のハイフン3つは、論理式に名前を付けるためのものです。

Xが有限集合だとは、適当な [n] = {0, 1, ..., n - 1} と1:1に対応することです。この定義は、納得しやすいものでしょう。

自然数nは、Xの要素の個数になります。しかし、上記の定義だけだと、有限集合Xに対してnが一意的に決まる保証がありません。次の定理が必要になります。

  • 論理式: (X ¥stackrel{¥sim}{=} [n] ∧ X ¥stackrel{¥sim}{=} [m]) ⊃ (n = m)
  • 自然言語: X ¥stackrel{¥sim}{=} [n] かつ X ¥stackrel{¥sim}{=} [m] ならば n = m である。

もし上の定理(今はまだ願望)が証明されれば、有限集合Xは(定義により)適当な[n]と同型で、そのようなnは一意的に決まるので、要素の個数が決まります。要素の個数を、有限集合Xの基数〈cardinality〉とか濃度と呼びます。有限でないXに対する基数は、今は考えません。

個数勘定の原理

前節で述べた定理は、我々が有限個のモノの集まりに対して、モノの個数を勘定できることを保証するものなので、個数勘定の原理と呼んでおきましょう。

すぐ後で使うので、集合の同型 ¥stackrel{¥sim}{=} に関して、次の法則を確認しましょう。

  1. X ¥stackrel{¥sim}{=} X
  2. X ¥stackrel{¥sim}{=} Y ⊃ Y ¥stackrel{¥sim}{=} X
  3. (X ¥stackrel{¥sim}{=} Y ∧ Y ¥stackrel{¥sim}{=} Z) ⊃ X ¥stackrel{¥sim}{=} Z

もう'∧'(かつ)と'⊃'(ならば)の記号には慣れましたか。

これらの法則は任意の集合に対して成立するので、全称記号を明示すると次のようになります。

  1. ∀X:Set.( X ¥stackrel{¥sim}{=} X ) ---(同型の反射律)
  2. ∀X, Y:Set.( X ¥stackrel{¥sim}{=} Y ⊃ Y ¥stackrel{¥sim}{=} X ) ---(同型の対称律)
  3. ∀X, Y, Z:Set.( (X ¥stackrel{¥sim}{=} Y ∧ Y ¥stackrel{¥sim}{=} Z) ⊃ X ¥stackrel{¥sim}{=} Z ) ---(同型の推移律)

変数X, Y, Zの型はSetです(僕の気分により X∈Set とは書きませんでした)。Setは普通の型とは違って、Set自体は集合ではありません。類〈class〉とか大きな集合〈{large | huge} set〉とか呼びます。普通の集合よりデカイので取り扱い注意です。が、ここではSetの正体に深入りしないでおきましょう。気にしない気にしない。

先の3つの法則は、¥stackrel{¥sim}{=} が同値関係(正確には“大きな”同値関係)であることですが、¥stackrel{¥sim}{=} の定義に従って証明すべきことです。これは練習問題 -- 証明要求の形に書いておきます。証明要求については証明の“お膳立て”シリーズを参照してください。

  1. Γ |-? ∀X:Set.( X ¥stackrel{¥sim}{=} X ) ---(同型の反射律)
  2. Γ |-? ∀X, Y:Set.( X ¥stackrel{¥sim}{=} Y ⊃ Y ¥stackrel{¥sim}{=} X ) ---(同型の対称律)
  3. Γ |-? ∀X, Y, Z:Set.( (X ¥stackrel{¥sim}{=} Y ∧ Y ¥stackrel{¥sim}{=} Z) ⊃ X ¥stackrel{¥sim}{=} Z ) ---(同型の推移律)

Γは、¥stackrel{¥sim}{=} の定義などを含む文脈(背景知識、予備知識)です。Γを具体的に書き下すことはしませんが、けっこう色々な知識が含まれます。僕が想定しているΓとあなたの実際のΓに不一致がると、証明はできない可能性があります。Γを合意・確認する作業は、けっこう困難なものです。

個数勘定の原理を再掲します。全称限量子を付けた論理式で書きます。

  • ∀X:Set.∀n, m∈N.( (X ¥stackrel{¥sim}{=} [n] ∧ X ¥stackrel{¥sim}{=} [m]) ⊃ (n = m) ) ---(個数勘定の原理)

これを示すために、次の補題があればいいことは分かるでしょう。

  • ∀n, m∈N.( ([n] ¥stackrel{¥sim}{=} [m]) ⊃ (n = m) ) ---(個数勘定の補題)

個数勘定の補題と鳩の巣原理

前節最後の個数勘定の補題の対偶を取ってみます(全称限量子は省略)。

  • (n ≠ m) ⊃ ([n] ¥stackrel{¥sim}{=} [m] ではない)

n ≠ m は、n < m か n > m のどちらかで、どっちでも話は同じなので、n < m としましょう。すると:

  • (n < m) ⊃ ([n] ¥stackrel{¥sim}{=} [m] ではない)

自然言語で言えば:

  • n < m ならば、[n] と [m] は同型ではない。

これは非常に当たり前です。ここまで当たり前だと証明の必要性を感じないし、どうやって証明していいかも分かりません。当たり前のことを別な当たり前のことに帰着するくらいしか出来そうにありません。「気休め」感が否めませんが、まーでも、ジタバタしてみましょう。(あるいは、練習としてジタバタしてみましょう。)

モノの個数に関する原理で割と有名なものに「鳩の巣原理」があります。

本物の鳩の画像で説明しましょう。

*2

画像の鳩の巣には9個の箱があります。よく見ると鳩は10羽います。左上の箱に2羽入っているのです。9羽を超える鳩を9箱の鳩小屋に入れると、2羽以上入る箱が必ず生じる -- これが鳩の巣原理〈pigeonhole principle〉です。

一般に、n < m であるとき、m個のモノをn個の箱に入れると、2個以上入る箱が必ず生じます。これは次のように表現できます。

  • n < m ならば、写像 f:[m]→[n] は単射ではない。

論理式で書けば(外側の全称限量子は省略):

  • (n < m) ⊃ ∀f:[m]→[n].( ¬(fは単射) )

お好みにより、ド・モルガンの法則で書き換えると:

  • (n < m) ⊃ ¬∃f:[m]→[n].( fは単射 )

鳩の巣原理を仮定して、個数勘定の補題を証明することはできます。鳩の巣原理と似た(双対っぽい)次の命題からも個数勘定の補題を証明できます。この命題は、鳩の数より箱の数が多いときは必ず空き箱が生じることを主張しています。

  • (n < m) ⊃ ¬∃f:[n]→[m].( fは全射 )

個数勘定の補題数学的帰納法

  • ∀n, m∈N.( ([n] ¥stackrel{¥sim}{=} [m]) ⊃ (n = m) ) ---(個数勘定の補題)

この命題に n = 0 を代入してみると、次が得られます。

  • ∀m∈N.( ([0] ¥stackrel{¥sim}{=} [m]) ⊃ (0 = m) )

これは、「空集合と同型な[m]は[0]に限る」という意味です。空集合の定義、空集合からの/への写像の定義などを使えば、普通に証明できそうです。(でも、空集合写像に関する予備知識はけっこう必要です。)

個数勘定の補題に出現する変数nを自然数の上で走らせるとすると、上記の命題は最初の状態 n = 0 での事実です。残りのnも全部倒すには、数学的帰納法を使えばよさそうです。数学的帰納法は思いの外強烈で、当たり前過ぎて証明できそうにないような命題が数学的帰納法で証明できるときがあります。やってみます。

変数nに注目して数学的帰納法の原理にうったえるならば、次の2つの命題を示せばいいことになります。

  1. ∀m∈N.( ([0] ¥stackrel{¥sim}{=} [m]) ⊃ (0 = m) ) ---(個数勘定の補題 帰納のベース)
  2. ∀k∈N.( ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ) ⊃ ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) ) ) ---(個数勘定の補題 帰納のステップ)

話の筋を見失わないようにここで注意しておくと; 我々のターゲット命題は個数勘定の原理でした。個数勘定の原理を示すには、自然数だけに関係する補題を示せばいいと分かりました。ターゲットに至るために、より“手前”のサブターゲットを設定したのです。こんな考え方をバックワード・リーズニングと呼びます。さらなるバックワード・リーズニングで、数学的帰納法を成立させる2つの命題に至ったのでした。

「個数勘定の補題 帰納のベース」はいいとして、「個数勘定の補題 帰納のステップ」のほうをなんとかします。これもバックワード・リーズニングでより攻略しやすい形に変形します。そういった変形を、証明の“お膳立て”と呼んだのでした(証明の“お膳立て”シリーズ)。

まず、証明要求を書いてみます。

  • Γ |-? ∀k∈N.( ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ) ⊃ ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) ) ) ---(個数勘定の補題 帰納のステップ)

お決まりのお膳立てを実行しましょう。論理式が長いので複数行で書きます。

 Γ |-? ∀k∈N.(
          ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) )
          ⊃
          ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) )
         )
 -------------------------------------------------------------[∀の変形]
 Γ/ k:N |-?
          ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) )
          ⊃
          ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) )
 -------------------------------------------------------------[⊃の変形]
 Γ/ k:N,
    ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) )
     |-?
    ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) )
 -------------------------------------------------------------[∀の変形]
 Γ/ k:N,
    ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ),
    m:N
     |-?
    ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m)
 -------------------------------------------------------------[⊃の変形]
 Γ/ k:N,
    ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ),
    m:N,
    [k + 1] ¥stackrel{¥sim}{=} [m]
   |-?
    k + 1 = m

もう少し数学的帰納法のためのお膳立て

前節一番下段の仮定 ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ) で、束縛変数が直後の自由変数と同じmです。混乱を招きやすいので、束縛変数をℓに変えておきましょう。そのうえで、使っていい宣言・仮定を箇条書きにすると:

  1. k:N (変数kは自然数を表す)
  2. このkに対して、∀ℓ∈N.( ([k] ¥stackrel{¥sim}{=} [ℓ]) ⊃ (k = ℓ) ) ---(仮定1)
  3. m:N (変数mは自然数を表す)
  4. 上記kとこのmに対して、[k + 1] ¥stackrel{¥sim}{=} [m] ---(仮定2)

これらの変数宣言(変数導入)と仮定命題のもとで、ターゲット命題 k + 1 = m を示したいわけです。ここで、ターゲット命題の代わりに次の命題を考えます。

  • [k] ¥stackrel{¥sim}{=} [m - 1] ---(代替ターゲット)

もし、代替ターゲットが示せれば、仮定1を使って k = m - 1 が出て、両辺に1を足してもとのターゲット k + 1 = m が得られます。よって、上記の仮定のもとで代替ターゲットを目指せばいいわけです。このとき、仮定1は使わないので削り落としてもかまいません。以上のことを証明要求に書いてみれば:

  • Γ/ (k, m:N), [k + 1] ¥stackrel{¥sim}{=} [m] |-? [k] ¥stackrel{¥sim}{=} [m - 1] ---(代替ターゲット)

この証明要求では、Nの部分集合に関する同型しか出てきません。証明要求に応えるには、N上で作業して、求められている同型(可逆写像)を作り出せばいいのです。

ただ、少し気になることがあります。代替ターゲットのなかで m - 1 が出てきますが、自然数の引き算は部分的にしか定義されてないので、m - 1 が意味を持つには 1 ≦ m が事前に分かっている必要があります。次のように、仮定に 1 ≦ m が欲しいのです。

  • Γ/ (k, m:N), [k + 1] ¥stackrel{¥sim}{=} [m], 1 ≦ m |-? [k] ¥stackrel{¥sim}{=} [m - 1] ---(代替ターゲット)

証明要求の仮定に好き勝手に命題を加えていいわけではありません。「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」で述べた「定義・補題の追加」の手順に従えば、仮定への命題追加ができます。

  Γ/ Δ |-? Q   Γ/ Δ |- R
 -----------------------------[定義・補題の追加]
      Γ/ Δ, R |-? Q

もともとの前提から 1 ≦ m が証明できれば、それを仮定に追加できます。つまり、次の補助的な証明要求が発生します。

  • Γ/ (k, m:N), [k + 1] ¥stackrel{¥sim}{=} [m] |-? 1 ≦ m

証明要求を順方向に並べてみる

今までバックワード・リーズニング、つまりターゲットからの逆方向の推論でサブターゲットを探ってきました。これを順方向に並べ替えて列挙してみます。

  1. Γ |-? ∀m∈N.( ([0] ¥stackrel{¥sim}{=} [m]) ⊃ (0 = m) ) ---(個数勘定の補題 帰納のベース)
  2. Γ/ (k, m:N), [k + 1] ¥stackrel{¥sim}{=} [m] |-? 1 ≦ m
  3. Γ/ (k, m:N), [k + 1] ¥stackrel{¥sim}{=} [m], 1 ≦ m |-? [k] ¥stackrel{¥sim}{=} [m - 1]
  4. Γ/ k:N, ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ), m:N, [k + 1] ¥stackrel{¥sim}{=} [m] |-? k + 1 = m
  5. Γ |-? ∀k∈N.( ∀m∈N.( ([k] ¥stackrel{¥sim}{=} [m]) ⊃ (k = m) ) ⊃ ∀m∈N.( ([k + 1] ¥stackrel{¥sim}{=} [m]) ⊃ (k + 1 = m) ) ) ---(個数勘定の補題 帰納のステップ)
  6. Γ |-? ∀n, m∈N.( ([n] ¥stackrel{¥sim}{=} [m]) ⊃ (n = m) ) ---(個数勘定の補題)
  7. Γ |-? ∀X:Set.( X ¥stackrel{¥sim}{=} X ) ---(同型の反射律)
  8. Γ |-? ∀X, Y:Set.( X ¥stackrel{¥sim}{=} Y ⊃ Y ¥stackrel{¥sim}{=} X ) ---(同型の対称律)
  9. Γ |-? ∀X, Y, Z:Set.( (X ¥stackrel{¥sim}{=} Y ∧ Y ¥stackrel{¥sim}{=} Z) ⊃ X ¥stackrel{¥sim}{=} Z ) ---(同型の推移律)
  10. Γ |-? ∀X:Set.∀n, m∈N.( (X ¥stackrel{¥sim}{=} [n] ∧ X ¥stackrel{¥sim}{=} [m]) ⊃ (n = m) ) ---(個数勘定の原理)

このように書くと、証明(リーズニング)の順方向の流れが分かりやすくなります。しかし、証明全体の構造は、直線状ではなくて有向グラフになります。直線上ではない依存関係を頑張ってテキストで書く例は、「証明の“お膳立て”のやり方 3: さらに事例」の「“お膳立て”の全体像」にあります。まー、無理してテキストで書く必要もなくて、マルと矢印線の手描きで十分です。

自然数の部分集合で有限なもの

今までやったことは、有限集合とは何かを定義して、有限集合の基数が一意に決まることを示しただけです。もうひとつくらい、有限集合に関する話題を入れておきましょう。

SをNの部分集合とします。Sが有界〈bounded〉であることを次のように定義します。

  • Sは有界 :⇔ ∃n∈N.∀k∈N.( k∈S ⊃ k ≦ n)

自然数の部分集合に限れば、有限性と有界性は同じことになります。つまり、次の命題が成立します。

  • (Sは有限 ⊃ Sは有界) ∧ (Sは有界 ⊃ Sは有限)

これは、少し一般化した次のような命題につながります。

  1. 有限集合からの写像の像は有限集合
  2. 有限集合の部分集合は有限集合

いずれも当たり前ですが、ジタバタしてみてください。

2017-11-27 (月)

日付の確認さえしないの? フェイクが通用してしまう事情

| 10:16 | 日付の確認さえしないの? フェイクが通用してしまう事情を含むブックマーク

以下に出てくる日付に注意しながら読んでください。

まず、11月24日夜配信のYahooニュース。見出しだけ見ればいいもんで、中身を読むほどのことじゃないです。

このニュースによると:

騒動の発端となったのは、東京都内の「サイゼリヤ」で彼ら[檜山注:YouTuber集団]と居合わせた伊藤さんが11月22日未明に投稿した次のような告発ツイートだ。

ツイートが11月22日未明ということは、大量食べ残し事件はおそらく11月21日夜でしょう。

ここに出てきたYouTuber集団とは、チョコレートスニッカーズというグループです。以下の記事には、チョコレートスニッカーズがすぐに謝罪動画をあげたが、その内容がふざけ過ぎだと記述されています。

さて、当の謝罪動画ですが:

11月21日、大量食べ残し事件をやらかした当日に“謝罪動画”が公開されています。twitterによる“告発”が翌日ですから、告発される前に謝罪を公開していたことになります。手回しが良すぎませんか?

いくら何でもオカシイので、謝罪動画を見てみると、確かにふざけまくってますが、大量食べ残し事件とは何の関係もないように思えます。少し調べれば、この動画は大量食べ残し事件とは一切無関係だと分かります。詳細はともかく(調べる気にならない)、少し前に、チョコレートスニッカーズと似た名前のチョコレートスモーカーズというYouTuberがなにかしらの不祥事を起こして、その謝罪動画をチョコレートスニッカーズがおちょくったもの(パロディ)です。

あー、紛らわしい名前でややこしい! 実際、名前が似ている2つのグループが混同されてます。さらに悪乗りしてワザと混乱させる情報を流したり…… 話がグチャグチャ。

もと動画であるチョコレートスモーカーズのオリジナル謝罪動画は(たぶん)もう無いようですが、コピーは残ってます。

まが悪く、誤解されやすいタイミングで誤解されやすい内容の動画を偶然あげていたわけですが、日付をみればオカシイことは分かるだろうに。その程度の確認さえしない人が多いってことなんですね。

そもそも、ほとんどの人にとってどうでもいい事件なので、事実確認さえアホらしい、ってこともあるでしょうが、情報に対する反応の仕方があまりに脊髄反射的である気がします。こういうの、マズイよなー、とても不安な気分になる*1

*1:話題はまったく違いますが、「「フローチャート」騒ぎ、もう少し頭使って考えてみようよ」のときも、なにも考えずに尻馬に乗るだけの人がたくさんいる事にウンザリすると同時に不安な気分になりました。「批判は何ら悪い事ではない、ただし根拠を持った批判をしましょう」って教育をすべきかと思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171127

2017-11-24 (金)

存在記号の除去規則について考える

| 14:08 | 存在記号の除去規則について考えるを含むブックマーク

全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。

存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業(記法のあいだの翻訳)に慣れて、その“どうでもよさ”(記法が変わっても内実は変わらないこと)を感じていただければ幸いです。

内容:

  1. 存在記号の除去規則
  2. 限量随伴性
  3. 引き戻しと存在限量子の随伴性
  4. 随伴性を証明に利用する
  5. 随伴性からサイド証明へ
  6. メタ循環構造

存在記号の除去規則

標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。

         P(a)
          :
          :
 ∃x.P    Q
 -------------[∃除去]
       Q

僕は、自然演繹に愚痴を言い悪態をついてます(「自然演繹はちっとも自然じゃない -- 圏論による再考」参照)。この規則も、これを見ただけでは何だかよくわかりません。自然演繹ったら、ほんとにもう。

全称記号の導入規則について考える」で、多少マシな形の推論規則が載っている解説"Natural deduction for predicate logic"(https://cs.uwaterloo.ca/~plragde/cs245old/06-prednd.pdf)を紹介しました。"Natural deduction for predicate logic"における全称記号の除去規則は次の形です。

あんまり代わり映えしないですね。でも、右側の証明部分をボックスで囲んでいるのはやっぱりマシです。このボックスで囲まれた部分の証明を、サイド証明〈サブ証明 | 補助証明〉と呼ぶことにします。

サイド証明があるなら、当然にメインの証明があります。メイン証明を左側に、サイド証明を右側に書くようにすると、次のようになります。すぐ上の規則とは記号が違っています; φ→P, x0→a, χ→Q と対応してます。記号の選び方は趣味の問題で、どうでもいいものです。

 メイン証明
   :
 ∃x.P
 -------+-[変数a]--
        | P(a)
        |  :
        | サイド証明
        |  :
        |  Q
 -------+----------
   Q
   :
 メイン証明

このメイン証明とサイド証明の関係をハッキリさせて、存在記号の除去規則の意味付けをします。

限量随伴性

述語論理とインデックス付き圏と限量随伴性」で述べたように、限量子の挙動を支配している原理は随伴性〈adjunction〉*1です。随伴性には色々な表現があります、ホントにウンザリするほど色々な書き方(描き方)があります。表現の多様性が目くらましとなって、単純な本質が見えにくいのです(ため息)。

集合Xごとに、Xの上の“述語”と呼ばれるナニモノカを要素とする集合Pred[X]が対応しているとします。いま「述語」という言葉を使いましたが、代わりに「命題」とか「論理式」とか「文」とか呼んでもかまいません。これらの言葉に合意された定義も識別もありません(人それぞれ、解釈と用法は異なります)*2

呼び名はホントにどうでもよくて、重要な点は、Pred[X]がデカルト閉圏の構造を持つことです。デカルト閉圏が難しそうなら、ハイティング代数やブール代数だと思ってもかまいません。Pred[X]内で、'∧'(連言)、'⊃'(含意)、'|-'(証明可能)などの解釈ができればそれでいいのです。

ここでは、分かりやすい例として、Pred[X]とは“Xベキ集合”のことだとしましょう。つまり Pred[X] = Pow(X) (Pow(X)はXのベキ集合)と置きます。そして:

  • Pow(X)の要素を、「命題」とか「述語」とか呼ぶ。Xの部分集合Aは、p(x) := (if x∈A then True else False) というブール値関数と1:1対応するので、部分集合を述語(あるいは命題)と呼んでも悪くはないでしょう(何と呼ぼうがどうでもいいんだけど)。
  • A, B∈Pow(X) に対して、A∧B は A∩B のことだとする。
  • A, B∈Pow(X) に対して、A⊃B は Ac∪B のことだとする。(-)cは、Xを全体集合としての補集合。
  • A, B∈Pow(X) に対して、A |- B は A⊆B のことだとする。

「ブール値関数←→部分集合」という対応に基づき、論理的演算/論理的関係である ∧, ⊃, |- を、集合の演算/集合の関係 ∩, (-)c∪(-), ⊆ と同一視してしまえ、ってことです。この発想はちょっと乱暴ですが、述語論理(のモデル)のイメージを手っ取り早くつかむには良い方法かと思います。

述語論理とインデックス付き圏と限量随伴性」で述べた一般論では、f:X→Y を写像とすると、f*:Pred[Y]→Pred[X] という逆方向の関手があります。今扱っている Pred[X] = Pow(X) という事例では、f*:Pow(Y)→Pow(X) は、逆像を対応させる写像です。その定義は次のとおり:

  • B⊆Y に対して、f*(B) = {x∈X | f(x)∈B}

f*がベキ集合のブール代数構造に対する準同型写像であることはすぐに分かります。次を確認してください。

  • f*(B∩B') = f*(B)∩f*(B')
  • f*(B∪B') = f*(B)∪f*(B')
  • f*(Bc) = (f*(B))c

包含順序も保存します。

  • B⊆B' ならば、f*(B)⊆f*(B')

さて、f*:Pow(X)→Pow(Y) (星が下付きなのに注意!)は、像〈順像〉を対応させる写像とします。その定義は次のとおり:

  • A⊆X に対して、f*(A) = {y∈Y | x∈A で f(x) = y となるxが存在する}

f*とf*のあいだには次の関係があります。

  • f*(A)⊆B ⇔ A⊆f*(B)

この関係があるとき、f*とf*は、随伴ペアであると言います。随伴ペアであることは、次の2つの包含関係式としても表現できます。

  • A ⊆ f*(f*(A))
  • f*(f*(B)) ⊆ B

詳しくは次の記事を参照してください。

f*とf*の随伴性(随伴ペアであること)が、存在限量子の存在限量子の性格と扱い方を規定します。別な言い方をすると、随伴性が存在限量子の背後にあるメカニズムなのです。

引き戻しと存在限量子の随伴性

f*はfの逆像写像、f*はfの順像写像です。順像写像f*を∃fとも書きます。論理の存在限量子が、事実上順像写像と同じなのでこの記法を使います。

随伴を表すために'-|'という記号を使いますが、次の2つの命題は同じ意味です。

  • f -| f*
  • 任意の A∈Pow(X), B∈Pow(Y) に対して、∃f(A)⊆B ⇔ A⊆f*(B)

そして、次のような言い方をします。

  • fとf*は(この順で)随伴ペアである。
  • fは、f*左随伴パートナーである。
  • f*は、∃f右随伴パートナーである。

逆像写像(逆写像じゃないよ!)f*は、もとの写像fと逆方向に集合を移動するので、引き戻し写像〈pull-back mapping〉とも呼びます。∃fは引き戻し写像の左随伴パートナーで、fと同じ方向に集合を移動します。この∃fを「fの存在限量子」と言ってしまうと混乱を招くかもしれません。「構文的な存在限量子に対応する意味的な存在物」とでも言えば正確でしょう。正確だけど鬱陶しいのでヤッパリ「存在限量子」と呼んじゃうもしれませんね*3

述語論理では、一般的なfに対する ∃f, f* を考えるわけではなくて、π:X×Y→X (射影)という特別な写像だけを考えます。πは、正確に書けば π1X,Y のように上下に添字が付きますが、(x, y) |→ x と1番目の成分を取り出す写像です。(x, y) |→ y (第二射影)を使っても同じことです。

写像 π:X×Y→X に対して、∃πとπ*の随伴性を述べれば:

  • π -| π*
  • 任意の A∈Pow(X×Y), B∈Pow(X) に対して、∃π(A)⊆B ⇔ A⊆π*(B)

この状況を雑に絵に描けば次のようです。この絵を目に焼き付けて続きを呼んでください。

随伴性を証明に利用する

前節で述べた随伴性 ∃π -| π* を意識しながら、存在限量子記号'∃'の扱い方を考えます。ここでは、構文と意味との対応をキッチリとは定義せず、前節で説明した随伴性を頭に置きながら、同様なことを構文的に表現してみよう、という態度で進めます。

まず、構文的な述語〈述語論理の論理式〉をP, Qなどで表します。Pが型Xの変数xを含むかも知れないことを P[x:X] と書きます。型とは、変数が走る集合のことです。Pに、x:X と y:Y という変数が含まれる(かも知れない)ことを表すには P[x:X, y:Y] と書きます。以下、Pは二変数を持ち P[x:X, y:Y]、Qは一変数で Q[x:X] であると仮定します。ここで使った記法に関するより詳しいことは次の記事で説明しています。

X上の変数を持つ述語 Q[x:X] に対して、それを二変数 x:X, y:Y の述語とみなしたものを [x:X, y:Y].P[x:X] と書きます。前置する [x:X, y:Y]. は変数水増しオペレーター〈variable thinning operator〉です。変数水増しオペレーターは、射影 π:X×Y→X による引き戻しπ*:Pow(Y)→Pow(X) に対応する構文的オペレーターです。

述語〈述語論理の論理式〉に対する存在限量子は、普通に ∃w:Y.P[x:X, w:Y] と書きます。束縛変数は何を使ってもいいのですが、主に w:Y を使います。

以上に述べた構文的な構成と、前節の部分集合/ベキ集合との対応をまとめると以下のようです。

部分集合/ベキ集合 述語論理
A∈P(X×Y) P[x:X, y:Y]
B∈P(X) Q[x:X]
π*:Pow(X)→Pow(X×Y) [x:X, y:Y]. 変数水増し
π*(B)∈Pow(X×Y) [x:X, y:Y].Q[x:X]
π:Pow(X×Y)→Pow(X) ∃w:Y. 存在限量子
π(A)∈Pow(X) ∃w:Y.P[x:X, w:Y]

この対応をもとに、随伴性を述語論理の言葉で表現してみます。随伴性をもう一度繰り返し書くと:

  • π(A)⊆B ⇔ A⊆π*(B)

左右に並べる代わりに上下に書くと:

π(A)⊆B ⇒ A⊆π*(B) を上下に書く:

   ∃π(A)⊆B
 -------------
   A⊆π*(B)

A⊆π*(B) ⇒ ∃π(A)⊆B を上下に書く:

   A⊆π*(B)
 -------------
   ∃π(A)⊆B

このように上下に並べる書き方は、論理の話ではよく使われます。上の対応表を見ながら、また'⊆'を'|-'に直して書き換えると:

   ∃w:Y.P[x:X, w:Y] |- Q[x:X]
 ------------------------------------
   P[x:X, y:Y] |- [x:X, y:Y].Q[x:X]


   P[x:X, y:Y] |- [x:X, y:Y].Q[x:X]
 ------------------------------------
   ∃w:Y.P[x:X, w:Y] |- Q[x:X]

これが何を主張しているのかと言うと:

  • 「∃w:Y.P[x:X, w:Y] を仮定して Q[x:X] が証明できること」と「P[x:X, y:Y] を仮定して [x:X, y:Y].Q[x:X] が証明できること」は同じである。

ちょっと言い方を変えると:

  • ∃w:Y.P[x:X, w:Y] を仮定して Q[x:X] を証明したいなら、P[x:X, y:Y] を仮定して [x:X, y:Y].Q[x:X] を証明しても(同じことだから)よい。

随伴性からサイド証明へ

いよいよ大詰めですが、時間に余裕がある方は、次の記事の冒頭と最初の節、最後の節を読んでみてください。

我々が何かを学ぶとき、記法に慣れるのに相当な労力が割かれます。同じ内容であっても、異なる記法で提示されると理解できません。異なる記法のあいだの翻訳にも手間がかかります。論理式や証明の書き方(記法)も色々あって、それらの翻訳でけっこう消耗してしまうことがあります。残念ながらどうにもならないので、記法の変更(書き換え、翻訳)に慣れるしか無いです。

この記事での縦と横の描き換えを体験すれば、僕がたまにしている「双対や随伴に強くなるためのトレーニング」が、冗談でないことが分かるでしょう。

さて、随伴性の表現に対して、'⇒'を使った横書きを横線区切りを使った縦書き(上段と下段を使用)にしました。さらにまた90度回転して書きます。

                  |
∃w:Y.P[x:X, w:Y] |  P[x:X, y:Y]
   ---            |     ---
    |             |      |
                  |
  Q[x:X]          |  [x:X, y:Y].Q[x:X]
                  |

“左側上下の証明可能性”と“右側上下の証明可能性”が同等であることを主張しています。内容的には前節とまったく同じですが、レイアウトが変わっています。

新しいレイアウトに沿って説明すると、左上から左下に至る証明をすることは、右上から右下に至る証明をすることと同等なのです。であるならば、左上から左下への証明はやらずに、右上から右下をやるだけでいいはずです。

もう一度図を描きかえて、事情を分かりやすくします。

      :               |
      :               |
(1) ∃w:Y.P[x:X, w:Y] |
                      |(2) P[x:X, y:Y]
                      |      :
                      |      :
                      |(3) [x:X, y:Y].Q[x:X]
(4) Q[x:X]            |
      :               |
      :               |

左側の証明記述が論理式(1)(存在命題)に到着したとき、(4)に至る経路として、いったん右の論理式(2)に移り、そこで証明をして論理式(3)に至り、そこで再び左側(4)に移って証明を続ければいいのです。

上記のレイアウトにおいては、左側がメイン証明が進行するレーン、右側がサイド証明〈サブ証明 | 補助証明〉が進行するレーンです。右側レーンは、いつも必要なわけではなく一時的なので、一時的に出現するボックスと考えてもいいでしょう。

      :
      :
(1) ∃w:Y.P[x:X, w:Y] +---------------------
                      |(2) P[x:X, y:Y]
                      |      :
                      |      :
                      |(3) [x:X, y:Y].Q[x:X]
(4) Q[x:X]            +----------------------
      :
      :

メイン証明は集合X上の証明、ボックス内のサイド証明はX×Y上の証明となっており、証明の舞台が異なります。その意味でも、メイン証明とサイド証明はしっかり区別したほうがいいのです。"Natural deduction for predicate logic"の記法(書き方/描き方)がマシなのは、サイド証明をちゃんとボックスで識別している点です。

紙面の節約のために、右側のボックスを左に押し込んでしまいます。ボックスの入り口と出口の区切り線は残します。(1)から(2)に移るときに束縛変数を自由変数に置き換えますが、これはどんな変数でもかまいませんが書き添えておくことにします。さらに、[x:X, y:Y].Q[x:X]とQ[x:X]を通常は区別しないので、変数水増しオペレーターは省略してしまうと:

      :
      :
(1) ∃w:Y.P[x:X, w:Y]
   +--[変数 b]------
  (2) P[x:X, b:Y]
        :
        :
  (3) Q[x:X]
   +----------------
(4) Q[x:X]
      :
      :

サイド証明ボックス内で使う変数は、ボックスの入り口で宣言しています。この変数の選び方は本来まったく自由ですが、それまで出現してない変数(フレッシュ変数)を選んで混乱を避けるのが普通です。

ここでまた愚痴と悪態を吐くと; 証明の書き方では、変数のブロックスコーピングを導入せずに、フラットスコープとフレッシュ変数を使うことが多いのですが、このやり方だと変数が増大してロクなもんじゃないです*4

メタ循環構造

ここまでの話で、存在限量子の背後には次の随伴性があることを説明しました(f*と∃fは同じ意味です)。

  • [随伴性] f*(A)⊆B ⇔ A⊆f*(B)

この随伴性は、次の2つの包含関係式と同値です(「順序随伴性: ガロア接続の圏論」参照)。

  • [単位関係式] A ⊆ f*(f*(A))
  • [余単位関係式] f*(f*(B)) ⊆ B

実は、「証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑」の例題は二番目の関係式(余単位関係式)でした。少しサボった記法で次のように書いていました。

  • f(f-1(B)) ⊆ B

余単位関係式の証明には、今回説明した存在限量子の除去規則を使います。「証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑」の最後のほうでゴニョゴニョ説明していることは、実質的には存在限量子の除去なのです。

存在限量子の除去規則の根拠は随伴性だと言い、その随伴性の証明には存在限量子の除去規則を使う … これって循環論法ではないのか?

たしかに循環しています。しかし、このような循環はしばしば出会うものです。我々が生きているこの世界で成立していると信じられている法則、ずっと使われ続けている手順などを、我々が構成・操作・調査できるモデルのなかで再構成し合理化することは意義があるのです。

このような循環が起きる状況には“入れ子の世界”が介在しています。“入れ子の世界”はミステリアスで、人を不安にさせるかも知れません。が、“入れ子の世界”とそれに伴うメタ循環〈メタ巡回 | meta-circlular〉構造は避けられないのです。次の記事も参照してください。

*1:随伴性は、双対対象ペア、随伴関手ペアを含む一般的な概念ですが、ここでは随伴関手ペアの意味です。

*2:もちろん、特定の文脈では定義され、識別もされます。

*3:世間一般に、不正確さや混乱のリスクがあっても、簡略な用語法・記号法を採用する傾向があります。面倒なのは嫌なんですが、こういう簡略さが、理解をおおいに阻害しているのも事実です。ほんとに頭が痛いところです。

*4プログラミング言語で、大域変数しかないものを想像してもらえれば、酷さが分かると思います。

2017-11-21 (火)

Firefox Quantum すごく良くなった

| 12:42 | Firefox Quantum すごく良くなったを含むブックマーク

量子だの光子だのという名前を話題にしたことがあった Firefox Quantum、確かに速くなりましたね。体感では、「劇的に」速くなったと言っていいくらいです。

それと、どうやらデフォルトのフォントが変わったらしくて、Unicodeの記号文字が読みやすくなりました*1。以前、「数学記号とか特殊な文字のUnicode」で次のように書きました。

テンソル積記号は文字としても存在しています。U+2297 'CIRCLED TIMES' です。HTMLの文字実体参照記法で &#x2297; と書きます。[...snip...] 通常の演算子として使うと明らかに小さすぎ…

今僕が見ている環境では、A⊗B(ソースは A&#x2297;B)はいい具合に見えてます。

Webページを印刷した場合も、以前よりスッキリして読みやすいです。

フォントや印刷は環境に依存するので、一概には言えませんが、僕のところでは改善されてます。ウリである高速性はもちろん、他の部分でも改善点があり、Firefox Quantum 随分と頑張ったなー、という印象。

*1[追記]フォントリソースが変わったのか、レンダリングの方式が変わったのかよく分からないのですが、ともかく色々と視認性は良くなってます。今までの画像の代わりに文字(グリフ)にするかどうかは悩むところ。みんながみんな、自分と同じ見え方しているとは保証できないので。[/追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171121

2017-11-20 (月)

証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑

| 14:52 | 証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑を含むブックマーク

“お膳立て”というより、証明そのものの話、しかも小ネタ。なのでオマケとします。

内容:

  1. 像と逆像に関する、とある命題
  2. 集合の内包的記法なら証明できる?
  3. 何が問題なのか
  4. 半分なら証明できる
  5. 仮定にある存在命題の使い方

像と逆像に関する、とある命題

A, Bは集合、f:X→Y は写像、A⊆X, B⊆Y とします。このとき、次の命題は一般的には成立しません。

  • f(f-1(B)) = B

f-1(B)は、Yの部分集合Bの逆像で、f(A)は、Xの部分集合Aの像〈順像〉です。

上記命題は成立しない、と言ったので、反例を挙げておきます。X = {1, 2}, Y = {1, 2, 3} として、f:{1, 2}→{1, 2, 3} を埋め込み写像として定義します。つまり、f(1) = 1, f(2) = 2。B = {2, 3} としたとき:

  • f-1(B) = f-1({2, 3}) = {2}
  • f(f-1(B)) = f({2}) = {2}
  • {2} ≠ {2, 3}

もっと簡単な反例は、X = {1}, Y = B = {1, 2}, f(1) = 1, {1} ≠ {1, 2} で与えられます*1

上記の f(f-1(B)) = B は反例があるので、間違った命題です。したがって証明はできません。間違った命題を証明できたなら、それは大変に困った事態です。

集合の内包的記法なら証明できる?

次のような形を集合の内包的記法と呼びます。

  • {x∈X | P(x)}

この形において、変数xは集合X上を走るとします。P(x)は、xに関する何らかの条件を表す命題(ちゃんと書けば述語論理の論理式となる)です。一例を挙げると:

  • {n∈N | nは2で割り切れる}

N自然数(非負整数)の全体のなので、これは非負の偶数全体を表します。

さて、f:X→Y の逆像と像を、集合の内包的記法で定義しましょう。

  • f-1(B) = {x | f(x)∈B}
  • f(A) = {f(x) | x∈A}

ちょっと雑ですが、xはX上の変数、yはY上の変数と決めれば、混乱はないでしょう。いま、A = f-1(B) と置いて、f(A) = f(f-1(B)) を計算してみます。左端は行番号で、後で参照しやすくするためのものです。

1:   f(A)
2: = {f(x) | x∈A}
3: = {f(x) | x∈f-1(B)}
4: = {f(x) | f(x)∈B}
5: = {y | y∈B}
6: = B

等式変形のそれぞれのステップに対する根拠は:

  • 1行から2行: fの像の定義
  • 2行から3行: A = f-1(B) と事前に約束した
  • 3行から4行: 逆像の定義より、x∈f-1(B) ⇔ f(x)∈B
  • 4行から5行: f(x) = y と置く
  • 5行から6行: B = {y | y∈B} は当たり前

結局、f(f-1(B)) = B が証明されたことになります。反例があったんだけどな?

何が問題なのか

前節の議論で採用した記法は色々と杜撰〈ずさん〉なところがありますが、一番の問題は次の書き方でしょう。

  • f(A) = {f(x) | x∈A}

直感的には意味が分かりますが、像の定義として正確さに欠けます。像をちゃんと定義するには、存在限量子が必要です。次のようです。

  • f(A) = {y | ∃x.(x∈A ∧ f(x) = y)}

変数x, yが走る範囲(変域、型)も明示すれば、

  • f(A) = {y∈Y | ∃x∈X.(x∈A ∧ f(x) = y)}

この定義を使って、前節と同じ議論を途中までしてみます。

1:   f(A)
2: = {y | ∃x.(x∈A ∧ f(x) = y)}
3: = {y | ∃x.(x∈f-1(B) ∧ f(x) = y)}
4: = {y | ∃x.(f(x)∈B ∧ f(x) = y)}

f(A) は {y | ∃x.(f(x)∈B ∧ f(x) = y)} と書けるのは分かりました。yはY上を走る変数ではありますが、自由な値を取れません。「f(x) = y となるxが在る」ような、そんなyしか考えないのです。f(A) = {f(x) | x∈A} という書き方は、存在命題による“縛り”が明白でないので、それを忘れがちなのです。その意味では好ましくない書き方です。

半分なら証明できる

f(f-1(B)) = B は反例があるので証明できません(証明できたらオカシイ!)が、f(f-1(B)) ⊆ B なら証明できます。集合の内包的記法はとても便利ですが、見通しが悪くなることもあるので、a∈{x | P(x)} ⇔ P(a) を使って、内包的記法を消去する方針にします。

言いたいこと、つまりターゲット命題は f(f-1(B)) ⊆ B ですが、これは次のように書けます('⇒'は含意記号です)。

  • y∈f(f-1(B)) ⇒ y∈B

ほんとは全称命題なので、全称限量子をちゃんと付ければ次のようです。

  • ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)

この命題を証明しなさい、という証明要求は、次の形です。「証明要求」という言葉や、'|-?'という記号については、“お膳立て”シリーズを読み返してください。

  • |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)

さらに言えば、証明で使う予備知識や事前の約束(言葉や記号の定義)をΓ(大文字ガンマ)で表すなら、

  • Γ |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)

これが言わんとしているところは、「あなたが知っている予備知識や事前の約束Γを使って、ターゲット命題 ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B) を証明しなさい」です。

[補足]

f(f-1(B)) ⊆ B という包含関係は、「順序随伴性: ガロア接続の圏論」で述べた順序随伴に関する余単位不等式です。写像fの順像と逆像は順序随伴ペアになるのです。順序随伴の事例は、「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の例題としても扱っています。

[/補足]

“お膳立て”として証明要求を書き換えます。

  Γ |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)
 --------------------------------------
  Γ/ y:Y, |-? y∈f(f-1(B)) ⇒ y∈B
 --------------------------------------
  Γ/ y:Y, y∈f(f-1(B)) |-? y∈B

予備知識や約束ごとΓのなかには、逆像と像の定義も入っています。それを使うと:

   y∈f(f-1(B))
⇔ ∃x∈X.(x∈f-1(B) ∧ f(x) = y)
⇔ ∃x∈X.(f(x)∈B ∧ f(x) = y)

証明要求の仮定を同値な命題で置き換えてもよいので、

  • Γ/ y:Y, ∃x∈X.(f(x)∈B ∧ f(x) = y) |-? y∈B

“お膳立て”はここまでにして、実際の証明(フォワード・リーズニング)をします。

仮定に存在命題があるときの処方箋は、(少なくとも1つは)存在が保証された要素に名前を付けて利用することです。f(x)∈B ∧ f(x) = y であるようなXの要素を選び、aと命名します。当然ながら、そのaに関しては:

  • f(a)∈B ∧ f(a) = y

f(a)∈B も f(a) = y も両方成立しているので、y∈B は成立します。これでターゲット命題 y∈ B が言えたので、証明要求を満たす〈satisfy | fulfill〉ことができました。すなわち、証明は終わりです。

仮定にある存在命題の使い方

前節の証明のキモは、仮定にある存在命題の使い方です。が、これは難しい。存在命題をうまく使えない、あるいは、使った証明に納得感を持てない人は多そうです。

パターン化するならば、次のようなブロック構造を使うのです。

 …… ナニヤラカニヤラ
 ∃x.P(x) … この存在命題を使ってよいことになった
 +---------------------------------+
 | P(a) であるaを選ぶ
 | …… aを使ってナニヤラカニヤラ
 | Q
 +---------------------------------+
 Qを使ってよい

ボックス(ブロック)の内部がaを使った推論が行われる範囲です。Qはaを含まない命題です。aを含まないのでボックスの外に持ち出してもいいのです。前節の例ならば:

 ……
 仮定に ∃x∈X.(f(x)∈B ∧ f(x) = y) があるので
 ∃x∈X.(f(x)∈B ∧ f(x) = y) を使ってよい
 +---------------------------------+
 | f(a)∈B ∧ f(a) = y であるaを選ぶ
 | f(a)∈B ∧ f(a) = y だ
 | だから
 | y∈B これはaを含まない
 +---------------------------------+
 y∈B を使ってよい

仮定に存在命題があることは、ナニカが存在する状況下で考えていいよ、ってことです。そのナニカをaと呼び、しばらくはaを自由変数のように扱って議論をします。しかし、aは実際は縛りがある変数なので、自由変数のように扱うのはボックス内に限定して、aがボックスの外に漏れることを防ぎます。aを含まない命題はボックス外に持ち出してもいいもので、ボックス内のサブ証明の成果物と言えるでしょう。

*1:X = ¥emptyset, Y = B = {1}, fは自明な写像, ¥emptyset ≠ {1} も反例です。が、簡単すぎてピンと来ないかもしれません。

2017-11-17 (金)

ほぼ絶滅 アンミラ

| 15:30 | ほぼ絶滅 アンミラを含むブックマーク

四半世紀前に「私がオバさんになっても」という歌をうたっていた森高千里さんは、実際にオバさんになりました -- とても美しいオバさんに。「私がオバさんになっても」よりさらに4年前、1988年リリースの「ストレス」における森高さんの制服コスチューム姿は話題になりました。「これってアンミラの制服だ」と。

アンミラ -- アンナミラーズ(Anna Miller's) は、1970年代に開業した飲食店チェーンです(でした)。僕のような田舎者にとっては、東京に出たら一度は行ってみたいお店でした*1。目的はウェイトレス(女性従業員)さんの制服。

アンミラの制服は、今でもコスプレ衣装のレパートリーにあるくらいです。

開業当時から制服デザインはあまり変わってないそうですが、今見ても全然古くないですね。というか、アンミラ制服は、現在のメイド喫茶などの制服の原点・原典と言っていいでしょう。

友人と連れ立って初めて行ったアンミラは原宿店だったと記憶しています。おのぼりさんの我々は感激してしまいました。が、目のやり場に困る、というか、挙動不審にならないように神経を使って疲れました。食べ物をたのんだほうが、長時間いても不自然でないと注文したのですが、アンミラのメニューって予想以上にボリュームあるんですよ。なんか、死ぬほどおなかイッパイになった。

それから何年もがたち、僕は、ソニーがある品川にたまに行くようになりました。たいていは、品川駅近くのアンミラでコーヒーを飲んでから帰ってました。たぶんその頃は、挙動不審に見えない所作を身につけていたと思います。現在のアンナミラーズ ウィング高輪店は、現存する唯一のアンナミラーズです。最盛期には20店舗あったということですが …。

GLOCOMが六本木テレ朝通りに引っ越す前は広尾にあったんですが、広尾にもアンミラがありました(小さめの店舗)。GLOCOMの行き帰りで時間をつぶすために、アンミラに入ることがありました。

子供たちが小さい頃、自由が丘ABCマートに運動靴を買いに行ってました。駅からABCマートまでの途中にアンナミラーズ自由が丘店がありました。「うわっ、なつかしい」と思い、子連れで入ったことがあります。自由が丘店は、2006年9月閉店で今はありません。残っているのは高輪店だけ。

懐旧の情だけで品川まで出かける気にはナカナカなれないのですが、高輪店もなくなると、僕はちょっと寂しい気分になりそうです。生き残れ、最後のアンミラ。


[追記]森高さんの公式チャンネルだから、リンクしてもよさそうなので:

D

なぜか大衆中華食堂ですが、これをお洒落なカフェにするとアンミラになります。実際のアンミラ制服は、森高さん衣装よりもっと胸が強調されるデザインです。

なお、大衆食堂にメイド服のウェイトレスさんという組み合わせは実在しました。以下の記事参照。

[/追記]

*1[追記]アンミラ原宿店の開業時期から考えると、この記述は事実として正確でないかも知れません。でも、ジジイの昔語りとしては、そこまで事実の正確性を気にすることもないのでいいとします。[/追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171117

2017-11-16 (木)

プログラム意味論の書き方サンプル: UMiToL

| 12:40 | プログラム意味論の書き方サンプル: UMiToLを含むブックマーク

プログラミング言語/プログラム実行の意味論を記述するには、ある程度決まったやり方(定石)があります。それを紹介します。単に書き方のルールを並べるのでは退屈ですから、具体的な例を使って説明します。その例に使う言語の名前がUMiToL(ウミトル) -- "Ultimately Minimum Toy Language"(究極的に最小なオモチャ言語)のアクロニム -- です。

UMiToL言語は超簡単で、UMiToL自体の学習負担はほぼゼロなので、その分、“プログラム意味論の書き方”のほうに集中できると思います。細かい定義を積み重ねて、最終的にUMiToLの意味論は関手として記述されます。

内容:

  1. UMiToL言語の構文
  2. 変数の構文
  3. リテラルの構文と意味
  4. 演算子記号の解釈
  5. 状態、状態空間、式の意味
  6. コンパイル時のチェック
  7. コンパイラが見る文/式
  8. 文のプロファイル
  9. 文の意味の定め方
  10. 宣言文の意味
  11. 代入文の意味
  12. プログラムの圏論的意味
  13. おわりに

UMiToL言語の構文

UMiToLはプログラミング言語なので、まずはその構文を定義しましょう。通常のプログラミング言語同様に、リテラル(値を直接に表す表現)と変数があります。演算子記号はプラス記号とマイナス記号の2つ、文は(変数の)宣言文と代入文と空文。これで全てです。

念のために、構文をBNFバッカス/ナウア形式〉記法で定義しておきます。とても短い構文定義です。リテラルと変数については、後で詳しく述べます。EMPTYは、何もないことを示す目印です。

式 ::= リテラル | 変数 | '(' 式 ')' | 式 '+' 式 | 式 '-' 式
宣言文 ::= 'var' 変数
代入文 ::= 変数 ':=' 式
空文 ::= EMPTY
文 ::= 宣言文 | 代入文 | 空文
プログラム ::= 文 | プログラム ';' 文

BNF正規表現に馴染みがない方は次の記事を読んでみてください。

変数の構文

変数はプログラミング言語において非常にポピュラーな概念です。ほとんどのプログラミング言語は変数を持つでしょう。しかしながら、変数はけっこう複雑で難しい概念で、きちんと理解してない方もいるのではないでしょうか。この記事の主たる目的は「変数とは何か?」に答えることです。

構文上は、変数は単なる名前または記号です。名前または記号であることを強調するときは、変数名(variable name)、変数記号〈variable symbol〉と呼びます。

UMiToLの構文を確定するには、変数名〈変数記号〉全体の集合をハッキリさせます。例えば:

  • 英字(ラテン文字)小文字の集合を変数名の集合とする。

この約束だと、変数名は1文字で、全部で26個の変数しか使えません。もちろん実用性はありませんが、これはこれでハッキリとした定義です。別な定義として:

  • 英字(ラテン文字)小文字の後に、アラビア数字を好きなだけ(0個でもよい)並べた文字列の集合を変数名の集合とする。

これだと、'a', 'a1', 'a2', 'a12' などの名前を変数名に使えます。いま、文字列をシングルクォートで囲んだのは、それが具体的な名前〈記号〉であることを明示するためです。変数を表す変数としては、v, wなどを使います。

念のために注意しておくと、上の段落において出現したvは、英小文字'v'という名前の変数そのものではありません。構文論/意味論では、記号の集合の上を走る変数が登場します。“記号そのもの”と、それらの“記号を表す変数”にたまたま同じ記号が使われることはあります。これが混乱の原因となることがしばしばありますので注意してください。

UMiToLでは、変数構文を決めないでおきます。変数〈変数名 | 変数記号〉の集合は、後からカスタマイズ可能としておきます。Vを変数〈変数名 | 変数記号〉の集合として、Vにより変数構文を確定したUMiToL言語をUMiToL(V)とします。

UMiToLの実際の構文は、変数の集合Vがハッキリしないと確定しません。その意味で、UMiToLはプログラミング言語そのものというより、プログラミング言語フレームワークです。変数の集合というパラメータを渡されて具体的な言語を作り出す装置のようなものです。

実際の(オモチャでない)プログラミング言語でも、隅々までカッチリ構文を決めないで、後で決める部分を構文的パラメータにしていることもあります。構文的パラメータを具体化すると、その言語ファミリーの特定のバージョン〈具体例 | インスタンス〉が定義できます。

例えば、UMiToLのパラメータである変数集合を、英字小文字の集合だと決めると:

となり、UMiToL言語ファミリーの特定バージョンであるUMiToL({'a', 'b', ..., 'z'})が定義できます。UMiToL({'a', 'b', ..., 'z'})が使いにくいと感じるなら、別な変数集合を準備して、UMiToL言語フレームワーク(具体的UMiToL言語の生成装置)に渡せばいいのです。

リテラルの構文と意味

文字列'12'は、数値十二を表すための記号です。値を直接的に表す記号をリテラル〈literal〉と呼びます。'12'は12を表すリテラルです。

リテラルとそれが表す値を区別することは滅多にありませんし、通常は区別する必要がありません。しかし、プログラム意味論では、(少なくとも一旦は)リテラルと値を区別します。

いま、「リテラルは値を表す」と言いました。ということは、リテラルと値は密接に関連しています。値が何であるかをハッキリさせないとリテラルもハッキリしません。

そこで、値の集合Xを考えます。この集合Xをどう決めるかもカスタマイズ項目、つまり言語フレームワークUMiToLのパラメータです。例えば、X = (10未満の自然数*1​) と決めてもかまいません。言語フレームワークUMiToLのパラメータを2つに増やして、値の集合も指定すると:

このケースでは、リテラルは '0', '1', ..., '9' の10個です。シングルクォートにより、値そのものとリテラルを区別しています。値とリテラルは1:1に対応しているとします。今の場合は、0←→'0', 1←→'1', ..., 9←→'9' です。値は、数学的・概念的存在物であり、リテラルは構文的・記号的存在物です。

もう少し詳しく言うと、リテラルを導入するには、次の3つの構成素が必要です。

  1. 値の集合 X
  2. リテラルの集合 L
  3. 写像 val:L→X

写像valは何でもいいのですが、話を簡単にするために双射〈全単射〉であることを要求しましょう*2。具体例を挙げれば:

  1. 値の集合 X = {0, 1, ..., 9}
  2. リテラルの集合 L = {'0', '1', ..., '9'}
  3. 写像 val:L→X は、val('0') = 0, val('1') = 1, ..., val('9') = 9,

値の集合Xと写像 val:L→X は、構文論というより、もはや意味論に入り込んでいます。なので、リテラルの導入では、構文論と意味論が混じった話をしています。構文論と意味論が混じらないようにキッチリ分けることも可能ですが、いずれは混ぜちゃう(一緒に考える)ので神経質になっても意味がありません。

リテラルの話を単純化するために、次のような方法をとることがあります。

  1. 値の集合Xを決める。
  2. リテラルの集合Lを L = X と決める。
  3. 写像 val:L→X は、val = idX = (Xの恒等写像) と決める。

要するに、値とリテラルをまったく区別しない立場です。こうしても、理論上の不都合は起きないので、値とリテラルを同一視してもかまいません。

演算子記号の解釈

前節の設定を引き継いで:

  • 変数の集合 V = {'a', 'b', ..., 'z'} (26文字)
  • 値の集合 X = {0, 1, ..., 9} (10個の自然数

とします。また、値とリテラルを同一視します。つまり、いちいち'3'のようにクォートせずに、3はリテラルでもあり値でもあるとします。

さて、プログラミング言語UMiToL(のコア部分)で演算子が決められています。'+'と'-'が演算子記号で、これはカスタマイズの余地がありません(演算子は決め打ち)。プラス記号'+'とマイナス記号'-'を見れば、誰でもそれは足し算と引き算だろうと連想します。それが暗黙の了解、あるいは常識というもんです。

だがしかし、暗黙の了解や常識に頼ることは、プログラム意味論では一番やってはいけない行為です。暗黙の了解や常識は完全に明白ではないので、定義が曖昧になり、その後の議論もイイカゲンでグダグダになります。

実際のところ、UMiToL({'a', 'b', ..., 'z'}, {0, 1, ..., 9})における'+'や'-'は暗黙の了解や常識では決めかねます。'5 + 8'や'2 - 5'はUMiToLの構文で許された式ですが、その意味はハッキリしません。5 + 8 = 13, 2 - 5 = -3 に決っているだろうって? いえ、13も-3もUMiToL({'a', 'b', ..., 'z'}, {0, 1, ..., 9})では扱えない値です。

では、上記の設定(変数の集合 V = {'a', 'b', ..., 'z'}、値の集合 X = {0, 1, ..., 9})のもとで、演算子記号'+'、'-'の意味を確定しましょう。事前準備として、エラー/未定義を表す特別な値として、ボトムと呼ばれる記号'⊥'を導入して、次のように定義します。

  • X = {0, 1, ..., 9} = {0, 1, ..., 9, ⊥}

数学的な関数〈写像〉 plus, minus を定義します。

  • plus:X×X→X
  • minus:X×X→X

plus(x, y), minus(x, y)の一覧表を作ってしまいましょう。

plus(x, y)の値
x\y 0 1 2 3 4 5 6 7 8 9
0 0 1 2 3 4 5 6 7 8 9
1 1 2 3 4 5 6 7 8 9
2 2 3 4 5 6 7 8 9
3 3 4 5 6 7 8 9
4 4 5 6 7 8 9
5 5 6 7 8 9
6 6 7 8 9
7 7 8 9
8 8 9
9 9
minus(x, y)の値
x\y 0 1 2 3 4 5 6 7 8 9
0 0
1 1 0
2 2 1 0
3 3 2 1 0
4 4 3 2 1 0
5 5 4 3 2 1 0
6 6 5 4 3 2 1 0
7 7 6 5 4 3 2 1 0
8 8 7 6 5 4 3 2 1 0
9 9 8 7 6 5 4 3 2 1 0

基本は普通の足し算と引き算です。うまく定義できないときは⊥にしてしまう方針です。

plus:X×X→X, minus:X×X→X をキチンと定義した上で、演算子記号'+'の意味は関数plus、演算子記号'-'の意味は関数minusと定めます。

状態、状態空間、式の意味

UMiToLの実行とは、破壊的代入により変数の値を変えることです。UMiToLは極小な言語ですが、典型的な手続き型言語です。手続き型言語の意味論では、状態と状態空間を使うのが定石ですから、その説明をします。

Vは変数全体の集合です。集合Vは構文的なカスタマイズ項目で、今考えている事例では V = = {'a', 'b', ..., 'z'} でした。26個の変数があり、それ以上の変数を使うことはできません。不便ですが、それはいいとします。必要なら、別なVを採用することもできます。

Vの部分集合をA, Bなどで表します。XAで、AからXへの写像全体の集合を表します(指数記号に慣れてない方は「なんでソコに、足し算、掛け算、累乗の記号を使うのですか?」参照)。Xは変数の値の集合、⊥は未定義を表す記号でしたね。

UMiToLにおける状態空間〈state space〉とは、A(A⊆V)に対するXAという形の集合のことです。状態空間XAの要素を状態点〈state point〉、または単に状態〈state〉と呼びます。A, B⊆V として、写像 f:XA→XB は2つの状態空間のあいだの写像です。このような写像状態遷移〈state transition〉と呼びます。状態空間に構造(順序構造、位相構造など)を入れたり、状態遷移として許される写像を制限したりもしますが、今は単なる集合と写像でいいとします。状態、つまり状態空間の要素をρ, τのようなギリシャ文字小文字で表すことにします。

式の意味を定めるには状態が必要です。なぜなら、式は特定の状態においてはじめて値が定まるからです。eが式のとき、状態ρにおける式eの意味を 〚e〛ρ と書きます。白抜きの太いブラケットは、スコット・ブラケット〈Scott brackets〉、表示ブラケット〈denotation brackets〉、セマンティック・ブラケット〈semantic brackets〉、オックスフォード・ブラケット〈Oxford brackets〉など、色々な名前で呼ばれてますが、意味写像を表す記号です。

スコット・ブラケットを使って式の意味を記述*3すると次のようになります。

  1. cがリテラル(c∈X)のときは、〚c〛ρ = c
  2. vが変数(v∈V)のときは、〚v〛ρ = ρ(v)
  3. 〚(e)〛ρ = 〚e〛ρ
  4. 〚e + e'〛ρ = plus(〚e〛ρ, 〚e'〛ρ)
  5. 〚e - e'〛ρ = minus(〚e〛ρ, 〚e'〛ρ)

補足説明をすると:

  1. 値とリテラルを区別しないことにしたので、リテラルcの値はcそのものです*4。リテラルの意味は状態ρと無関係です。
  2. 変数の意味は、そのときの状態ρにより決定されます。ρ:A→X で、v∈A のときだけ意味を持ちます。v∈A でないときには〚v〛ρは定義できません。
  3. 式を括弧で包んでも意味に影響はありません。
  4. 演算子'+'の意味は、写像 plus:X×X→X で記述されるのでした。前節を参照。
  5. 演算子'-'の意味は、写像 minus:X×X→X で記述されるのでした。前節を参照。

状態は、式が評価されるときの環境を与えるので、評価環境〈evaluation environment〉、または単に環境〈environment〉と呼ばれることもあります。

コンパイル時のチェック

構文的に正しいプログラムは、BNFだけで定義することはできません。UMiToLのような単純な言語でも次の点を考えなくてはなりません。

  1. 式のなかに宣言してない変数が出現したらどうするか。
  2. 式のなかに初期化(最初の代入)してない変数が出現したらどうするか。
  3. 代入文の左辺が宣言してない変数だったらどうするか。
  4. 既に宣言済の変数をもう一度宣言したらどうするか。

ここでは、実行の前にUMiToLコンパイラが動くとして、コンパイラが次の動作をするとします。

  1. 式のなかに宣言してない変数が出現したらコンパイルエラーとする。
  2. 代入文の左辺が宣言してない変数だったらコンパイルエラーとする。

実行できるプログラムは、コンパイラのチェックをパスしているので、実行時に次のことを前提できます。

  1. 式のなかに宣言してない変数は出現しない。
  2. 代入文の左辺が宣言してない変数であることはない。

しかし、次は保証されません。

  1. 式のなかに初期化(最初の代入)してない変数は出現しない。
  2. 既に宣言済の変数をもう一度宣言することはない。

言い方を換えると:

  1. 式のなかに初期化(最初の代入)してない変数が出現するかもしれない。
  2. 既に宣言済の変数をもう一度宣言するかもしれない。

コンパイラが見る文/式

前節で述べたように、UMiToLにはコンパイラがあるとします。コンパイラ構文解析〈パージング〉や実行可能コード生成を行いますが、今は変数の出現チェックに注目しましょう。これは前節で述べた「宣言してない変数の出現はコンパイルエラーにする」機能です。

例として次のUMiToLプログラムを考えます。(このプログラムはコンパイルエラーしません。)

var a;
a := 1;
var b;
b := 3;
a := a + b

コンパイラは、上から順に変数宣言と変数使用を追いかけます。 宣言済み変数の集合〈有効な変数の集合〉は、1行ごとに次のように変化します。

  • {} → {'a'} → {'a'} → {'a', 'b'} → {'a', 'b'}

各行に書いてある文が(変数使用に関して)適正であるかどうかは、そのときの宣言済み変数の集合に依存します。コンパイラは、単に注目している1つの文を見ているのではなく、そのときの宣言済み変数の集合も一緒に見ています。

コンパイラが見ている宣言済み変数の集合を、プログラム・コードに記入してみます。縦棒'|'の左に変数の集合を添えます。

({} | var a);
({'a'} | a := 1);
({'a'} | var b);
({'a', 'b'} | b := 3);
({'a', 'b'} | a := a + b)

(変数の集合 | 文) の形を“コンパイラが見る文”と考えましょう。同様に、(変数の集合 | 式) が“コンパイラが見る式”です。コンパイラが見る文/式が適正〈suitable〉であるとは次のことだとします。

  1. 宣言文 (A | var v) はAが何であっても適正
  2. 代入文 (A | v := e) が適正である ⇔ ({v}∪Var(e))⊆A
  3. 空文 (A |) はAが何であっても適正

ここで、Var(e)は式eに出現する変数の集合で、次のように定義されます。

  1. cがリテラルのとき、Var(c) = {}
  2. vが変数のとき、Var(v) = {v}
  3. Var(eを括弧で包んだ式) = Var(e)
  4. Var(e + e') = Var(e)∪Var(e')
  5. Var(e - e') = Var(e)∪Var(e')

コンパイラが見る式 (A | e) が適正であることはもちろん:

  • (A | e) が適正 ⇔ Var(e)⊆A

適正という概念は、構文的に整形式〈well-formed〉であることと、意味的に妥当〈valid〉であることの中間的な“正しさ”概念です。

[補足]

プログラムの“正しさ”について補足しておきます。プログラムの構文はBNFのような文法記述言語で記述されます。文法に対して“正しい”とは構文解析木が作れることです。しかし、“整形式=構文解析木が作れた”だけでは実行時に問題がある(ことが多い)ので、コンパイラは追加のチェックをします。このチェックを通ったプログラムは適正ということにします。

実行時の“正しさ”は妥当性と呼びましょう。例えば、次の条件を満たすとき妥当だとします。

  • プログラムが停止する。
  • 停止したときの変数の値に未定義(⊥)がない。

UMiToLの場合、そもそも繰り返し構文がないので、すべての適正なプログラムは停止します。しかし、変数の値が未定義でないことは保証されません。例えば、var a という宣言文だけのプログラムは妥当ではありません(宣言されただけでは、変数の値は⊥)。

理想的なコンパイラにおいては、適正なプログラム=妥当なプログラムです。つまり、コンパイラを通ったプログラムは実行時に問題を起こしません。この理想を実現するのはなかなか難しいですが、邪悪な挙動を制限することにより理想に近づけることはできます。

[/補足]

文のプロファイル

ここから先では、単に文と言ったら、コンパイラが見る文であって適正なものです。Aは変数の集合、つまり A⊆V だとして:

  1. 宣言文 (A | var v) Aは何でもよい
  2. 代入文 (A | v := e) {v}∪Var(e))⊆A を仮定する
  3. 空文 (A |) Aは何でもよい

それぞれの文に対してプロファイル〈profile〉というものを考えます。文のプロファイルは、2つの変数の集合のあいだに矢印を入れた記号です。具体的には:

  1. 宣言文 (A | var v) のプロファイルは A→(A∪{v})
  2. 代入文 (A | v := e) のプロファイルは A→A
  3. 空文 (A |) のプロファイルは A→A

文とそのプロファイルをまとめて書けば:

  1. (A | var v):A→(A∪{v})
  2. (A | v := e):A→A
  3. (A |):A→A

書き方だけ見ると、写像の域・余域〈始域・終域〉と同じですが、とりあえず単なる記号だと思ってください。気持ちの上では次のように解釈します。

  1. (A | var v) の実行前に有効な変数の集合はA、実行後に有効な変数の集合は(A∪{v})
  2. (A | v := e) の実行前に有効な変数の集合はA、実行後に有効な変数の集合はA
  3. (A |) の実行前に有効な変数の集合はA、実行後に有効な変数の集合はA

文の意味の定め方

前節に述べたように、文には変数の集合をくっつけて考えます。そして、文にはそのプロファイルが一意的に決まります。

文の意味もスコット・ブラケットで書くことにします。スコット・ブラケットのなかに書く文では丸括弧を省略します。次のように書きます。

  1. 宣言文 (A | var v) の意味は 〚A | var v〛
  2. 代入文 (A | v := e) の意味は 〚A | v := e〛
  3. 空文 (A |) の意味は 〚A |〛

まず、変数の集合Aに対してスコット・ブラケット〚A〛を次のように定義します。

  • 〚A〛 = XA

〚A〛はA上の状態空間です。Aが空集合¥emptyset、単元集合{v}のときは次のようになります。

  • ¥emptyset¥stackrel{¥sim}{=} 1
  • 〚{v}〛 ¥stackrel{¥sim}{=} X

1は特定された単元集合ですが、1 = ¥emptyset = {⊥} と定義しておけばいいでしょう(何でもいいんだけどね)。

実は、文とプロファイルの記法 (A | v := e):A→A などは、スコット・ブラケットと相性が良いように決めたものです。文の意味は、状態空間のあいだの写像なので、集合と写像の意味で次が成立します。

  1. 〚A | var v〛:〚A〛→〚A∪{v}〛
  2. 〚A | v := e〛:〚A〛→〚A〛
  3. 〚A |〛:〚A〛→〚A〛

空文の意味は簡単で、次のように定義できます。

  • 〚A |〛 = id〚A〛 (A上の状態空間の恒等写像

宣言文と代入文の意味は節を改めて定義します。

宣言文の意味

UMiToLのプログラムは、その実行中に必ず状態を持ちます。実行に伴い状態が変化します。その状態は、変数の集合A(A⊆V)を使って ρ:A→X と書けるのでした。ここで、Aは、有効な変数の集合です。有効とは、宣言済みであることです。

  • 宣言済み変数の集合 = 有効な変数の集合 = dom(ρ)

宣言文 (A | var v) は、有効な変数の集合〈宣言済み変数の集合〉Aに、変数vを追加します。追加直後のvの値は⊥(未定義)とします。vが既に宣言済み、つまり v∈A ならば何も起こりません。

以上に述べた宣言文 (A | var v) の効果〈作用 | effect〉は、次のような写像として定式化できます。

  • XA→XA∪{v}

前節で定義した記法を使えば:

  • 〚A | var v〛:〚A〛→〚A∪{v}〛

この写像〚A | var v〛を具体的に定義します。まず、v∈A の場合は:

  • 〚A | var v〛 = id〚A〛 :〚A〛→〚A〛

つまり、変数vが既に宣言済みのときは、A∪{v} = A で、〚A | var v〛は何もしない写像(恒等写像)です。次に、v∈A でない場合: ρ∈〚A〛(〚A〛 = XA)に対して、〚A | var v〛(ρ) = ρ' と置くと、

  • w∈A ならば ρ'(w) = ρ(w)
  • ρ'(v) = ⊥

A上ではρをそのまま、vの値は⊥とした新しい状態ρ'が〚A | var v〛(ρ) です。この場合は〚A〛と〚A∪{v}〛は違う集合なので、〚A | var v〛:〚A〛→〚A∪{v}〛 ρ|→ρ' は異なる状態空間のあいだを飛び移る状態遷移となります。

もしコンパイラが、重複した変数の宣言をチェックするなら、宣言文の意味は常に異なる状態空間のあいだの写像となります。今の前提では重複した宣言文をチェックしてないので、宣言文の意味が恒等写像になることもあります。ここらは大した問題ではありません。

代入文の意味

UMiToLの唯一の実行文は代入文です。

  • 〚A | v := e〛:〚A〛→〚A〛

ρ∈〚A〛 に対して、〚A | v := e〛(ρ) を定義しましょう。〚A〛 = XA だったので、ρ∈〚A〛 とは ρ:A→X のことです。次の3つの命題は同じ意味です。

  • ρ∈〚A〛
  • ρ∈XA
  • dom(ρ) = A, cod(ρ) = X

ρ∈〚A〛に対して、〚A | v := e〛(ρ) = ρ' と置くと、

  • w∈A、w ≠ v ならば、ρ'(w) = ρ(w)
  • ρ'(v) = 〚e〛ρ

代入文 (A | v := e) の作用〈効果 | effect〉は、変数vの値を式eを評価した結果で置き換えること(その他の変数の値は変えない)です。

〚e〛ρは既に定義した式の意味ですが、式eに変数集合Aを添えたほうが明確・正確です。また、下付きのρを丸括弧に入れても同じことですから:

  • 〚A | e〛ρ = 〚A | e〛(ρ) (ρ∈〚A〛)

〚A | e〛は、〚A〛の要素(状態)ρを引数にしてXの値を返すので、写像 〚A | e〛:〚A〛→X です。ところで、X ¥stackrel{¥sim}{=} 〚単元集合〛 なので、〚A | e〛:〚A〛→〚単元集合〛 とみなせます。この形から、変数集合Aを添えた式 (A | e) のプロファイルは、r∈V を選んで次のように決めてかまいません。

  • (A | e):A→{r}

ハードウェアで例えれば、rは式の評価値を入れる役割のレジスタです。

プログラムの圏論的意味

いままでに述べた話を圏論を使って整理しましょう。プログラム意味論を圏論なしで行うのは辛いものがあるので、圏論の基礎知識は仮定します。圏論に馴染みがない方は、次の記事からのリンクを辿ってみてください。

いまここで必要なのは圏の定義だけなので、次の記事を読むだけで十分かも知れません。

今回は、集合圏Setをベースにします。より精密な議論をするには、順序集合の圏Ord位相空間の圏Topを使います。部分写像の圏Partialを使うと⊥(ボトム)の扱いが少しスマートになります。

変数の集合Vと値の集合X、それと写像 plus, minus:X×X→X を固定します。以下では、plus, minusも“込み”でXと書くことにします(記号の乱用 X = (X, plus, minus)*5)。このセッティングにより、UMiToL言語ファミリーの特定インスタンスUMiToL(V, X)を考えます。具体的な事例としては、V = {'a', 'b', ..., 'z'}, X = {0, 1, ..., 9}。

さて、UMiToL(V, X)のプログラムの全体を圏として定義します。その圏をPorgとしましょう。圏Progは以下の通り。

  1. Obj(Prog) = |Prog| = Pow(V) (Pow(V)はVのベキ集合)
  2. Mor(Prog) = (適正な全ての文)
  3. dom, cod, idはすぐ下に記述
  4. 圏の結合〈composition〉もすぐ下に記述

dom, codは文の種類ごとに定義します。

  1. 宣言文 dom(A | var v) = A, cod(A | var v) = A∪{v}
  2. 代入文 dom(A | v := e) = A, cod(A | v := e) = A
  3. 空文 dom(A |) = A, cod(A |) = A

idは、

  • idA = (A |) (空文)

結合の定義は次のようです。

  • (A | α);(B | β) = (A | α;β)

これにはちょっと説明が必要でしょう。

  • 左辺の';'は、圏の結合を表す記号(図式順結合記号)です。
  • αとβは、BNFで定義した文を表します。
  • 右辺の';'は、2つの文を構文的に繋ぐときに使う分離子記号〈セパレータ〉です。

圏の演算記号と文の分離子に同じセミコロンが使われているので紛らわしいのですが、一方で、これは便利な記法でもあります。

Progにおける結合律と単位律は簡単そうですが、実際は「文が同じ」であることを正確に定義しないといけなくて、けっこう難しいです。今回は割愛します。

先に導入したプロファイル (A| v := e):A→A などは、実は圏Progにおける射を表す記法だったのです。Progが圏であることが分かれば、スコット・ブラケットで表された意味写像が関手であることも分かります。

〚-〛は、プログラムの圏Progから集合圏Setへの関手なのです。次が成立します。

  1. 対象 A∈|Prog| に対して、〚A〛は集合、つまりSetの対象である。
  2. 射 (A | α):A→B in Prog に対して、〚A | α〛は写像、つまりSetの射である。
  3. dom(〚A | α〛) = 〚dom(A | α)〛, cod(〚A | α〛) = 〚cod(A | α)〛
  4. id〚A〛 = 〚idA〛 = 〚A |〛
  5. 〚(A | α);(B | β)〛 = 〚A | α〛;〚B | β〛 (右辺の';'は写像の結合)

UMiToLの意味論は、関手 〚-〛:ProgSet により完全に記述できます。

おわりに

超簡単な手続き型言語UMiToLに対して、圏論的意味論を与えました。UMiToLの実行文は代入文だけであり、代入文は変数の値を変えるものです。したがって、UMiToLの意味論は変数の意味論だと言ってもいいでしょう。

現在では、表示的意味論〈denotational semantics〉と操作的意味論〈operational semantics〉の境界は曖昧です。UMiToLの意味論は、集合と写像(集合圏)を意味とするので表示的意味論のようではあります。しかし、代入文の意味は状態遷移系であり、一種の抽象機械を考えていることになり操作的ともいえます。もはや、意味論の分類を云々してもしょうがない気がします。計算現象をキチンと写し取れるモデルが作れればそれでいいのです。

いずれにしても、手続き型言語の意味論には状態概念が必要でしょう。状態は純関数的ではないので嫌う人もいますが、そういう拘りはナンセンスに思えます。仮にプログラミング言語に状態も副作用もなくても、ファイルシステムやデータベースを扱えば状態が入り込んでしまいます。ファイルシステムもデータベースも一切触らない、というのは現実性がないでしょう。

UMiToLは状態と副作用(実は主作用)を扱う最も簡単なモデルですが、その意味論はそれなりに複雑な構造を持ちます。構文的パラメータである変数集合Vや、意味的パラメータである値の集合X(plus, minusを含む)などのメカニズムをチャンと分析すると、もっと複雑な構造(たぶんインスティチューション)が現れます。また、条件分岐や繰り返しの制御構造を入れれば、それも複雑さにつながります。

オモチャでない実用的プログラミング言語の意味論が随分と複雑そうなことは想像できるでしょう。しかし、その複雑さのなかに面白くて深い構造が潜んでいると期待もできるのです。

*1:0は自然数に含めます。

*2:valが何でもいいときは、違うリテラルが同じ値を指すことがあり、また、リテラルでは表現できない値も存在します。リテラルで表現できなくても、リテラルから作った式で表現できれば、値を指すことができます。式でも表現できない値があっても別にかまいません。

*3:厳密に言えば、文字列/トークン列としての式に意味を定めるのではなくて、構文解析後の構文解析木に対して意味を定めます。UMiToLの場合、構文解析は非常に簡単なので、構文解析木を引き合いに出す必要はないでしょう。

*4:⊥を表すリテラルはないことに注意してください。

*5:Xにplus, minusを加えた構造は、特に演算法則を要求していません。何の法則性もない二項演算を持つ代数系をマグマと呼びます。(X, plus, minus)は、二項演算を2つ持つマグマと言えます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171116

2017-10-30 (月)

はてなダイアリーのgoogle検索ULRが間違っている

| 16:29 | はてなダイアリーのgoogle検索ULRが間違っているを含むブックマーク

[追記]「間違っている」と指摘しているタイトル文言が間違ってます。"ULR"じゃなくて"URL"。[/追記]

はてなダイアリーの機能に、[google:ナントカ] と書くと、指定した文字列"ナントカ"をgoogleで検索できる記法があります。

しかし、今はうまく動きません。展開されたURLを見ると、https://www.google.co.jp/search に渡すクエリーパラメータとして、"q="に続けてパーセントエスケープされた検索文字列、"ie="に続けて文字エンコーディングが指定されています。で、文字エンコーディングの値が euc-jp になっていますね。「はてな」は、いつからかutf-8に切り替えたはず。[追記]euc-jpのままだそうです。コメント欄参照。[/追記]

"ie=utf-8"にすればうまく動きます。

「はてな」はもうはてなダイアリーをメンテナンスする気はないでしょうし、google記法を使う機会も滅多にないから別にいいっちゃいいですけど、数文字修正で治るバグ。

emkemk 2017/11/04 11:08 はてなブログはutf-8ですが、はてなダイアリーは今でもeuc-jpです。
バグがあるのはGoogleのほうです。はてなはgoogle記法で
http://www.google.com/search?q=%A4%CF%A4%C6%A4%CA%A5%C0%A5%A4%A5%A2%A5%EA%A1%BC&ie=euc-jp
のようにちゃんと"q="をeuc-jpでエンコードしたURLを生成していますが、これでGoogleにアクセスすると、Googleは
https://www.google.co.jp/search?q=%E3%81%AF%E3%81%A6%E3%81%AA%E3%83%80%E3%82%A4%E3%82%A2%E3%83%AA%E3%83%BC&ie=euc-jp&...
のように、"q="のエンコーディングをutf-8に変換しているのに、なぜか"ie="の値はeuc-jpのままというURLにリダイレクトするので、おかしくなります。Googleはもうろくにutf-8以外をサポートする気がなくて、テストもしていないのでしょう。

m-hiyamam-hiyama 2017/11/04 20:37 emkさん、
そうだったんですか。情報ありがとうございます。
どっちが悪いかは置いとくとして、ワークアラウンドとしての対処は、はてなが行ったほうが早い気はします。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171030