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

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

2017-11-17 (金)

ほぼ絶滅 アンミラ

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

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

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

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

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

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

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

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

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

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


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

D

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

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

[/追記]

トラックバック - 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

2017-10-28 (土)

閉塞的純粋主義者と拡張的純粋主義者

| 11:08 | 閉塞的純粋主義者と拡張的純粋主義者を含むブックマーク

データベースとカン拡張と思い出」にて:

僕は、純粋主義が心情的に嫌いなんですけど、[...snip...]


純粋関数主義も純粋オブジェクト主義もずっと嫌い。そして、純粋リレーション主義も嫌いです。理屈じゃなく嫌い。

と、「純粋主義者は嫌いだ」と叫んでいるのですが、ちょっと語弊があると思うので補足します。

僕が言っている純粋主義とは、何らかの純粋さに価値を置き、その価値観からみて不純なものを排除しようとする態度のことです。「純粋さ」を一般的に定義するのは無理ですが、先に挙げた具体例 -- 純粋関数主義、純粋オブジェクト主義、純粋リレーション主義などがあります。

純粋主義者は、純粋さの基準を持っています。それを成文化すれば経典になります。絶対的な基準=教義を作ろうとしたり、既にある教義を遵守して暮らそう、という態度が僕は気に入らないのです。

とか言いながら、僕も何らかの純粋主義に陥っていて、同族嫌悪の感情なのかも知れません。そうだとしても、僕が“より嫌い”な同族がいるのは確かです -- それを仮に、閉塞的(あるいは閉鎖的)純粋主義者と呼びます。一方、シンパシーを感じる純粋主義者を拡張的(あるいは開放的)純粋主義者と呼ぶことにします。

閉塞的純粋主義者は、純粋さの基準=教義をより洗練させて、クリアな境界線を引こうとします。そして、境界線の外=不純なものを悪とみなします。一方で拡張的純粋主義者は、不純なものを包み込んで、純粋・不純の境界線を消し去ろうとします。

純粋関数主義を例にするのが分かりやすいでしょう。純粋関数こそがよきものだと思っている純粋関数主義者は、副作用はダメだ/状態はダメだ/未定義はダメだ/大域変数はダメだ/例外はダメだ、とか主張するでしょう。現在では、このテの純粋さへの拘りはあまり見かけなくなりましたが、昔は実際に言われていました。

「ダメだ」と言われてもねぇー。「ダメなんですか、じゃーやめます」とはなりません。多くの人が長年続けている不純な事は、単なる悪癖ではなくて、不純さが必要な理由があるのです(たまに、単なる悪癖もあるけど)。

副作用/状態/未定義(部分性)/大域変数/例外(大域脱出)などを包み込んで、純粋関数のメリットをあまり失わない手法といえば … そう、モナドです。僕がモナド、つうかモナド的発想が好きなのは、不純なものを目のかたきにせずに、懐柔して手なずけている点です。みんなが蛇蝎のごとく嫌っているgoto制御やフローチャートだって、手なずける方法があるはずです。

自分は、ほんと閉塞的純粋主義者とは相性悪いわ、と改めて感じたのは:

どこがダメなのか」記事を書いた後で、クリス・デイト(C.J. Date)の本『データベース実践講義 ―エンジニアのためのリレーショナル理論』も眺めてみたんですけど、どうも純粋リレーション主義者とでも呼ぶべき人々がいるようです。

クリス・デイトの、純粋リレーション主義の観点からのSQL標準規格やER図への批判を読んだからです。もちろん、同意できる批判も多いのですが、単に「純粋じゃないからダメ」と言っている部分もあり、正当な根拠とは思えない。なぜなら、徳目的・教条的な純粋さに価値があるとは思ってないから。

関数的不純さをモナドで取り込むように、データベース理論においても、非リレーショナルな不純さを手なずけるメカニズムが必要なんだろうと思います。

2017-10-27 (金)

集合の宇宙論

| 12:13 | 集合の宇宙論を含むブックマーク

現場の集合論としての有界素朴集合論」において、プログラミング言語やデータベースを扱うときは、そんなに立派な集合論は要らないだろう、という話をしました。

プログラミング言語やデータベースを扱うことを現場的日常作業と考えましょう。すると、日常作業にそうたくさんの集合は使わないし、'∈'(所属関係)の階層を無限に昇ることもしません。だったら、全数学を展開できるような強烈な集合論は不要で、小規模で弱い集合論でも足りるでしょう。

小規模で弱い集合論と、そのモデル(意味的世界)である“宇宙”の話をもう少し続けることにします。

内容:

  1. ZFCの宇宙と小宇宙
  2. 小宇宙と圏論
  3. ちょうどよい小宇宙

ZFCの宇宙と小宇宙

ZFC公理的集合論を直接使うことはほとんどないと思いますが、素朴集合論による議論は“頑張れば”ZFC集合論に翻訳できて、合理化できます。ただし、翻訳の労力がハンパない*1ので、やりませんけどね。

一階古典述語論理の上の公理系としてのZFC集合論のモデル(意味的世界)をVとします。Vって何なんだ? にうまく答えることは僕にはできません(苦笑)。ともかく、したいことは何でもできる環境として、Vがあると思ってください。VをZFC宇宙と呼びます*2

ZFCの宇宙Vが一意的に存在するのかというと、そうでもないようです。ZFC集合論からは決定できない命題Pがあれば、Pが成立する宇宙とPの否定が成立する宇宙は別物です。しかしどちらもZFC集合論のモデルになれます。ここでは、ZFC集合論の定理がすべて成立する宇宙を選んで固定し*3、それをVと呼びます。

Vの部分クラスでVより小さいW(W⊆V、W≠V)が、ZFC集合論のモデルになることはあるだろうし、それは別にかまいません。そのようなWで、W∈V となるものはあるんでしょうか? ちょっと僕には分かりません。もし、そんなWがあるなら、外側のVはもの凄く大きいことになります。

U⊆V という部分クラスUがあって、UがZFC集合論のモデルではなくても、“ある種の集合論”のモデルになっている場合、Uのことも宇宙(ZFC宇宙ではないが)と呼ぶことにします。さらに、U∈V のとき、Uを小宇宙(small universe)と呼びます。小宇宙は、宇宙でありながら、それ自体がZFCの集合であるものです。

小宇宙と圏論

現場の集合論としての有界素朴集合論」で紹介した有界宇宙は小宇宙の例です。有界な小宇宙Uは、ZFC集合論のモデルにはなれません。ZFC集合論で成立してる定理が、有界なUのなかでは成立しないからです。特に、新しい集合の構成が制限されます。

有界宇宙Uとその集合論は、小さい宇宙と弱い集合論ということになります。いつでもパワフルな集合論が必要なわけではないし、構成の自由さがむしろ邪魔になることもあります。その意味で、小さい宇宙と弱い集合論にも意義と価値があると思います。

さて、圏論を行うのにZFC集合論のフルパワーが必要でしょうか? グロタンディーク宇宙と呼ばれる宇宙のなかで圏論は行えると言われています。しかし、自明でないグロタンディーク宇宙が存在するかどうかはZFC集合論のなかではよく分かりません。

ZFC+αの集合論のなかでグロタンディーク宇宙Uが小宇宙として存在すると、圏論には好都合です。というのも、ZFCの大宇宙Vのなかで圏を定義すると、それをVのなかの集合とみなせることが保証されないからです。例えば、ZFC宇宙Vの集合を対象とする集合圏SetVでは、その対象類|SetV|がV内の集合とはなりません。圏の圏CatVも同様に、V内の集合をベースに捉えることができません。

もし、グロタンディーク宇宙Uが、U∈V として(小宇宙として)存在すれば、 SetU∈|CatV| や CatU∈|2CatV| (2圏の圏)などが言えます。この状況が成立すれば、たまに登場する(せざるを得ない)「必ずしも小さくはない圏の圏CAT」も安心して使えます。

僕は、集合論的な議論はよく知らないし理解できそうにないのですが、CATが存在し、Catに関する議論はCATに対しても適用可能だろう、と楽観的に考えています。なぜ楽観的になるか? というと、そう考えないと不安で、精神衛生上よろしくないからです。

ちょうどよい小宇宙

グロタンディーク宇宙は、大宇宙V内の集合だとはいいながら、そのなかでたいていの事は出来るので、十分に大きな宇宙です。実用上不便を感じることはないでしょう。

一方、「現場の集合論としての有界素朴集合論」で例に出した U = N∪Pow(N)∪{Pow(N)} は、ほんとに小さな宇宙で、不便を感じるかも知れません。

冒頭で言った現場的日常作業の場合、大宇宙Vをほんとに必要とすることはないように思います。目的に応じてちょうどよい小宇宙を作って、そのなかで議論するのも良いんじゃないでしょうか。この方法のメリットは、メタな議論が気兼ねなく自由に出来ることです。

ホントの宇宙Vは、その性格上、外に出ることが出来ません。なにしろホントの宇宙なので、宇宙の外なんて無いんです。この点は、物理的・天文学的大宇宙と同じことです。それに対して小宇宙は、ガジェット(手に取れる小物)ですから、外側から好き放題にいじり倒せます。

宇宙を意識しはじめたのは割と最近なんですが、プログラミング言語型理論/データベース/証明系が使う論理、などのモデルを考えるときは、宇宙をハッキリさせないとグダグダした感じになっちゃうんですよ。なので、自分が使っている/必要とする宇宙を明示的に定義したほうが良いと感じてるんですわ、ここんとこ。

*1:人手では大変ですが、ソフトウェアによるコンパイラは作れるでしょう。ひょっとしたら、もうあるかも。コンパイルを機械にやらせても、コンパイル結果の論理式を人間が理解するのはほぼ無理だと思います。

*2:ここで使っているVは、フォン・ノイマン宇宙とは限りません。ZFC集合論のなんらかのモデルです。

*3:宇宙を選んで固定するなんて作業が、人間に出来るかどうかは疑わしいですが。

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

2017-10-25 (水)

データベースとカン拡張と思い出

| 17:10 | データベースとカン拡張と思い出を含むブックマーク

雑談日記エントリーです。雑多な話題の寄せ集めです。カン拡張のちゃんとした説明とかはありませんからアシカラズ。

タイトルにある3つの単語:

  • データベース
  • カン拡張
  • 思い出

は、10月8日(日曜)にあった圏論食事会で話題になったことです。

内容:

  1. 圏論勉強会の系譜
  2. データベースの話
  3. データベースとカン拡張
  4. カン拡張祭り

圏論勉強会の系譜

圏論食事会に集まったメンバーは、

  • 深川くん(a.k.a. ジョニー)
  • たけをさん
  • Kuwataくん、
  • 日比野さん
  • たんちけさん

と僕です。集まった名目は、「圏論勉強会100回達成を祝う」というものです。

圏論勉強会」という名前の勉強会はいくつかあります。混乱をさけるために、主催者の名前から「たんちけ勉強会」としましょう。100回を迎えたのはたんちけ勉強会です。

たんちけ勉強会の発端は、竹内さんの『層・圏・トポス』を皆んなで読もう、とジョニーが呼びかけたことです。

この日付を見るに、たんちけ勉強会は2009年5月から始まったのでしょう。

勉強会テキストである『層・圏・トポス』について、2009年4月30日にコメントしています。


たんちけ勉強会が始まるずっと以前に、僕は、別な圏論勉強会に参加しています。

たんちけ勉強会開始の2年前、2007年5月ですね。主たる目的は量子ファイナンス工学の普及活動だと記憶してます(たけをさんにも確認済み)。

今日、2007年の記事を確認して驚いたことがあります。当該記事から次の記事へのリンクがあります。

当時、どうも僕はこのテ(↑)の話をしたようです。なんと、10年後の2007年に名古屋で話したネタが同じ(フロベニウス代数)だった、-- という事に気が付きました。ほんと進歩ないなー >自分

僕が2007年から顔を出すようになった圏論勉強会は、さかいさんが主催者エライ人なのでさかい勉強会と呼びましょう。さかい勉強会は、「さかいさんが学部学生の頃から始まった」とたけをさんから聞きました。

僕のこのブログ内での言及は2005年3月にあります(「なんと、圏論記事への言及が」)。さかいさんの「ヒビルテ」のアーカイブを探すと2005年10月に「第十回圏論勉強会」への言及があります。ということは、2004年か2005年初頭にさかい勉強会は始まったのでしょう。

さかいさんは、2002年(学部2年)の時点で、「圏論への誘い」なんて発表をしています。今から15年前です!

当時の少年たちは大人になり、当時既にオッサンだった僕はジイサンになりました。

データベースの話

割と最近、「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」という記事を書きました。このネタも、実は圏論食事会で話題にしたものです。そのとき話したことは:

  1. zhanponさんのQiita記事をみつけた。
  2. トンデモ本を期待して奥野本を買った。
  3. 残念! まともな本だった。
  4. が、zhanponさんの気持ち(「奥野さん、イイカゲンなこと書き過ぎ」)はよく分かる。
  5. でも、冷静になると擁護できる点もある。
  6. 2章はダメだが、2章を修正しても後で論理を使ってないので、その事のほうがダメだと思う。

と、口頭で言った内容をまとめたのがくだんの記事です。

「どこがダメなのか」記事を書いた後で、クリス・デイト(C.J. Date)の本『データベース実践講義 ―エンジニアのためのリレーショナル理論』も眺めてみたんですけど、どうも純粋リレーション主義者とでも呼ぶべき人々がいるようです。

僕は、純粋主義が心情的に嫌いなんですけど、理屈からいっても純粋リレーション主義は全然ダメだと思う。「どこがダメなのか」はおいおい書いていくつもりですが、ザックリ言えば、徳目主義・教条主義に堕していて、破綻に目をつむり、自己欺瞞のなかで閉塞しています。

奥野さんは、「ER図とリレーショナルモデルは何の関係もありません」と言い、クリス・デイトもER図を嫌っているようです。この事から、純粋リレーション主義者は、ER図も拒否していると気付きました -- SQL標準規格とSQL準拠製品に批判的なのは昔から知ってました。批判は全然いいのだけど、近隣分野との境界線を引いて、その境界の内側に篭もるのはどうなのよ?

データベースに対する新しい定式化としてスピヴァックの関手データモデルがあります。スピヴァックは、リレーショナルデータベースの言葉を使って説明しようと試みているので、「関手データモデルはリレーショナルモデルと相性がいい」と僕は思い込んでいました。しかし、改めてスピヴァック理論を眺めてみると、ER図の圏論的定式化の形になっています。そして、使っている言葉はSQLの用語(テーブル、カラム)です。

となると、「ER図は嫌い、SQLはけしからん」と言っている純粋リレーション主義者は、関手データモデルをハナから相手にしないでしょう。関手データモデルは、リレーショナルモデルと対立するものではなくて、むしろ、クリーンな再定式化と拡張のチャンスを与えるものなんだけど。

データベースとカン拡張

スピヴァックは当初、関手データモデルの説明に、圏論的概念・用語を出来るだけ使わないようにしていました。データベースコミュニティに受け入れられやすいようにだと思います。しかし一方で、背後にある圏論的構造が見えにくくなる弊害もありました。

例えばスピヴァックは、実際のデータの圏として集合圏Setだけを使っています。僕は、なんで関係圏Relを使わないのか疑問でした。どうも、関係の代わりに集合圏のスパンを使えばいいだろう、ということらしいです。あるいは、ベキ集合モナドによるクライスリ圏を使ったクライスリ・データベースを使ってもいいでしょう。

圏論的概念・用語を出来るだけ使わない」なら、カン拡張なんて持ち出してはダメです。実際、以前のスピヴァックの論文にカン拡張はほとんど出てきません(最近の代数データベース論では平気でカン拡張使ってますが)。これは、言葉を出してないだけで、当初からカン拡張は本質的に使っています。

スピヴァックの言うスキーマとは、およそER図のことです。スキーマSインスタンスとは、ER図のノードに集合、辺に写像を対応付ける写像圏論用語の関手)です。スキーマSからスキーマTへのスキーマとは、およそ(有向グラフと考えた)ER図の埋め込み*1のことです。

[追記]スピヴァックのスキーマと、リレーショナルデータベース(RDB)におけるスキーマは、雰囲気は似てますが別物です。RDBスキーマは、どちらかと言うとスピヴァックのインスタンスです。もっと正確に言うと、部分的に定義されたインスタンス -- 部分インスタンス(partial instance)とでも呼ぶべきものです。このへんの齟齬も、誤解や混乱を招く原因となります。困ったもんだ。[/追記]

J:STスキーマ射(関手)で、G:SSetインスタンス(これも関手)のとき、S上のインスタンスGを、スキーマ射Jに沿って拡張したい時がしばしばあります。既存データベースへの問い合わせ結果の構成や、スキーマ変更にともなうデータ移行に必要なのです。

スキーマ射Jに沿ってインスタンスGをうまいこと拡張した新しいインスタンスJG:TSet とします。「うまいこと」の意味は、次の同型が成立することです。ここで、'*'は図式順の関手の結合、[-, -]は関手圏を表します。

  • [S, Set](J*F, G) ¥stackrel{¥sim}{=} [T, Set](F, JG)

JGは、Gの(Jに沿った)右カン拡張(right Kan extension)と呼びます。上の同型(カン対応(Kan bijection))は、Jによる前結合(pre-composition)とJに沿った右カン拡張が随伴ペアになることを示しています。今使った記号法などは次の記事を参照してください。

右カン拡張の双対である左カン拡張も、使う機会は少ないものの、データベース操作に実際に使います。左右のカン拡張は、関手データモデル(あるいは、その拡張である代数データベース)における重要なデータベース操作なのです。

カン拡張祭り

たんちけ勉強会の100回記念(なのか?)で、カン拡張祭りが企画されています。企画があるという以上の情報を僕は知りません。開催が決まれば、@tanchikeや@hiroki_fあたりで告知があると思います。

"All Concepts are Kan Extensions"は有名な言葉で、カン拡張は、すべての普遍的構成を生み出す母のように見なされています。僕自身はシリアスにカン拡張を使う機会がなかったので、カン拡張のご利益をうまく説明できないのですが、右も左も(だいた極限と余極限に相当する)カン拡張がデータベース操作として出てくることは、カン拡張が普遍的である証左でしょう。

*1:埋め込みでない、一般の関手も考えますが、埋め込みの場合が簡単です。

TuvianNavyTuvianNavy 2017/10/26 15:23 DateがSQLを継子扱いする姿勢に説明しがたいモヤモヤを感じていたのですが、明快に言い切って頂いて自分も頭が整理できた気がします。しかしあの人の教科書が一応権威なんだよなあ。。

SQLの話をすれば、スキーマにNOT NULL制約をつけてDISTINCT句とORDER BY句で結果行を統制して外延性を強要しようとしても、外結合(凸結合、でいいでしょうか)クエリを排除しない限り、WHERE句で特性関数を定義できている保証はないですよね。。

bonotakebonotake 2017/10/27 03:34 たんちけ勉強会はある時期からたんちけさんが主催を引き継いだので間違いないですが、さかいさんは主催はしてないかも。招聘講師というか監修者というか、そんな(もっとエライ)立場だった感じです。

m-hiyamam-hiyama 2017/10/27 10:06 TuvianNavyさん、
デイトは、コッド理論をさらに純粋化して経典に仕立てたいのでしょうかね -- そんなふうに見えます。SQLが不純なのは、不純にならざるを得ない事情があるからでしょう。
純粋関数主義も純粋オブジェクト主義もずっと嫌い。そして、純粋リレーション主義も嫌いです。理屈じゃなく嫌い。
とはいえ、デイトの教条主義が破綻しているのは(感情論じゃなく)指摘できます。
気が向いたら、いつか書くかも。たぶん。

> 外結合(凸結合、でいいでしょうか)
凸結合は別物です。

m-hiyamam-hiyama 2017/10/27 10:09 bonotakeさん、
なるほど。エラかったんだ。でも、最年少だったんですよね?
言い出しっぺはさかいさんなんですか? もしそうなら、主催者というよりファウンダー&スーパーバイザあたりか?

2017-10-24 (火)

現場の集合論としての有界素朴集合論

| 16:36 | 現場の集合論としての有界素朴集合論を含むブックマーク

奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで、ピンクで「(詳細は別途記述予定。)」と書いてあるところが6箇所あります。これらの“ピンクの宿題”を順不同で片付けていくシリーズ第二弾です。

データベース理論などを展開するのにお手頃な集合論・述語論理について云々します。

ピンクの宿題 その1

[奥野さんが言う集合論・述語論理とは、]あくまでリレーショナルモデル界隈を説明・分析する道具・枠組みのことであって、一般的集合論と一般的述語論理の話ではありません。(詳細は別途記述予定。)

ピンクの宿題 その3

[奥野さんは、]述語論理のある特定の体系に対して、ある種の集合論(ZFCってことではない)の宇宙が健全な(ひょっとすると完全な)モデルになっている、ってことを言いたいのだと思います。(詳細は別途記述予定。)

これらの宿題の完全解決とは言い難いですが、思うところを述べます。

なお、ピンクの宿題解決の第一弾は:

内容:

  1. 述語論理と集合論
  2. 素朴集合論とは何か
  3. アトムと集合
  4. 宇宙と銀河
  5. 有界素朴集合論
  6. 有界素朴集合論の使い途

述語論理と集合論

論理の体系(ナントカ論理と呼ばれるモノ)は、目的や趣味に応じて山のようにあります。多種多様なので、論理の分類学や論理の博物学が成立しそうです。しかし、典型的なものをひとつだけ選べと言われれば、一階古典述語論理を選ぶ人が大多数でしょう。

一階古典述語論理(first-order classical predicate logic/calculus)は、完成度が高く使いやすく強力な推論能力を持っています。一階古典述語論理を実際に使うときは、プレーンな体系ではなくて、定数記号/関数記号/述語記号/公理/推論規則を足してカスタマイズしてから使います。

例えば、自然数の理論を展開したいなら、定数記号'0'、1変数関数(単項演算子)記号's'、2変数述語(2項関係)記号'='を足して、それらしい公理(証明なしに認める命題)と数学的帰納法の推論規則も足します。足し算'+'や大小順序'≦'などは、あとから定義により導入できます。

特筆すべきは、ZFC公理的集合論(Zermelo–Fraenkel axiomatic set theory with Choice)も一階古典述語論理により記述されていることです。カスタマイズは自然数論よりむしろ簡単で、追加する記号は'∈'だけです。これに幾つかの公理を足して、あとは一階古典述語論理の推論能力を使って定理を証明していくだけです。

ZFC公理的集合論は、一階古典述語論理の上に構築できる理論の一例に過ぎません。しかし、特別なものだと見なされています。現状の全ての数学的理論は、ZFC公理的集合論の内部で展開できると信じられています。例えば、集合論とは独立に構築した自然数論も、ZFC公理的集合論のなかに埋め込める(集合論の言葉に翻訳できる)のです。

ZFC公理的集合論の万能性・普遍性は認めたとしても、だからと言って、何でもZFC公理的集合論のなかでやる必要はありません。つーか、そんなことはしません自然数論は、集合論とは独立な体系内でやればいいのです。必要があれば、ZFC公理的集合論への埋め込み(翻訳)を作ればいいのです。

素朴集合論とは何か

集合概念が必要な場面では、ZFC公理的集合論が使われているのでしょうか? -- 使われません。日常的にZFC公理的集合論を使う人なんていない、と言うと言い過ぎだけど、極めて少数です。

我々が日常的に使っている集合論素朴集合論(naive set theory)です。要するに、直感的でイイカゲンでカジュアルな集合論です。

厳密な定義や公理系を持たない集合論を総称して素朴集合論と呼んでいるので、素朴集合論を定義するのは無理があります。が、素朴集合論を二種類に分けて考えたほうがよさそうです。ひとつはユーザーフレンドリーなZFC集合論、もうひとつは原始集合論です。

ユーザーフレンドリーなZFC集合論とは何か? -- ソフトウェアで喩えてみましょう; シンプルで強力だが使いにくいプログラミング言語(例えば、仮想機械のアセンブラ言語)があったとします。そこに、スクリプト言語の処理系を載せて、ツールとライブラリもバンドルして、UIも備えたオールインワンのパッケージを作成したとしましょう。ユーザーは元の低水準言語を意識することはないでしょう。一部の好き者は低水準言語を触りたがります。

まー、そんな感じ。この意味の素朴集合論は、直感的かつ安直に使える集合論ですが、頑張ればZFC集合論に“コンパイル”して合理化できます。

もうひとつの原始集合論とは、集合論を学ぶ以前に知っている集合論とでも言えばいいでしょうか。人間が持つ認識能力の一種です。集合論や論理を学ぶ際に、この種の認識能力が事前にないと、そもそも学ぶことが出来ません。原始的な認識能力に僕は興味を持っているのですが、今日はこれ以上、この話はしません。

アトムと集合

以下、素朴集合論とはユーザーフレンドリーなZFC集合論の意味だとします。

素朴集合論には、集合でないモノがあります。例えば、整数3は集合でしょうか? 普通の感覚では、3は集合ではありません。しかし、ZFC集合論では全てのモノが集合です。もちろん、整数3もZFC集合論における集合です。

要素を持たないモノをアトム(atom; 原子)と呼びます。素朴集合論で、3はアトムです。ZFC集合論では、3はアトムではありません。このギャップを埋める方法は、割とイイカゲンで、いくつかの集合を特定して、それらの集合の要素は「アトムと見なそう」と約束するだけです。

例えば、プログラミング言語の意味論を作るときなら、整数の集合/実数の集合/文字の集合/二値真偽値の集合あたりを特定して、その要素である整数/実数/文字/真偽値はアトム扱いする、とかです。

aとbがアトムのとき、ペア(順序対)(a, b)はアトムでしょうか? ZFC集合論の標準的な構成だと、ペアはクラトフスキー・ペア {{a}, {a, b}} として定義されます。しかし、(a, b)もアトムだと見なすほうが都合が良いので、「アトムのペアはアトムである」と約束します

アトムを認めると、何がアトムで何がアトムでないかイチイチ決めなくてはいけないので面倒になります。ですが、我々がプログラミング言語やデータベースの話をするときは、スカラー型、複合データ型、コレクション型のような区別をするので、アトムを認めたほうがよいでしょう。

宇宙と銀河

ZFC集合論の集合の全体からなる集まりをVとしましょう。オイッ、ちょっと待った! Vって何だよっ?! って話ですが、「aは集合である」を記号的に a∈V と書くだけだと思ってください。Vはもちろん集合ではありませんから、 V∈V ではありません。「a∈V」と書くときの'∈'と、a, b∈V に対する「a∈b」の'∈'は意味が違いますが、同じ記号を使います。VはZFC集合論宇宙(universe)と呼びます。

我々が日常的に使う集合論、特にプログラミング言語やデータベースの話をするときに使う素朴集合論の宇宙をUとします。前節の議論より、Uにはアトムも入っているとします。したがって、a∈U は、「aはアトム、または集合」という意味です。宇宙Uのアトムの全体をAtomU、集合の全体をSetUとします。U内に存在するモノはアトムか集合なので、U = AtomU∪SetU です。通常は、AtomU∩SetU = {¥emptyset} (¥emptyset空集合)とします。

我々の日常宇宙Uは、ZFCの宇宙Vに埋め込むことが出来るので、U⊆V です。それだけではなくて、日常宇宙Uは、ZFC宇宙Vの単一の集合とみなせるでしょうから、U∈V と考えていいでしょう。日常宇宙Uは小規模な宇宙で、外側に広がる大宇宙Vのなかでは普通の集合に過ぎないのです。

さて、日常宇宙Uのなかで、アトムの双対概念を考えます。aがアトムであることは次のように書けます。

  • 論理式: ¬∃b∈U.b∈a
  • 自然言語: aの要素となるbが、Uのなかには存在しない。

上の命題のaとbの役割を入れ替えます。

  • 論理式: ¬∃a∈U.b∈a
  • 自然言語: bを要素とするaが、Uのなかには存在しない。

この条件をbが満たすとき、bを銀河(galaxy)と呼びましょう。銀河はローカルな用語です。もちろん、宇宙から連想して選んだ言葉です。アトムの子(アトムに含まれる要素)は存在しないし、銀河の親(銀河を含む集合)は存在しないのです。bが銀河であっても、b∈U ですが、この意味で使う'∈'は要素と集合の所属関係ではなくて、「bは宇宙U内のモノです」を略記しただけです。

通常、ZFC集合論でも素朴集合論でも、銀河の存在を認めてません。次の命題のほうを認めているのです。

  • 論理式: ∀b∈U.∃a∈U.b∈a
  • 自然言語: U内の任意のbに対して、bを要素とするaが、Uのなかには存在する。

外側に広がる大宇宙Vに関しては、上記命題(のUをVに置き換えたもの)が必須でしょうが、日常宇宙Uでは銀河を認めてもいいと思います。銀河を認めると、単元集合の構成 a|→{a} や、ベキ集合の構成 a|→Pow(a) が自由に出来ないことになります。不便ちゃ不便ですが、強烈過ぎる集合論的構成を制限したいこともあります。銀河は、そのような制限に使えます。

宇宙Uは銀河を持ち、U内のすべてのモノ(アトムでも集合でも)が、いずれかの銀河内に在るとします。これは、a0∈a1∈... という系列が無限に続くことはなくて、銀河で終端することを意味します。この性質を、∈-系列の有界と呼び、すべての∈-系列が有界な宇宙を有界宇宙(bounded universe)と呼びましょう。

有界素朴集合論

有界宇宙Uを持つような素朴集合論有界素朴集合論(bounded naive set theory)と呼ぶことにします。アトムも銀河も許します。そのため、ZFC集合論では認められない(否定が証明できる)次の命題が成立します。

  • 論理式: ∃a.¬(a=¥emptyset)∧∀b.¬(b∈a)
  • 自然言語空集合¥emptysetではないアトムが存在する。
  • 論理式: ∃b.(¬∃a∈U.b∈a)
  • 自然言語: 銀河が存在する。

有界素朴集合論に対する宇宙Uは、ZFC集合論の宇宙(非有界素朴集合論の宇宙でもある)Vのなかの集合なので、普通の集合概念/集合操作で作れます。

例えば、N = {0, 1, ...} として、次の宇宙Uを考えます。

  • U = N∪Pow(N)∪{Pow(N)}

自然数がUのアトム*1Nの部分集合がUの集合、Pow(N)がUの銀河になります。この宇宙はアトムを可算個、銀河を1個持ちます。

  • AtomU = N∪{¥emptyset}
  • SetU = Pow(N)∪{Pow(N)}

宇宙Uのなかで、親の集合を持つモノを要素(element)と呼び、要素の全体をElmU、銀河の全体はGalUとすれば:

  • ElmU = N∪Pow(N)
  • GalU = {Pow(N)}

いま定義した AtomU, SetU, ElmU, GalU は、単一の大宇宙だけを考えているときは意味ありませんが、様々な小宇宙を考えるときは、宇宙の性質として意味を持ちます。

ZFC宇宙Vに関して言えば:

  • AtomV = {¥emptyset}
  • SetV = V
  • ElmV = V
  • GalU = {}

有界素朴集合論の使い途

リレーショナルモデルでは、ドメイン(RDB用語のドメイン)の要素はアトムであり、タプル(RDB用語のタプル)を要素とする有限集合だけが集合(リレーション)であり、それより高階の集合は考えない、という態度を取ります。こういう態度が良いか悪いかはともかくとして、この態度に対応する集合論と述語論理が必要でしょう。それが有界宇宙に関する有界素朴集合論です。

僕の意見としては、上記のごとき制限を付け過ぎるのは良くないと思ってますが、「何がどう良くない」かを説明しようとすると、制限付き(=有界集合論という概念を導入せざるを得ません。定義もしてないナニカに対しては、「それは良くない」とさえ言えないじゃないですか。

リレーショナルモデルとは別な話で、型理論において、型の全体の型Typeを導入して、Type : Type という循環を作ることがあります。または、Type1 : Type2 : Type3 ... のような人為的な無限チェーンを想定したりします。このような細工も、銀河を認めない態度からだと思われます。

ある一定の階数以上の高階なモノが不要なら、階層を打ち切って銀河(=最上階)にしてしまえばいいと思います。自己言及が必要なら、レイフィケーション機構を導入して、Type : Type を合理化すればいいでしょう。

*1Nの空部分集合も定義上はアトムですが、空集合はアトムから除外してもいいでしょう。気にする程の問題ではないです。

2017-10-23 (月)

にゃんごすたーがお気の毒

| 16:14 | にゃんごすたーがお気の毒を含むブックマーク

『キングオブコント 2017』準優勝の「にゃんこスター」のWikipedia項目を見ると、最初の行に、

ゆるキャラの「にゃんごすたー」とは異なります。

と注意書きがあります。

にゃんごすたーは、青森県黒石市のゆるキャラで、林檎ネコらしい。ドラムが異常に得意で、林檎の赤からか『紅』の演奏が多いようです。

D

キャラクターを比べてみると:

*1*2

全然違うので、にゃんこスターはにゃんごすたーを知らずに命名したんじゃないのかな。それにしても、「にゃんごすたー、パクられて持って行かれた感」があってかわいそう。

[追記]いやむしろ、「ほとんど同名」ネタで話題にされる機会が増えたからラッキー、という発想もありますね。[/追記]

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

2017-10-18 (水)

巨大ロボットバトルの興行は成立するか?

| 16:53 | 巨大ロボットバトルの興行は成立するか?を含むブックマーク

水道橋重工 vs MegaBots の巨大ロボットバトル:

D

  • 第1戦は Iron Glory (MK2) vs Kuratas : Kuratasがパンチ一撃でIron Gloryを横倒しにして勝利
  • 第2戦は Eagle Prime(MK3) vs Kuratas : Eagle PrimeがチェーンソーでKuratasを切り裂きにかかり ……

巨大ロボットは、多くのマンガ・アニメ・映画に描かれた題材ですが、僕が思い出したのは、『リアル・スチール』。リアル・スチールの世界では、ロボット格闘技がスポーツ・エンタテインメントとしてビジネスになっています。

水道橋重工 vs MegaBots のバトルは、観客無しで行われて、撮影された動画が公開されているだけです。安全面などを考慮してのことでしょう。観客とパイロットの安全が担保されて、ルールが整備されれば、興行として成立するのかな?

一試合を行う準備にけっこうな資金と労力がかかりそうだし、試合でロボットが壊されること考えると、ちょっとペイしない気もしますね。戦闘用ロボットを量産して、一定の範囲内のカスタマイズとパイロットの腕前を競う、ならコストを抑えられか。あるいは、ロボット企業が自社製品の技術をアピールする場として、広告のために参戦するとか。

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

2017-10-16 (月)

証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則

| 14:19 | 証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則を含むブックマーク

このシリーズのひとつ前の記事「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論法則として使う」において、証明可能性判断と推論規則を同義語のように使ったのですが、これはミスリーディングかも、と思うので補足します。

内容:

  1. メタな立場と証明可能性判断
  2. 推論規則と証明可能性判断
  3. 仮定の命題を推論規則に変換して使う

メタな立場と証明可能性判断

証明を実行する主体であるあなた、あなたが行う証明行為、そのときのあなたの頭の中などを外から観察している超越的存在がいるとします。手っ取り早いのは、超越的存在として神様を想定することです(「論理を身に付けるには」参照)。

上記のような、証明行為を外から眺める超越者は、メタなヤツと言えます。メタなヤツによる観察や主張はメタな立場からなされます。そういうメタな立場からの発言として証明可能性判断(provability judgement)があります。

  • P1, ..., Pn |- Q

メタな立場から、行為主体(コイツと呼ぶ)の証明行為を眺めて、「コイツは確かに、P1, ..., Pn からQを証明しているぞ」と発言している、あるいは保証しているのが証明可能性判断です。

我々人間は、証明可能性判断を発言できるメタな立場に立つことができるでしょうか。ある状況では、ハッキリとメタな立場に立てます。あなたが、証明を実行するソフトウェアの実装者であり利用者でもあるとします。あなたは、証明を実行するソフトウェアの挙動を外から観察できるし、その動作のメカニズムも理解しているでしょう。そして次のような発言ができます。

  • 「このソフトウェアは確かに、P1, ..., Pn からQを証明しているぞ」

生きている人間であれ、ソフトウェアであれ、抽象的・概念的な仕掛けであれ、証明を行うようなシステムは演繹系(deductive system; 証明系、論理系、推論系)と呼びます。証明可能性判断は、演繹系を外から眺めて記述するときの命題(メタな立場の命題なのでメタ命題)です。

演繹系の性質は、結局はメタ命題=証明可能性判断により記述されるので、もとの演繹系の研究が、証明可能性判断の体系の研究に移ってしまうことになります。対象物である演繹系と、外側にある証明可能性判断の体系を一緒に扱うべきだ、といった話になります。

今言ったことは、数理論理学や形式的体系の方法論というだけではなくて、普通の非形式的(半形式的)証明の場合にも適用されるのです。我々は、ほとんど無意識にメタな立場を使っています。証明ソフトウェアに対してメタな立場に立つだけでなくて、自分自身に対してもメタな立場に立つことがあるのです。このシリーズで話題にしている“証明のお膳立て”も、メタな立場からの発想だと言っていいでしょう。「自分自身に対してもメタな立場に立つ」現象の不思議さに付いては次の記事で述べています。

推論規則と証明可能性判断

「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」では、推論規則と証明可能性判断を同じ形で書きました。同じ形で書いて差し支えないですが、厳密には、推論規則と証明可能性判断は別物です。

推論規則とは、その名のとおり、どのような推論が可能かを書き下したものです。例えば、命題Pが証明済み、命題Qも証明済みのとき、連言命題P∧Qを導いてかまいません。これは次のように書けます。

     証明済みの命題  P    Q
 -----------------------------[推論のステップ]
 推論で導出された命題 P∧Q

縦の図式を横1行で書けば、

  • P, Q |- P∧Q

これは証明可能性判断と同じです。

推論規則と証明可能性判断が違う点は、推論規則が演繹系の内部にあり、証明可能性判断は演繹系の外にあることです。

今我々はメタな立場ではなくて、地面を這いつくばってひたすら証明作業に従事しているとします。そのときでも、推論規則は見えています。見えてないと作業ができないので、推論規則は地面にあるのです。それに対して、我々を上空から(文字通り上から目線で)観察している超越者の発言(つぶやきやナイショ話かも知れない)を、地上の我々は知ることができません。

仮定の命題を推論規則に変換して使う

論理学では通常、証明の最中に演繹系を変化させることはしません。しかし、我々が実際に行う証明行為(リーズニング)では、必要なら推論規則を足していくことは普通です。そのことを「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」で述べたかったのです。

混同と混乱を避けるために、推論規則を横書きにしたものは、次の形で書くことにします。

  • Γ/ Δ |-! P

ビックリマークを付けています。'|-?'と'|-!'だとバランスがいいかな、と思って。

推論規則はビックリマーク付きで書く、という約束で「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で述べたお膳立てを書き直しましょう。

  Γ/ ∀x∈X.(P(x)⇒Q(x)), Δ |-? R
 ---------------------------------------------[前提を推論規則に]
  Γ/ Δ |-? R     Γ/ (x : X), P(x) |-! Q(x)

右下の Γ/ (x : X), P(x) |-! Q(x) は推論規則なので、次のように解釈します。

  • Γは文脈(予備知識、背景知識)。
  • (x : X) と P(x) は既に証明済みで、得られている。
  • この状況で、推論の1ステップの結果として、Q(x)を結論してよい。Q(x)は証明済みとなる。

これは超越者が上空(メタな立場)で言っていることではなくて、地上の作業者が利用してよい手順です。

証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で出した具体例を再掲すると; 証明要求は次です。

  • Γ/ ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T), (x : X), x∈S, ¬(x∈W) |-? x∈T

前提に、命題 ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) が含まれます。これを推論規則に直すと:

  • Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T

したがって、もとの証明要求は、新しい証明要求と新しい推論規則に分解されます。

  1. 新しい証明要求 : もとの証明要求の前提から ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を除いた*1証明要求
  2. 新しい推論規則 : ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を推論規則に直したもの

具体的には、

  1. Γ/ (x : X), x∈S, ¬(x∈W) |-? x∈T
  2. Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T

要求のほうが「… を(可能なら)証明せよ」であるのに対して、推論規則が「… は1ステップ推論で証明済みとしてよい」と保証しているので、実質的な作業は何もしなくても、「証明できました」と納品(「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル』参照)できます。

*1:前提の命題を取り除かなくても問題は起きないのですが、同じ知識が二重にエンコードされる冗長性を排除するために取り除いています。

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