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

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

2017-06-12 (月)

平面タングル、空間タングル、ブレイドなんかが“もつれた”話

| 09:27 | 平面タングル、空間タングル、ブレイドなんかが“もつれた”話を含むブックマーク

単純平面タングルとカウフマン図のキャンバス・基準点について」において、平面タングルに触れました。平面タングルを空間タングルに一般化して、その後で特殊化することでブレイドが出てきます。結び目や絡み目もタングルの特殊なものとして出現しますが、それらの相互関係はけっこうややこしいです -- 絡み合い、もつれ合っています。

内容:

  1. 平面タングルとその変種
  2. 空間タングルとその変種
  3. 方体タングル
  4. ブレイド
  5. タングルの定義
  6. 幾何タングル
  7. 結び目、絡み目、ブレイド
  8. 方体タングルのモノイド圏
  9. 記号的モノイド圏
  10. 組み合わせブレイド
  11. タングルの圏の公理的な特徴付け
  12. もつれを整理すると

平面タングルとその変種

平面タングル(planar tangle)は、穴あき円板をキャンバス(描画領域)にして、その上に紐(ワイヤー、糸、ロープなど)で模様を描いたものです。「単純平面タングルとカウフマン図のキャンバス・基準点について」では、平面タングルの特殊なものとして円環タングル(annular tangle)と、キャンバスが矩形となる矩形タングル(rectangular tangle)も紹介しました。

(一般的な)平面タングル、円環タングル、矩形タングルの三者について表にまとめましょう。

タングルの種類 キャンバス 入口境界 出口境界
平面タングル 穴あき円板 幾つかの円 ひとつの円
円環タングル 円環 ひとつの円 ひとつの円
矩形タングル 矩形 線分 線分

キャンバスは2次元の領域です。キャバスの境界の一部が入口境界(incomming boundary)と出口境界(outgoing boundary)になっています。入口境界と出口境界上に点(ドット)が乗っていて、それらの点が紐の両端になります。

キャンバス上に描かれた紐模様が圏の射となります。圏の対象は、ドットの集合です。入口境界上のドットの集合が射の域、出口境界上のドットの集合が射の余域となります。ドットに個性はないので、ドットの個数を指定すればドットの集合を記述できます。そのため、圏の対象は自然数(0, 1, 2, ...)と同一視します。

空間タングルとその変種

平面タングルのキャンバスを2次元から3次元へと一般化します。空間領域をキャンバスとします。ここで「空間」は、我々が棲んでいる3次元空間のことです。

タングルの種類 キャンバス 入口境界 出口境界
空間タングル 穴あき球体 幾つかの球面 ひとつの球面
球殻タングル 球殻 ひとつの球面 ひとつの球面
方体タングル 方体(直方体) 矩形 矩形

「平面→空間(3次元)」という一般化にともない、「円板→球体」、「円(周)→球面」、「矩形→方体」、「線分→矩形」のような一般化をしています。球殻は、球体から内部の球体を抜いた形、アンコを取り去ったおまんじゅうのような形です。入口境界と出口境界の面上にいくつかのドットを打ち、紐はドットとドットを結ぶように配置します。全般に次元が1上がります。

紐は交差したり分岐したり切れたりしませんが、3次元なので絡み合う/もつれ合うことができます。事情は非常に複雑になります。上の3種のタングルのなかでは、方体タングル(cubical tangle)が一番扱いやすいでしょう。以下、方体タングルに注目することにします。

方体タングル

方体タングルのキャンバス領域は、3次元の方体(直方体)なので、箱とか部屋にたとえることができます。入口境界が天井で、出口境界が床と考えましょう。紐の端になるドットは、直線上に配置されていることにします。

上の絵で、赤はドットが並ぶ直線(線分)で、4個のドットが並んでいます。ドットからドットへと向かう紐は、部屋の内部を通ります。紐の様子は次のような図で描けるでしょう。結び目図(knot diagram)と同じ要領で、交差部分で奥行きが分かるように描きます。

方体タングルでも、複雑な絡み合い/もつれ合いは生じます。

絡み合い/もつれ合いは難しいですね。

ブレイド

方体タングルでは、天井から天井、床から床への紐を認めています。このような紐がつながると、天井にも床にも壁にも触らないで、部屋の内部で閉じる紐ができます -- 結び目(knot)ですね。単一の結び目に限らず、複数の結び目がさらに絡み合う状況も生じます -- 絡み目(link)ですね。

事情を単純にするために、天井から床に向かう紐しか認めないことにします。このように制限した方体タングルはブレイド(braid; 組み紐)になります。ブレイドについては次の記事に書いてあります。

*1

ブレイドを平面に投影して、2種の交差が区別できるように描いた図をブレイド図(braid diagram)と呼ぶことにします。ブレイド図の全体は圏をなします。ブレイド図の圏に関しては、次を参照してください。

2つの結び目図(結び目の射影図)が同じ結び目を表すのは、ライデマイスター移動(Reidemeister moves)で互いに移れるときです。同様に、ライデマイスター移動で互いに移れる2つのブレイド図は同じブレイドを表します。このとき使うライデマイスター移動は、II番とIII番だけで、ライデマイスター移動I番は使いません。(以下の図の左と右を入れ替えるのがライデマイスター移動。まん中は移動の中間状態。)

ブレイドの同値性を定義するにはもう少し精密な議論が必要ですが、後でまたブレイドの話題に触れます。

タングルの定義

今まで、タングルやブレイドという言葉を正確には定義していませんでした。キッチリ議論するなら、例えば「タングル」という言葉の4種の意味を区別すべきです。

  1. 幾何タングルのインスタンス: 幾何的に定義された個々の図形(のパラメータ表示)
  2. 幾何タングルのクラス: 幾何的に定義された個々の図形の同値類
  3. 組み合わせタングルのインスタンス: 組み合わせ的に定義された語(記号の組み合わせ)
  4. 組み合わせタングルのクラス: 組み合わせ的に定義された語の同値類

方体タングルに関して、幾何的な定義をしてみましょう。定義の舞台となる圏の選び方が色々ありますが、ここでは位相多様体連続写像の圏で考えることにします。図形はこの圏の対象 -- つまり位相多様体だけを考えます。

I = {x∈R | 0≦ x ≦1} とします。I3 = I×I×I を(標準的な)方体とします。z軸が鉛直方向(重力方向)下から上に向かうとみなして、床の線分H0と天井の線分H1を定義しておきます。

  • H0 = {(x, 1/2, 0)∈I3 | 0< x <1 }
  • H1 = {(x, 1/2, 1)∈I3 | 0< x <1 }

床の中央線H0の代わりに床全体、天井の中央線H1の代わりに天井全体でもいいのですが、線分H0, H1を定義しておくと若干話が簡単になります。例えば、線分上に乗る有限個の点には全順序を付けることができます。

さて、Xを1次元コンパクト(位相)多様体とします。1次元(境界を許す)コンパクト多様体は線分と円周の有限直和です。円周をS1と書くなら:

  • X ¥stackrel{¥sim}{=} I + ... + I + S1 + ... + S1

と書けます。線分Iの個数をn、円周S1の個数をmとして、次のように書くことにします。

  • X ¥stackrel{¥sim}{=} nI + mS1

3I + 2S1 = (| | | ○ ○)

同相な図形は同一視してしまう、あるいは同相な類から代表を1つだけピックアップすると考えれば、

  • X = nI + mS1

としてもかまいません。

幾何タングルのインスタンス(geometric tangle instance)は、α:X→I3 という連続写像で、次の条件を満たすものです。XはXの内部、∂XはXの境界です。

  1. αは埋め込みである。Xと像α(X)は同相な多様体
  2. α(X) ⊆ (I3)
  3. α(∂X) ⊆ (H0∪H1)

2番目の条件は、紐の両端以外の部分は、部屋の天井・床・壁に接触しないことを表しています。仮に接触しても、少し紐を動かせば部屋の内部に収まりますが、最初からこの条件を付けておくことにします。

3番目の条件は、紐の両端は天井と床の中心線(H0とH1)に乗ることを表しています。X = nI + mS1 だったので、∂Xは2n個の点からなります。k0 + k1 = n + m となる2つの整数k0, k1があり、次の状況となります。

  • α(∂X)のうちk0個の点がH0内にあり、k1個の点がH1内にある。

今定義した幾何タングルのひとつひとつのインスタンスを別々なものとみなすのではなくて、似たものは「同じ」とみなします。「同じ」とみなす基準を次節で述べます。

幾何タングル

α:X→I3, β:Y→I3 を2つの幾何タングルのインスタンスとして、XとYが τ:X→Y で同相であり、α = τ;β のとき、αとβは「同じ」とみなします。αとβがこの意味で「同じ」とき、α(X)とβ(Y)はI3の部分多様体として同じになります。αとβは、描いた図形の形状(=点集合)は同じでパラメータ表示方法(=動作としての描きっぷり)の差があるだけです。

描かれた図形をグニグニ動かしてもいいということを表すためには、アンビエント・イソトピーを使います。Φ:[0, 1]×I3I3 という連続写像があるとき、φt(p) := Φ(t, p) と書くことにします。

2つの幾何タングルのインスタンス α, β:X→I3 に対して、Φ:[0, 1]×I3I3 が、αからβへアンビエント・イソトピー(ambient isotopy)だとは:

  1. tがなんであっても、φt:I3I3同相写像である。
  2. tがなんであっても、φt(H0) = H0 で、φtをH0に制限したものはH0同相写像となる*2
  3. H1に関しても前項と同様。
  4. φ0I3の恒等写像
  5. φ1¥circα = β ('¥circ'は反図式順結合の記号)

αからβへのアンビエント・イソトピーΦがあるとき、αとβはアンビエント・イソトピック(ambient isotopic)と呼びます。1次元コンパクト多様体Xを固定すると、Xからの幾何タングル・インスタンスの全体にはアンビエント・イソトピックによる同値関係が入ります。

「パラメータ表示の違いしかないなら同じ」と「アンビエント・イソトピックなら同じ」という2つの同値関係を組み合わせた同値関係を考えて、これを幾何タングルのインスタンスのあいだの同値関係とします。

幾何タングルのインスタンス全体に今述べた同値関係を入れて、その同値類を幾何タングルのクラス(geometric tangle class)と呼びます。単に幾何タングルと言ったときは、幾何タングルのクラスのことです。あるいは、クラスの代表としてのインスタンスのことです。個々のインスタンスを別物として扱うことはありません。

ここまでの定義では、幾何タングルのインスタンスとクラスを区別しましたが、実際に区別されることはほとんどなくて、文脈により適宜解釈を変えます。

結び目、絡み目、ブレイド

αは幾何タングル(クラスの代表となるインスタンス)とします。αの定義域は X ¥stackrel{¥sim}{=} nI + mS1 だとします。ここで、n, mは任意の自然数で、nが線分(閉区間)の個数、mが円周の個数です。Xの位相同型類は自然数n, mで完全に決まります。

n = (線分の個数), m = (円周の個数) に対して制限を付けます。すると、タングルの特殊ケースが定義できることになります。

  1. n = 0, m = 1 : ただひとつの円周S1から方体I3への写像で定義されるタングル。
  2. n = 0, m = m (制限なし) : m個の円周mS1から方体I3への写像で定義されるタングル。
  3. n = n (制限なし), m = 0 : n個の線分nIから方体I3への写像で定義されるタングル、ただし、天井から床に向かう紐しか認めない。

上記の特殊なタングルには名前が付いていて、次のように呼びます。

  1. 結び目(knot)
  2. 絡み目(link)
  3. ブレイド(braid)

ブレイドだけを相手にしたいときは、パラメータ表示 β:nII3 をもっと制限して考えたほうが便利です。例えば:

  • 紐の境界の点を (i/(n + 1), 1/2, 1), (i/(n + 1), 1/2, 0) (i = 1, 2, ..., n)に限定する。
  • βを β(i, t) (i = 1, ..., n, 0≦ t ≦1) の形に書くとして、π3はz方向への射影として、iがなんであっても π3(β(i, t)) = t。

こうすると、tを時間パラメータと考えて、ブレイドに対する次の描像が生まれます。

  • 初めは直線状にキチンと整列していたn個の点が、2次元矩形内で互いに接触せずに動き回り、最後はまたキチンと整列する。ただし、各点がもとの位置に戻るとは限らず、入れ替わるかも知れない。

方体タングルのモノイド圏

平面の一部に描かれる円環タングルや矩形タングルは、キャンバスの貼り合わせとサイズ調整(リスケーリング)により圏になりました。矩形タングルの場合は、左右に並べて貼り合わせることによりモノイド積が定義できて、モノイド圏となるのでした。

方体タングル(クラス)の全体もモノイド圏になります。モノイド圏の構造を与える方法は矩形タングルのときと同じです。

  • 圏の対象はドットの集合だが、自然数と同一視する。
  • 圏の射は方体タングル(のクラス)
  • 射の域(domain)は天井に並ぶ紐の境界であるドット(結合方向が上から下とする)
  • 射の余域(codomain)は床に並ぶ紐の境界であるドット(結合方向が上から下とする)
  • 射の結合は、キャンバス方体を縦にくっつけて位置とサイズを調整する。紐もちゃんと繋ぐ。
  • 対象のモノイド積は自然数の足し算、射のモノイド積はキャンバス方体を横に並べて位置とサイズを調整する。

こうして方体タングルの全体は圏となります。結び目、絡み目、ブレイド達は、方体タングルの圏の部分圏を形成します。しかし、結び目の圏と絡み目の圏は対象が1つ(0だけ)しかなく、モノイド積と結合が一致してしまい、モノイド圏と考えてもあまり嬉しくないです。でもブレイドの圏は、モノイド圏として考えることに意味があります。

記号的モノイド圏

幾何タングルは図形的な存在なので、絵に描けるし幾何的直感で扱うこともできます。しかし、記号計算の対象にはなりません。これでは不便なので、記号的な計算体系が欲しくなります。

記号的な計算体系を作るには次のようにします。

  1. 有限個の基本記号を準備する。
  2. 基本記号を組み合わせて記号列(複合記号)を作る規則を決める。
  3. 2つの記号列が「同じ」と判定する規則を決める。

記号列のことを(word)と呼びます。基本記号から語を作る規則(文法)は次のようなものです。

  1. 空列()は語である。()を空語とも呼ぶ。
  2. 基本記号は語である。
  3. AとBが語のとき、(A*B)は語である。
  4. AとBが語のとき、(A,B)は語である。
  5. 以上により定義されたものだけが語である。

この規則のなかで使われた丸括弧、星印、カンマは、基本記号(ユーザー指定記号)とは別に最初から準備されているシステム組み込み記号です。a, bが基本記号だとすると、次のような語を作れます。

  1. ()
  2. b
  3. (a*b)
  4. ((a*b);())
  5. (((a*b);())*(b;b;()))

この定義だと圏論的議論には適さないので、もう少し構造を追加します。基本記号の集合Σに、src, trg:Σ→N という写像を付けます。語に対しても src, trg を拡張しながら語を再定義します。

  1. 空列()は語である。src(()) = 0, trg(()) = 0 。
  2. 自然数nは語である。src(n) = n, trg(n) = n 。
  3. 基本記号xは語である。src(x), trg(x) は、x∈Σ なので最初から定義されている。
  4. AとBが語のとき、(A*B)は語である。src((A*B)) = src(A) + src(B), trg((A*B)) = trg(A) + trg(B) 。
  5. AとBが語で、trg(A) = src(B) のとき、(A,B)は語である。src((A,B)) = src(A), trg((A,B)) = trg(B) 。
  6. 以上により定義されたものだけが語である。

以上のようにして定義した語の集合をWord(Σ)とします。src, trg:Σ→N を拡張した写像 src, trg:Word(Σ)→N があり、埋め込み inj:Σ→Word(Σ) もあります。Word(Σ)に適当な同値関係を入れると、Nを対象とするモノイド圏ができます。このモノイド圏はPRO(「PROと代数系 -- toward 量子と古典の物理と幾何@名古屋』参照)なので、PRO(Σ)と書くことにします。

PRO(Σ) = (N, Word(Σ)/〜, dom, cod, id, ;, ¥otimes) として、語Aの同値類を[A]と書くなら:

  • dom([A]) = src(A)
  • cod([A]) = trg(A)
  • idn = [n]
  • [A];[B] = [(A,B)]
  • [A]¥otimes[B] = [(A*B)]

Word(Σ)上の同値関係が煩雑で退屈なので省略しましたが、PRO(Σ)は、我々が厳密モノイド圏に対して行う計算を形式化した記号的体系になっており、それ自身が厳密モノイド圏です。

組み合わせブレイド

自然数を対象、幾何ブレイド(クラス)を射とするモノイド圏をBraidとします。自然数Braidの対象)nに対してエンドセットBraid(n, n)を考えると、これは圏の結合を演算として群になります。これを、n-紐のブレイド群(braid group on n-strands)、あるいはn-ブレイド群と呼びます。

n-ブレイド群は、群の生成系(system of generators)と関係系(system of relations)による表示(presentation)を持ちます。(n - 1)個の生成元 σ1, σ2, ..., σn−1 から生成された自由群を考えて、そのなかで次の関係を導入します。

  1. |i - j| ≧ 2 のとき、 σiσj = σjσi (i, j∈{1, ..., n - 1})
  2. σiσi+1σi = σi+1σiσi+1 (i∈{1, ..., n - 2})

生成系と関係系で定義した群は組み合わせブレイド群(combinatorial braid group)または代数ブレイド群(algebraic braid group)と呼びましょう。組み合わせブレイド群の要素は、σ1, σ2, ..., σn−1 という(n - 1)個の記号とその逆σi-1を何個か(重複を許す)選んで並べたもの(これをブレイド語と呼ぶ)です。ただし、逆元の性質と上記の関係で同値なものは同一視します。

幾何ブレイド群と組み合わせブレイド群は同型です。この事実はアルチン(Emil Artin)により示されました*3(アルチンの定理)。上記の関係式はアルチン関係(Artin relations)と呼ばれます。2番目のアルチン関係は、幾何ブレイドのライデマイスター移動III番に対応します。

ブレイド群はブレイドの圏のエンドセットを取り出したものです。ブレイドの圏全体を組み合わせ的に(生成系と関係系により)定義できないでしょうか。これはアルチンの定理とほぼ同じように示せます。

  • Σ = {b, b'} を基本記号の集合とする。
  • src(b) = trg(b) = 2, src(b') = trg(b') = 2 とする。
  • 基本記号の集合Σから厳密モノイド圏PRO(Σ)を作る。
  • PRO(Σ)にアルチン関係と同様な関係を入れる。

PRO(Σ)に入れる関係は:

  • (b,b') = (b',b) = 2 (bとb'は互いに逆)
  • ((b*1),(1*b),(b*1)) = ((1*b),(b*1),(1*b)) (ライデマイスター移動III)

圏論の標準記法でもっと分かりやすく書けば:

  • b;b' = b';b = id2
  • (b¥otimesid1);(id1¥otimesb);(b¥otimesid1) = (id1¥otimesb);(b¥otimesid1);(id1¥otimesb)

“幾何ブレイドの圏”と“組み合わせブレイドの圏”を区別しないのは、アルチンの定理の圏論*4があるからです。つまり、次が成立します。

  • 幾何ブレイドの圏と組み合わせブレイドの圏のあいだには、対象類(N)上で恒等で可逆な厳密モノイド関手が存在する。

これは具体的で強い結果ですが、もっとザックリ言えば:

  • 幾何ブレイドの圏と組み合わせブレイドの圏は、モノイド圏として同値である。

幾何ブレイドの圏と組み合わせブレイドの圏は、モノイド圏としての構造からは区別できません。そして実際に、ほとんどの場合区別していません。

タングルの圏の公理的な特徴付け

モノイド圏にブレイド構造を入れたものとしてブレイド付きモノイド圏(braided monoidal category)があります。ブレイド付きモノイド圏の概念を使うと、ブレイドの圏は、単一の対象(1個の点)から生成されたブレイド付き厳密モノイド圏として特徴付けられます。別な言い方をすると、ブレイドの圏は「一番簡単なブレイド付きモノイド圏」です。

同様に、タングルの圏やその部分圏、変種の圏などを「一番簡単なナントカ圏」として特徴付けられないでしょうか? この問に答えるのはなかなかに面倒な話です。完成度の高い結果として、シャム(Mei Chee Shum*5)の定理をザッと紹介します。

太さも幅も持たない紐の代わりに幅を持つ帯を使ったタングルを考えます。幅を持ったタングルを枠付きタングル(framed tangle)と呼びます。「枠」とは、向き付き曲線の接ベクトルと接ベクトルに直交する法ベクトル、接ベクトル×法ベクトルというベクトル積で作られる3次元座標系に起因します。ただし、向きも接ベクトルも考えなくても、枠付きタングルの圏を幅(区間との直積)だけで定義できます。パラメータ空間のあいだの同型や、方体のなかでのアンビエント・イソトピーを使って同値関係を入れるのも同じです。

一方、モノイド圏に構造を付けたものとしてリボン圏ribbon category, a.k.a tortile category)があります。名前から、幅付き紐の公理化であろうと想像できます。シャムの定理は、この想像が当たりであることを教えてくれます。

  • 単一の対象から生成されたリボン圏は、枠付きタングルの圏とモノイド圏として同値である。

これは、アルチンの定理の圏論的な発展形と捉えることができます。

もつれを整理すると

タングルやブレイドを素材とする圏、あるいはそれらを公理化した圏(の種別)はたくさんあります。

  • ブレイド付きモノイド圏(braided monoidal category)
  • 対称モノイド圏(symmettric monoidal category)
  • トレース付きブレイド付きモノイド圏(traced braided monoidal category)
  • トレース付き対称モノイド圏(traced symmetric monoidal category)
  • バランス(ひねり)付きモノイド圏(blanced monoidal category)
  • 自律圏(autonomous category)
  • 旋回圏(pivotal category)
  • コンパクト閉圏(compact closed category)
  • リボン圏(ribbon category, tortile category)
  • ...

あまりに色々ありすぎてウンザリします。

セリンガーがこれらを整理するレポートを書いています。

モノイド圏の博物学という感じもしますが、一種のモデル理論と捉えることができます。記号的な定義が構文論で、幾何的な定義が意味論です。アルチンの定理やシャムの定理は、構文的定義と意味的定義の一致を主張しているので完全性定理です。

この種の完全性定理は、“テキスト=記号表現”と“絵=幾何表現”の関係を示しています。テキストと絵の関係を調べることは、証明やコミュニケーションのスタイルを変革する基盤形成になるかも知れません。

*1:画像は http://missanga.seesaa.net/article/21655811.html より

*2同相写像でも扱いが面倒なので、φtはH0, H1を動かさない、あるいはもっと強く、方体の境界は動かさないことにしてもいいです。

*3:アルチンの原論文(1946)がインターネット上にあります。http://www.maths.ed.ac.uk/~aar/papers/artinbraids.pdf 。同名(Theory of braids = Theorie der Zöpfe)のドイツ語論文は、それより20年も前の1926年に出ているようです。

*4圏論版アルチンの定理をハッキリと述べたのはジョイアル/ストリート(Andre Joyal, Ross Street)らしいです。知っていた人はたくさんいるでしょうが。

*5:Mei-Chi Shum という表記もありますが、本人による表記はCheeです。ちなみにMei Chee Shumは女性で、現在は保険会社の幹部です。

2017-06-06 (火)

滝沢カレンさんの言語芸術 その3

| 12:56 | 滝沢カレンさんの言語芸術 その3を含むブックマーク

滝沢カレンさんの言語芸術 その2」で、滝沢カレンさんのインスタグラムを紹介しました。

このインスタグラムから、滝沢さんの長文コメントを12個抜粋した紹介記事があります。

↑この抜粋だけでも、滝沢さん独自の言語世界をうかがい知ることは出来るでしょう。

最初に引用されている滝沢コメントに「国語はなんせ学生時代一番好きな学業だった」とありますが、他でも「子供の頃から読書も文章を書くことも好きだった」旨語っているので、書くことは苦ではないのでしょう。写真にコメントというより、もはや執筆活動です。

滝沢さんの日本語が「わざとだ」という可能性は非常に低いだろうと「滝沢カレンさんの言語芸術 その2」で書きましたが、別な見解として彼女は「言語障害ではないか?」と言う人もいます。「障害」を「常識的な範囲を逸脱している」という意味で使っているなら、「異能」とか「天才」と言い換えても差し支えないでしょう。ともかくも、良くも悪くも、あの語の組み合わせ方と造語のセンスは常人のものではないです。

情報伝達の機能性からは褒められた文章じゃないですが、これはやはり一種の芸(芸術 and/or 芸能)と見るべき言語表現のように思えます。

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

2017-06-05 (月)

単純平面タングルとカウフマン図のキャンバス・基準点について

| 12:40 | 単純平面タングルとカウフマン図のキャンバス・基準点についてを含むブックマーク

僕は、圏の具体例として、テンパリー/リーブ圏TLや平面単純タングルの圏SPTを出すことが多いです。例えば、2008年に書いた「圏論勉強会:3点テンパリー/リーブ代数の掛け算九九」はテンパリー/リーブ圏TLのホムセットTL(3, 3)の話です。2009年のモニャドセミナー「モニャドセミナー2の資料やら補足やらナニヤラ」のホワイトボード写真は、“単純平面タングル=SPTの射”の絵です。

テンパリー/リーブ圏TLや平面単純タングルの圏SPTをよく知っているわけではななくて(僕、よく知らないです)、「圏の対象=集合、圏の射=写像」という誤った思い込みをしないように、紐模様を射とする圏を例に出しています。

TLSPTの射は模様(絵柄)なので、キャンバスに描きます。キャンバスは2次元の領域です。キャンバスには基準点(マーク)が付いているのですが、この基準点のことを忘れてしまうと混乱します。つうか、僕自身が基準点を忘れて、アレレ?な状況になったので、キャンバスと基準点のことを確認しておきます。

内容:

  1. 絵の引用元
  2. 平面タングル
  3. 平面タングルの結合
  4. 矩形タングルと円環タングル
  5. 単純平面タングルの切り開き

絵の引用元

次の3つの論文に掲載されている絵を引用します。

上から順にJones-1999, Henriques-Penneys-Tener-2016, Penneys-2009と略称します。

平面タングル

平面タングル(planar tangle)の実例を出します。下は、Jones-1999にある絵です。

平面内に大きな(つっても大きさはテキトー)な円を描いて、その大きな円板(big disk)から幾つかの小さな円板(little disks)をくり抜きます。穴あきの円板がキャンバスです。上の実例では、小さな円板(穴)がD1からD7の7個あります。外側の大きな円板を入れると全部で8個の円板があります。

それぞれの円板(大小の円板すべて)に星印が1個ずつ付随しています。8個の星印がありますね。これが基準点(マーク)です。絵の描き方としては、星を円周上に乗せたほうが、「円板←→星」の対応関係がハッキリすると思います。

模様(絵柄)は、紐と影(shade)です。今回の話題はキャンバスと基準点なので、模様について詳しくは述べませんが、影のないバージョンがあることを注意しておきます。次の絵は、ジョーンズ(Vaughan F.R. Jones)の講義資料(https://math.berkeley.edu/~vfr/VANDERBILT/pl21.pdf)からの引用ですが、影はありません。基準点は星印じゃなくてドルマークになっています。それと、紐が触ってない穴に基準点(ドルマーク)がないですが、描いておいたほうが整合性が取れるでしょう(使わないので描いてないのですが、描いて悪いことはありません)。

平面タングルの結合

平面タングルの結合(composition)は、通常の圏の結合より少し複雑でオペラッド結合(operadic composition)と呼ばれるやり方をします。絵を見てもらったほうが早いでしょう。再び、Jones-1999にある絵を引用します。

T¥circ2S の'¥circ'は反図式順(anti-diagrammatic order)の結合記号です。下付きの2は、Tの2番めの穴D2を使うことを示しています。つまり、Tの2番めの穴にSを縮小してピタッとはめ込むのです。そのとき穴(小さな円板)D2の基準点とS(の大きな円板)の基準点を合わせます。

基準点は、結合の“位置合わせ”のためにあったのです。基準点どうしが重なるだけでなく、模様もズレなくきれいにつながる必要があります。調整のためにトポロジカルな変形*1は自由にしてかまいません。

別な絵も見てみましょう。Henriques-Penneys-Tener-2016からの引用です。模様は影なしで、基準点は赤丸で表示してあります。これは分かりやすい絵ですね。結合結果では、穴のリナンバリング「右側1→2, 右側2→3」がされていることに注意してください。

さらにもうひとつ。Penneys-2009からの引用。穴がひとつだけの例です。穴がひとつだけの平面タングルに限れば、普通の圏の結合と同じように結合できます。

矩形タングルと円環タングル

平面タングルは、穴あき円板に描かれた模様です -- キャンバスが穴あき円板なのです。穴がひとつの穴あき円板は円環(annulus)と呼びます。円環をキャンバスとする平面タングルは円環タングル(annular tangle)と呼びます。前節最後の絵は、円環タングルの結合の絵です。

円板ではなくて矩形(rectangle)をキャンバスとする平面タングルは矩形タングル(rectangular tangle)です。矩形タングルの紐は、左右の辺を突き抜けたり左右の辺に触ったりはできません。紐は、上の辺と下の辺に乗っている点を繋ぐだけです。

矩形タングルと円環タングルは次のようにして対応付けできます。(Penneys-2009からの引用)

これは、矩形の左右の辺を糊付けしていったん円筒を作り、その円筒をベチャッと潰して、平面内に押し込んだと考えるといいでしょう。上の図では、矩形の上の辺が外側の円に対応しています。また、矩形の左の辺が、円環内の点線で描かれた線に対応しします。

矩形タングルの影無しのバージョンは、テンパリー/リーブ図(Temperley-Lieb diagram)、またはカウフマン図(Kauffman diagram)と呼びます。次の絵はFrederick M. GoodmanとHans Wenzlの短めの解説 http://www.math.ucsd.edu/~hwenzl/miknot.pdf からの引用です -- 影がないテンパリー/リーブ図(カウフマン図)ですね。

テンパリー/リーブ代数の発見者はテンパリーとリーブですが、図と圏による定式化はカウフマンによるものです。テンパリー/リーブ/カウフマン図という長ったらしい名前を使うと公平でいいかも知れません。

“影なし矩形タングル=テンパリー/リーブ/カウフマン図”を、適当なスカラー係数で線形結合した“ベクトル”達で張られる圏がテンパリー/リーブ圏(Temperley-Lieb category)です。スカラー係数を考えない圏のほうを、僕はカウフマン圏(Kauffman category)と呼んでいます。詳しくは、「テンパリー/リーブ圏とカウフマンのスケイン関係式」を参照してください。テンパリー/リーブ圏とカウフマン圏は大差ないので、神経質に区別しなくてもいいかも知れませんけどね。

円環タングルの影無しのバージョンのほうは、僕は単純平面タングルと呼んでいます。したがって、“影なし円環タングル=単純平面タングル”を射とする圏が単純平面タングルの圏(category of simple planar tangles)となります。

「矩形タングル→円環タングル」という対応の影なしバージョンを考えれば、カウフマン圏(線形構造を持たないテンパリー/リーブ圏)は、単純平面タングルの圏に埋め込むことができます。図のなかに生じるサークル(ループ)を処理するためにモノイド係数を考えることがあります。それについては、「テンパリー/リーブ圏とカウフマンのスケイン関係式」に書いてあります。

単純平面タングルの切り開き

カウフマン圏をKaufとします(テンパリー/リーブ圏TLと大差ないです)。単純平面タングルの圏をSPTとします。前節の議論から、KaufSPT という関手があります。モノイド係数を考えるならば、モノイドMとMの要素δを指定して Kauf(M, δ)SPT(M, δ) ですが、細かいことは気にしないことにします。(気になるなら「テンパリー/リーブ圏とカウフマンのスケイン関係式」参照。)

埋め込み関手 KaufSPT は可逆でしょうか? 別な言い方をすると、任意の単純平面タングルに対して、対応するカウフマン図(=影なし矩形タングル)があるでしょうか? この対応において、単純平面タングルの2個の基準点を繋ぐ線(模様の紐ではない)が、カウフマン図の左のキャンバス境界辺に対応しなくてはなりません。これは、円環を基準点を繋ぐ線に沿って切り開いて、トポロジカルな変形をしてカウフマン図(影なし矩形タングル)にできるか? という問題になります。

単純平面タングルの切り開きは一般的には無理です。紐が一本だけのケースでも切り開けない単純平面タングルがあります。

左の単純平面タングルは点線で切り開いてカウフマン図にできますが、右の単純平面タングルは切り開くときに紐も切ってしまうのでカウフマン図にはなりません。これで、SPTKaufより大きいことが分かりました。実際のところSPTKaufより格段に複雑です。

*1[追記]「トポロジカルな変形」とは言っても、連続な可逆写像なら何でも使っていいことにはなりません。例えば、鏡に写った形にひっくり返す変換(鏡映)はできません。ここの「トポロジカルな変形」は、アンビエントイソトピー(ambient isotopy)と呼ばれる変形のことです。[/追記]

2017-06-01 (木)

電卓のパーセントキーってムチャクチャじゃん

| 16:02 | 電卓のパーセントキーってムチャクチャじゃんを含むブックマーク

ハードウェアの電卓って、機種によって違うかも知れないけど、1 + 2 × 3 と打つと 9 になっちゃいますよね。あれイヤ。でも、ハードウェアの電卓を持ち歩くことなんてなくて、僕はiPhone付属の電卓アプリを使います。電卓アプリでは、イコールキーを打つまでは計算式を内部に保存するので、足し算・掛け算の優先順位はちゃんと認識します。つまり:

  • 入力「1 + 2 × 3 =」で答は 7

入力した式を常識的に解釈してくれるんだ、と安心(?)してたんですが、奇妙な挙動が:

  • 入力「50 % + 50 % =」で答は 0.75

%は、優先度が最も高い「1/100を掛ける」オペレータとして解釈して

  • 50×(1/100) + 50×(1/100)

を計算してくれるかと思ったら、違う!

いろいろやってみると、アプリがパーセントを受け取ると内部の計算式を変更してしまうようです。%の直前の演算が×か÷のときは、特に何もしないのですが、%の直前の演算が+か-のときは、次のような解釈をします。

  • %の直前の演算が+の場合、入力列が A + x % であるとき、A + A×(x/100) を計算する。
  • %の直前の演算が-の場合、入力列が A - x % であるとき、A - A×(x/100) を計算する。

50 % + 50 % ならば、(50 %) + (50 %)×(50/100) = 0.5 + 0.5×0.5 = 0.5 + 0.25 = 0.75 だったのです。

掛け算を先にするという規則と、パーセントによる式変形効果はどういう関係でしょうか?

  1. 100 + 30 % × 2 = 160
  2. 100 + 2 × 30 % = 100.6

一番目は、掛け算優先により 30%×2 = 60% が計算されて、100 + 60 % ⇒ 100 + 100×60% の変形が施された後に評価(evaluate)されて160です。

二番目は違うようです。2 × 30 % を先に見ますが、%の直前が×なので、%の特殊効果が殺されて、2×(30/100) という単なる数(変形効果なし)に退化します。100 + 2×(30/100) が評価されて100.6。

ウワーーッ、ナンダこの変な仕様は? ヤダなー、もう。


手元のハードウェア電卓、CASIO MW-12Aというヤツですが、これで試してみます。

  • 100 + 50 % = 200
  • 100 - 50 % = 100

ハァーー??

パーセントキーは1/100という単純な意味ではなくて、事前の入力の意味を変える修飾キーなんですね。その直前に打った演算キーとパーセントキーのコンボで、特定の関数をトリガーする仕掛けのようです。

  • x + y % は f(x, y) という関数呼び出しに変形される。ここで、f(x, y) = x/(1 - y/100)
  • x - y % は g(x, y) という関数呼び出しに変形される。ここで、g(x, y) = 100*(x - y)/y

「+ y %」という打鍵列は、λx.(x/(1 - y/100)) という関数を意味します。「x + y %」では、既に打鍵され評価されている値xに、この関数が適用されるわけです。「- y %」, 「x - y %」の解釈も同様です。

  • 「100 + 20 %」 = 100/(1 - 20/100) = 100/0.8 = 125
  • 「100 - 20 %」 = 100*(100 - 20)/20 = 100*80/20 = 400

%でトリガーされる関数fとgは、次の用途から選ばれたようです。

  • f: 原価をx円として、売値に対する利益率をyパーセントとするときの、売値を求める関数
  • g: 売値をx円、原価をy円とするとき、原価に対する利益率のパーセント値を求める関数
  • gの別解釈: 値引き後売値をx円、元売値をy円とするとき、値引き率のパーセント値を求める関数

ウゲーッ。制限されたインターフェイスで苦し紛れに考えた出された歪んだ仕様ですね。ハードウェアに拘らなければ素直でまともな入力形式を使えるのだから、ソフトウェア実装では、こんな奇妙な機能は無意味だよな …… んっ、その無意味な知識を僕は調べたんだな …… アーアッ。

[追記]

変な仕様を擁護する理由としてひとつ思い付いたことは、消費税計算。3000円の商品の税込み価格が、「3000 + 8 %」で計算できます。「3000円に8%増し」という日本語表現とも相性がいいし。

カシオ電卓だと、「3000 + 8 %」の意味は「原価を3000円として、売値に対する利益率を8パーセントとするときの売値」なので、3260.86… という結果。代わりに、1.08を掛ける演算としてズバリ[税込み]ボタンがあります。

まーいずれにしても、入力シーケンスの特定のコンビネーションに例外的な意味を持たせるアプローチは、整合性がなく記憶負担を強いるので、僕は大嫌いです。

[/追記]

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

2017-05-31 (水)

Scilabの演算子オーバーロード

| 12:03 | Scilabの演算子オーバーロードを含むブックマーク

Scilabでは演算子オーバーロードができます。そのメカニズムは原始的ですが、素朴で分かりやすいとも言えます。Scilabに興味がなくても、オーバーロードに興味がある方には面白い話だと思います。


Scilabはたくさんの演算子記号を持っています。それらの演算子記号の意味を、ユーザーは拡張することができます。論理否定演算子「~」を例にしましょう。

--> ~%T
 ans  =

  F


--> ~0
 ans  =

  T


--> ~"hello"

指定したオペランド用の演算子が未定義です.
オーバーロード用の関数 %c_5 を確認または定義してください.

%T(真を表す定数)の論理否定はF(偽)です。論理否定演算子「~」は数値0に対しても使えて、0の否定はT(真)となります。しかし、論理否定演算子「~」を文字列には使えません

文字列"hello"の否定に対してエラーメッセージが出てますが、このエラーメッセージが演算子オーバーロードに対する適切なアドバイスになっています。関数 %c_5 を定義すればオーバーロードができるのです。

と言ってもまだ謎ですよね。説明しましょう。Scilabの式に演算子が出現した場合、Scilab組み込み演算子と解釈できるなら何ら問題はありません。そうでないとき、Scilabインタプリタは演算子に対応するユーザー定義関数を探すのです。対応する関数が見つかればそれを実行します。

演算子に対応する関数の名前は前もって約束されています。ネーミングルールがあるのです。そのルールは help overloading コマンドで見ることができます。インターネット上なら https://help.scilab.org/docs/6.0.0/en_US/overloading.html です。

まず、演算子記号には、英数字1文字の“コード”が決まっています。overloadingヘルプに記号とコードの対応表がありますが、最初の幾つかを挙げると:

演算子記号 コード
' t
+ a
- s
* m
/ r

記号コードだけでは不十分で、データ型もコード化する必要があります。実際、型コードも決まっています。型コードは1文字から4文字の英字です。またヘルプから最初の幾つかを挙げると:

データ型 コード
数値行列 s
多項式行列 p
論理値行列 b
疎行列 sp

記号コードと型コードの組み合わせ方のルールは以下のとおりです。

  • 単項演算子に対応する関数名: %型コード_記号コード
  • 二項演算子に対応する関数名: %型コード_記号コード_型コード

論理否定演算子を文字列データに対して定義したいならば:

  • %文字列の型コード_論理否定の記号コード

という名前の関数を定義します。ヘルプで調べれば分かりますが、先のエラーメッセージに、

  • オーバーロード用の関数 %c_5 を確認または定義してください.

とありました。これを見ればすぐに分かります。

  • 文字列の型コードは c
  • 論理否定の記号コード 5

ではさっそく関数 %c_5 を定義してみます。

function ret = %c_5(str)
    ret = strrev(str) // 文字列をひっくり返す
endfunction

関数 %c_5 を定義した後では、

--> ~"hello"
 ans  =

 olleh


--> ~"live"
 ans  =

 evil

「~」演算子が文字列をひっくり返す演算として使えるようになりました。回文のチェックに使えます、日本語もOK。

--> ~"madam Im adam"
 ans  =

 mada mI madam


--> ~"たけやぶやけた"
 ans  =

 たけやぶやけた


二項演算子もやってみます。

--> "hello"*5

指定したオペランド用の演算子が未定義です.
オーバーロード用の関数 %c_m_s を確認または定義してください.

もうお分かりですね。

  • 文字列の型コードは c
  • 乗法の記号コード m
  • 数値の型コードは s

なので、文字列と数値を引数に取る関数 %c_m_s を定義すればいいわけです。

function ret = %c_m_s(str, n)
    ret = ''
    for i=1:n do
        ret = ret + str
    end
endfunction
--> "hello"*5
 ans  =

 hellohellohellohellohello


--> "イヤ"*2
 ans  =

 イヤイヤ

文字列を指定回数だけ繰り返す演算子「*」が定義できました。

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

2017-05-29 (月)

Scilabで行列計算をしてみる

| 10:13 | Scilabで行列計算をしてみるを含むブックマーク

今までR言語で行列計算してたんですが、Scilabに替えてみました。行列計算に限れば、Scilabのほうがずっと使い勝手がいいです。

  1. R言語には不満が募ってきた
  2. Scilab
  3. Scilabコンソール
  4. 行列計算をはじめる
  5. 行列のブロック操作と寸法
  6. 成分と部分行列の取り出し
  7. インデックス・アクセスと関数呼び出し
  8. 逆行列行列式
  9. おわりに

R言語には不満が募ってきた

数値的行列計算が必要なとき僕は、R言語を使っていました。Rコンソールを立ち上げれば、その場ですぐ計算できるので便利ではあるのですが、いくつか不満もあります。

  1. 行列を直接表現するリテラル表記がなくて、matrix(c(1, 3, 2, 4), 2, 2) のような関数呼び出しが必要でうっとうしい。
  2. 行列の掛け算記号が %*% 。基本演算子が3打鍵必要なのがイヤ。
  3. 行列のブロック操作がサクサクできないのでフラストレーションを感じる。

ここでRの悪口を言っても生産的ではないので詳細は書きませんが、3番目の不満が意味不明でしょうから説明します。「行列のブロック操作」と書きましたが、正式になんと言うのか知りません。例示するなら、

A = ¥begin{bmatrix}1 & 2 ¥¥ 3 & 4¥end{bmatrix} ¥¥B = ¥begin{bmatrix}5 & 6 ¥¥ 7 & 8¥end{bmatrix}

という行列A, Bがあったとき、例えばAとBを対角位置に並べてCを作る操作とかです。

C = ¥begin{bmatrix}A & O ¥¥ O & B¥end{bmatrix} = ¥begin{bmatrix}1 & 2 & 0 & 0 ¥¥3 & 4 & 0 & 0 ¥¥0 & 0 & 5 & 6 ¥¥0 & 0 & 7 & 8 ¥end{bmatrix}

もっと簡単な例だと:

X = ¥begin{bmatrix}1 ¥¥ 2 ¥end{bmatrix} ¥¥Y = ¥begin{bmatrix}3 ¥¥ 4¥end{bmatrix} ¥¥Z = ¥begin{bmatrix}X & Y ¥end{bmatrix}  = ¥begin{bmatrix} 1 && 3 ¥¥ 2 && 4 ¥end{bmatrix}

Scilab

ちょっと調べてみて、Scilab(サイラボ)がヨサゲな印象でした。Scilabのホームページは:

https://www.scilab.org/download/latestから各プラットフォームごとのインストール用アーカイブ(バイナリ配布物)をダウンロードできます。現時点(2017年春)での最新バージョンは Scilab 6.0.0 です。インストールは簡単です、特に説明することはないです。

https://www.scilab.org/resources/documentation/tutorials から、日本語PDF文書Scilab_beginners_jp.pdf(はじめてのScilab -- 33ページ)、Xcos_beginners_jp.pdf(はじめてのXcos -- 15ページ)をダウンロードできます。もう少し詳しい解説はintroscilab.pdf(INTRODUCTION TO SCILAB -- 87ページ)。文書は若干古めで、最新バージョンとはズレがあります。が、深刻な問題にはならないでしょう。

ソフトウェアに付属のヘルプも日本語化されていて(見出しは英語のまま)、かなり充実しています。ブラウザでマニュアルを見たいなら、インターネット上のページがあります。

ソフトウェア付属のヘルプとWebオンラインマニュアルは、最新バージョンの情報だと期待してよさそうです。

どうでもいいことですが、Scilabのlabを「ラボ」と読むのは「ラボラトリー(laboratory)」の略だという前提があるからで、labだけなら「ラブ」に近いと思うのだけど…。僕は「サイラブ」と読んで(呼んで)しまいますね。

[追記]次のサイトに、日本語を含む多言語による情報があります。

機械翻訳を使っているのか? 日本語の品質はよくありません。何言ってるのかワケワカンナイことがあるので注意してください。

[/追記]

Scilabコンソール

Scilabをインストールしたら起動します。初期状態では、メインウィンドウ内にいくつかのサブウィンドウが詰め込まれた最近のIDEっぽい外観です。ゴチャゴチャしていてい僕は好きじゃないのですが、カスタマイズとかは後回しにしてスーパー電卓(a super desktop calculator)*1としてScilabを使ってみます。

Scilab 6.0.0 コンソール」(日本語UI)とタイトルされたペイン(サブウィンドウ)がScilabコンソールです。このコンソールが対話的インタプリタのコマンドラインインターフェイスです。今回はScilabコンソールしか使いません。

「-->」がインタプリタのプロンプトマークで、この後にキーボード入力して、Enter/Returnキーを押せばScilabインタプリタが応答を返します。

--> disp("Hello, world")

 Hello, world


--> 1 + 2
 ans  =

   3.


--> x = 1 + 2
 x  =

   3.


--> y = x*2 + 1
 y  =

   7.


--> sqrt(y) // yの平方根
 ans  =

   2.6457513

1行目のdisp()はプリント用関数です。1 + 2 のような計算式を入力すれば結果が表示されますが、その結果はansという変数に代入されます。ただし、明示的な代入文を書けば(x = 1 + 2)、ansへの自動代入はされません。計算は倍精度浮動小数点数(64ビット実数)で行われ、値がちょうど整数でも小数点は表示されます*2。関数呼び出しは、たいていのプログラミング言語と同じ func(arg) の形です。スラッシュ2個から行末まではコメントです。

行列計算をはじめる

Scilabでは、行列を非常に分かりやすい形式で入力できます。1行分のデータはカンマか空白で区切り、次の行に移るにはセミコロンを使います。

--> [1, 2; 3, 4]
 ans  =

   1.   2.
   3.   4.


--> [1 2; 3 4] // カンマの代わりに空白でもよい
 ans  =

   1.   2.
   3.   4.


--> a = [1 2; 3 4] // 行列を変数に代入
 a  =

   1.   2.
   3.   4.

行列の掛け算はアスタリスク1文字です。加減はもちろんプラスとマイナス。

--> b = [5 6; 7 8]
 b  =

   5.   6.
   7.   8.


--> a*b
 ans  =

   19.   22.
   43.   50.


--> a + b
 ans  =

   6.    8.
   10.   12.


--> a - b
 ans  =

  -4.  -4.
  -4.  -4.

スカラー倍もアスタリスクです。

--> 2*a
 ans  =

   2.   4.
   6.   8.


--> a*-1
 ans  =

  -1.  -2.
  -3.  -4.

Scilabにベクトル型データはありません*3が、1行n列-行列かn行1列-行列でベクトルを表現できます。どっちにするかは「決め」(約束)の問題です。例えば、ベクトルをn行1列-行列=列ベクトルで表現するとして、行列とベクトルの積は次のようです。

--> a*[2; -1]
 ans  =

   0.
   2.


--> b*[2; -1]
 ans  =

   4.
   6.

行列の転置(縦と横の入れ替え)は、'(シングルクォート)を後置します*4

--> a'
 ans  =

   1.   3.
   2.   4.


--> [2; -1]'
 ans  =

   2.  -1.

ベクトルの内積は転置して掛ければいいので:

--> x = [2; -1]; y = [5; 3]; // 2つの代入文を行って、結果の表示は行わない

--> x'*y // ベクトルxとyの内積
 ans  =

   7.

行列のブロック操作と寸法

特別な行列を表現する関数が用意されています。対角成分が1で他は0である行列は eye(行数, 列数) で、すべての成分が0である行列は zeros(行数, 列数) で作れます。

--> eye(2, 2)
 ans  =

   1.   0.
   0.   1.


--> eye(3, 2)
 ans  =

   1.   0.
   0.   1.
   0.   0.


--> zeros(3, 2)
 ans  =

   0.   0.
   0.   0.
   0.   0.

冒頭に挙げたブロック操作をやってみます。

--> a
 a  =

   1.   2.
   3.   4.


--> b
 b  =

   5.   6.
   7.   8.


--> o = zeros(2, 2)
 o  =

   0.   0.
   0.   0.


--> c = [a o; o b]
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> x = [1; 2]; y = [3; 4];

--> z = [x y]
 z  =

   1.   3.
   2.   4.

簡単でしょ。

行列の行数と列数が欲しいときはsize()関数、成分の個数が欲しいときはlength()関数を使います。

--> size(c)
 ans  =

   4.   4.


--> length(c)
 ans  =

   16.


--> size([1; 2])
 ans  =

   2.   1.


--> size([1; 2]')
 ans  =

   1.   2.


--> length([1; 2])
 ans  =

   2.

成分と部分行列の取り出し

多くのプログラミング言語では、配列、リスト、タプル、ベクトル、行列などの成分(要素、項目)を取り出すにはブラケットを使って、x[2], a[1, 2] のように書きます。Scilibでは、丸括弧で x(2), a(1, 2) のように書きます。

--> x
 x  =

   1.
   2.


--> x(1)
 ans  =

   1.


--> a
 a  =

   1.   2.
   3.   4.


--> a(1, 2)
 ans  =

   2.

関数呼び出しと区別が付かなくて困らないか? 困りません。それどころか、区別が付かないのでかえって便利です、後で例を挙げます。JVM上で動く関数型言語Scalaでは、やはりインデックス・アクセスと関数呼び出しが同じ形式ですね。

次に、行列の単一成分に限らず、いくつかの成分をまとめて取り出してみます。そのために範囲記法を説明しておくと、n:m で「nからmまでの整数範囲」*5を意味します。

--> 0:3
 ans  =

   0.   1.   2.   3.


--> 1:10
 ans  =

   1.   2.   3.   4.   5.   6.   7.   8.   9.   10.

範囲の実体は横ベクトル(1行n列の行列)です。この範囲記法を使うと、行列の一部を素早く抜き出せます。

--> c
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> c(1:4, 2:3)
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c([1 2 3 4], [2 3])
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c([2 3], [2 3])
 ans  =

   4.   0.
   0.   5.

範囲は横ベクトルなので、直接横ベクトルを書いても同じです -- 長い範囲だと直接書くのはシンドイですがね。範囲を示すコロンの特別な用法として、次のような書き方ができます。

--> c(:, [2, 3])
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c(:, 2)
 ans  =

   2.
   4.
   0.
   0.


--> c(1, :)
 ans  =

   1.   2.   0.   0.

コロンだけだと、その行列が持つ行範囲、列範囲になるのです。行列のサイズを意識せずに「行全部/列全部」を指定できるので便利です。

抜き出す部分は、範囲では記述できないパランパランな部分でもいいです。

--> c
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> c(:, [1 4])
 ans  =

   1.   0.
   3.   0.
   0.   6.
   0.   8.

インデックス・アクセスと関数呼び出し

前節で、「インデックス・アクセスと関数呼び出しを区別しないほうが便利だ」と書きました。実例を挙げましょう。

整数引数の関数fと、整数n, m(n≦m)に関して次の総和を考えます。

 ¥sum_{i = n}^{m} f(i)

これを、関数f, 整数n, mを引数とする関数(高階関数)と考えて、

 total(f,¥, n,¥, m) ¥: := ¥sum_{i = n}^{m} f(i)

としましょう。これをScilabの関数で書くと次のようになります。プログラムとして見やすいように、f→fun、n→from、m→to とリネームしています。

function ret = total(fun, from, to)
    ret = 0
    for i = from:to do
        ret = ret + fun(i)
    end
endfunction

Scilabの関数定義構文の説明はしませんが、何となくは分かるでしょう。

さて、奇数の総和は平方数になるという事実があります。

 ¥sum_{i = 1}^{n} 2n - 1 ¥: = ¥: n^2

この事実を関数total()を使って確認してみます。

--> function ret = odd(n)
  >     ret = 2*n - 1
  > endfunction

--> odd(1)
 ans  =

   1.


--> total(odd, 1, 4)
 ans  =

   16.


--> total(odd, 1, 5)
 ans  =

   25.

関数odd()を定義して、関数(高階関数)total()に渡したのですが、奇数の列は別に関数でなくてもかまいません。

--> 1:2:9
 ans  =

   1.   3.   5.   7.   9.


--> total(1:2:9, 1, 4)
 ans  =

   16.


--> total(1:2:9, 1, 5)
 ans  =

   25.

ここで、1:2:9は範囲(実体は行ベクトル)ですが、1から2ずつ増加して9に至る整数並びです。

関数も行ベクトル(あるいは列ベクトル)も同じ形式でアクセスできるので、total()の第1引数は関数でもベクトル(特殊な行列)でもいいのです。計算手順とデータを統一的に扱えて便利です。

逆行列行列式

行列Aの逆行列はA-1と書きます。この書き方にならって、Sailabでも a^-1 という記法で逆行列を表現できます。また、逆数と同じ 1/a でも逆行列です。


--> a
 a  =

   1.   2.
   3.   4.


--> a^-1
 ans  =

  -2.    1.
   1.5  -0.5


--> 1/a
 ans  =

  -2.    1.
   1.5  -0.5


--> a*1/a
 ans  =

   1.   0.
   0.   1.

ウーン、まーいいんですけど、僕は inv(a) という書き方が落ち着きます。


--> inv(a)
 ans  =

  -2.    1.
   1.5  -0.5


--> a*inv(a)
 ans  =

   1.          0.
   8.882D-16   1.


--> inv(a)*a
 ans  =

   1.          0.
   2.220D-16   1.

アレッ? a*inv(a)が単位行列になってませんね。2.220D-16はものすごく小さい数なので、浮動小数点数の誤差でしょうが、1/aだと正確に0だったのは不可解。ちょっと事情が分かりません。

逆行列の存在・非存在は行列式を見れば分かりますが、aの行列式はdet(a)です。

--> a
 a  =

   1.   2.
   3.   4.


--> det(a)
 ans  =

  -2.


--> inv(a)
 ans  =

  -2.    1.
   1.5  -0.5


--> det(inv(a))
 ans  =

  -0.5


--> det(a*inv(a))
 ans  =

   1.

おわりに

というわけで、Scilabだと行列計算が気持ちよく出来るよ というお話でした。

*1:"INTRODUCTION TO SCILAB"の22ページに、Scilabは"a super desktop calculator"であり、またそれ以上のものである、と書いてあります。

*2:デフォルトが実数(浮動小数点数)ですが、n = int32(10) のような型変換を使うと、適当なビット長(この場合は32ビット)の整数データを作れます。整数の10は、10. ではなくて 10 と表示されます。

*3:実は、厳密に言えばスカラー型もありません。1行1列の行列がスカラーとして扱われています。

*4:'(シングルクォート)は実際はエルミート転置(Hermitian transpose, conjugate transpose)です。単なる転置は.'(ドットとクォート)という演算子ですが、実数成分の場合は単なる転置もエルミート転置も変わりはありません。

*5:x:y という書き方の意味は、xを初項とする等差数列のyを越えない部分です。例えば、1.2:5 の値は [1.2, 2.2, 3.2, 4.2] となります。今の文脈では、初項と上限に整数値(データ型は実数)を取っているので整数範囲を表すことになっています。

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

2017-05-24 (水)

無料で入手できる本格的(紙なら高額)な理数系専門書15選 第2回(2017年春)

| 10:16 | 無料で入手できる本格的(紙なら高額)な理数系専門書15選 第2回(2017年春)を含むブックマーク

去年・2016年の夏に、「無料で入手できる本格的(紙なら高額)な理数系専門書15選」という記事でインターネットから入手可能な専門書を15冊紹介しました。

出版されている書籍と同じ内容のPDFファイルやHTMLページがインターネットに公開されている例は意外と多いみたいで、一年たたずに新しい15冊のリストができました。前回(2016年夏)と同様に、著作権があやしいものは除外し、著者本人または著者の所属組織のWebサイト、あるいはarXiv.org, TAC (Theory and Applications of Categories)で公開されているものだけを紹介します。また、この記事の後半で過去に紹介した20冊のタイトルとURLを再掲します。

  1. Differential Algebraic Topology: From Stratifolds to Exotic Spheres
  2. Lectures on the Geometry of Manifolds
  3. 3次元多様体入門
  4. Parametrized Homotopy Theory
  5. Noncommutative Geometry
  6. Category Theory in Context
  7. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist
  8. Category Theory for Computing Science
  9. Higher Operads, Higher Categories
  10. Axiomatic Method and Category Theory
  11. Practical Foundations of Mathematics
  12. Geometric Integration Theory
  13. Foundations of Algebraic Specification and Formal Software Development
  14. Stochastic Integration with Jumps
  15. Optimal transport, old and new

幾何

Differential Algebraic Topology: From Stratifolds to Exotic Spheres

著者Kreckが創始したストラティフォールドという概念をベースにした代数トポロジーの教科書です。ストラティフォールドを使うことにより、代数的不変量を幾何的に構成しています。目標は、エキゾチック7-球面の構成(19章)で、11章あたりからその準備がはじまるようです。

Lectures on the Geometry of Manifolds
Lectures On The Geometry Of Manifolds

Lectures On The Geometry Of Manifolds

初版は1996年で、それ以来メンテナンスされているようで、最新の修正は今年(2017年)です。大部な教科書で、多様体について必要なことは解析寄りのことまで、たいていのことが書いてあります。

3次元多様体入門
3次元多様体入門

3次元多様体入門

紙の本は絶版になっていて入手困難です。PDF版だけの追補もあります。他の本では書いてないような話題を扱っていて、3次元幾何の貴重な情報源です。

Parametrized Homotopy Theory

本格的なホモトピー論の教科書です。本格的過ぎて、まったく歯が立ちませんわ。パラメータ付き(parametrized)というのは、バンドルやファイバー空間のような状況を言っているようです、よく知らんけど。

最初だけ眺めると、空間のコンビニエント圏(onvenient category)の議論があります。ほかでもコンビニエント圏の話を見たので、けっこう重要な概念かもしれないです。

Noncommutative Geometry: Alain Connes
Noncommutative Geometry

Noncommutative Geometry

コンヌの非可換幾何の教科書です。翻訳本も出てます。幾何と言っても非可換幾何は、通常の幾何と相当に様子が違います。なんか物理っぽい。僕は、全体のオーバービューが書いてあるIntroductionを読んで、不思議な雰囲気を味わうだけ。

圏論

Category Theory in Context
Category Theory in Context (Aurora: Dover Modern Math Originals)

Category Theory in Context (Aurora: Dover Modern Math Originals)

気鋭の圏論家・Riehl女史による解説書。内容は標準的です。トム・レンスターの『ベーシック圏論』とマックレーンのThe Bookの中間くらいのレベルでしょうか。

Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist

このテキストは、昔、圏論勉強会で使ったことがあります。古い本で多少読みにくいかも知れません。でも、型理論、ラムダ計算、圏論の関係についてはシッカリ書いてあります。

Category Theory for Computing Science

コンピューティング・サイエンスを意識しながら圏論を丁寧に解説しています。スケッチ(sketche)の説明があるのは珍しいですね。トポスも説明されています。

Higher Operads, Higher Categories
Higher Operads, Higher Categories (London Mathematical Society Lecture Note Series)

Higher Operads, Higher Categories (London Mathematical Society Lecture Note Series)

高次圏(n-圏)の解説書です。高次圏へのアプローチは矢鱈に色々ありますが、これはオペラッドを使うものです。通常の圏も含めて予備知識も書いてあるので、高次圏の概要を知るには良い本だと思います。

Axiomatic Method and Category Theory
Axiomatic Method and Category Theory (Synthese Library)

Axiomatic Method and Category Theory (Synthese Library)

紙の初版が285ページ、改訂版で300ページですが、PDFは337ページもあります。通常の圏論の本とは毛色が違います*1。科学哲学っぽい雰囲気です。歴史や思想に興味がある人には面白いかも。

Practical Foundations of Mathematics

HTMLで提供されています。PDFに比べて視認性は悪いですが、ハイパーテキストである点は便利です。圏論の本と言っていいでしょう。圏論型理論とか圏論的論理についての解説です。

その他

Geometric Integration Theory
Geometric Integration Theory (Cornerstones)

Geometric Integration Theory (Cornerstones)

幾何積分論(幾何測度論)とは、プラトー問題などを扱う分野のようです。解析はまったく苦手なんで、コメントできません。

Foundations of Algebraic Specification and Formal Software Development

表記のURLはディレクトリインデックスです。章ごとのPDFと全体のPDFが置かれています。題名通り、一般代数(universal algebra)や形式的体系を使った仕様技術について書かれています。インスティチューションについての解説があります。例えば、大乗仏教中観派の話の予備知識が得られます。

Stochastic Integration with Jumps

紙の本とタイトルが違いますが、内容は同じようです。確率微分方程式の話、という以上のことは分かりません、あしからず。

Optimal transport, old and new

最適輸送理論(Optimal Transport Theory)とは「物質をある場所から他の場所へ最小費用で移す」理論だそうです(「最適輸送理論梗概」)。この本は、この分野の定番本みたいです。

著者のヴィラニは「数学界のレディー・ガガ」("The Lady Gaga of mathematics")と呼ばれているそうです。常にクラバットに蜘蛛のブローチという独特なファッション、なかなか強烈です。その姿と話しっぷりはTEDトークで見ることができます。

過去に言及したオンラインの専門書

無料で入手できる本格的(紙なら高額)な理数系専門書15選
  1. Algebraic Topology / Allen Hatcher
    https://www.math.cornell.edu/~hatcher/AT/ATpage.html
  2. Elementary Applied Topology / R. Ghrist
    https://www.math.upenn.edu/~ghrist/notes.html
  3. Category theory for scientists (Old version) / David I. Spivak
    http://arxiv.org/abs/1302.6946
  4. Higher Topos Theory / Jacob Lurie
    http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
  5. Tensor Categories / Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik
    http://www-math.mit.edu/~etingof/egnobookfinal.pdf
  6. Lectures on tensor categories and modular functor / Bojko Bakalov, Alexander Kirillov Jr
    http://www.math.stonybrook.edu/~kirillov/tensor/tensor.html
  7. Monoidal Functors, Species and Hopf Algebras / Marcelo Aguiar, Swapneel Mahajan
    http://www.math.cornell.edu/~maguiar/a.pdf
  8. Homotopy Theory of Higher Categories / Carlos T. Simpson
    http://arxiv.org/abs/1001.4071
  9. The Blind Spot / Jean-Yves Girard
    http://iml.univ-mrs.fr/~girard/coursang/coursang.html
  10. Bayesian Reasoning and Machine Learning / David Barber
    http://web4.cs.ucl.ac.uk/staff/D.Barber/textbook/090310.pdf
  11. An introduction to measure theory / Terence Tao
    https://terrytao.files.wordpress.com/2011/01/measure-book1.pdf
  12. Towards the mathematics of quantum field theory (An advanced course) / Frederic Paugam
    https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-mathematical-physics.pdf
  13. Eloquent JavaScript: A Modern Introduction to Programming / Marijn Haverbeke
    http://eloquentjavascript.net/Eloquent_JavaScript.pdf
  14. Advanced R / Hadley Wickham
    http://adv-r.had.co.nz/
  15. Software Engineering for Internet Applications / Eve Andersson, Philip Greenspun, and Andrew Grumet
    http://philip.greenspun.com/seia/
無料で入手できる本格的(紙なら高額)な微分幾何の専門書4選
  1. Functional Differential Geometry / Gerald Jay Sussman, Jack Wisdom, Will Farr
    https://groups.csail.mit.edu/mac/users/gjs/6946/calculus-indexed.pdf
  2. The Convenient Setting of Global Analysis / Andreas Kriegl, Peter W. Michor
    http://www.mat.univie.ac.at/~michor/apbookh-ams.pdf
  3. Synthetic Differential Geometry Second Edition / Anders Kock
    http://home.math.au.dk/kock/sdg99.pdf
  4. Synthetic Geometry of Manifolds / Anders Kock
    http://home.math.au.dk/kock/SGM-final.pdf
英語版無料PDFか、それとも日本語版商業出版物か:圏論と測度論
  1. Basic Category Theory / Tom Leinster
    https://arxiv.org/abs/1612.09375
  2. An introduction to measure theory / Terence Tao (再度)
    https://terrytao.files.wordpress.com/2011/01/measure-book1.pdf

*1:「毛色が違う」は差別表現だ、なんて言う人もいるようですが、三毛猫と黒猫は実際に毛色が違うけど、その事実を指摘すると猫に失礼なの?

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

2017-05-23 (火)

型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のために

| 11:49 | 型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のためにを含むブックマーク

型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のために」の続きです。

前回 1/2 の内容:

  1. 予備知識と参考資料
  2. 大きなラムダ計算とは何か
  3. 概要と目標
  4. 集合と写像に関する基礎的事項
  5. 型システム

今回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

疑似ラムダ項の構文

ラムダ項の構文を定義したいのですが、まずはザックリとした構文定義をします。ザックリなので、ここでの定義だけでは不十分です。ここで定義される項(構文的な表現)はちゃんとしたラムダ項ではないので疑似ラムダ項(lambda pseudoterm)と呼びます。なお、「ラムダ項」と「ラムダ式」は原則として同義語ですが、小さなラムダ式をラムダ項と呼ぶことが多いです。

変数(と呼ばれる記号)の集合をVarとします。疑似ラムダ項とは次のようなものです(帰納的な定義)。

  1. [変数] xが変数(x∈Var)ならば、x は疑似ラムダ項である。
  2. [ユニット] !は疑似ラムダ項である。
  3. [適用] E, Fが疑似ラムダ項ならば、E▷F は疑似ラムダ項である。
  4. [ペア] E, Fが疑似ラムダ項ならば、(E F) は疑似ラムダ項である。
  5. [第一成分] Eが疑似ラムダ項ならば、E_1 は疑似ラムダ項である。
  6. [第二成分] Eが疑似ラムダ項ならば、E_2 は疑似ラムダ項である。
  7. [関数抽象] xが変数、Aが型、Eが疑似ラムダ項ならば、λx:A.E は疑似ラムダ項である。
  8. [括弧] Eが疑似ラムダ項ならば、(E) (Eを括弧で囲んだ形)は疑似ラムダ項である。
  9. 以上により定義されたものだけが疑似ラムダラムダ項である。

E▷F とまったく同じ意味(別記法)で F・E も使います。'▷'と'・'で左右が逆になりますが、どっちを使うのも自由です。今後'・'を多く使うでしょうが、'▷'のほうが圏論の図式順記法や絵算との相性がいいです。

レヴィ(Paul Blain Levy)によるCBPV(Call-By-Push-Value)の項言語でも、適用の書き方は「引数 適用記号 関数」の語順です。レヴィは適用記号にバックスラッシュを使っていました。左から右にデータと制御が流れるイメージですね。「Call-By-Push-Valueの不純な関数型言語」参照。

演算子の優先順位は次のようです。演算子の優先順位に頼ると間違いを犯しやすいので、なるべく丸括弧を使いましょう。

優先順位 演算子 演算子形式 結合性 注意
1 _1, _2 後置単項 なし
2 中置二項
2 中置二項 ▷と左右が逆だが同じ
3 (- -) 中置二項 空白が演算子記号

疑似ラムダ項の例をいくつか挙げます。

  1. x
  2. x▷y
  3. y・x (x▷yと同じ)
  4. (x y)
  5. (! x)
  6. ((x y) z)
  7. x_1
  8. ((x y) z)_2
  9. f・(((x y) z)_2)
  10. λx:A.(f・(((x y) z)_2))

記号のインフォーマルな意味を説明しておきます。正式な意味論を述べるわけではなくて、心理的な納得感・安心感が目的です。

  • [ユニット] !は、単元集合1(型の記号はI)の唯一の要素を表す定数記号だと思ってください。Eが0引数関数を表すとき、E・! として評価します。実際のプログラミング言語では、ユニット定数に()を使うことが多いみたいです。
  • [適用] '▷'と'・'は適用(appとapp')を表す中置演算子記号です。'▷'の右、'・'の左に関数オブジェクト(の表現)を置きます。E▷F の値は、Eの評価結果とFの評価結果である関数オブジェクトをappに渡した結果です。適用の記号を省略することはありません
  • [ペア] 空白は関数のペアを作る中置演算子記号です。書き方はLispのリスト記法と同じです。使い方はLispのドットペア記法と同じになります。空白ペアの意味は、関数のデカルト・ペア、または関数の直積です。空白ペアがデカルトペアを表すか直積を表すかは、型証明系(後述)により変わります。
  • [第一成分][第二成分] E_1は、Eの第一成分を意味します。'_1'自体は、第一成分を取り出す後置演算子です。'_2'も同様です。
  • [関数抽象] λx:A. は、型付き変数xによる関数抽象(ラムダ抽象)で、変数xを仮引数とする関数オブジェクトを作ります。
  • [括弧] 曖昧さを避けたり、優先順位を変えるために丸括弧を使います。

疑似ラムダ項Eの自由変数の集合FreeVar(E)は次のように定義します。

  1. xが変数(x∈Var)ならば、FreeVar(x) = {x}
  2. FreeVar(!) = 空集合
  3. E, Fが疑似ラムダ項ならば、FreeVar(E▷F) = FreeVar(E)∪FreeVar(F)
  4. E, Fが疑似ラムダ項ならば、FreeVar((E F)) = FreeVar(E)∪FreeVar(F)
  5. Eが疑似ラムダ項ならば、FreeVar(E_1) = FreeVar(E)
  6. Eが疑似ラムダ項ならば、FreeVar(E_2) = FreeVar(E)
  7. xが変数、Aが型、Eが疑似ラムダ項ならば、FreeVar(λx:A.E) = FreeVar(E)\{x}
  8. Eが疑似ラムダ項ならば、FreeVar((E)) = FreeVar(E)

FreeVar(E)\{x} は、FreeVar(E)から変数xを(あれば)取り除いた集合です。

疑似ラムダ項に対しても、通常の手順によりアルファ変換(alpha conversion)を行えます。アルファ変換は束縛変数をリネームしますが、自由変数のリネームも同様に行えます(リネームで意図せぬラムダ束縛が生じないように注意)。アルファ変換と自由変数のリネームは似てますが、リネーム対象(束縛変数か自由変数か)が違うので区別してください。

ラムダ項の構成と型付け

x:A, y:B のように、変数ごとの型宣言が並んだものをΓ, Δなどのギリシャ文字大文字で表すことにします。この並びのことも型宣言(type declaration)と呼びます。他に、型環境(type environment)とか型コンテキスト(type context)とか呼ぶこともあります。でも、人によって用語法は異なります→「型理論ってば」。

型宣言Γは、変数:型 の形をカンマで区切って並べたものです。変数が重複してはダメで、すべて異なる変数が出現します。Γは空であってもかまいません。Γに出現する変数の集合をVarSet(Γ)とします。

型宣言Γと疑似ラムダ項Eを組にした〈Γ| E〉 を型宣言付き擬似ラムダ項(type-declared lambda pseudoterm)と呼びます。型宣言付き疑似ラムダ項のなかには、不適切なものが含まれています。適切な項とは、型が確定するものです。項の適切さ=項の型付け可能性を定義するために、型判断というものを導入します。

型宣言付き疑似ラムダ項〈Γ| E〉と型Aを組にした 〈Γ| E〉 :A の形を型判断(type judgement)と呼びます。型判断は、「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。型判断の書き方を変えて、Γ |- E:A とか Γ ⇒ E:A とするとシーケント計算に繋がります。が、今回はシーケント形式は使いません。シーケント形式でのラムダ計算は次の記事に書いています。ラムダ式の構文や推論規則は今回と微妙に違いますが、本質的な差はありません。

最初から正しいと認める型判断を公理型判断(axiom type judgement)、型公理(type axiom)、あるいは混乱の心配がなければ単に公理(axiom)と呼びます。以下に公理型判断のパターンを列挙します。

  • [変数] Γのなかに x:A が含まれるならば、〈Γ| x〉:A は公理である。
  • [ユニット] 〈Γ| !〉:I は公理である。Γは任意で、空でもよい

型推論規則(type inference rule)は、型判断から新しい型判断を作り出す規則です。型推論規則は、次のような型推論図(type inference (rule) figure)で記述します。「推論図」、「推論規則」、「規則」という言葉は同義語として使われるので注意してください。

(適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| E〉:A  〈Δ| F〉:A->B
 --------------------------[適用]
   〈Γ, Δ| E▷F〉:B

 〈Γ| E〉:A 〈Γ| F〉:B
 ------------------------[デカルトペア]
   〈Γ| (E F)〉:A×B

  〈Γ| E〉:A×B
 ----------------[第一成分]
 〈Γ| E_1〉:A

 〈Γ| E〉:A×B
 ----------------[第ニ成分]
 〈Γ| E_2〉:B

 〈x:A, Γ| E〉:B
 ------------------------[関数抽象]
  〈Γ| λx:A.E〉:A->B

型推論規則は、ラムダ項の構文構成規則(term forming rule)と、型付け規則(typing rule)の両方を兼ねています。項の構成と同時にその型も与えているのです。

変数と定数(!は定数)は公理で規定し、他の構文的構成は推論規則で表現しています。しかし、後で出てくる代入(substitution)を前提にして、推論規則を公理に移すこともできます。例えば、ペアの構成を公理にできます。

  • [ペア] Γのなかに x:A と y:B がこの順で(x:A が先で)含まれるならば、〈Γ| (x y)〉:A×B は公理である。

型推論図を積み重ねた図形を型証明図(type proof figure)と呼びます。しばしば、単に証明図ともいいます。次は型証明図の例です。☆は、直下が型公理であることを示す目印です。

     ☆                     ☆
 -----------[変数] -------------------[変数]
〈x:A| x〉:A     〈f:A->B| f〉:A->B                 ☆
 --------------------------------------[適用]  -----------------[変数]
        〈x:A, f:A->B| x▷f〉:B                〈g:B->C| g〉:B->C
 -------------------------------------------------------------------[適用]
              〈x:A, f:A->B, g:B->C| (x▷f)▷g〉:C
            ----------------------------------------[関数抽象]
            〈f:A->B, g:B->C| λx:A.(x▷f)▷g〉:A->C

型証明図の最下段に現れる型判断を、その型証明図の結論(conclusion)と呼びます。最上段がすべて星印(☆)である型証明図は閉じた型証明図(closed type proof figure)と呼びます。閉じた型証明図の結論となる型判断は型証明可能(type provable)だといいます。混乱の恐れがないなら単に証明可能(provable)でもいいです。

型宣言付き疑似ラムダ項〈Γ:E〉が、〈Γ|E〉:A という型判断と、この型判断を結論とする閉じた型証明図を持つとき、型付け可能(typable)と呼びます。次の2つの言い方は同じ意味です。

  • 型判断 〈Γ|E〉:A が型証明可能である。
  • 〈Γ|E〉は型付け可能で、ΓのもとでのEの型はAである。

型宣言付き疑似ラムダ項〈Γ|E〉が型付け可能なとき、それを型付きラムダ項(typed lambda term)、または型付きラムダ式(typed lambda expression)と呼びます。文脈から分かるなら、「型付き」を省略して単にラムダ項、ラムダ式でもかまいません。

〈Γ| E〉が型付きラムダ式のとき、全体を大きなラムダ式、内部にある疑似ラムダ項Eを小さなラムダ式とも呼びます。この呼び名は、内部のEだけでは不十分なことを強調するために使っています。小さなラムダ式だけでは、型付け可能かどうかは分かりません。

[適用]推論規則を、次のデカルト適用(Cartesian application)に置き換えたほうが理論的な扱いは楽になります。[適用]でも[デカルト適用]でも、どっちを採用しても証明系の能力は変わりません。

〈Γ| E〉:A  〈Γ| F〉:A->B
 --------------------------[デカルト適用]
   〈Γ| E▷F〉:B

しかし、[デカルト適用]を使う前に型宣言を揃えるのがめんどくさいので、[適用]を採用しました。

大きなラムダ式のアルファ変換

例として次の大きなラムダ式を考えてみましょう。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉

この大きなラムダ式は、次の型判断を持ちます(型判断を持つ型宣言付き疑似ラムダ項を、大きなラムダ式と呼ぶのでした)。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

この型判断の根拠(型証明図)は次です。

                        ☆                         ☆
                   ------------[変数]  -----------------------------[変数]
    ☆             〈x:A| x〉:A        〈f:A->(B->C)| f〉:A->(B->C)
 -----------[変数] -------------------------------------------------[適用]
〈y:B| y〉:B       〈x:A, f:A->(B->C)| f・x〉:B->C
 --------------------------------------------------[適用]
      〈y:B, x:A, f:A->(B->C)| (f・x)・y〉:C
      -------------------------------------------[関数抽象]
      〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

大きなラムダ式のインフォーマルな解釈は写像です。型は集合だと思うと、〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉は次の写像を表します。

  • x∈A, f∈(A->(B->C) に対して、式 λy:B.(f・x)・y で表される(B->C)の要素を対応させる。

写像の表現としては、入力変数の名前はどうでもいいので、〈s:A, k:A->(B->C)| λy:B.(k・s)・y〉でも同じ写像を表します。この事情を考慮して、大きなラムダ式にもアルファ変換を定義します。大きなラムダ式のアルファ変換は、内部の小さなラムダ式に対して自由変数のリネームになります。その点を注意すれば、要領は通常のアルファ変換と同じです。混乱しそうなときは、大きなアルファ変換という言葉を使います。

大きなアルファ変換は、必要なときにいつでも実行してかまいません。例えば[適用]推論規則には、「適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない」という制限がついてましたが、事前にアルファ変換をするなら、この制限はないも同然です。大きなアルファ変換を明示的に書くときは、次の推論図を使います。

  〈Γ| E〉:A
  ---------------[アルファ変換]
  〈Γ'| E'〉:A

Γ'とE'は、変数をリネームした結果

今後は、大きなアルファ変換で移れる大きなラムダ式は同一視することにします。大きなアルファ変換による同値関係の商集合を考える、とも言えます。

大きなラムダ式の構造規則

推論規則の上段・下段を比べると、関数抽象以外では、上段の型宣言はそのまま下段に引き継がれます。関数抽象では、一番左の個別宣言が取り除かれます。現状では、個別宣言の順序を変えたり、個別宣言を足すことはできません。これでは困ります。

そこで、大きなラムダ式の型宣言部分を操作する規則を導入します。それらの規則を構造規則(structural rule)と呼びます。構造規則も型判断に対する推論図として表現します。構造規則の名前は、直積以外はシーケント計算にちなみます。

  • (interchange)
  • (thinning)
  • (contraction)
  • 直積(direct product)
 〈Γ, x:A, y:B, Δ| E〉:C
 --------------------------[換]
 〈Γ, y:B, x:A, Δ| E〉:C

 〈Γ| E〉:A
 ---------------------[増]
 〈Δ, Γ, Π| E〉:A

 〈Δ, x:A, y:A, Π| E〉:C
 --------------------------[減]
 〈Δ, x:A, Π| E[x/y]〉:C

 〈Δ, x:A, y:B, Π| E〉:C
 --------------------------------------[直積]
 〈Δ, p:A×B, Π| E[p_1/x, p_2/y]〉:C

[増]構造規則を使う前提で、型公理を減らすことができます。

  • [変数] 〈x:A| x〉:A
  • [ユニット] 〈| !〉:I

別にうれしくないので型公理を減らしませんけどね。

[換]構造規則を何度か使うと、型宣言の順序を自由に入れ替えることができます。入れ替えても型判断はそのまま成立する(あるいは、やっぱり成立しない)ので、型判断における型宣言の順序はどうでもいいことが分かります。

[直積]構造規則は、シーケント計算では論理規則に分類されています。論理における構造規則と論理規則の区分は、ラムダ計算の構文論/意味論の観点からは重要ではありません。割とどうでもいい区分です。なお、ラムダ計算とシーケント計算の関係は、次の記事でも触れています。

マルチ代入

E1, ..., En が小さなラムダ式、x1, ..., xn は変数とします。小さなラムダ式Fに対して、Fのなかに出現する自由変数xi(それがあれば)をEi(i = 1, ..., n)で置き換えた式を、

  • F[E1/x1, ..., En/xn]

と書きます(書き方については「型推論に関わる論理の概念と用語 その6:substitutionの記法」参照)。これは、同時置き換えであって、変数1個ずつ順番に置き換えるわけではありません。複数の変数に対する同時置き換えをマルチ代入(multi-substitution)と呼ぶことにします。「マルチ」を使ったのは、複圏(multicategory = operad)と関係しているから、という理由もあります。代入(置き換え)で、意図せぬラムダ束縛が生じないように注意する点は自由変数のリネームと同様です。

マルチ代入は、代入(置き換え)の並列実行だと言っていいでしょう。しかし、並列実行は直列逐次実行でシミュレートできます。何も考えずに逐次実行すると、奇妙な結果になるので、適切に変数のリネームをする必要がありますが、個々の変数出現を1つずつ順番に処理することでマルチ代入をシミュレートできます。

置き換え操作は、型を考慮せずに実行することができますが、型を考慮した正しい置き換えのルールは、次の型推論図で示されます。この推論図(推論規則)もマルチ代入と呼びます。

(マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn), VarSet(Δ) は、どの2つも共通部分が空(disjoint)でなくてはならない)
 〈Γ1| E1〉:A1
  ...
 〈Γn| En〉:An
 〈x1:A1, ..., xn:An, Δ| F〉:B
  -------------------------------------------[マルチ代入]
 〈Γ1, ..., Γn, Δ| F[E1/x1, ..., En/xn]〉:B

横線の上段は、n個の型判断を横に並べたものですが、スペースとレイアウトの関係上縦に並べています。Δは、代入で手付かずの変数が含まれる型宣言です。[マルチ代入]推論規則はΔを許すので、変数すべてを置き換える必要はありません。参考に、[マルチ代入]推論規則に対応するストリング図変形を挙げておきます。

Δが空のときはフル・マルチ代入(full multi-substitution)といいます。

(フル・マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn) は、どの2つも共通部分が空(disjoint)でなくてはならない)
 〈Γ1| E1〉:A1
  ...
 〈Γn| En〉:An
 〈x1:A1, ..., xn:An| F〉:B
  -------------------------------------------[フル・マルチ代入]
 〈Γ1, ..., Γn| F[E1/x1, ..., En/xn]〉:B

推論規則としての[マルチ代入]と[フル・マルチ代入]は同等(どっちを採用しても同じ)ですが、実用上の便利さからマルチ代入を採用します。

型証明系TPS1

今まで述べたことの中間まとめをしておきましょう。

疑似ラムダ項Eと型宣言Γの構文を説明して、それらの組み合わせとして型判断〈Γ| E〉:A (Aは型)を導入しました。型判断は「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。その主張が正しいことを保証するメカニズムが型証明系(type proof system)です。

一般に論理的証明系(演繹系)は、証明すべき主張を表現する(sentence)の集合、最初から正しいと(天下りに)決めた文である公理(axiom)の集合、新しい文を作り出す手順を示す推論規則(inference rule)の集合からなります。今回の型証明系では、文は型判断であり、公理の集合と推論規則の集合は次のように与えられました。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [デカルトペア]推論規則
  5. [第一成分]推論規則
  6. [第ニ成分]推論規則
  7. [関数抽象]推論規則
  8. [マルチ代入]推論規則

補助的に、(大きな)アルファ変換と構造規則があります。

  1. アルファ変換
  2. [換]構造規則
  3. [増]構造規則
  4. [減]構造規則
  5. [直積]構造規則

推論規則/アルファ変換/構造規則の組み合わせが証明ですが、証明は証明図という図形で表します。

今回我々が定義した型に関する証明系をTPS1(Type Proof System 1 固有名詞)と呼ぶことにします。いちおうのまとまりが付いたので、TPS1という名前を付けましたが、TPS1は型付きラムダ計算を展開するには機能不足だし、意味論がないので文字通り意味不明だと注意しておきましょう。後でもう少し拡張します。圏論的意味論もいずれ述べる予定です(今回は正式な意味論はなし)。

型判断をα, βなどのギリシャ文字小文字で表すことにします。型判断αがTPS1において証明可能なことを、記号的に次のように書きます。

  • |-TPS1 α

証明図の最上段に現れる型判断を、その証明図の仮定(assumption)と呼びます。星印が上に位置する公理は仮定ではありません。TPS1において、型判断α1, ..., αnを仮定して型判断βが相対証明可能(relatively provable)とは次の意味です。

  • βを結論として、α1, ..., αn の全部または一部を仮定として持つTPS1の証明図が存在する。

記号的には次のように書きます。

  • α1, ..., αn |-TPS1 β

相対証明可能なことも単に証明可能性という場合が多いです。

メタな記号 |-TPS1 を定義したのですが、このようなメタな定義でよいのか? は議論の余地があります。上記の定義では、証明系が仮定を使うとき、「仮定の一部を捨ててもよい」「1つの仮定を何度も使ってよい」「仮定をどの順番で使ってもよい」などを暗黙に前提しています。つまり、仮定の“集まり”を集合だと前提していて、リストやマルチセットは考えてません。

メタな概念である「証明可能性」をさらに形式化して扱うときは、このへんのところをもっと検討する必要があります。

TPS1における代入消去と型付けの一意性

大きなラムダ式〈Γ| E〉は、定義により型付け可能です。つまり、TPS1で証明可能な型判断〈Γ| E〉:A があります。しかし、型Aが一意に決まるかどうかは明らかではありません。

TPS1において、型判断 〈Γ| E〉:A が証明可能なとき、その証明図がひとつとは限りません。例えば、 〈| (! !)〉:I×I は次のようにして証明できます。

     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I
 ----------------------------------[デカルトペア]
        〈| (! !)〉:I×I

これより短い証明図はありませんが、長い証明図は書けます。例えば:

[ユニット2つ]は次の図とする。
     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I


                  ☆                      ☆
            ----------------[変数]  ----------------[変数]
           〈x:I, y:I| x〉:I       〈x:I, y:I| y〉:I
            ----------------------------------------------[デカルトペア]
 [ユニット2つ]     〈x:I, y:I| (x y)〉:I×I
 ---------------------------------------------[マルチ代入]
             〈| (! !)〉:I×I

2つの証明図に対応するグラフ(ツリー)は次のようになります。

このような冗長で回り道をした証明ができてしまうのは、マルチ代入規則があるせいです。マルチ代入規則を除外して、他の規則だけにすると(多少の工夫もして)、型判断に対する証明図が(あれば)ひとつだけになります。

しかし、今まで在った推論規則をなくしてしまうので、今まで証明できていた型判断が証明できなくなるリスクがあります。幸いなことに、この心配は無用で、次のメタ定理が成立します。

  • ある型判断がTPS1で証明可能なとき、マルチ代入規則なしでも証明できる。

もっと具体的に言えば:

  • ある型判断のTPS1の証明図があるとき、その証明図を変形して、マルチ代入規則なしの証明図を構成できる。

この事実は、シーケント計算のカット消去定理(Cut elimination theorem)の対応物です。代入消去定理(Substitution elimination theorem)と呼びましょう。

代入消去により得られた証明図は、それ以上は短くできない形をしているので一種の正規形(normal form)となります。正規形の証明図=マルチ代入なしの証明図に限定すれば、型判断と証明図が1:1に対応します。型判断がなんにしろ証明可能なら、それは唯一の正規形証明図を持ちます。

正規形証明図の一意性から、型付けの一意性が従います。

  • 大きなラムダ式〈Γ| E〉が型付け可能なら、その型は一意的に決まる。

適切なアルゴリズムにより、型と共に型付けの証拠である正規形証明図も一意的に得られます。これは大変に都合の良い性質で、TPS1はラムダ計算の構文的基盤として適切であると言っていいでしょう。

証明図に対する代入消去は、代入計算の実行を意味するので、代入消去のアルゴリズムは、“証明図を実行する手順”=“証明図のインタプリタ実装”を与えます。証明図の実行結果である正規形証明図はメタレベルの“値”と解釈されます。つまり、TPS1の証明図をプログラム・ソースコードとするプログラミング・システムがあると考えることができるのです。

ラムダ計算のポリ化: 型証明系TPS2

今まで、型宣言付き疑似ラムダ項は〈Γ| E〉という形で、内部に必ず1個の疑似ラムダ項を持っていました。これを一般化して、内部に複数個の疑似ラムダ項を書いていいことにします。次のような形です。

  • 〈Γ| E1, ..., En〉 (n ≧ 1)

この形を、型宣言付きポリ疑似ラムダ項(type-declared lambda poly-pseudoterm)と呼びます。名前が長すぎるので、ポリ・ラムダ式(poly-lambda expression)とも呼ぶことにします。「ポリ」を付けたのは、多圏(polycategory)と関係するからです。

疑似ラムダ式の並びをΦ, Ψなどのギリシャ文字大文字で表すことにすると、ポリ・ラムダ式は〈Γ| Φ〉という形になります。並び(リスト)の長さをlength(-)と書くことにして、ポリ・ラムダ式の(width)と余幅(cowidth)を次のように定義します。

  • width(〈Γ| Φ〉) = length(Γ)
  • cowidth(〈Γ| Φ〉) = length(Φ)

width(〈Γ| Φ〉) = 0 はあり得ますが、cowidth(〈Γ| Φ〉) ≧ 1 です(cowidth(〈Γ| Φ〉) = 0 は今のところ認めません、後で許容するように変更しますが)。任意のn, m(n ≧ 0, m ≧ 1)に対して、width(〈Γ| Φ〉) = n, cowidth(〈Γ| Φ〉) = m であるポリ・ラムダ式が存在します。

ポリ・ラムダ式に対するポリ型判断(poly type judgement)は、次の形です。

  • 〈Γ| E1, ..., En〉:A1, ..., Am

ポリ型判断の幅と余幅もポリ・ラムダ式の場合と同様に定義できます。

ポリ型判断の証明可能性に関して、次が成立することが要請されます。

  1. n = 1 のとき、〈Γ|E〉:A が証明可能かどうかは、既にTPS1で定義されている通り。
  2. n ≧ 2 のとき、〈Γ| E1, ..., En〉:A1, ..., An が証明可能なのは、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能なとき。

二番目の要請を、推論図として表現すると、次のようになります。

 〈Γ| E1〉:A1
   ...
 〈Γ| En〉:An
 ------------------------------[デカルト併合]
 〈Γ| E1, ..., En〉:A1, ..., An

この推論図は、デカルト・タプルの構成法と似てるので、デカルト併合(Cartesian merge)と呼びます。参考に、[デカルト併合]推論規則に対応するストリング図変形を挙げておきます。

ポリ型判断に対して[マルチ代入]推論規則はうまく機能しないので、ポリ型判断に関する代入規則であるポリ代入(poly substitution)を導入します。

(ポリ代入の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
 〈Γ| E1, ..., En〉:A1, ..., An
 〈x1:A1, ..., xn:An, Δ|Ψ〉:B1, ..., Bn
 --------------------------------------------------------[ポリ代入]
 〈Γ, Δ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn

ここで、Ψ[E1/x1, ..., En/xn] は、リストΨに含まれるすべての疑似ラムダ項にマルチ代入[E1/x1, ..., En/xn]を施したリストを意味します。参考に、[ポリ代入]推論規則に対応するストリング図変形を挙げておきます。

上記の推論図において、Δが空のときはフル・ポリ代入(full poly-substitution)と呼びます。

ポリ型判断を扱う新しい型証明系TPS2を次のように定義します。

  1. TPS2の文は、ポリ型判断だとする。この定義より、(TPS1の文の集合) ⊆ (TPS2の文の集合)。
  2. TPS2の公理の集合は、TPS1の公理の集合と同じ。
  3. TPS2の推論規則(推論図)の集合は、TPS1の推論規則(推論図)に[デカルト併合]を加え、[マルチ代入]を[ポリ代入]と交換したもの。
  4. TPS2の推論図として、TPS1の構造規則(の推論図)もそのまま採用する。推論規則が冗長になる(不要なものまで入る)が気にしない。

TPS1とTPS2に関して、次のメタ定理が成立します。

  1. 〈Γ|E〉:A がTPS1で証明可能ならば、TPS2でも証明可能である。(自明)
  2. 〈Γ|E〉:A がTPS2で証明可能ならば、TPS1でも証明可能である。(非自明)
  3. 〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能ならば、〈Γ| E1, ..., En〉:A1, ..., An がTPS2でも証明可能である。(自明)
  4. 〈Γ| E1, ..., En〉:A1, ..., An がTPS2で証明可能ならば、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An はすべてTPS1でも証明可能である。(非自明)

これらのメタ定理の証明(証明系を外から見てのメタレベルの証明)は、もう少し準備して組み合わせ的・帰納的議論をする必要があります。今回は割愛します。

TSP2の証明可能性がTSP1での議論に帰着できるので、ポリ・ラムダ式の型付けの一意性が言えます。

もうひとつの型証明系TPS3

TPS1は、単一のラムダ式の型付けや代入計算を行うのに便利です。TPS2は、複数のラムダ式を一度に扱うために導入しました。TPS2の1個の型判断(ポリ型判断)は、TPS1の複数の型判断をまとめただけと言えます。

さて、大きなラムダ式の圏論的な扱いに適した型証明系としてTPS3を導入します。まず、TPS3では、〈Γ|〉という形の大きなラムダ式を認めます。TPS2における型は、単一型の非空リストでしたが、TSP3では空リスト()を認めます。これに伴い型判断(ポリ型判断)の構文も拡張します。

型証明系→ TPS1 TPS2 TPS3
型判断の幅 n n ≧ 0 n ≧ 0 n ≧ 0
型判断の余幅 m m = 1 m ≧ 1 m ≧ 0
単一の型 長さ1以上の型のリスト 任意長の型のリスト

Γは空も許す型宣言の並び、Φは空も許す型宣言の並び、A1, ..., An を空(n = 0)も許す型の並びとして、TPS3の型判断は、〈Γ| Φ〉:A1, ..., An の形です。3種類の並び(リスト)から構成されますが、並びの長さに何の制限もありません

型証明系としてのTPS3を定めるために、型公理と型推論規則を決めましょう。TPS2で使った以下の型公理/型推論規則はそのまま使い続けます。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [第一成分]推論規則
  5. [第ニ成分]推論規則
  6. [関数抽象]推論規則

(大きな)アルファ変換も使います。構造規則は廃止します。

TSP3では次の公理を追加します。

  • [空] 〈Γ|〉:()

小さなラムダ式は無し、型は空リストです。Γは任意の型宣言です。特に、〈|〉:() は型公理です。

[デカルトペア]推論規則と[ポリ代入]推論規則、[デカルト併合]推論規則は、対応する別な規則と入れ替えます。対応する別な規則の名称は、モノイドペア(monoidal pair)、フル・ポリ代入(full poly-substitution)、モノイド併合(monoidal merge)です。

(モノイドペアの条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
 〈Γ| E〉:A 〈Δ| F〉:B
 ------------------------[モノイドペア]
   〈Γ, Δ| (E F)〉:A×B


 〈Γ| E1, ..., En〉:A1, ..., An
 〈x1:A1, ..., xn:An| Ψ〉:B1, ..., Bn
 --------------------------------------------------------[フル・ポリ代入]
 〈Γ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn


(モノイド併合の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
  〈Γ| Φ〉:A1, ..., An
  〈Δ| Ψ〉:B1, ..., Bm
   -------------------------------------[モノイド併合]
  〈Γ, Δ| Φ, Ψ〉:A1, ..., An, B1, ..., Bm

型証明系TPS3を次のように定義します。

  1. TPS3の文は、空を許すポリ型判断だとする。この定義より、(TPS2の文の集合) ⊆ (TPS3の文の集合)。
  2. TPS3の公理の集合は、TPS2の公理の集合に、[空]公理を追加したもの。
  3. TPS3の推論規則(推論図)の集合は、TPS2の推論規則(推論図)の[デカルトペア]、[ポリ代入]、[デカルト併合]をそれぞれ、[モノイドペア]、[フル・ポリ代入]、[モノイド併合]に入れ替えたもの。
  4. TPS2の構造規則(それはTPS1の構造規則)は採用しない。TPS3では、構造規則は不要。

念のため、TPS3の公理/推論規則を列挙しておきます。'*'はTPS2から変更しているものです。

  1. [変数]公理
  2. [ユニット]公理
  3. [空]公理 *
  4. [適用]推論規則
  5. [モノイドペア]推論規則 *
  6. [第一成分]推論規則
  7. [第ニ成分]推論規則
  8. [関数抽象]推論規則
  9. [フル・ポリ代入]推論規則 *
  10. [モノイド併合]推論規則 *
  11. アルファ変換

TPS3に関して、次のメタ定理が成立します。

  • TPS2で証明可能なポリ型判断はTPS3でも証明可能である。
  • TPS3で証明可能な余幅が0でないポリ型判断はTPS2でも証明可能である。

上記メタ定理の証明も割愛します。

TPS3の証明可能性がTPS2に帰着できるので、TPSでもポリ・ラムダ式の型付けの一意性が言えます。

LLEの定義

型証明系TPS3を定義したのは、TPS3が圏LLE(前回の「概要と目標」参照)を定義する道具に便利だからです。(実際の型証明に使うなら、TPS2のほうが便利でしょう。)

ポリ・ラムダ式〈Γ| Φ〉がTPS3で型付け可能なとき、そのポリ・ラムダ式を、あらためて大きなラムダ式と呼びます。今ここで「大きなラムダ式」の意味を拡張したわけです。すべての大きなラムダ式からなる集合をLLEとします。

大きなラムダ式αが、〈x1:A, ..., xn:An| E1, ..., En〉の形をしているとき、定義によりこれは型付け可能なので、次のポリ型判断がTPS3で証明可能です。

  • 〈x1:A, ..., xn:An| E1, ..., En〉:B1, ..., Bm

ここで、B1, ..., Bm は一意的に決まります。この事実を使って、大きなラムダ式αの域(domain)と余域(codomain)を次のように定義します。大きなラムダ式には余域が一意に決まることがポイントです。

  • dom(α) = (A1, ..., An)
  • cod(α) = (B1, ..., Bm)

dom(α)もcod(α)も型の並び(リスト)です。型の集合をType、型のリストの集合をType*とすれば、写像として、

  • dom:LLE→Type*
  • cod:LLE→Type*

となります。

(A1, ..., An)∈Type* とするとき、(A1, ..., An)に対する恒等ラムダ式(大きなラムダ式)は次のように定義できます。

  • idA1, ..., An = id(A1, ..., An) = 〈x1:A, ..., xn:An| x1, ..., xn

以上で、dom, cod, idが定義できました。LLEとType*を圏に仕立てるには、圏の結合(composition)が必要です。結合は、フル・ポリ代入によって定義します。cod(α) = (B1, ..., Bm), dom(β) = (B1, ..., Bm) のとき、α;βは次の推論図で定義されます。

  α    β
 -----------[フル・ポリ代入]
    α;β

次の圏の条件を示せます。

  1. dom(idA1, ..., An) = (A1, ..., An)
  2. cod(idA1, ..., An) = (A1, ..., An)
  3. cod(α) = dom(β) ならば、α;β が定義できる。
  4. dom(α;β) = dom(α)
  5. cod(α;β) = cod(β)
  6. (α;β);γ = α;(β;γ)
  7. idA1, ..., An;α = α
  8. α;idB1, ..., Bn = α

結合法則 (α;β);γ = α;(β;γ) 以外は自明だと思います。結合法則は、ポリ代入に関するメタ定理です。

以上により、LLEを射の集合、Type*を対象の集合とする圏LLEが定義できました。

LLEのモノイド構造

LLEにはモノイド構造が入ります。それをこの節で述べます。LLEのモノイド積の記号を□とします。

まず、LLEの対象に対するモノイド積を定義します。(A1, ..., An), (B1, ..., Bm)∈Type* に対して、(A1, ..., An)□(B1, ..., Bm) は連接で定義します。

  • (A1, ..., An)□(B1, ..., Bm) = (A1, ..., An, B1, ..., Bm)

Type*は、□をモノイド演算、空リスト()を単位元とするモノイドとなります。

LLEの射(大きなラムダ式)α, βに対しては、α□βを次の推論図で定義します。

  α   β
 ----------[モノイド併合]
   α□β

(LLE, □, ())は厳密モノイド圏になります。そのことを示すには、次の等式群を確認します。

  1. dom(α□β) = dom(α)□dom(β)
  2. cod(α□β) = cod(α)□cod(β)
  3. id(A1, ..., An)□(B1, ..., Bm) = (idA1, ..., An)□(idB1, ..., Bm)
  4. (α;β)□(γ;δ) = (α□γ);(β□δ)
  5. (α□β)□γ = α□(β□γ)
  6. α□id() = id()□α = α

交替律 (α;β)□(γ;δ) = (α□γ);(β□δ) は、(α□id);(id□β) = (id□β);(α;id) という簡略な形でもいいので、これらの証明は難しくありません。モノイド演算□が、列の連接に過ぎないので事情が非常に簡単になっています。繰り返し注意しますが、大きなアルファ変換は必要なら自動的に実行されると考えます。

ラムダ式の変換と同値に関する注意

ここまでの話では、ラムダ計算では非常に重要であるベータ変換やイータ変換、それらの変換により導入されるラムダ式の同値性が出てきてません。これらの変換と同値性は、構文論だけだと解釈が難しいでしょう。

大きなラムダ式α, βがあって、適切な意味論的解釈〚-〛があるとき、〚α〛 = 〚β〛 ならば、大きなラムダ式αとβは同値だと定めて α ≡ β と書くことにします。メタな命題である α ≡ β を、形式的に証明できる証明系(形式的体系)はどんなものか? と考える必要があります。

同値性に関する証明系は、TPS*より上位の体系になります。仮に、同値性に関する証明系をEPS(equivalence proof system)とすると、次のようなメタ命題のあいだの関係が問題になります。

  • [EPS証明可能性] 形式化された同値性 α ≡ β が形式的証明系EPSで証明可能である。
  • [意味論的同値] 意味論的解釈〚-〛に関して、〚α〛 = 〚β〛 が成立する。

EPSがマトモな証明系であるためには、次(健全性)が要求されます。

  • α ≡ β がEPSで証明可能ならば、〚α〛 = 〚β〛 が成立する。

ベータ同値やイータ同値はEPSの公理となる性質です。EPSに必要な公理はベータ同値/イータ同値だけではなくて、実は色々な公理が要請されます。例えば、〈u:I| u〉と〈u:I| !〉は同値であるべきです。

おわりに

ラムダ式の意味論やラムダ式の同値性の議論が、型付きラムダ計算論の中核でしょう。今回説明したことは、ラムダ式の型付けと代入計算だけ、つまり、圏論的意味論を展開する土台になる構文論の部分です。

型付きラムダ計算の圏論的意味論が目指すべきランドマークは、次の2つのメタな命題が同値であることを主張する“完全性定理”です。

  • |-EPS (α ≡ β)
  • CCCC.( C |= (α ≡ β) )

EPSはラムダ式の同値性に関する証明系で、CCCはすべてのデカルト閉圏(Cartesian Closed Categories)からなるクラスです。C |= (α ≡ β) は、Cに値を持つ解釈(意味関手)〚-〛C に関して 〚α〛C = 〚β〛C であることを意味します。

型付きラムダ計算に関する手法や結果を、このビッグピクチャーのなかに位置付けると、けっこう納得感があると思います。今回の一連の話も、ビッグピクチャーのピースを眺めたことになります。

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

2017-05-22 (月)

型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のために

| 09:25 | 型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のためにを含むブックマーク

カリー/ハワード対応への障壁」において、カリー/ハワード対応(Curry-Howard correspondence/isomorphism)をうまく説明するのは難しい、という話をしました。その記事の最後の一言は:

いまだベストと思える説明に届かず。

その後も、ベスト(に近い)説明とはどんなものかと考えています。以前から僕は「大きなラムダ計算」という方法を使っているのですが、これをベースにするのがやはり良いように思えます。大きなラムダ計算は型付きラムダ計算の定式化のひとつです。大きなラムダ計算をまともに紹介したことがなかったので、この記事と引き続く記事の2回に分けて説明します(続く第2回もほぼ書き終えていますよ ^_^)。

この2回の記事で、大きなラムダ計算の構文的・証明論的側面を紹介します。ラムダ式への型付けアルゴリズムを形式的証明と捉えて、その証明系の性質を調べます。カリー/ハワード対応を意識してのことです。証明系に関するメタ定理は、ラムダ式と証明図の構造に沿った帰納法で(メタに)証明できますが、煩雑で若干テクニカルなのでだいたい省略します(いつかちゃんと書くかも)。

「型付きラムダ計算を、構文だけで理解するのは苦しい」と思うので、集合圏におけるインフォーマルな意味論にも少しだけ触れます。少数ですが、複圏/多圏のストリング図も(次回に)載せます。本格的な意味論や絵算(pictorial/graphical/diagrammatic calculation)は展開しませんが、単なる構文解説だけよりは実感が増すと思います。

今回 1/2 の内容:

  1. 予備知識と参考資料
  2. 大きなラムダ計算とは何か
  3. 概要と目標
  4. 集合と写像に関する基礎的事項
  5. 型システム

次回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

予備知識と参考資料

ゼロからのラムダ計算入門には、10年前(2007年)に書いた一連の記事が、今でも役立つと思います。

  1. JavaScriptで学ぶ・プログラマのためのラムダ計算プログラミング言語JavaScriptを引き合いに出して、ラムダ計算をインフォーマルに説明しています。意図的ではありますが、関数抽象を(狭い意味の)「ラムダ式」と呼んだり、通例(「関数を引数に適用する」)とは逆の表現「引数を関数に適用する」をしているので注意してください。
  2. JavaScriptで学ぶ・プログラマのためのラムダ計算 問題集 : すぐ上の記事に対する練習問題集です。
  3. 絵を描いて学ぶ・プログラマのためのラムダ計算 : ラムダ項の構文解析木を使ってベータ変換を解説しています。なお、この過去記事で使っている絵はベータ変換の可視化が目的で、圏論ベース絵算のストリング図ではありません。

型無しラムダ計算の構文とベータ変換(簡約)を簡潔にまとめた記事として、id:tarao(たらお)さんによる次があります。

僕は、アルファ変換について説明してない(予告して不履行)ですが、アルファ変換はけっこう厄介です(ラムダ計算 - Wikipedia)。アルファ変換を知るには、id:sumii(住井)さんの次のテキストの1.5節あたりまで読むのがいいと思います。

ちなみに、上記テキストで"typing"の訳語が「型つけ」なのですが、ナルホド! 口頭でも「片付け」と混同しなくて良いですね。

型付きラムダ計算とデカルト閉圏の関係は次の記事達に書いています。解説というより、雰囲気を伝える“お話”です。興味があれば眺めてみてください。

大きなラムダ計算とは何か

型付きラムダ計算のラムダ式は、変数の型がハッキリしてないとダメなんです。ですから、λx.(g・(f・x)) のような式(ドット'・'は適用だとする)だけ出してもダメです。x, f, g の型を明示する必要があります。型の明示には型宣言を使うことにします*1。A, B, Cを型(の名前)だとして次のように宣言します。

  1. xの型は、A
  2. fの型は、AからBへの関数型
  3. gの型は、BからCへの関数型

これらの宣言を記号的に次のように書きます。

  1. x:A
  2. f:A->B
  3. g:B->C

'->'は関数型を作る記号で、普通の矢印'→'じゃなくて、ハイフンと不等号です。矢印'→'は他でも多用されるので記号を変えました。[A, B] という書き方も多いですが、ブラケットも他の目的で使うので、関数型は A->B にします。

ラムダ式と型宣言を一緒にしてパッケージしたものが大きなラムダ式*2です。ただし、ラムダ束縛変数の型宣言は'λ'の直後に埋め込んでいます(それが普通の書き方)。次は大きなラムダ式の例です。

  • 〈f:A->B, g:B->C| λx:A.(g・(f・x))〉

大きなラムダ式との対比のために、内側に置かれたラムダ式を小さなラムダ式とも呼びます。大きなラムダ式の基本的な形は次のようです。

  • 〈型宣言| 小さなラムダ式〉

小さなラムダ式(裸のラムダ式)ではなくて、常に大きなラムダ式を使って進めていくのが大きなラムダ計算です。基本はそれだけのことです。

この記事(+次回)で大きなラムダ計算について最初から説明するので過去記事を参照する必要はありませんが、歴史的経緯を言えば、2008年/2009年あたりのセミナーでは、大きなラムダ計算をインフォーマルに導入しています。

大きなラムダ計算の短い説明ならば次の記事にあります。

概要と目標

前節で説明したような大きなラムダ式(後で少し定義を拡張します)の全体を考えます。すべての大きなラムダ式からなる集合をLLE(large lambda expressionから)とします。LLEに、圏の構造を与えることができます。正確な言い方をすると、集合LLEをベースに圏を作れる、となります。集合LLEをベースに作った圏のほうは太字でLLEと書くことにしましょう。

集合LLEと圏LLEとの関係は、

  • Mor(LLE) = LLE

です。つまり、大きなラムダ式は圏LLEの射(morphism)となります。

では、圏LLEの対象は何でしょうか? それは、大きなラムダ計算で使う型の集合です。当該ラムダ計算で使用できるすべての型の集合をTypeとすると、

  • Obj(LLE) = |LLE| = Type*

です。Type*はTypeの要素を並べたリストの集合、つまり“単一の型を並べたリスト”の集合です。

この記事(+次回)の目標は、圏LLEを構成することです。

注意すべきは、圏LLE完全に構文的に作られているということです。(型付き)ラムダ計算に意味を与えることは、構文領域である圏LLEから意味領域となる圏Cへの関手を作ることです。(意味関手は、単なる関手以上にモノイド構造や閉構造などを保つことも要請します。)例えば、C = Set として、意味関手 SetSem:LLESet を作れば、ラムダ計算を集合と写像の計算として解釈することになります。

意味関手が値を取る圏Cを変えればまったく別な意味論ができます。例えば、順序代数構造(Heyting algebraなど)から作られたやせた圏Cとすることもできます。Cを固定しても意味関手は色々作れます*3

今回(+次回)は圏LLEを作るまでで、その上に意味関手を定義はしませんが、意味論を展開する構文的基盤を準備するのだと思うとよいでしょう。

集合と写像に関する基礎的事項

この節は、インフォーマルな意味論の説明に必要となる用語のまとめです。ザッと眺めるだけ、あるいは飛ばしてしまってもけっこうです。

A, B, Cなどは集合を表すとします。fがAからBへの写像であることを f:A→B と書きます。x∈A ならば、f(x)∈B です。A×Bは集合の直積で、g:A×B→C とは、「gが、AとBのペアを入力としてCの要素を返す写像である」ことです。x∈A, y∈B ならば、g(x, y)∈C です。なお、写像と関数は同義語として扱い、特に区別しません。

関数集合

AからBへの写像の全体を集合と考えたものをBAと書きます。この指数記法は入れ子にするのが辛いので、BAを A->B とも書きます。矢印風記法なら、入れ子も問題ありません; 例えば、A->(B->C) 。A->B を指数集合(exponential set; もともと指数記法で書いたので)とか関数集合(function set)と呼びます。

関数オブジェクト

f:A→B と f∈(A->B) は同じ意味ですが、「AからBへの写像」と「A->B の要素」を区別しないと混乱してしまうことが多いので、関数集合 A->B の要素を関数オブジェクト(function object)と呼ぶことにして、写像fに対応する関数オブジェクトを^fと書きます。(f^とも書きますが、今回は左肩にハットを付けます。)

  • f:A→B ⇔ ^f∈(A->B)

関数オブジェクト^fは、働きとしてのfをコンパイルした結果であるバイナリコードだと思うといいでしょう。^fはバイナリコード=実行可能データです。

適用

入力データxと実行可能データ^fを渡して実行する仮想マシン(の概念的モデル)をappとすると、appは次のような写像です。

  • app:A×(A->B)→B

実行結果は、もとの写像fの値となるので、次の等式が成立します。

  • app(x, ^f) = f(x)

appと入力の順序が逆である写像をapp'とします。

  • app':(A->B)×A→B
  • app'(^f, x) = f(x)

appやapp'を適用写像(application)とか評価写像(evaluation)と呼びます。

写像の直積

集合だけでなくて、写像にも直積を定義しましょう。f:A→X, g:B→Y のとき、f×g:A×B→X×Y は次のように定義します。

  • (f×g)(x, y) := (f(x), g(y))
デカルトペア

<f, g>(x) = (f(x), g(x)) と定義される写像を、fとgのデカルト・ペア(Cartesian pair)と呼びます。写像の直積とデカルトペアは、対角写像Δ(定義: Δ(x) = (x, x))により次のように関係付けられます。

  • <f, g> = Δ;(f×g)
射影と成分

A×B→A という射影をπ1、A×B→B という射影をπ2と書きます。f:C→A×B のとき、f1 = f;π1、f2 = f;π2 と書きます。f1をfの第一成分(first component)、f2をfの第ニ成分(second component)と呼びます。具体的に書くと:

  • f(z) = (x, y) のとき、f1(z) = x、f2(z) = y
単元集合と廃棄写像

1 = {0} として単元集合(シングルトン集合; singleton set)と呼びます。単元集合の唯一の要素は何でもいいです。単元集合を型とみなすときはユニット(unit)型とかヴォイド(void)型とか呼びます。

任意の集合Aから1への写像がただひとつだけあるので、それを!Aと書きます; !A:A→1。!Aには様々な呼び名があります: terminal morphism, final morphism, discarder, discharger など。ここでは、入力を捨ててしまうので廃棄写像(discarding map)と呼びましょう。

型システム

これから先「型」という言葉を頻繁に使います。「型」という言葉の解釈は、めちゃくちゃイッパイあります。ここでは、次の2つの立場を適宜使い分けます。

  1. 型とは集合である。
  2. 型とは単なる記号である。

インフォーマルな意味論としては、「型」は集合を表すと考えます。しかし今回は、オフィシャルな意味論の話はなくて、構文論だけです。実際のところは“ある種の記号”を「型」と呼ぶことになります。

インフォーマルな意味論も含めて、型を構成する手順を説明しましょう。まず、有限個の集合を選びます。例えば、自然数の集合 N = {0, 1, 2, ...} ひとつだだけを選びます。選んだ集合に名前(の記号)を割り当てます。例えば、自然数の集合に英字大文字'N'を割り当てます。他に、英字大文字'I'を単元集合1を表す記号として予約します。これで基本型記号(basic type symbol/name)が決まります。

何でもいいので2種類の結合子記号(connective symbol)を決めます。例えば'△'と'♂'にします。一般的な型記号(type symbol)、あるいは型項(type term)を帰納的に定義します。

  1. 基本型記号は型記号である。
  2. AとBが型記号ならば、(A△B) は型記号である。
  3. AとBが型記号ならば、(A♂B) は型記号である。
  4. 以上により定義されたものだけが型記号である。

心づもりとしては、型記号は集合を表すものです。基本型記号がNとIの場合、型記号Aが表す集合を〚A〛とすれば:

  1. 〚N〛 = N, 〚I〛 = 1
  2. 〚A△B〛 = 〚A〛×〚B〛
  3. 〚A♂B〛 = 〚A〛->〚B〛

例えば ((N△I)♂(N♂N)) の意味は 〚((N△I)♂(N♂N))〛 = (N×1)->(N->N) と計算できます。

以上の“記号の意味”はあくまで心づもり、想定であって、実際には意味論なしの構文論を考えます。したがって、オフィシャルには型とは型記号(型項)のことです。

型が等しいとは、集合の同一性や同型性ではなくて、記号として(図形として)の等しさです。(I△N) と N は違う記号なので違う型です。((N△N)△I) と (N△(N△I)) も違う記号なので違う型です。型Aと型Bがイコールだとは、AとBがまったく同じ記号のことです。

いま、結合子記号に'△'と'♂'を選びましたが、'×'と'->'にします。そうすると、集合のホントの直積/指数と区別が付かない問題が起きますが、文脈により、単なる結合子記号か集合の演算子記号かは区別できるでしょう。

また、(I×N) とか ((N×N)×I) のように律儀に括弧は付けず、I×N、N×N×I のように書きます。要するに、混乱がない限り普通の書き方をする、ということです。普通に書くと、人間の心理として集合を想定してしまいがちですが、オフィシャルには単なる記号だと肝に銘じてください。

続く

次回に続きます。次回で大きなラムダ式の構文を定義して、型付け(typing)を行うための形式的証明系を導入します。そして、構文論だけから得られる圏LLEを定義します。次回内容は:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

*1:変数に型情報をくっ付けるとか、型ごとに別な変数集合を準備するとかの方法もあります。ですが、型宣言が一番実用的だと思います。

*2:大きなラムダ式は、実質的には型付きラムダ項(typed lambda term)と変わりません。型宣言とのパッケージを徹底することが意図されています。

*3[追記]構文的な体系をひとつに固定したとして、圏Cに値を取る意味関手がたくさん定義できるのは事実です。しかし、これは鬱陶しくてイヤな状況です。できるなら、Cを決めれば一意的に意味関手が定まって欲しい -- この希望をかなえるように意味論を構成することは可能です。僕が「セマンティック駆動」と言ってきた方法は、Cを先に与えて、それから一意に意味関手を作る方法です。[/追記]

2017-05-18 (木)

よくあるタイポ

| 14:42 | よくあるタイポを含むブックマーク

キーボードで文字を書くと、余分な打鍵が発生して重複した2文字になることがあります。日本語だと、1文字2打鍵なので、それほど起こらないように思えますが、そうでもない。

僕のダイアリー内で「をを」「とと」「のの」を探したらけっこうありました。「とと」「のの」は正しい場合がありますが、「をを」はすべて誤入力です。修正した。

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