Janusコンポネント・アーキテクチャに含まれる計算系（calculus）について 述べる。用語や予備知識の説明などはしてない（別記事でする予定）。メイヤー の契約（contract）概念に興味があるなら、「極性付きのアリティ計算」だけ を拾い読みできる。
記事「Janusについて雑多なこと」で述べたように、 Janusの目的は、既存のコンポネント・アーキテクチャのそれとは異なる。複 数のコンポネントの構成演算（composing operation）、組み合わせ方や出来 た複合構築物（composite, compsition）を明確に記述し、計算できるようにすることだ。
だからJanusには、最初から多くの計算系／計算方法（calculus、 複数はcalculi）が備わっている。コンポネントの組み合わせや、組み合わせ の変更などが計算により系統的に行える（はずだ）。どうも、既存のコンポネ ント・アーキテクチャには、まともなカルキュラスがないように思える（僕の 見落とし／勘違いかもしれないが）。
Janusのなかには、次のようなカルキュラスが存在している。
この3つは、いずれも演繹系（deduction system）あるいは証明系（proof system）として定式化できるようなカルキュラスになっている。まだ、十分に 形式化（formalize）できてないし、これらのカルキュラスを外から調べて、 健全性や完全性を示すのは今後の課題だ。が、そんなに堅いことを言わなくて も、これらのカルキュラスをある種の“算数=計算の技術”として実用に使う ことができると思う。むしろ、使っているうちに、これらのカルキュラスの性 質が分かってくるかもしれない。
以下に、アリティ計算、プロファイル計算、形式的リファクタリングを簡単 に説明する。最後に、バートランド・メイヤーの契約概念と極性の関係につい て触れる。 用語や予備知識の説明はあまりしてないし、参照先も示してない。 とりあえずの備忘であり、いずれももっと詳しく書くつもりだ。
σA,Bを、AとBを入れ替える操作（クロス、対称）、ΔAをAを2倍に クローンする操作（重複、二倍化、対角）だとする(*注1)。σA,B:A, B →B, Aと、ΔA:A→A, Aを推論だと考えると、次のような推論図（NK風） を書ける。
A, B ------σ B, A A ------Δ A, A
記事「ETBダイアグラム」では、σ、Δ、ιではな くて、それぞれX、∇、Iだった。また、この記事の×は、「ETBダイアグラム」 では+である。
ジャンクションが推論図に対応し、σは論理の「換」に、Δは論理の「増」 にほぼ対応する。推論図の積み上げ（上から下だから、“積み下げ”か）が直 列結合。推論図や証明図を横に並べることが並列結合になる。たとえば、A, B →B, A, Aというワイヤリングができることは、次の証明図が示している。
A, B ------σ B, A ~~~~~~~~~~ B A ---ι ------Δ B A, A ~~~~~~~~~~~~ B, A, A
この図で、ιは恒等射である。横波線は、特に何もしてないが、証明図を分 岐させたり合流させたりする印だ。この証明図を式（記号的表現）(*注2)で 書けば次のようになる。この式が表す射が、証明図のセマンティクスだといっ てもよい。
正確に言えば、形式的圏論の項である。式（項）が表す射とは、モデル（解 釈）である対称モノイド圏の射である。
アリティ計算系は簡単な系だ。今の例なら、A, B |- B, A, A が示せたわ けだが、一般に、「x |- y ⇔xからyへのワイヤリングが存在する」となる。
プロファイルは A1, ..., An → B1, ..., Bm の形なので、これは シーケントとみなせる。よって、プロファイル計算はケーケント計算である。極性 を考えるときは、極性（プラスとマイナス）が肯定・否定と似た役割を演じる。 たとえば、次の推論が使える。
A, B → C ----------- A → B*×C
ここで、B* はBの極性を逆転したもので、×はなんらかの積である（実際に は、並列結合）。B*×Cを含意B⊃Cだと思えば、見慣れた規則になる。この推 論が使える理由（セマンティクスの裏付け）は、コンパクト閉圏Cでは、 C(A×B, C)とC(A, B*×C)のあいだに1対1の対応があることだ。
プロファイル計算に現れる証明図は、あるコンポネントから、別なプロファ イルのコンポネントを構成する自然な方法を示している。このとき、コンポネ ント実装に手を加えるのは望ましくないから、基本推論図が実装非依存のプロ ファイル操作に対応するような証明系がよいと思う。そのような証明系を構成 すれば、 「x |- y ⇔プロファイルxからプロファイルyへのプロファイル操作が存在す る」となる。
形式的リファクタリングは、あんまりよく分かってない。雰囲気を説明しよ う。tが、プロファイルA→Bである項だとしよう。「項」とは、記号的表現だ と思っても、ETBダイアグラムのような図式だと思ってもどっちでもよい。い ずれにしても、項を単純化する操作は存在する。たとえば、2回続けたクロス は削除してよい（σA,B;σB,A=ιA×B）。
tをより簡単にするとは、項に関する等式的体系があり、その等式的体系を項 書き換え系とみなして計算が実行されることだろう。tが簡単になっても、プ ロファイルもセマンティクス（コンポネントの機能性、振る舞い）は変わらな い。というか、変わらないような変形操作でないとまずい。形式系（formal system）上で行えるリファクタリングだから、形式的リファクタリングと呼ん だわけだ。
圏論との関係で言えば、次の表のような対応があるだろう。
| カルキュラス | 命題／計算対象 | 推論／計算行為 |
|---|---|---|
| アリティ計算 | 圏の対象 | 圏の射 |
| プロファイル計算 | 圏の射 | 圏的オペレータ、自然変換 |
| 形式的リファクタリング | 圏の射 | hom-圏の射（2セル） |
ここで、バートランド・メイヤーの「契約」（contract）概念について考え てみる。メイヤーの契約概念を、上で述べたアリティ計算に取り込みたい下心 があるからだ。
インターフェースAを、利用者と実装者の契約書とみなそう。契約が成立すれ ば（つまり合意がとれれば）、利用者はAを使う権利を手に入れ、実装者はAを 実装する義務を負う。権利と義務には、次の性質がある。
このことから、権利と義務には双対性（duality）があるような感じがする。 この点をもう少しハッキリさせるため、インターフェース間の“大小関係”を 定義しよう。
Java言語では、インターフェースBがインターフェースAから派生したことを、
interface B extends A と書く。これは、「Bは、Aを拡大している」という
ことだから、比喩的に「BはAより大きい」となる。そこで、不等号を用いて、
A≦B と書くことにしよう(*注3)。
この不等号の向きは、後の話とツジツマをあわせるためのこじつけだ。たと えばRubyでは、"B extends A" を "B < A" と書くから、これを根拠に「BはA より小さい」というこじつけも可能なのだ。
ところでJanusでは、インターフェースに極性（プラス・マイナス）を付けて 型を指定する。+Aは「Aを利用する権利」を示し、-Aは「Aを実装する義務」を 意味する。いま、次の形の推論図を「αがOKなら、なおのことβもOK」と解釈 しよう。αやβは、権利や義務を表現する。
α ---- β
インターフェースAとBのあいだに A≦B （B extends A）の関係があるとき、 次が成立する。
+A ---- +B
これは、「+AがOKなら、なおのこと+BもOK」ということだが、「OK」の意味 を「この権利で十分である」「顧客として満足している」と解釈しよう。そうする と、「Aを利用する権利で満足しているなら、なおのことBを利用する権利にも 満足する」ということになる。これはつまり、「権利が縮小すると利用者は困るが、 拡大しても何も困らない」ことを表現している。
同様に、A≦B の関係があるとき、次が成立する。
-B ---- -A
その解釈は、「Bを実装する義務を果たしているなら、Aを実装する義務も果 たしている」であり、「義務が拡大すると実装者は困るが、縮小しても何も困 らない」ことを表現している。
A、Bがインターフェースや仕様であるとき、A≦Bが前もって分かっていれば、 極性付きアリティ計算の計算系に、+A |- +B と -B |- -A を、推論規則とし て組み入れることができる。おおざっぱに言えば、A ≦ B という絶対値の不 等式があれば、+A ≦ +B と -B ≦ -A という符号付きの不等式を導入してよ い、ということだ。
例えば、A≦B、C≦Dの仮定のもとで、次の証明図が書ける。
+A, -D ~~~~~~~~~~~ +A -D ---- ---- +B -C ~~~~~~~~~~~ +B, -C
よって、+A, -D |- +B, -C だが、これは、「Aの利用権限で満足しており、 Dの実装義務を果たしているなら、Bの利用権限にも満足し、Cの実装義務を果た しているといってもよい、大丈夫」という解釈になる。
実際には、極性付きアリティ計算は、極性付きプロファイル計算（シーケン ト計算）の一部となるだろう。そうなると、「入力側の権利と義務、出力側の 権利と義務」という4つの契約要素に関する計算ということなる。
どうやら、こういうハナシは線形論理と関係するらしいのだが、僕は線形論 理をよく知らないので、詳しいことはわからない。