檜山正幸 (HIYAMA Masayuki)
Wed May 11 2005:start
Sat May 14 2005:draft
Mon May 16 2005:prefinal
形式的体系の初歩的知識を仮定して代数と余代数の紹介を試みる。特別な条 件を満たすソート付き形式的体系の指標（signature）を代数指標／余代数指 標と定義して、それのモデルとして代数／余代数を導入する。余代数とオブジェ クト指向との関係にも言及する。
1. はじめに
後々の説明の都合を考えると、代数と余代数について早めに解説すべきだ、 と感じた。そこでこの記事では、あまり予備知識を仮定しない(*注1)で、代数 と余代数をラフかつインフォーマルに紹介する。
注1
圏論はまったく使わない。
「余代数」は聞き慣れない言葉かもしれないが、「代数」という言葉には、 なにかしら（それぞれに）印象を持っているだろう。そういう印象や先入観 はすべて捨てたほうがいい。この記事で導入する概念・用語である「代数／ 余代数」とは、特定の分野における専門用語（ほとんどジャーゴン）である。 既にあなたが知っている代数とは接点を持たない概念かもしれない(*注2)。分 かりにくいと感じたら、見出しに「解説：」と付いているノートも一緒に読む とよいだろう（原則としてノートは飛ばしてもよいが）。
注2
実際のところ、この記事で導入する代数概念の特殊ケースとして通常の代数 概念が説明できる。だが、最初はそのようなことを気にしないほうがいい と思う。
2. 事例の提示
この記事全体で、記事「『形式的』とは何だろう」 と記事「『正規（regular）』とは何なんだ 3 補足、実例など」を参照する。特に、 「『正規（regular）』とは何なんだ 3」の第3節で導入したソート付き の形式的体系の概念を再確認してほしい。
この節では、いくつかのソート付き形式的体系を事例として挙げる。なお、 事例に付けられた名前（例：「ペアノ流の自然数」）は、気持ち（下心）を表現し たものであり、その名前から連想されような"意味"を持つとは限らない。体 系の名前は、名目上は単なるラベルである。なお、下心（したごころ）につい ては、 「『形式的』とは何だろう」の第5節を参照。 理解をうながすために、下心（「××に使いたい」、「××に使うつもり」） も説明されているが、あくまでも「こんな下心もあり得る」というだけであ ることに注意。
・ 事例1： ペアノ流の自然数
- ソートの集合：{Nat}
- プロファイル「->Nat」の関数記号の集合：{0}
- プロファイル「Nat->Nat」の関数記号の集合：{suc}
ソートの集合が単元（singleton）集合{Nat}なので、これはソートなしの体 系として定式化してもいいのだが、ここでは明示的にソートNatを考える。Nat は自然数の全体、sucは1を足す関数（例：suc(1)=2）のつもりである、
・ 事例2： 自然数の算数
- ソートの集合：{Nat}
- プロファイル「->Nat」の関数記号の集合：{0, 1}
- プロファイル「Nat, Nat->Nat」の関数記号の集合：{add, multiply}
気持ち（下心）としては、足し算（add）と掛け算（multiply）を含む計算式 （項）を記述したい。定数は0と1だけだが、もちろん実際はもっとたくさんの 定数を導入するほうが便利だ。今は便利さを問題としてはいないけれど。
・ 事例3：スタック
- ソートの集合：{Item, Stack}
- プロファイル「Stack->Item」の関数記号の集合：{top}
- プロファイル「Stack->Stack」の関数記号の集合：{pop}
- プロファイル「Stack, Item->Stack」の関数記号の集合：{push}
これは単純化してあって、スタックがあふれたり、空になっても特にエラー や例外は出ないとしている。適当に特殊値を選んで、スタックが空であること を知らせるような状況を考えよう（あくまでも気持ちの問題）。
・ 事例4： Tiny Toy XMLのインスタンス
「『正規（regular）』とは何なんだ 3」 の第4節とは違って、Tiny Toy XMLのインスタンスについて考えるから注意。 choiceは言語に対する演算でインスタンスには定義できないので除いてある。 （といったことも、気持ちの問題だが）。- ソートの集合：{Name, Tree, List}
- ソートの順序： Tree < List
- プロファイル「->Name」の関数記号の集合：すべての名前リテラル
- プロファイル「->List」の関数記号の集合：{empty}
- プロファイル「List,List->List」の関数記号の集合：{concat}
- プロファイル「Name,List->Tree」の関数記号の集合：{surround}
NOTE: 解説：形式的体系は無意味な記号システムに過ぎない
くどいが、形式的体系を理解するカナメは、記号とその意味を区別する ことである。記号システムが提示された段階では、その意味は特定されていな い。例えば、上の「事例1： ペアノ流の自然数」に出てくる、Nat、0、sucという 記号は単なる記号であるから、Foo、hoge、helloと改名しても本質的な変化は ない。
「まったく意味を持たない」ことと、それでも「暗黙には使用法を想定して いる」という、やや矛盾した状況を表現するために僕は、「下心 = まだ行使さ れてない隠れた意図」という言葉を使っているのだ。
3. 形式的体系の指標（シグニチャ）
前の節で挙げた4つの例を、次のような構文で記述することにしよう。
/* 事例1： ペアノ流の自然数 */ signature Peano { sort: Nat; function: 0:->Nat; suc:Nat->Nat; } /* 事例2： 自然数の算数 */ signature Arith { sort: Nat; function: 0, 1:->Nat; add, multiply:Nat->Nat; } /* 事例3：スタック */ signature Stack { sort: Item, Stack; function: top:Stack->Item; pop:Stack->Stack; push:Stack, Item ->Stack; } /* 事例4： Tiny Toy XMLのインスタンス */ signature TinyToyXMLInstance { sort: Name, Tree, List; order: Tree < List; function: // // 名前リテラルは膨大になるので省略 // empty: ->List concat:List, List ->List surround: Name, List ->Tree } この記法で、signatureという綴りが出てきたが、「ソート集合、ソートの順 序（あれば）、関数記号集合」の記述を、形式的体系の'指標'（シグニチャ、 signature）と呼ぶ。指標が与えられると、（変数を含まない）項の集合が完 全に定まる。例えば、Peanoという指標の項は、0, suc(0), suc(suc(0)) など である(*注3)。
注3
