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

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

2018-10-19 (金)

クリーネ代数: 不等式的定義と等式的定義

| 12:04 | クリーネ代数: 不等式的定義と等式的定義を含むブックマーク

クリーネ代数 再論」で、クリーネ代数の定義を(いまさらに)述べたのですが、不等式と等式に関してちょっと微妙なところがあります。

最小な前不動点は不動点になる

クリーネ代数もコンウェイ半環も、最小不動点を扱う代数系だと言えます。最小不動点と最小前不動点に関して次のように書きました。

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じなので、次の2つの条件を満たすtは最小不動点となります。

「同じ」という言い方は誤解をまねくかな、と思って次のように修正しました。

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同様に扱えるので、次の2つの条件を満たすtは最小不動点とみなせます。

しかし、修正後もまた別な誤解がされそう。文言の削除挿入ではうまく説明できそうにない。ので、この記事で説明します。

Kを順序半環、a∈K とします。集合 PreFix(a) を次のように定義します。

  • PreFix(a) := {x∈K | ax + 1 ≦ x }

PreFix(a)は、アフィン線形写像 f(x) = ax + 1 の前不動点〈pre-fixed point〉の集合です。PreFix(a)は空でないと仮定して、t∈PreFix(a) に関する次の条件を考えます。

  • x∈PreFix(a) ならば t ≦ x

この条件は、前不動点tが、他のfの前不動点より小さいことを意味します。このようなt(最小前不動点)があれば、それはfの不動点になります。

まず、f(t)がfの前不動点になることを見ます。f(t) ≦ t は成立しているので、両辺にfを適用して f(f(t)) ≦ f(t) 、これは「f(t)がfの前不動点」であることです。tに関する条件 ∀x∈K.(f(x) ≦ x ⇒ t ≦ x) から、

  • t ≦ f(t)

最初から

  • f(t) ≦ t

は成立しているので、上記ニ条件から

  • f(t) = t

よって、fの最小前不動点があれば、それはfの最小不動点です。

不等式と等式

クリーネ代数では、最小不動点の存在を最小前不動点の存在として定式化しています。クリーネスターa*は最小不動点を与えるので、

  • aa* + 1 = a*

を公理に入れるのは別に問題はない(冗長になるだけ)ですが、実際に使いたいのは、

  • ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

という不等式条件のほうです。この不等式条件を使った証明法は不動点帰納法と呼ばれたりします。クリーネ代数の公理は、不等式による推論が出来るように選ばれているのです。

一方で、コンウェイ半環のスターも不動点を与えます。次の積スター等式で、b = 1 とすると、a*の不動点等式です。

  • (ab)* = 1 + a(ba)*b

大雑把に言えば、クリーネ流はアフィン不動点の不等式的な性質に注目し、コンウェイ流は等式的な性質に注目しています。この流儀の違いはどうも後々まで影響しそうで、「不等式でも等式でも同じ」とは言いにくいのです。

トレース付きデカルト圏のような不動点理論の圏論的な定式化は、等式的なので、クリーネ代数よりコンウェイ半環の圏化(亜化)と言えそうです。クリーネ代数の圏化では、順序/不等式を、どのように表現するかが鍵となるでしょう。

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

2018-10-18 (木)

微分幾何の特殊な習慣をもう少し詮索

| 15:21 | 微分幾何の特殊な習慣をもう少し詮索を含むブックマーク

微分幾何の特殊な習慣 -- 知らんかった」で、「dsはdとsに分解しない。単なる習慣的記法。s単独で意味などない」と書いたのですが、書いた後で「ちょっと言い過ぎかな」と思いました。で、追記しときました。

長い期間、広く使われている記法には、なにかしらの意味はあるものです。“意味”が心理的なもの(メンタルモデル)かも知れませんが、適切な解釈のもとでの整合性は期待できるでしょう。

内容:

  1. dxはdとxに分けて考える
  2. 微小量にはdを付けるという習慣
  3. 長さの微小量はどう書くか?
  4. sは弧長パラメータ
  5. まとめ

dxはdとxに分けて考える

記事「微分幾何の特殊な習慣 -- 知らんかった」で、dsは、'd'と's'の二文字まとめて単一の記号で、分解したら無意味だと言いました。しかし、dfとかdxとかは、そもそも分解したら無意味だと思っている方もいるでしょう。そうじゃないです。“普通は”分解しても解釈できます。何が“普通”かの議論は大いにあるでしょうが。

外微分計算〈exterior calculus〉では、dfと書いたら、dとfに分解できます。fが関数で、dは微分(外微分作用素)です。dが作用素で、fが被作用項〈オペランド〉であることを強調して d(f) と書くとして、例えば2次元での話なら:

 d(f) ¥:=¥: ¥frac{¥partial f}{¥partial x}dx ¥;+¥; ¥frac{¥partial f}{¥partial y}dy

ここで出てきたdx, dyも、それぞれ関数xと関数yの微分です。xはどんな関数かというと、(a, b) |→ a という第一射影を取る関数です。yは第二射影ですね。dxとdyが、“1次微分形式=余接ベクトル場”の(加群としての)基底になります。

df/dx = g(x) という簡単な微分方程式は、df = g(x)dx と書いても同じです。より一般に、df, dx などが出現している等式は、なんらかの微分方程式だと解釈できます。

微小量にはdを付けるという習慣

気分を変えて、長さではなくて体積を話題にしましょう。体積をラテン文字・大文字'V'で表すことにします。文字'V'は体積を表すために固定(あるいは予約)するとしましょう。このとき、dVに意味を持たせることはできます。ただし、「関数Vを外微分したものがdV」という解釈はできません。

Vを関数と考えるなら、その域〈domain〉は何でしょうか? 「微分幾何の特殊な習慣 -- 知らんかった」で例に使ったような開集合 U⊆Rn を選んで、V:U→R と考えていいでしょうか? ちょっと無理がありますよね。

Vの引数になり得るのは、なにか“体積を持つ図形”でしょうから、

  • V:(“体積を持つ図形”の集合)→R

でしょう。図形をR3の部分集合だと考えれば、

  • (“体積を持つ図形”の集合)⊆Pow(R3)

ここで、Pow(R3)はR3のベキ集合 -- R3のすべての部分集合からなる集合です。

(“体積を持つ図形”の集合)を定義するのは難しいですが、うまく定義できたとすると、Vは(“体積を持つ図形”の集合)の上の測度になります。測度は積分として表示するのが自然でしょうから:

 V(A) = ¥int_{A} dV

ここで出現した被積分項dVは、「微小な体積」という解釈を持ちます。「R3に内在する(最初から在る)微小な体積を、図形Aの上で寄せ集めたら、Aの体積になる」と読めます。

この被積分項dVを、dとVに分解して「Vにdしたもの」と解釈するのは無理ですが、「マクロ量Vの微小バージョンdV」というメンタルモデルとしての意味はあります。

長さの微小量はどう書くか?

体積と同じことを長さに関して議論してみます。ラテン文字・大文字'V'はvolumeの'v'から取ったので、長さはlengthの'l'からラテン文字・大文字'L'を採用しましょう。

Lの引数になるのは、なにか“長さを持つ図形”でしょうから、

  • L:(“長さを持つ図形”の集合)→R

先ほどと同様に図形をR3の部分集合だと考えれば、

  • (“長さを持つ図形”の集合)⊆Pow(R3)

A∈(“長さを持つ図形”の集合) に対して、

 L(A) = ¥int_{A} dL

話のスジは、体積でも長さでも同じです。が、しかし、“長さを持つ図形”をR3の部分集合として測度論的に扱うのは面倒で計算もやりにくいですね。扱い方を変えましょう。

部分集合Aではなくて、関数 f:I→R3 を考えます。ここで、Iは実数の区間で、fはなめらか(いくらでも微分可能)とします。fの域である区間Iは、2つの実数a, bにより I = [a, b] と書けますが、位置をズラせば、I = [0, a] とできるので、区間の左端は常に0に取ると約束します。また、fの微分係数〈速度ベクトル〉はゼロベクトルにはならないことも仮定します。

以上の設定で、L(f) はどう表現できるでしょうか。

 L(f) = ¥int^{a}_{u = 0} |f’(u)|du

ここで、f'は関数fの微分係数〈導関数 | 速度ベクトル〉で、|-| はベクトルの長さ〈ノルム〉です。fを (f1, f2, f3) と成分表示するなら:

 L(f) = ¥int^{a}_{u = 0} ¥(¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

前節同様に、「マクロ量Lの微小バージョンdL」というメンタルモデルに従うと、

 L(f) = ¥int^{a}_{u = 0} dL

被積分項どうしを比較して、

 dL = ¥( ¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

fの存在を暗黙に前提するなら、LとdLの関係はとても自然なものだと思います。体積と長さだけでなくて、この記法は一般的に使用していいでしょう。次のようにルール化できます。

  • なんらかのマクロな量Xがあるとする。
  • その量Xは、Aなどを測って得られるとする。
  • 量Xの微小バージョンをdXと書く。
  • マクロ量 X(A) は、微小量 dX をAに関して積分して得られる。

sは弧長パラメータ

さて、最初に取り上げた微分幾何の's'に話を戻しましょう。長さを'L'とするか's'とするかは別にどうでもいいので、伝統に則り's'にしましょう。

 s(f) = ¥int^{a}_{u = 0} ¥(¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

 s(f) = ¥int^{a}_{u = 0} ds

 ds = ¥( ¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

自然な記法であり、なんら問題ありません。

しかし、文字's'の出自は別なところにあります。弧長パラメータです。弧長パラメータは、“長さを持つ図形”の表示を正規化〈一意化〉する手段として使われます。異なる出自と異なる経緯でも、同じ記法に到達するのですが、「異なる経緯」を追ってみます。

なめらかな関数 f:I→R3 で“長さを持つ図形”を表そうとすると、かなりの任意性・恣意性・自由度があります。任意性を潰すために同値関係を入れましょう。

f:I→R3 と g:J→R3 が同値だとは、次のことだとします。

  • 区間のあいだの関数 h:I→J があり、hはなめらかで微分係数はいたるところ非ゼロな可逆関数とする。そんなhを使って、f = g¥circh と書けるとき、fとgは同値。

個々の関数ではなくて、同値類を使えばパラメータ付けの任意性は消えますが、同値類よりは、代表元である関数を選んで、それを使ったほうが分かりやすいです。

f:I→R3 に次の条件を課します。

  • 微分係数〈速度ベクトル〉f'の長さはいたるところで1。

この条件を満たすfは、先の同値類の代表元になります。この条件を満たすfに関しては:

 s(f) ¥:=¥: ¥int^{a}_{u = 0}|f’(u)|du ¥:=¥: a

長さs(f)が区間の右端aで与えられます。この等式左辺のsはマクロ量としての長さです。

「微分係数f'の長さはいたるところで1」であるfに関しては、実数区間を走るパラメータに's'を使うと約束します。この約束から、今までuと書いてきたところがsに変わるので:

 s(f) ¥:=¥: ¥int^{a}_{s = 0}|f’(s)|ds ¥:=¥: a

fに課した条件から |f'(s)| = 1 なので、

 s(f) ¥:=¥: ¥int^{a}_{s = 0} ds ¥:=¥: a

[追記]

すぐ上の等式  s(f) ¥:=¥: ¥int^{a}_{s = 0} ds ¥:=¥: a は、だまされた/バカにされたような気がするかも知れません。右辺側で暗黙に前提しているfを明示的に書いて、

 s(f) = ¥int_{f} ds

ならどうでしょう。fのマクロ量s(f)を測ることは、dsという微小量をfに関して積分して求めるのです。となると、積分操作は、f達がいる空間とds達がいる空間のあいだで行うことになります。これは、微分形式やチェーンの代数を出さないと、うまく表現ができない気がします。

[/追記]

まとめ

  • dX という書き方に対して、「dが外微分作用素、Xが被作用項」という解釈がある。
  • dX という書き方に対して、「Xがマクロな量、dXがその微小バージョン」という解釈がある。
  • 上記ニ種類の解釈がたまたま一致することもあるが、一般的には異なった解釈となる。
  • よって、解釈の選択肢を間違えると、意味不明になるかも知れない。
  • 実際に解釈の選択肢を間違えて混乱するヤツがいる(それは私だ)。
トラックバック - http://d.hatena.ne.jp/m-hiyama/20181018

2018-10-17 (水)

微分幾何の特殊な習慣 -- 知らんかった

| 09:42 | 微分幾何の特殊な習慣 -- 知らんかったを含むブックマーク

「郷に入っては郷に従え」という諺がありますが、従うべき郷の習慣を知らないと、何がなんだかサッパリ分からなかったり、とんでもない誤解をしたりします。

内容:

  1. 微分幾何の習慣は知らない
  2. 特別な意味の文字
  3. dsって何だろう
  4. 接ベクトル場、余接ベクトル場
  5. 内積場、ノルム場
  6. 内積場/ノルム場の表示
  7. ノルム場がdsだった
  8. 習慣の由来は

微分幾何の習慣は知らない

添字をたくさん使うテンソル計算と、そんなテンソル計算を使う微分幾何は、早い段階で「やってられん!」と投げ出しました。そこらへんの事情は昔書いたことがあります。

後になって、ネルソンの本で少し勉強しました。

ネルソンの本はモダンですが、ネルソンが考案した記法で書かれていて、伝統的な微分幾何とはだいぶ違います*1

そんな事情で、伝統的な微分幾何では常識であっても、僕はまったく知らないことが多々あります。

特別な意味の文字

特定の文字が、固有名詞として特定の対象物を指すことは珍しくありません。ギリシャ文字・小文字'π'は円周率を表します。ラテン文字・小文字'e'はネイピア数ですね。もちろん、この約束が破られることもあります。正確に言えば、特定の分野や文脈において、特定の文字が、固有名詞として特定の対象物を指すことがある、です。

微分幾何にけるラテン文字・小文字's'、物理の相対論におけるギリシャ文字・小文字'τ'が、そのような特別な意味を持つ文字だったようです(知らなかった)。s, τは、「特定の対象物を指す」というより、「特別な使い方の習慣がある」ということです。ほんとに特別なんです。なかなか推測は出来ないので、知ってないとアウトだと思います。

以下では、ラテン文字・小文字's'の特別な使い方の習慣を話題にします。実は、's'については「そう言えば、そんな習慣あったな」くらいの記憶はあるのですが、'τ'についての習慣はまったく知らなかったので、ホントに何がなんだかサッパリ分からなかったです*2

dsって何だろう

多様体を持ち出すと面倒なので、関数やベクトル場を考える領域は、Rnの開部分集合Uに限定します。なんなら、n = 2 とか n = 3 に次元を固定してもいいです。

's'について特に何も知らないとして、ds と書かれていたら、どう解釈するでしょう? 僕は、dは微分(外微分)と思うので、sは関数 s:U→R で、それを微分してdsなんだ、と解釈します。dsは、U上の1次微分形式(の場)ですね。

ds2 ならどうでしょう? d(s2) とは考えにくいので、(ds)(ds) と解釈します。dsの併置(並べること)は、なんらかの掛け算でしょう。1次微分形式には自然な掛け算があります。αとβが1次微分形式だとして、

  • (αβ)(v) = α(v)β(v) (右辺の併置は実数値関数の普通の掛け算)

ここで、vはU上の接ベクトル場です。Uの一点pで考えるならば、

  • (αβ)p(vp) = αp(vpp(vp) (左辺の併置は実数の普通の掛け算)

ds2 とは、たぶんそんなもんだろう、と思いますよね。実際はまったく違うんですわ。

接ベクトル場、余接ベクトル場

Uの一点pでの接ベクトルの全体を TpU と書きます。U⊆Rn なので、TpU ¥stackrel{¥sim}{=} Rn です。点pごとに、TpU の要素(つまり接ベクトル)を割り当てる写像が接ベクトル場です。接ベクトル場vは、v:U→Rn と考えてかまいません(あくまで U⊆Rn, TpU ¥stackrel{¥sim}{=} Rn だからです)。点pでのvの値は、v(p)ではなくてvpと書くことにします(後で理由は分かるでしょう)。

TpU の標準双対空間を T*pU と書きます。

  • T*pU := (TpU)*

T*pU の要素を、点pにおける余接ベクトルといいます。点pごとに、T*pU の要素(つまり余接ベクトル)を割り当てる写像は余接ベクトル場です。余接ベクトル場αは、α:U→(Rn)* と考えてかまいません。しかし、(Rn)*Rnを同一視することはしません。点pでのαの値は、α(p)ではなくてαpと書くことにします。余接ベクトル場の一点での値αpは、TpU→R という線形写像です。

余接ベクトル場と1次微分形式はまったく同じ概念です。ここから先は、「余接ベクトル場」のほうを使います。

α:U→(Rn)* が余接ベクトル場、v:U→Rn が接ベクトル場のとき、

  • U∋p |→ αp(vp) ∈R

は、U上の実数値関数、つまりスカラー場になります。点引数pを下付きにしたのは、α(p)(v(p)) だとちょっと分かりにくいからです。

内積場、ノルム場

Uの点pごとに、接ベクトル空間TpUに内積が入っているとします。点pにおける内積を (-|-)p と書きます。ハイフン'-'は無名変数です。(-|-)p:TpU×TpU→R で、(-|-)p は内積の公理を満たす双線形写像です。

  • U∋p |→ [内積 (-|-)p:TpU×TpU→R]

これは、点pごとに内積を割り当てているので、内積場という言い方をしてもいいでしょう。普通は、内積場とは言わないで計量場ですけど。

v, w:U→Rn が2つの接ベクトル場のとき、

  • U∋p |→ (vp|wp)pR

はスカラー場です。内積場があれば、2つの接ベクトル場を内積してスカラー場を得ることができます。例えば、(vp|wp)p がpによらず恒等的に0なら、「vとwは直交する接ベクトル場だ」とか言えます。

接ベクトル場 v:U→Rn に対して、

  • U∋p |→ sqrt((vp|vp)p) ∈R

と定義すると、これは、各点pでの接ベクトルの長さを与えることになります。長さはノルムとも言うので、p |→ sqrt((vp|vp)p) という割り当てをノルム場と呼びましょう。点pでのノルムは |-|p と書きます。この記法を使ってノルム場を次のようにも書けます。

  • U∋p |→ [ノルム |-|p:TpU→R]

接ベクトル場 v:U→Rn に対するノルム |v| は、次のようなスカラー場(U上の実数値関数)になります。

  • U∋p |→ |vp|pR

内積場/ノルム場の表示

v:U→Rn をU上の接ベクトル場とします。成分表示して、

  • v = (v1, ..., vn)

とします。横ベクトル形式で書いてますが、実際は縦ベクトル形式なんだと思ってください。vの転置 vT が横ベクトル形式です。点pごとの値は、

  • vp = (vp 1, ..., vp n)

vp i と書くか、vi p と書くか悩みますが(どっちでもいい)、この形式にします。

U上の内積場 p |→ (-|-)p を具体的に定義するとき、点pごとにn×n行列を与えればいいですね。Gがそのような行列の場だとします。

  • G:U→Mat(n, n)

ここで、Mat(n, n)はn×n行列の空間です。この行列場Gを使って、

  • (vp|wp)p := (vpT)Gpwp

と内積の値を定義できます。n = 2 の場合をもっと具体的に書けば:

(¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix} | ¥begin{pmatrix}w_{p¥, 1} ¥¥ w_{p¥, 2}¥end{pmatrix})_p ¥: :=¥: ¥begin{pmatrix}v_{p¥, 1} & v_{p¥, 2}¥end{pmatrix}¥begin{pmatrix}G_{p¥, 1 1} & G_{p¥, 1 2} ¥¥G_{p¥, 2 1} & G_{p¥, 2 2} ¥¥¥end{pmatrix}¥begin{pmatrix}w_{p¥, 1} ¥¥ w_{p¥, 2}¥end{pmatrix}

対応するノルム場は、

  • |vp|p := sqrt((vpT)Gpvp)

n = 2 の場合のノルム場は、

¥|¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix}¥|_p ¥: :=¥: ¥sqrt{¥begin{pmatrix}v_{p¥, 1} & v_{p¥, 2}¥end{pmatrix}¥begin{pmatrix}G_{p¥, 1 1} & G_{p¥, 1 2} ¥¥G_{p¥, 2 1} & G_{p¥, 2 2} ¥¥¥end{pmatrix}¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix}}

上記のルート内を展開して書いてみます。ここから先では、下付きpが煩雑なので省略します。点pごとではなくて、U全体に対して記述していると思ってください。

¥|¥begin{pmatrix}v_{1} ¥¥ v_{2}¥end{pmatrix}¥| ¥: :=¥: ¥sqrt{G_{1 1}v_1 v_1 + G_{1 2}v_1 v_2 +  G_{2 1}v_2 v_1 +  G_{2 2}v_2 v_2}

あるいは両辺を二乗して:

¥|¥begin{pmatrix}v_{1} ¥¥ v_{2}¥end{pmatrix}¥|^2 ¥: :=¥: G_{1 1}v_1 v_1 + G_{1 2}v_1 v_2 +  G_{2 1}v_2 v_1 +  G_{2 2}v_2 v_2

一般的な次元nでは:

| v |^2 ¥: :=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

ここで、vは接ベクトル場、Gは行列場ですが、添字が付いた Gji, vj, vi 達はスカラー場です。

ノルム場がdsだった

前節のノルム場をNという1文字で表すことにします。

N(v) ¥: :=¥: sqrt{¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i}

ノルム場Nの二乗はN2とします。

N^2(v) ¥: :=¥: N(v)^2 ¥;=¥; ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

内積場やノルム場を、dxi を使って書く場合もあります(それが普通)。

N^2 ¥::=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i

これは、完全に合理的な記法です。なぜなら、dxiは余接ベクトル場で、ベクトル場vに対して dxi(v) = vi と成分を取り出す働きがあるからです*3

N^2(v) ¥:=¥: (¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i)(v) ¥:=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j(v) dx_i(v) ¥:=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

辻褄が合ってますね。

辻褄が合わなくなるのはここからです。ノルム場Nを、dsと書く習慣があるのです。ノルム場の二乗N2ならds2です。

ds ¥::=¥: ¥sqrt{¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i}

ds^2 ¥::=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i

dsをdとsに分解してはダメです。s自体に意味があるわけではなくて、'ds'を単一の記号とみなして、それはノルム場を表すために予約されていると解釈します。sは関数ではなく、dsは余接ベクトル場〈1次微分形式〉ではありません。ノルム場(またはその二乗)の定義式を見て、「sは何だろう?」「sはどこから来たのだろう?」「sの正体は?」とか考えるのはまったくのナンセンスです。だって、単なる習慣的記法だもの。

それ相応の文脈があれば誤解はないでしょうが、ノルム場の具体的な定義として、 ds = (なんか具体的な式) という等式がポンと出されると、「sを微分したのが (なんか具体的な式) なのね」てなことになります。で、ワケワカメ状態。

習慣の由来は

ノルム場をdsと書くようになった由来は、割と容易に想像がつきます。弧長パラメータという概念があり、その弧長パラメータをsと書く習慣があります。無限小な弧長だから「d(無限小) + s(弧長)」となったのでしょう。

「sという関数にdという作用素を適用した」のではなくて、「無限小弧長」を表す符丁だったんですね。ほぼ固有名詞みたいなもんです。

この特殊な用法でのdsを、「線素」とも呼ぶようです。「線素」という言葉は聞いたことがありますが、「線」が1次元のモノを意味し、「素」が無限小で、「線素=接ベクトル」だろうと僕は解釈していました。「線素=接ベクトルの長さ=無限小弧長」という意味もあるんですね。

理解を妨げたり、誤解を招く言葉や記法というのは、いたるところにあって落とし穴になるのですが、僕も落とし穴にマンマと落とされました。

  • dsはdとsに分解しない。単なる習慣的記法。s単独で意味などない

[追記]これ(↑)は言い過ぎかな。'd'と's'に分解した上で、それぞれ単独での意味は、探せば在りますね、解釈法を変えれば。'd'を微分(外微分作用素)と解釈している限りは's'に意味を持たせられない、ということです。[/追記]

[さらに追記]この記事の修正はしませんが、言い過ぎに対する補正をするために続きの記事を書きました。

[/さらに追記]

*1:普通のテンソル代数とは少し違った、ネルソン代数とでも呼ぶべき代数を定義して、それをベースにしています。見た目は伝統的微分幾何と似せる工夫をしているのですが解釈は違います。ちょっとトリッキーな印象を受けました。

*2:結論を言えば、's'に関する習慣と'τ'に関する習慣は同じものです。

*3:それに、dxiは関数xiの微分であるという点でも整合的記法です。

2018-10-15 (月)

論理/メタ論理の記法をどうするか

| 16:05 | 論理/メタ論理の記法をどうするかを含むブックマーク

最近割と、論理/メタ論理の話をする機会があるのですが、そのとき、どんな書き方をすればいいか悩みます。

内容:

  1. キーワード方式とターンスタイル方式
  2. 正しさを分類する
  3. 書き方の変種や修飾
  4. 意味的帰結の書き方

キーワード方式とターンスタイル方式

正確な記述と演繹のための非日本語記法」で次のような書き方をしました。

For x∈R, y∈R.
For x ≧0, y ≧0.
  IsCorrect x + y ≧ 0

少し前までは、次のような書き方をしてました。これ(↓)は、誰か(誰だか忘れた)の真似をしたものです。

Given x∈R, y∈R.
Given x ≧0, y ≧0.
  Holds x + y ≧ 0

キーワードの差(ForとGiven、IsCorrectとHolds)以外何の違いもありません。IsCorrectとHoldsは、ターンスタイル記号'|-'と同じ意味です。論理/メタ論理における標準的記法はターンスタイル記号です。

ターンスタイル記号より、上に紹介した書き方がいい点は:

  1. 英単語由来のキーワードのほうが、見慣れない記号'|-'より幾分か親しみやすい。
  2. 文脈(前提)を、何行かに分けてグルーピングして書ける。

「幾分か親しみやすい」は気分的なもので、たいした理由ではないです。「何行かに分けて書ける」もターンスタイル記法でもやれば出来ます。文脈をグルーピングしたいなら、区切り記号(例えばスラッシュ)を導入すればいいでしょう。

x∈R, y∈R / x ≧0, y ≧0 |- x + y ≧ 0

どう書こうが同じだろ、ってのが僕の感想ですが、“気分的な差”とか“視覚的な(見た目の)差”とかが実にバカにできなくて、「どう書くべきか」の判断は難しくなります。

正しさを分類する

前節のキーワード 'IsCorrect', 'Holds' は、「正しい」「成立する」という意味です。それ以上の説明は要らないように思えますが、そうではありません。メタ論理(モデル論や証明論)のモットーは、正しさや成立することを厳密に分析することです。

少なくとも、'|-'(ターンスタイル記号)と'|='(ダブルターンスタイル記号)はシッカリと区別する必要があります。ターンスタイル記号は“構文的に正しい”、ダブルターンスタイル記号は“意味的に正しい”という主張(に使う記号)です。今日は、内容的説明をする気はなくて、記法の話ですから、“構文的に正しい”と“意味的に正しい”がどう違うかは説明しません。

'|-' と '|=' をキーワードにするなら何がいいのだろう? 'IsProvable'と'IsValid'かな。

  • IsProvable x + y ≧ 0
  • IsValid x + y ≧ 0

'|-' と '|=' は、形は似てますが、使い方がだいぶ違います。'|-'の左側には証明の前提を書きます。

  • x ≧0, y ≧0 |- x + y ≧ 0

キーワードで書くなら(ピリオド打つのはやめた)、

For x ≧0, y ≧0
IsProvable  x + y ≧ 0

あるいは、

Given x ≧0, y ≧0
IsProvable  x + y ≧ 0

なんかGivenのほうがいいような気がしてきた。まったくの気分だが。

'|='の左側には、右側の命題を成立させるモデルを書きます。モデルとは、命題を解釈するための構造です。例えば、自然数の変数・定数・演算・関係を使うモデルをN-model、実数の変数・定数・演算・関係を使うモデルをR-modelとしたとき:

  • N-model |= ∀x, y.(x + y ≧ 0)
  • R-model |=/ ∀x, y.(x + y ≧ 0)

'|=/'は「正しくない」の意味です。全称限量子を付けないで、自由変数が残っていると妥当性〈validity〉の判断はできません。

  • R-model |= x + y ≧ 0 (なんともいえない)

変数への具体的な値の割り当てを、変数の状態〈state〉、束縛〈binding〉、付値〈valuation〉などと呼びます。状態まで付ければ妥当性が判断できます。

  • (R-model, {x←1, y←1}) |= x + y ≧ 0
  • (R-model, {x←0, y←(-1)}) |=/ x + y ≧ 0

状態の記述に'←'を使ったのは臨時の記法です(特に正式な記法はないと思います)*1

書き方の変種や修飾

'|-'で示す証明可能性は、証明を行う仕掛けである演繹系〈deduction system | 証明系〉が決まらないと定義できません。演繹系をSとして、「Sにより証明可能」は '|-S' を使えばいいでしょう。

  • x ≧0, y ≧0 |-S x + y ≧ 0

キーワード方式だと:

Given x ≧0, y ≧0
IsProvableBy S  x + y ≧ 0

By S はお尻のほうがいいか。

Given x ≧0, y ≧0
IsProvable x + y ≧ 0 By S

キーワードを使うと、“気分”と“見た目”が気になりだす。やはり、自然言語には言霊が宿るせいか?

'|='では、基本的には左側にモデルを書くのですが、何も書かないときがあります。

  • |= ∀x, y.(x + y ≧ 0)

実は、左が空白のときの解釈が場合により違うんですよ。ヤダナー。

  1. モデルをひとつに固定しているので、あえてモデルは書かない。
  2. 複数のモデルを想定するが、左側空白は、どのモデルに対しても成立することを意味する。

モデルがひとつであってもチャンと書くことにして、複数のモデルのどれでも成立するならワイルドカードの'*'を付けるとかすれば混乱は少ないでしょう。

  • N-model |= ∀x, y.(x + y ≧ 0)
  • * |= ∀x, y.(x + y ≧ 0)

モデルの集まりをMとして、左側にはモデルの集まりを書く約束なら:

  • {N-model} |= ∀x, y.(x + y ≧ 0)
  • M |= ∀x, y.(x + y ≧ 0)

左側にモデルの集まりを書く習慣はたぶんないと思うけど、「何も書かないで省略する」はたいていトラブルを招くんだよなー。

意味的帰結の書き方

ダブルターンスタイル'|='の左側にはモデルを書くので、論理式を書くことはできません。しかし、意味的判断で左側に論理式を書きたいことがあります。標準的記号がないので、僕は'|⇒'を使っています。

  • x ≧0, y ≧0 |⇒ x + y ≧ 0

これは、次の意味です。

  • いま考えているどんなモデルMと状態ρに対しても、 (M, ρ) |= x ≧0 かつ (M, ρ) |= y ≧0 ならば、(M, ρ) |= x + y ≧ 0 である。

論理式 A1, ..., An, B のあいだの関係 A1, ..., An |⇒ B は、通常は論理的帰結〈logical consequence〉と呼びます。しかし、これは意味的判断なので、意味的帰結〈semantic consequence〉と呼んだほうが適切でしょう。意味的帰結を伴意〈entailment〉ともいいます。次の記事を参照してください。

意味的帰結〈伴意〉を'|⇒'で表すと、左側に論理式を書けるようになりますが、今度は判断の根拠であるモデルの集まりが書けなくなります。右下添字かな。

  • x ≧0, y ≧0 |⇒M x + y ≧ 0

Mは、モデル(と状態)の集まりで、この意味的帰結を主張するときの根拠となったものです。こう約束すると、次の2つの書き方は同じ意味になります。

  1. M |= x + y ≧ 0
  2. |⇒M x + y ≧ 0

'|-' と '|=' は似てませんが、'|-' と '|⇒' は似た使い方ができます。左側に前提となる命題の並び、右下添字に判断の根拠となる仕掛けや集まりを書くことになります。'|=' は、'|⇒' を定義するための補助的なものと捉えたほうがいいような気がします。


関係しそうな過去記事:

*1:「型推論に関わる論理の概念と用語 その6:substitutionの記法」で色々な記法があることを書きました。状態〈束縛 | 付値〉と置換〈substitution | 代入〉は似てますが違う概念です。

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

2018-10-11 (木)

simulate

| 12:41 | simulateを含むブックマーク

"simulate"を「シュミレート」と言ってしまう、ときに「シュミレート」と書いてしまう。知っていても言ってしまう/書いてしまう。ウーム。

なんでだろう? 「シミュ」が発音しにくいことが原因のひとつだと思う。「シミュ・レート」とちゃんと発音しようとすると、「ミュ」で口をとんがらかす必要があり、負担がかかる。「シュミ」は言いやすい -- 「趣味」という日本語と同じ。

ジジ臭い感じにはなるが「シミ・レート」を心がけることにしようかな。「シミュ・レート」よりは楽に発音できる。「趣味・レート」から「染み・レート」へ。

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

2018-10-10 (水)

クリーネ代数 再論

| 10:07 | クリーネ代数 再論を含むブックマーク

クリーネ代数の圏化: ちょびっと」で、クリーネ代数を幾つかの方法で圏化/無限タワー化したら面白いかもなー、と書きました。で、圏化のもとになるクリーネ代数ですが、何度も取り上げている割には定義はしたことないですね。定義は「探せばあるだろう」という前提ですが、圏化を見越した定義を改めてしておいたほうがいいかな、と思いました。

内容:

  1. 何に使えるのか/何に使いたいのか
  2. クリーネ代数とは何か
  3. 順序構造と最小不動点
  4. クリーネ代数の定義
  5. 可換性とベキ等性
  6. コンウェイ半環

何に使えるのか/何に使いたいのか

「クリーネ代数〈Kleene algebra〉とは何か」の前に、クリーネ代数は何に使えるのか? 僕が何に使いたいと思っていた/いるのかを説明します。僕が想定している用途は主に2つで、

  1. プログラム意味論
  2. 形式言語理論

です。今ここではプログラム意味論のほうだけ述べます。クリーネ代数は、非決定性プログラムの記述と分析に使えます。だいぶ古いですが、次の3つの記事を読むと事情はわかるでしょう。

非決定性プログラムの意味論をやりたい場合は、単なるクリーネ代数ではなくて、論理条件〈logical condition〉に相当するテストも入れたほうが便利です。これはテスト付きクリーネ代数〈Kleene algebra with tests〉です。テスト付きクリーネ代数については、次の記事で書いています。

テスト付きクリーネ代数を使えば、if文やwhile文も代数的に定義できます。ホーア論理〈Hoare logic〉を組み立てることもできます。以下の記事はホーア論理に関するものですが、テストフレームワークを実際に作っていたときに書いた記事なので、現実的な考慮が色々入っていて、理論的な筋は若干見えにくいかも知れません。

クリーネ代数とはちょっと離れますが、ホーア論理の圏論的扱いについては:

というわけで、クリーネ代数/テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を与えてくれます。これが、クリーネ代数/テスト付きクリーネ代数に興味を持つ(ひとつの、しかし大きな)動機です。

クリーネ代数とは何か

クリーネ代数を一言でいえば、アフィン線形不動点方程式を扱うための代数系です。となると、アフィン線形不動点方程式とは何か、から説明を始めるべきでしょう。

次は中学校で習った1次関数です。

  • f(x) = ax + b

aを比例定数〈proportionality constant | coefficient of proportionality | proportional coefficient〉、bを定数項〈constant term〉と呼びます。関数のグラフの形状から、aを傾き、bをy切片とも呼びますね。

アフィン線形関数〈affine linear {function | map | mapping}〉は1次関数の別名に過ぎません。fをアフィン線形関数として、次の形の方程式をアフィン線形不動点方程式〈affine linear fixed point equation〉と呼びます*1

  • f(x) = x

f(x)の定数項が特に1の場合は:

  • ax + 1 = x

この形のアフィン線形不動点方程式の解は、比例定数aだけから決まるので、それをa*と書きます。このa*のaのクリーネスター〈Kleene star〉と呼びます。つまり、次が成立することになります。

  • aa* + 1 = a*

両辺に右からbを掛けると:

  • a(a*b) + b = a*b

したがって、a*b は、一般的アフィン線形不動点方程式 ax + b = x の解です。

以上のような議論ができるためには、a, b, xが所属する代数系に何が要求され、何は要求されないでしょうか?

  • 足し算と掛け算がないと、1次式(アフィン線形式) ax + b が書けないので、足し算と掛け算は必要。
  • しかし、引き算と割り算はなくてもよい。
  • ax と xa を別に扱えば、掛け算の可換性も必要ない。

というわけで、アフィン線形不動点方程式を云々するには、足し算と(可換とは限らない)掛け算を持っている代数系が必要です。そのような代数系を半環〈semiring〉と呼びます。

クリーネ代数は、半環に、アフィン線形不動点方程式の解を与えるクリーネスターが付いたものです。が、もう少し構造が要求されます。それは実例を挙げた後で説明します。

順序構造と最小不動点

H = {x∈R | x ≧ 0}∪{∞} とします。∞はどの実数よりも大きいとします。足し算と掛け算は普通どおりですが、∞との足し算・掛け算は別途定義します。

x, yを非負実際として、

足す x
y x + y

x, yを正実数として、

掛ける 0 x
0 0 0 0
y 0 xy
0

この定義で、足し算・掛け算の計算法則はすべて成立します(引き算・割り算は考えない)。クリーネスターは次のように定義します。

  • 0 ≦ a < 1 のとき、a* := 1/(1 - a)
  • 1 ≦ a のとき、a* := ∞

ここで、1/(1 - a) に引き算と割り算を使ってますが、これはクリーネスターの定義のなかで実数の引き算/割り算を使っているだけで、H上の演算として引き算/割り算を認めているわけではありません。

記号の乱用で、H = (H, +, 0, ・, 1, (-)*) と定義します。・は掛け算です。Hは足し算/掛け算/クリーネスターを持った代数系です。

今定義したクリーネスター付き半環Hにおいて、アフィン線形不動点方程式 ax + b = x の具体例として、a = 1/2, b = 1 を考えると、

  • (1/2)x + 1 = x

x = 2 は不動点方程式の解ですが、x = ∞ も解です。一般に、アフィン線形不動点方程式の解はひとつとは限りません。クリーネスターa*は、ax + 1 = x の最小の解とします。最小が意味を持つためには、大小が比較可能、つまり順序構造を持つ必要があります。

クリーネ代数の要件として順序構造も追加すると:

  • クリーネ代数は、足し算、掛け算、順序を持つ順序半環である必要がある。
  • クリーネスターa*は、ax + 1 = x の最小の解を与える。

クリーネ代数の定義

クリーネ代数の公理を整備したのはデクスター・コゥゼン(Dexter Kozen)です。コゥゼンの定義では、足し算はベキ等、つまり a + a = a を仮定します。しかし、ベキ等性は要らない(強すぎる)でしょう。ベキ等性を要求すると、前節のHは除外されてしまいます。僕は、Hはクリーネ代数の仲間に入れてもいいと思うのです。

足し算のベキ等性は、半環上に順序を定義するために使われるのですが、足し算から誘導しなくても、順序が最初から在るとすればいいでしょう。クリーネ代数の下部構造を、ベキ等半環〈idemopotent semiring | ISR〉から順序半環〈ordered semiring | OSR〉に切り替えればいいのです。正確に言うと、0 ≦ a が成立する順序半環です。念の為、公理を書き出しておきます。以下の8番目までが半環の定義、その後は順序に関する定義です。全ての等式・不等式の前に全称限量子が付きますが、通常の習慣(悪習)にしたがって省略します。

  1. (a + b) + c = a + (b + c)
  2. 0 + a = a + 0 = a
  3. a + b = b + a
  4. (a・b)・c = a・(b・c)
  5. 1・a = a・1 = a
  6. 0・a = a・0 = 0
  7. a・(b + c) = a・b + a・c
  8. (a + b)・c = a・c + b・c
  9. ≦ は順序関係(全順序とは限らない)
  10. 0 ≦ a
  11. a ≦ b ⇒ a + c ≦ b + c
  12. a ≦ b ⇒ a・c ≦ b・c
  13. a ≦ b ⇒ c・a ≦ c・b

Hはこれらの公理を満たします。ZRでは ∀a.(0 ≦ a) が成立しないので、ZRは上記の公理は満たしません。

さて、Kは今提示した公理を満たす順序半環だとします。Kは半環なので、アフィン線形関数 f:K→K, f(x) = ax + b を考えることができます。t∈K がfの前不動点〈pre-fixed point | pre-fixpoint〉だとは、次が成立することです。

  • f(t) ≦ t

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じな同様に扱えるので、次の2つの条件を満たすtは最小不動点となりみなせます。

  1. f(t) ≦ t (tは前不動点である)
  2. ∀x∈K.(f(x) ≦ x ⇒ t ≦ x) (前不動点のなかではtが最小)

[追記]等式で定義される不動点と不等式で定義される不動点は、似た扱いはできますが、完全に同じと言うのは不適切でした。ホントに同じなら区別する必要がなくなるので。最後の節に書いたように、不等式的不動点理論と等式的不動点理論の差と関連を僕は理解してないのですが、安直に同じってのはマズイですね。[/追記][さらに追記 date="2018-10-16"]修正したけど、それはそれで別な誤解をまねきそうな気がしてきた。ウーン。補足記事を書いたほうがいいかも(書くとは言ってない)。[/さらに追記][さらにさらに追記 date="2018-10-19"]結局、補足説明を書きました。

[/さらにさらに追記]

f(x) = ax + b と展開した形で書くと:

  1. at + b ≦ t
  2. ∀x∈K.(ax + b ≦ x ⇒ t ≦ x)

aのクリーネスターa*を使えば、t = a*b で与えられるはずなので、

  1. a(a*b) + b ≦ a*b
  2. ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

一番目の不等式を簡略化して:

  1. aa* + 1 ≦ a*
  2. ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

これがクリーネスターを規定する公理です。順序半環Kと、写像 (-)*:K→K の組 (K, (-)*) が上記の2つの公理を満たすとき、右クリーネ代数〈right Kleene algebra〉と呼ぶことにします。なぜ「右」が付くのかは次節で。

可換性とベキ等性

クリーネ代数の定義では、掛け算の可換性は仮定しません。例えば、Kが非決定性プログラムの代数だとすると、掛け算はプログラムの順次結合なので、まったく可換ではありません。非可換の場合は、一次式〈アフィン線形式〉は2種類になります。

  1. ax + b
  2. xa + b

比例定数を左から掛けるバージョンと右から掛けるバージョンです。比例定数ではなくて変数の位置のほうに注目すると、上が右アフィン線形式、下を左アフィン線形式と呼びましょう。毎度注意してますが、左右の決め方は恣意的なので、二種類を区別する以外の意味は何もありません。

前節では、右アフィン線形不動点方程式に基づきクリーネ代数を定義しました。なので、右クリーネ代数です。左アフィン線形不動点方程式に基づき定義すれば、左クリーネ代数〈left Kleene algebra〉になります。左クリーネ代数を定義する公理は:

  1. a*a + 1 ≦ a*
  2. ∀x∈K.(xa + b ≦ x ⇒ ba* ≦ x)

ひとつのクリーネスター(-)*が、同時に右クリーネ代数と左クリーネ代数の構造を与えるとき、(K, (-)*) をクリーネ代数〈Kleene algebra〉と呼びます。

下部構造の順序半環が可換のとき、左右の区別はなくなるので、右クリーネ代数は左クリーネ代数にもなり、常にクリーネ代数になります。

半環の足し算がベキ等で、順序と整合している(a + b = b ⇔ a ≦ b)とき、クリーネ代数はベキ等クリーネ代数〈idempotent Kleene algebra〉です。コォゼンのオリジナルの定義によるクリーネ代数は、ベキ等クリーネ代数のことです。ベキ等性を外すとうまくいかないことも当然にあるでしょう。そのときはベキ等性を追加します*2

コンウェイ半環

前節まででクリーネ代数の話はオシマイ。この節はオマケです。

不動点を扱うための代数系というと、コンウェイ半環〈Conway semiring〉もあります。ちなみに、コンウェイ代数〈Conway algebra〉は別な代数系を意味するので、コンウェイ半環と呼びます。

コンウェイ半環は、スターオペレータを持つ半環 L = (L, (-)*) で、次の等式を満たすものです。

  1. (a + b)* = (a*b)*a* --(和スター等式)
  2. (ab)* = 1 + a(ba)*b --(積スター等式)

和スター等式(公式)については、次の記事で説明しています。

クリーネ代数は不等号(順序)に基づく法則で規定されますが、コンウェイ半環は、完全に等式的な代数系です。この2つは別物なんですが、圏化するとクリーネ代数とコンウェイ半環の違いはハッキリしなくなります。不動点を扱う圏は、クリーネ代数の圏化とも言えるし、コンウェイ代数の圏化とも言えるような圏になります(たぶん、だいたい)。

クリーネ代数とコンウェイ半環は別だが似てるのは知ってました。が、相互関係を僕は理解してません。圏化すると、ほんとに違いが消えるのか、やっぱり別な圏になるのか? 正確には知らないなー。気力が湧いたら考えます。

*1:不動点は、"fixed point", "fix point, "fixpoint", "fixed-point", "fix-point"などの表記の揺れがあるので、検索しにくいですね。

*2[追記]ベキ等性をいったん外したのは、ベキ等性の役割をハッキリさせたかったからです。もし、大部分の結果がベキ等性に依存していることが分かれば、ベキ等性は最初から入れたほうがいいでしょう。[/追記]

2018-10-09 (火)

クリーネ代数の圏化: ちょびっと

| 13:44 | クリーネ代数の圏化: ちょびっとを含むブックマーク

マイクロコスモ原理とクリーネ構造」の続きの話。ほんのちょびっと分かったこと。

内容:

  1. 圏化の多様性
  2. 狭義の圏化と亜化〈oidification〉
  3. クリーネ代数の場合は

圏化の多様性

前の記事に書いたように、僕は、クリーネ代数に関して「なんか違う」「なんか足りない」という感じをいだいてました。

今思えば、それは「クリーネ代数を圏化〈categorify〉せねば」という感覚だったのかも知れません。トレース付きデカルト圏は、クリーネ代数の圏化と捉えることができます。クリーネ代数より強力で使いやすいです。で、それで「めでたし、めでたし」なのかと言うと、そうでもないのです。

クリーネ代数の圏化がトレース付きデカルト圏だけでよいのか? どうもそうじゃない。クリーネ代数の特徴的機能であるクリーネスターに関しては、大規模な一般化ができそうな気配があります。

トレース付きデカルト圏は、クリーネ代数の圏化の one of them に過ぎないのではないか? 他にもっと別な圏化があるのではないか? -- こういう問に答えが出てないので、スッキリしない。「マイクロコスモ原理とクリーネ構造」でも、次のように書いています。

マイクロコスモ原理を信じるなら、1-クリーネ構造=クリーネ代数、2-クリーネ構造=クリーネ圏、3-クリーネ構造=メタ・クリーネ圏、… というクリーネ構造の無限タワーがあるはずです。構造の無基底性・多様性から、無限タワーが一意ではなくてたくさんのバリアントがあるかも知れません。

「たくさんのバリアント」がどんなものなのか、もっと具体的に分からないと、スッキリはしないですよね。「マイクロコスモ原理とクリーネ構造」の記述では(修正はしませんけど)、複数の圏化がゴッチャになって書かれているようです。状況が整理されてないですね。

狭義の圏化と亜化〈oidification〉

確かバエズ〈John C. Baez〉が言っていたと思うんだけど、圏化には少なくとも二種類があると(もっとあるかも知れないが)。何らかの概念Xに対して、X categoryと名付けるタイプの圏化と、X-oidと名付けるタイプの圏化です。

名付けの際に、語尾を形容詞にするとか綴り・発音を整えるとかしないことにして、「X → X category」タイプの典型例は「monoid → monoid category」(= monoidal category)です。「X → X-oid」の典型例は「group → group-oid」(= groupoid)です。日本語訳が難しいけど、前者を狭義の圏化、後者を亜化としておきます(苦しい訳だ)。「X圏化」と「亜X化」のほうが落ち着くかな。

X圏化は、集合を台〈underlying thing〉とする構造を、圏を台とする構造に拡張することです。集合を台とする構造Xとそのあいだの準同型写像からなる圏を太字のXとします。X圏化した構造とそのあいだの関手からなる圏をXCatとします(自然変換は考えないことにします)。そのとき、次の図式が可換になります。

 X - D → XCat
 |     |
 U     U
 |     |
 v     v
Set- D → Cat

ここで、Uは台集合/台圏を対応させる忘却関手、Dは集合を離散圏として埋め込む関手です。X = Monoidの場合なら:

Monoid-D→ MonoidCat
 |     |
 U     U
 |     |
 v     v
Set - D → Cat

この可換図式からX圏化の特徴はつかめるでしょう。

亜X化は、対象が1つだけの亜XとしてXが再現するような拡張です。亜X化した構造とそのあいだの関手からなる圏をX-oidとします。そのとき、次の圏同値が成立します。

  • X ¥stackrel{¥sim}{=} X-oid1ob

ここで、X-oid1ob は、単対象X-oidからなる部分圏です。X = Group の場合なら:

  • Group ¥stackrel{¥sim}{=} Group-oid1ob

Group-oidのエンドセットGroup-oid(A, A)は、すべて群の構造を持つので、一般的X-oidの圏X-oidにおいても、エンドセットX-oid(A, A)がXの対象という状況を考えるのもアリです。

クリーネ代数の場合は

クリーネ代数の圏化の場合も、X圏化と亜X化を考えることができます。トレース付きデカルト圏、半加法圏〈双積圏〉などは、亜X化の意味でのクリーネ代数の圏化です。つまり、KleeneAlgebra-oidを求める方向ですね。それとは別に、KleeneAlgebraCategoryを求める方向もあるわけです。

どうも僕は、KleeneAlgebra-oidとKleeneAlgebraCategoryをゴッチャにしてきたようです。関連はあるでしょう*1が、KleeneAlgebra-oidとKleeneAlgebraCategoryは区別しないと混乱します。圏化の多様性に目が眩んでしまう、というか…

KleeneAlgebra-oidは、ある程度は分かっているし、形式言語理論/プログラム意味論との関係も分かります。が、KleeneAlgebraCategoryはそれほどハッキリしません。半環のX圏化であるSemiringCategoryに、クリーネスター自己関手が付いたものだろうとは思います。関数に対する再帰の定式化がKleeneAlgebra-oidで、領域に対する再帰の定式化がKleeneAlgebraCategoryという感じかな。

KleeneAlgebraCategoryの実例がまったくないのか? というと、そんなことはありません。集合圏Setは、リストモナドをクリーネスターと考えておそらくKleeneAlgebraCategoryになるだろうと思います。今のところ、KleeneAlgebraCategoryのチャンとした定義がないので、実例だと言い切ることは出来ませんが。

前節で述べたように、圏化にはバリエーションがあり、もとの構造(圏化する前の構造)が、台が離散圏の場合に再現したり、台が単対象圏の場合に再現したり、あるいはエンドセットとして再現したりします。さらに、マイクロコスモ原理との関連では、圏化した圏がもとの構造をホストできるか? も問題になります。

クリーネ代数(あと、テスト付きクリーネ代数も)の圏化/無限タワー化は、モノイド構造やデカルト構造に比べると、事情が複雑になるでしょう。が、部分的にでも出来れば、もともとの動機である形式言語理論/プログラム意味論にもフィードバックがあると期待できます。


2005, 2006年くらいに考えていたことがメモ編には残っているので、読み直してみようかな。色々な種類の圏化を比較したり組み合わせたりが重要なんじゃないかと思います。

*1:2-圏のレベルでは、KleeneAlgebra-oidとKleeneAlgebraCategoryを統合できるだろう、と思っています。

2018-10-05 (金)

マイクロコスモ原理とクリーネ構造

| 16:41 | マイクロコスモ原理とクリーネ構造を含むブックマーク

昨日の記事は妄想に近い話でしたね。とりとめのない雑感/思いつき/妄想のたぐいは、積極的に書こうとは思わないのだけど、後でなんかのヒントになる可能性がある事は書き留めておこうかな、と。

十数年前から、クリーネ代数にある種の“違和感”をいだいているんですよ。マイクロコスモ原理により、その違和感の正体がわかるかも知れない。(分からないかも知れない。)

内容:

  1. クリーネ代数
  2. クリーネ行列とクリーネ圏
  3. クリーネ圏とクリーネ構造のタワー

クリーネ代数

このブログは2005年初頭から始めました。始めた当時から最近まで、散発的にクリーネ代数〈Kleene algebra〉の話題を取り上げています。クリーネ代数は、形式言語やプログラムの意味論に使えます。よく出来た代数系だと思うのですが、一方で、「なんか違う」感がつきまとってました。その“違和感”に言及した記事を3つ挙げれば:

クリーネ代数に対する僕の印象は、「クリーネ代数という代数系は、現象の一部をうまくモデル化しているが、現実的には不十分なことが多い」というものです。不十分な感じに対しては、「より強力なトレース付きデカルト圏に乗り換えればいい」と思っていました。このような印象や対処は、間違っているとは思いませんが、別な見方がありそうです。

別な見方とは、マイクロコスモ原理の観点からの解釈です。マイクロコスモ原理は、次のように主張します。(例えば「マイクロコスモ原理の恐怖」参照)

  • 特定の代数構造は、その代数構造を圏化した構造を備える圏のなかで定義可能である。

クリーネ代数も代数構造なので、次のように言えます。

  • クリーネ代数は、クリーネ代数を圏化した構造を備える圏のなかで定義可能である。

「クリーネ圏」〈Kleene category〉という言葉は、既に定義して使っている人がいますが、ここでは、マイクロコスモ原理で言うところの「クリーネ代数を圏化した構造を備える圏」という(若干曖昧な)意味で使います。

クリーネ代数に関するマイクロコスモ原理を信じるなら、クリーネ代数という構造は、必然的にクリーネ圏という圏論的構造を要求することになります。

クリーネ行列とクリーネ圏

クリーネ代数は、ベキ等な足し算と可換とは限らない掛け算、それとクリーネスターを備えた代数構造(代数系)です。ベキ等な足し算から順序が入り、クリーネ代数は順序半環になります。クリーネ代数を K = (K, +, 0, ・, 1, (-)*, ≦) のように書きましょう。≦ は、足し算 + から導かれた順序です(x ≦ y ⇔ x + y = y)。

クリーネスターを仮定する代わりに、次のように言っても同じです。

  • a, b∈K に対するアフィン線形不動点方程式 x = ax + b は、常に唯一の最小解を持つ。

b = 1 の場合の不動点方程式 x = ax + 1 の解を a* と定義することによりクリーネスターは後から導入できます。

アフィン線形不動点方程式は1次方程式(の特殊形)なので、多次元化したくなります。連立の不動点方程式は次の形になります。

x1 = a1,1x1 + ... + a1,nxn + b1

...

xn = an,1x1 + ... + an,nxn + bn

クリーネ代数Kを係数域とするn×nの正方行列 [aj,i] が出てきます。正方行列に対してもクリーネスターが定義できて、有限オートマトン理論とうまく繋がります。

行列計算をするなら、正方行列に限定する必然性はありません。任意の n, m に対するn×m行列を考えることができます。クリーネ代数K上の行列線形代数が構成できます。行列線形代数は、K上の有限次元自由加群を議論していることになります。単なる線形代数というわけではなくて、アフィン線形不動点方程式/クリーネスターの話も入ります。

クリーネ代数Kを調べるには、K上の行列線形代数は必須です。よって、クリーネ代数を定義して調べることができる環境は、少なくとも行列線形代数を展開できるような環境ということになります。そんな環境は半加法圏〈semiadditive category〉だと言っていいでしょう。次の記事で書いています。

クリーネ圏が在るとすれば、それは半加法圏の構造を備えているはずです。

クリーネ圏とクリーネ構造のタワー

クリーネ代数Kを、K = (K, +, 0, ・, 1, (-)*, ≦) と書きました。これは、足し算(中立元は0)/掛け算(中立元は1)/クリーネスター/順序を持つ構造であることを表しています。クリーネ代数の圏化〈categorification〉を仮にクリーネ圏と呼ぶことにしたのですが、クリーネ圏の構成素〈constituents | stuff〉はまだハッキリしません。クリーネ代数との対応を考えるなら:

代数系
足し算 双積(半加法構造)
掛け算
クリーネスター
順序

足し算に対応する双積以外は不明です。が、以前に半加法圏を考えたとき、テンソル積〈モノイド積〉も一緒に考えてました。掛け算の対応物は、双積と協調するテンソル積でしょう。

クリーネスターは不動点方程式の解なので、圏論的対応物は(圏論的)不動点オペレーターでしょう。もし、圏がデカルト圏なら、カザネスク/ステファネスク/ハイランド/長谷川の定理より、不動点オペレーターはトレースと同じことになります。ここいらのことは:

半加法構造(双積)とデカルト構造はうまく両立しない(たぶん)ので、カザネスク/ステファネスク/ハイランド/長谷川の定理が使えるのか? は現状よく分かりません。よく分からないながらも、先の対応表を(暫定的に)埋めてみると:

代数系
足し算 双積(半加法構造)
掛け算 テンソル積
クリーネスター 不動点オペレーター
順序 EPペア

EPペアについては、次を参照してください。

今までは「クリーネ代数は不十分だ、代わりにもっと強力な圏を考えよう」というだけの発想でした。クリーネ代数が不十分なのは、その環境を一緒に考えてなかったからかも知れません。「クリーネ代数を圏化する」、あるいは「クリーネ代数達に、適切な棲息環境を見つけてあげる」と考えると、別な景色が見えるかも知れません。

クリーネ代数が定義される環境であるクリーネ圏が定義できたとして、マイクロコスモ原理の無限階層性から、クリーネ圏が定義される環境であるメタ・クリーネ圏が必要になります。実は、半加法圏に関してはメタ圏を考えたことがあります。

マイクロコスモ原理を信じるなら、1-クリーネ構造=クリーネ代数、2-クリーネ構造=クリーネ圏、3-クリーネ構造=メタ・クリーネ圏、… というクリーネ構造の無限タワーがあるはずです。構造の無基底性・多様性から、無限タワーが一意ではなくてたくさんのバリアントがあるかも知れません。

マイクロコスモ原理を信じてみようかと宗旨変えしたのは割と最近(2018年9月13日あたりから)で、その有効性を確信はしてないのですが、クリーネ構造タワーが見つかれば面白いし、マイクロコスモ原理への確信が生まれるかも。

2018-10-04 (木)

チャーチ/チューリングの提唱とバーウィック/ショマー=プリの定理

| 12:54 | チャーチ/チューリングの提唱とバーウィック/ショマー=プリの定理を含むブックマーク

妄想かも知れない、トンチンカンかも知れない、雑感。

内容:

  1. チャーチ/チューリングの提唱
  2. 高次圏論
  3. バーウィック/ショマー=プリの唯一性定理
  4. もう一度チャーチ/チューリングの提唱

チャーチ/チューリングの提唱

チャーチ/チューリングの提唱〈Church-Turing thesis〉とは、およそ次のような主張です。

  • 計算可能性の概念は、どのような方法で定義しても同値になる。

これは、チャーチ/チューリングの定理でもチャーチ/チューリングの公理でもなく、提唱〈テーゼ〉です。主張を正確に述べることもできないし、もちろん証明もできません。経験則を指導原理として位置付けたものでしょう。

計算可能関数の定義は色々とあります。

これらの方法で定義される関数のクラスが同じであることは証明できる(証明された)定理です。まったく異なる定義が同じ関数のクラスを定義するのです。この事実から、直感的な「計算可能」という概念は、定義によらない普遍的な概念であるように思えます。

その「思い」を言葉にしたのがチャーチ/チューリングの提唱なんでしょうが、それを言ったからってなんなんだ? というスッキリしない感じが残ります。

高次圏論

高次圏論でも同じような事情があります。誰かが提唱したわけではないので、名前は付いてませんが、多くの人が次のような「思い」を抱いているでしょう。

  • 高次圏の概念は、どのような方法で定義しても同値になる。

高次圏の定義も色々とあります。2004年に書かれたチェン/ラウダの高次圏の教科書がありますが:

その目次を見てみましょう。

  • 2. Penon
  • 3. Batanin and Leinster
  • 3.3 Leinster
  • 3.4 Batanin
  • 4. Opetopic
  • 5. Tamsamani and Simpson
  • 5.3 Simpson's definition .
  • 5.4 Tamsamani's definition
  • 6. Street
  • 7. Joyal
  • 8. Trimble and May
  • 8.1 Trimble
  • 8.2 May

4章のOpetopic以外はすべて人名です。OpetopicもBaez-Dolanとすれば、11人の人名が並びます。それぞれの人がそれぞれの定義を提案しています。

計算可能性の場合とは違って、異なる定義が同値であることの証明は難しく、同値性が証明された例は少数です。「どのような方法で定義しても同値になる」は、経験則と呼ぶには弱く、希望的観測や努力目標といったところでしょう。

n-圏は、次元n以外のもうひとつの整数mを使ってより細かい分類がされます。(n, m)-圏とは、m次を超える射がすべて可逆であるn-圏です。チェン/ラウダの教科書で扱っているのは(n, n)-圏(nが無限でもよい)で、その後で多用されるようになった高次圏に(∞, n)-圏があります。

バーウィック/ショマー=プリの唯一性定理

高次圏の場合は、定義がたくさんあり、それらの定義を書き出すのも難しく、定義の同値性を示すのも難しく、「いったいどうすりゃいいんだ?」な状況です。一見、混沌とした状況に対して、別なアプローチをする人もいます。「高次圏とは何か?」に答えるのではなくて、「高次圏“論”とは何か?」に焦点を移すのです。

「高次圏とは何か?」にはたくさんの人がそれぞれの定義を持ち、それぞれに高次圏論を展開しています。それらの高次圏論(高次圏ではない)に共通する特徴を探して、高次圏論を公理化しよう、というわけです。

卑近な例で言えば; 「ベクトルとは何か?」は今は問題にされないでしょう。単に「ベクトル空間の要素」です。公理化されて興味の対象となっているのは「ベクトル空間」のほうです。同様に、高次圏とは単に「高次圏論で扱う対象」で済ませるのです。

バーウィックとショマー=プリは、(∞, n)-圏論を公理化して、その公理を満たす(∞, n)-圏論は、本質的には(ある種のupto-isoで)1つしかないことを示しています。

  • Title: On the Unicity of the Homotopy Theory of Higher Categories
  • Autohrs: Clark Barwick, Christopher Schommer-Pries
  • Pages: 45p
  • URL: https://arxiv.org/abs/1112.0040

上記論文の最初の投稿は2011年末(30 Nov 2011)ですが、今年(7 Aug 2018)になって大幅にリライトされてます(Completely rewritten)。改善が続けられて、読みやすくなったのでしょうが、僕にはハードル高すぎ。

テクニカルな内容は追えないまでも、バーウィック/ショマー=プリの戦略は見当が付きます。

  1. 対象物そのものではなくて、対象物を扱っている理論に注目する。
  2. その理論を公理化する。
  3. 公理化された理論は、本質的には唯一であることを示す。
  4. 現在知られている理論が公理を満たすことを確認する。
  5. 複数の理論が同値であることが分かる。
  6. どの理論を使っても、(ある抽象レベルでは)同じ結果が出ることが保証される。

もう一度チャーチ/チューリングの提唱

さて、冒頭のチャーチ/チューリングの提唱ですが、バーウィック/ショマー=プリと同様な戦略で、定理にできないものでしょうか? 「計算可能性とは何か?」ではなくて「計算可能性の理論とは何か?」に注目して、計算可能性理論を公理化するというアプローチです。計算可能性の場合は、直接的・個別的に同値性が証明できたので、理論の公理化の必要性はなかったのでしょうが、計算可能性が「定義によらない普遍的な概念」だとすれば、定義・定式化をどうしようが本質的に唯一の概念的実体を記述する、という形の定理があってもよさそう、と思うんですが。

2018-10-02 (火)

ゲーデル化をどうするか? その2

| 12:17 | ゲーデル化をどうするか? その2を含むブックマーク

昨日の「ゲーデル化をどうするか?」の続きです。

内容:

  1. 「コード」という言葉
  2. ゲーデル符号が自然数であることのメリット
  3. ゲーデル化を具体的に定義したいわけ
  4. ツリー構造が良さそうなわけ
  5. そんなわけで

「コード」という言葉

昨日の記事の途中「ゲーデル化をどうするか? // プログラミング言語の利用」で、「コード」という言葉の多義性で“ウワーってなって”います。

ゲーデル化=ゲーデル符号化の写像 G:S→D に対して、Sの要素を「コード」と呼ぶときもあれば、Dの要素を「コード」と呼ぶときもあるのです。「コード」という言葉は、ものすごくよく使うし、とても便利な言葉なんですが、混乱を避けるには使わないのが無難かな。

写像Gの余域である集合Dの要素は、漢字で「符号」と書き、encode/encodingは「符号化」、decode/decodingは「脱符号化」。D自体は「データ領域」「符号集合」「符号空間」とか呼びましょう。

では、写像Gの域である集合Sの要素は何と呼ぶ? … … ウーン。Sはのっぺらぼうな集合じゃなくて、「原子記号、定数記号、項、論理式、証明」のような階層があるんですよね。みんなひっくるめて呼ぶときは … 「式」〈expression〉かな。データの種類としては文字列とみなすので、「テキスト」でもいいかな。論理ってさ*1、いうほど概念・用語が整理・整備されてないんだよね。

ゲーデル符号が自然数であることのメリット

ゲーデル化をどうするか?」で、ゲーデル化=ゲーデル符号化の値が自然数であるのは辛い、と書きました。しかしもちろん、符号が自然数であることによるメリットがあります。

扱うデータは自然数だけなので、集合(基本データ型)は、Nだけでこと足ります。関数は、f:NnN という形のものだけ考えれば十分です。データ領域を含む意味論的システムが単純であり、それに伴い構文論的システムもまた単純なもので済みます。単純さはメリットです。

ゲーデル化をどうするか?」より:

構文的対象Aに対するG(A)は巨大な数になってしまい、...[snip]... ゲーデル数G(A)を見て、Aを想像するのもほぼ不可能です。

ゲーデル符号G(A)を見ても、もとの構文的対象Aがサッパリ分からないのはメリットと捉えることもできます。ゲーデル符号化は、構文的対象の無意味化/脱意味化という側面も持ちます。もともとは意味を持っていた構文的対象から意味を剥ぎ取って単なるデータにする働きがあります。G(A)を見ても意味が分からないことは、十分に無意味化/脱意味化されていることになります。

コード[構文的対象]とデータ[符号]があまりにもソックリだと、コード[構文的対象]とデータ[符号]の違いを意識できなかったり混乱したりするかも知れません。

ホモアイコニック言語を使ったゲーデル符号化(クォーティング)の難点は、無意味化/脱意味化の効果が薄いことです。意味が容易に想像できるデータに対して「意味を考えるな!」と言われても難しいんですよ。人間の意味的連想力って、ほんとに強烈で制御困難なんです*2

ゲーデル化を具体的に定義したいわけ

ゲーデル自身が使ったゲーデル化(符号化)を「オリジナルのゲーデル化」と呼ぶことにします。オリジナルのゲーデル化は、 G:S→N という写像で、Nの演算や性質(算術〈arithmetic〉と呼ぶ)で組み立てられます。Gは、原理的には明確で簡単な関数です。が、現実的にはほぼ計算できません。

現実的(理論的じゃないよ!)に計算できるかどうかは、ゲーデルの不完全性定理にとってはどうでもいいことです。なんなら、「G:S→N という写像があったとしましょう」からスタートしてもいいかも知れません。Gの存在を信用できない人のために、具体的な定義を一応は出すだけで、値をホントに計算したいわけじゃないのです。

でも僕は、値をホントに計算したいのです。しかも手で。Gに対して、「定理の証明のための概念上の道具」とは若干別な用途を想定しています。Nとは限らない(つうか、Nじゃない)データ領域Dに対して、G:S→D を具体的に定義することは、Sの構造をハッキリと理解する助けになります。そして、具体的な式(項/論理式/証明)Aに対して、G(A)をホントに手で計算することは、システムに対する実感を得るのに効果があるからです。

以上の動機からは、写像Gは、明示的/具体的に定義される必要があるし、現実的に手で計算できる写像であることも要件です。オリジナルのゲーデル化ではうまくないですね。手で計算できないもん。

ツリー構造が良さそうなわけ

ゲーデル化をどうするか?」で、テキストとしての式(構文的対象)をパーズしたツリーをデータにする案を述べました。まだ、決定ではなく案ですが。

ノードにラベル(文字列だと思ってください)をくっつけたツリー構造というのは、かなり馴染み深いデータ構造だと思います。実際によく利用されます。その操作や性質もよく知られています。小学生でも知っている自然数には負けますが、ポピュラーなデータ/データ領域と言っていいでしょう。

オリジナルのゲーデル化では、項や論理式は(下位の)記号の列とみなします。それはまーいいのですが、証明も論理式の列とみまします -- これはどうなの? 「定理の証明のための概念上の道具」としてはそれでもいいでしょう。しかし、手で符号化/脱符号化を実際に計算する場合は嬉しくないです。

命題の列が証明であるのは、列内の命題が、それより前に出現する命題(複数でもよい)から、なんらかの推論規則で導出できる場合です。この基準で、命題列が最後の命題の証明になっているか/なってないかを判断できます。実際の(形式化してない)証明も、おおむね命題の列だと言えるでしょう。

でもね、命題の列としての証明というのは分かりにくい。自然演繹でもシーケント計算でも、(形式化された)証明は、ツリー構造に編成されています。証明をデータとして扱う場合、リストよりはツリーのほうがずっと扱いやすいです。この理由もあって、証明も含めた構文的対象の符号化データはツリーがいいと思うのです。

データ領域Dを、ラベル付きツリーの集合と決めると、自然数の加減乗除に対応するものは、ツリーに対する様々な操作です。ツリーの操作(演算)は、大雑把な合意はあるでしょうが、算術のように強い標準はないので、あらためてハッキリと決める必要があります。ツリーの算術を設定するわけです。

そんなわけで

自然数の算術の代わりにツリーの算術を確定して、ツリー算術の意味での計算可能性/定義可能性/表現可能性/構成可能性(どれも似たりよったり)を考えようかな*3、と思っています。ツリーの算術は自然数の算術ほどにポピュラーじゃないにしろ、学習負担はさほどではなく、表現力は相当に強力です。

先に述べた「符号が自然数であることによるメリット」は失われるけど、それはトレードオフだからしょうがない。あと、ちょっと懸念があるのは、「ゲーデル化をどうするか?」で触れた心理的インパクトかな。心理的な問題だから、優先度は高くないですけど。

*1:他の分野もたいてい事情は同じです。

*2:誤解・曲解・混乱などの原因の多くは、自動的に働いてしまう連想じゃないかと思います。

*3:データ領域を自然数の集合からツリーの集合に切り替えると、計算可能関数(帰納的関数)の定義をやり直さないといけなので、そこは手間が増えます。

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