このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

指標と不完全インスタンス

指標に対する不完全インスタンス〈不完全モデル〉という概念を導入します。不完全インスタンスは、記号の乱用、オーバーロードなどの分析に使うつもりです。

内容:

指標の例

指標〈signature〉の例を幾つか出したいと思います。指標はプレーンテキストで書くので、フォントを変えたり添字を使ったりができません。次の約束をします。

プレーンテキスト $`\TeX`$ 説明
Set $`{\bf Set}`$ 集合圏
Nat $`{\bf N}`$ 自然数全体の集合
Int $`{\bf Z}`$ 整数全体の集合
Real $`{\bf R}`$ 実数全体の集合
Bool $`{\bf B}`$ 真偽値の二元集合
String $`{\bf String}`$ 文字列全体の集合
1 $`{\bf 1}`$ 特定された単元集合
id_U $`\mathrm{id}_U`$ 恒等写像
α_{U,U,U} $`\alpha_{U,U,U}`$ 結合律子〈associator〉

1 は「数の 1」の意味でも使うのでオーバーロードになります。

では指標の例です。

// (例1) 付点集合の指標
signature PointedSet {
  sort U in Set
  operation p : 1 → U in Set
}

// (例2) 半群の指標
signature Semigroup {
  sort U in Set
  operation m : U×U → U in Set
  equation assoc :: (m × id_U);m = α_{U,U,U};(id_U × m);m
                 : (U×U)×U → U
}

以上は、簡単ながらも“代数構造”の指標と言えます。以下は、データベースのテーブルスキーマのようなもの、あるいはデータ構造の定義に近い指標です。

// (例3) 人物データの指標
signature Person {
  element givenName in String
  element familyName in String
  element age in Nat
}

// (例4) 平面の座標の指標
signature XYCoord {
  element x in Real
  element y in Real
}

// (例5) 整数と実数の指標
signature IntReals {
  element n in Int
  element r in Real
  element s in Real
  equation e : r = s in Real
}

指標記述のキーワードとして、element, sort, operation, equation などを使ってますが、これらは「n-圏のk-射」のニックネームです。それを表にしましょう。

0-圏 1-圏
0-射 element sort
1-射 equation operation
2-射 - equation

つまり:

  1. 0-圏〈集合〉の0-射〈対象〉を element とも呼ぶ。
  2. 0-圏〈集合〉の1-射を equation とも呼ぶ。
  3. 1-圏〈通常の圏〉の0-射〈対象〉を sort とも呼ぶ。
  4. 1-圏〈通常の圏〉の1-射を operation とも呼ぶ。
  5. 1-圏〈通常の圏〉の2-射を equation とも呼ぶ。

味気ないですが、k-射を k-mor というキーワードにして、equation の「=」も矢印(一重または二重)にすると次のようになります。

// (例1) 付点集合の指標
signature PointedSet {
  0-mor U in Set
  1-mor p : 1 → U in Set
}

// (例2) 半群の指標
signature Semigroup {
  0-mor U in Set
  1-mor m : U×U → U in Set
  2-mor assoc :: (m × id_U);m ⇒ α_{U,U,U};(id_U × m);m
               : (U×U)×U → U in Set
}

// (例3) 人物データの指標
signature Person {
  0-mor givenName in String
  0-mor familyName in String
  0-mor age in Nat
}

// (例4) 平面の座標の指標
signature XYCoord {
  0-mor x in Real
  0-mor y in Real
}

// (例5) 整数と実数の指標
signature IntReals {
  0-mor n in Int
  0-mor r in Real
  0-mor s in Real
  1-mor e : r → s in Real
}

k-mor方式のいいところは、次元が上がってもキーワードを考える必要がないことです。例えば、モナドの定義は“圏の2-圏”のなかで3-mor(自然変換の等式)まで使った指標で表現できます。

// モナドの指標
signature Monad {
  0-mor C in CAT
  1-mor F : C → C in CAT
  2-mor μ :: F*F ⇒ F : C → C in CAT
  2-mor η :: Id_C ⇒ F : C → C in CAT
  3-mor assoc ::: (μ * ID_F);μ ≡> (ID_F *  μ);μ
              :: F*F*F ⇒ F
              : C → C in CAT
  3-mor lunit ::: (η * ID_F);μ ≡> ID_F
              :: F ⇒ F
              : C → C in CAT
  3-mor runit ::: (ID_F * η);μ ≡> ID_F
              :: F ⇒ F
              : C → C in CAT
}

指標のモデル〈インスタンス〉

指標は、構造/データの公理系やスキーマを与えるものです。その公理系やスキーマを満たす実物をモデル〈model〉と呼びます。インスタンス〈instance〉といったほうが馴染みがあるかも知れません。

モデルを定義するには、指標のすべてのラベル〈label〉(宣言された名前)に具体物を割り当てます。モデル定義の構文は次のようにしましょう。

// (例1) 付点集合のモデル
model NatZero of PointedSet {
  U := Nat
  p := 0
}

NatZero は特定の付点集合の名前、つまりモデルの固有名詞になります。

次は付点集合の別なモデル〈インスタンス | 実例〉です。

// (例1-2) 付点集合のモデル
model NatTen of PointedSet {
  U := Nat
  p := 10
}

半群のモデルも与えましょう。

// (例2) 半群のモデル
model NatAdd of Semigroup {
  U := Nat
  m := natAdd
  assoc := (自然数の足し算の結合律)
}

ここで、natAdd は自然数の足し算(の写像)を意味します。assocに割り当てる“具体物”を書き記すのは難しいのですが、自然数の足し算の結合律が成立するという事実そのもの、あるいは結合律の証明がassocに割り当てる“具体物”です。assocに割り当てられたモノが結合律成立の証拠なので、これがないと「半群のモデル」とは言えません。

他の指標にもモデルを定義します。

// (例3) 人物データのモデル
model Tonkichi of Person {
  givenName := "坂東"
  familyName := "トン吉"
  age := 25
}

// (例4) 平面の座標のモデル
model O of XYCoord {
  x := 0.0
  y := 0.0
}

// (例5) 整数と実数のモデル
model OneTwo IntReals {
  n := 1
  r := 2.0
  s := 2.0
  e := (2.0 = 2.0)
}

(2.0 = 2.0) は、ラベル r に割り当てられた実数 2.0 とラベル s に割り当てられた実数 2.0 が実際に等しい証拠という意味です。

無名のモデル

前節のモデルは、すべて名前〈固有名詞〉を持っていました。

  • (例1) NatZero
  • (例1-2) NatTen
  • (例2) NatAdd
  • (例3) Tonkichi
  • (例4) O
  • (例5) OneTwo

しかし、モデルにいちいち固有名詞を付けていくのは面倒な話です。無名のモデルも認めましょう。無名のモデルを定義する構文としては、名前のところに何も書かないことにしましょうか。

// (例1) 付点集合のモデル
model of PointedSet {
  U := Nat
  p := 0
}

// (例1-2) 付点集合のモデル
model of PointedSet {
  U := Nat
  p := 10
}

悪くはないですが、もっと短く書くために model of を除いて、指標名をタグとするタグ付きデータにします。

// (例1) 付点集合のモデル
@PointedSet {
  U := Nat
  p := 0
}

// (例1-2) 付点集合のモデル
@PointedSet {
  U := Nat
  p := 10
}

タグの先頭にアットマークが付いているのは目立つように(視認性を良くするため)です。横一行で書きたいときは、区切り記号としてカンマを付け加えたほうがよいかも知れません。

// (例1) 付点集合のモデル
@PointedSet {U := Nat, p := 0}

// (例1-2) 付点集合のモデル
@PointedSet {U := Nat, p := 10}

ラベルの省略

指標のモデルは、“ラベルに対する具体物の割り当て”ですが、ラベルを省略して具体物を並べるだけでもモデルを表現できます。例えば、2つの付点集合(のモデル)なら:

// (例1) 付点集合のモデル
@PointedSet (Nat, 0)

// (例1-2) 付点集合のモデル
@PointedSet (Nat, 10)

スッキリしました。もちろん、具体物を並べる順番は、指標の出現順を守る約束です。

他の事例もこの構文で書いてみます。

// (例2) 半群のモデル
@Semigroup (Nat, natAdd, (自然数の足し算の結合律))

// (例3) 人物データのモデル
@Person ("坂東", "トン吉", 25)

// (例4) 平面の座標のモデル
@XYCoord (0.0, 0.0)

// (例5) 整数と実数のモデル
@IntReals (1, 2.0, 2.0, (2.0 = 2.0))

リスト内での出現位置順番をラベルの代わりにすることはよく行われることです。必要があれば指標と突き合わせれば、順番とラベルの関係は確認できます。

不完全モデル

「自然数の足し算の半群」を表すとき我々は、@Semigroup (Nat, natAdd, (自然数の足し算の結合律)) とフルに書かずに、次のような省略をします。

  • @Semigroup (Nat, natAdd)
  • @Semigroup (Nat)

「自然数の足し算が結合律を満たすのは当たり前だから省略してもいいだろう」という気はしますが、単に @Semigroup (Nat) では、足し算の半群とは断定できません。掛け算だって半群になるし、二数の小さい方をとる演算だって半群になります。

あるいは、次のように省略されたモデル〈インスタンス〉記述から、完全なモデルを再現できるでしょうか?

  • @Person ("坂東", "トン吉")
  • @XYCoord (0.0)
  • @IntReals (1)

一部の情報から残りを推測するのは無理です。これらは、「省略された」というより欠損のあるモデルだと考えましょう。欠損部分に疑問符を書けば、次のように書けます。

  • @Semigroup (Nat, natAdd, ?)
  • @Semigroup (Nat, ?, ?)
  • @Person ("坂東", "トン吉", ?)
  • @XYCoord (0.0, ?)
  • @IntReals (1, ?, ?, ?)

指標で定義されたすべてのラベル(すべての順番位置)に具体物が割り当てられてはいない、欠損のあるモデルを不完全モデル〈incomplete model〉または不完全インスタンス〈incomplete instance〉と呼びましょう。

記号の乱用、オーバーロードなどから生じる問題〈課題〉は、与えられた不完全モデルをなんとかして完全にする問題だと言えます。

モデルの不完全さには、次のような欠損もあります; @? ("坂東", "トン吉", 25), @? (0.0, 0.0) -- つまり、データは揃っているが指標〈種別 | タイプ〉が欠損している状況です。

指標と不完全モデルという概念がハッキリすれば、不完全さ〈欠損〉を補完する作業や手法を議論することが出来るようになります。例えば、「型クラスと忘却・追憶構造」は忘却された結果の不完全モデルを補完(再現)する話です。これ以上の「不完全さ〈欠損〉を補完する作業や手法」の話はまたの機会にします。