Chimairaの構文的モジュール化のベースは、再帰代入系という概念である。 再帰代入系は一種の形式的体系である（形式的体系としては非常に単純）。だ が、単一の形式的体系を考えるだけでは意味がなく、すべての再帰代入系を同 時に考えて、その上の演算を考察することが重要である。この記事では、再帰 代入系の定義までを扱い、その上の演算については続く記事に予定している。
随分と以前（なんと、Sat Dec 04 2004）から、BNF（Backus Naur Form） 構文定義をモジュール化（modularize）する記事を書こうとしているのだが、進んでいない。 頓挫している理由は、1つの記事で2つのことをやろうとしたからだ。1つの目 的は、BNFという比較的よく知られた素材により、構文のモジュール化の事例 を提供すること。もう1つの目的は、モジュール化の背景を明らかにすること である。この2つの目的を1つの記事にとりまとめるのはけっこう難しい。
そこで、とりあえず、「モジュール化の背景」だけを別な記事に切り出すこ とにした。それがこの記事ということになる。この記事では、あまりシリアスな実 例が出てこない。それにより、説明としての説得力に欠けるかもしれないが、 実例は後で書く（予定の）記事で色々と取り上げるのでカンベンしていただき たい(*注1)。
[Sat Mar 05 2005 追記] 第8節を追加したので、少しだけ事情が改善 したと思う。
この記事の主題である再帰代入系とは、ある種の等式系（system of equations）であるが、等式達を2つのグループに分け、一方のグループの等式 は代入文と解釈し、別なグループの等式は再帰方程式と解釈するものである。 文法を、再帰代入系だとみなすのが、Chimairaの構文モジュール化の基本方針 である。こうすると、構文的なモジュールをJanusコンポネントに比較的自然 に埋め込める。（そのへんの事情は後の記事で書くことになるが。）
「モジュール化の背景」だけを切り出したにもかかわらず、再帰代入系の定 義をしたところで息切れした。再帰代入系の性質をもっと調べなくてはならな いのだが、それは続く記事にしたい。それで、続きがあることを前提に、タイ トルに「1」を入れた。（「2」も書けますように:-)）
なお、この記事で使っているy=f(x) のような記法は、かなりイ ンチキ臭い。伝統的に使われてきた記法だし、記号操作の経験と直感に頼れば、 理解はできる（むしろ、厳密な方法より理解しやすい）。だが、ハッキリと合 理化されてないのはチョット気持ち悪い。正確な記述をノートとして挿入しよ うかとも思ったが、ノートが長くなりそうなのでやめた。この記事の補遺とし て、説明を追加するかもしれない(*注2)。
[Sat Mar 05 2005 追記] この記事に補遺を書くのではなくて、続く記事の中で、 だんだんと厳密化することになるでしょう、たぶん。
この記事を読むための予備知識はあまり要らないと思うが、形式的体系 （formal system）に慣れてないと辛いかもしれない。形式的体系は、たいて いの論理学の教科書に説明されている。ここで使うのは、形式的体系の項 （term）の定義までで、式（formula）は非常に制限されているし、述語記号、 関係記号、論理結合子などは登場しない。等号が登場するが、これは便宜上の もので、等号なしで定式化することもできる。
形式的体系の説明を含む教科書を、2冊だけ紹介しておく。
『情報科学における論理』は、大きな本ではないが、話題は非常に豊富で、 辞書代わりにも使えて便利である。密度が濃いぶん、説明はそっけない。この 本のなかで、「形式体系」という言葉は多用されているが、この言葉が明確に 定義されている箇所はないようである。形式（的）体系の例がたくさんあるの で、それらから形式（的）体系の一般的な概念は自然に獲得できる、というこ とだろう(*注3)。述語論理に対するtermとformulaは、第2章第2節で定義されて いる。
一般的な形式的体系を“形式的に”定義することに、それほどの意味がある わけではない。どのように定義してみても、その枠からはみ出るような形式的 体系が登場したりする。
『論理学をつくる』は大判で厚みもある本である。教科書／副読本としてよ くできた本で、動機、背景、ココロなども含めて説明は懇切丁寧である。形式 的体系のことを、「（論理のための）人工言語」と呼んでいる。
第2章で命題論理のための人工言語L、第5章で単項述語論理のための 人工言語MPLを導入している。さらに、第7章でMPLから多項述語を加えてPPLへ、 第8章でPPLに等号を加えてIPLに拡張している。形式的体系（人工言語）の 構成や成長がよく分かる。
なお、『論理学をつくる』の体系では、関数記号を使ってない。n引数（n項） の関数記号を(n+1)項述語で置き換えることができるので、関数記号なしでも 間に合うのだが、最初から必要な関数記号は入れておいたほうが便利なときが 多いだろう。『情報科学における論理』では、関数記号ありの定式化をしてい る。
[Thu Mar 10 2005 追記] 形式的体系への導入として、 「『形式的』とは何だろう」という記事を書い た。第4節を読み終わったら、あるいは第4節と並行して、「『形式的』とは何 だろう」を読むといいと思う。
集合XからYへの関数（写像）f:X→Yを、古典的な記法では、y=f(x) と書くこ とがある。この古典的記法では、「xは変域X上の（独立）変数」で、「yは変 域Y上の（従属）変数」ということになる。また、2つの関数f:X→Y、g:Y→Zの 結合（合成）の古典的記法はg・f（実際は、黒丸でなくて白丸）である。
古典的記法g・fでは、fとgが逆順で出現するので、それを嫌って、図式順 （diagrammatic order）の記法f;gもよく使われる。この記事では、古典的な 記法をメイッパイ使うが、図式順も併用する。そのため、結合順を常に意識し てないと混乱するかもしれないので、注意。
古典的な記法 y=f(x) は、式と関数、関係と関数が、あまり 区別されてない時代のなごりである。そのような不明瞭さが、古典的記法の欠 点であるが、この記事では、古典的記法の曖昧さを利用して、記号を節約する ようにしている。
「はじめに」でも述べたように、y=f(x)という書き方や、機械的 な記号操作に慣れていれば、以下の定義に違和感がないだろうが、厳密に言え ばいくつかギャップがある。ただし、経験上、古典的記法とそれに伴う記号操 作でやってもうまくいくことが知られているので、神経質にならなければ問題 はない。
変数として使う記号を前もって十分たくさん用意して、その記号の全体をKと する(*注4)。例えば、一文字'x'（ほんとにエックスという文字）に接尾番号を 付けた記号 x1, x2, x3などの全体をKとする。この場合、Kは無限個の変数記 号を含む。Kとしてどのような記号の集合を選んでもよいが、（潜在的には） 無限個の変数を必要とするから、いくらでも変数を作り出せるメカニズムが必 要である。
Kとしたのは、V（variable）、U（universe）、T(total)などは後で使う予定 があるので、後で使う予定がない文字を選んだだけのことである。
Kの部分集合を‘変数集合’と呼ぶ。Kを上の例のような集合だとすれば、 {x1, x2}, {x100, x200, x300}, {}, {x5}などは変数集合である。変数集合を X, Yなどで示す。ここで出てきた'X'は、「大文字エックス」ではなくて、こ の記事のなかで説明に利用する変数（メタ変数）である。空な変数集合はOで 示す -- O⊆K、O={}である。
次に、項と式を定義するために、関数記号の集合を準備する。定数は0引数の 関数だとみなす。記号の集合F0, F1, F2, ... があるとする。それぞれ、 0引数の関数記号、1引数の関数記号、2引数の関数記号、…の集合である。 i≠jに対して、Fi∩Fjが空であることは要求しない。つまり、関数記 号のオーバロードを許す。Fiの全体をまとめてFと書くこともある。つまり、 F=(F0, F1, F2, ...)。
これらの例に対する項と式は後で示す。
関数記号F0, F1, F2, ... が与えられたとき、‘項’（term）は次の ように帰納的（inductive）に定義される。
上の定義で得られる項の全体をTermF(K)と書く。変数をX（X⊆K）に限定し た項の全体は‘TermF(X)’と書く。特に、TermF(O)は変数を含まない項の 全体である。
先に出したFの例に対して、項の例を挙げる。
0、 suc(0)、 suc(suc(0)) などが項の例である。この例では、項は、「0」 または変数に対して、「suc」を何回か適用した形をしている。suc(x) （successor of x）は、x+1を表すつもりで、気持ちとしては、項は自然数を 表す。
0、 1、 -(1)、 +(1, -(1))、 -(0, 1)、 +(1, +(1, 1), -(0)) などが項の 例である。気持ちとしては、項は整数を表す。「+」と「2引数の-」を中置記 法にすれば、項を 「1 + -(1)」,「0 - 1」, 「1 + (1 + 1) + -(0)」などと書ける。
x, y, zを変数（記号）だとして、EMPTY、 |(x, EMPTY)、 ;(y, *(z))、 ;(|(x, EMPTY), ;(y, *(z))) などは項である。気持ちとしては、項は言語を 表す。 「;」と「|」を中置記法、「*」を後置記法にすれば、項を「x | EMPTY」, 「y ; z*」, 「(x | EMPTY);(y ; z*)」などと書ける。
上の各例で、「気持ちとしては、××を表す」と書いてあるが、これはあく まで気持ちであり、記号に意味を与える必要はない。項とは、無意味な記号 の組み合わせに過ぎない。意味を与えることはあるかもしれないが、それは まったく別なハナシとなる。今の段階では、徹底的に無意味である。
式は、以下のごとく、左辺が変数だけの等式として定義する。式をこのよう に定義するは一般的ではない。再帰代入系のための特別な定義であるから注意。
再帰代入系は等式系とみなせるが、等号「=」が構文構成素として必須なわけ ではない。式は等式の形をしてはいるが、等式的な推論をするわけではない。 左辺は常に変数なので、「v=t」という式の集合の代わりに、Xのメンバーで添 字付けられた項の集合{tv | v∈X}を考えてもよい。これは、変数の集合Xか ら項の集合への写像と言っても同じことである。
しかしそれでも、「=」があったほうが理解しやすいし、等式としての側面も あるにはあるから、無理に「=」を排除することはないだろう。
再帰代入系の定義を与える前に、短くインフォーマルな説明を与える。
多くのプログラミング言語では、等号「=」を代入の記号として使っている。 そして、等号には別な記号「==」などを割り当てる。だが、等号に「=」をそ のまま使い、代入のほうを別な記号（例えば「:=」）で表すプログラミング言 語もある（例：Pascal）。
いずれにしても、代入文と等式（方程式）は別物である。「x=x+1」は代入文 と見ればインクリメント処理であるが、等式と見ると、（通常は）解を持たな い方程式である。だが、記号が流用されるにはそれなりの理由があり、 同じ表現を、代入文とみたり等式とみたりすることもある。
再帰代入系とは、前節で定義した式（変数=項の形）の集合であるが、代入文 と等式（再帰方程式）の区別を明示的にしたものである。その一方で、代入文 を等式として解釈し直す操作も許している（その逆は許さない）。つまり、再 帰代入系では、計算結果を変数に（1回だけ）代入するという操作と、再帰方 程式を解くという操作の2種の操作を表現可能である。つまり、インフォーマ ルには、再帰代入系とは、代入操作と再帰方程式（の解）の表現である。
もっと別なインフォーマルな見方を知りたいならば、再帰代入系の定義（次 節、次々節）をひととおり読んでから、 記事「再帰代入系 2」の 第3節、 第4節、 第5節を読むとよい。
以下で、XとYが共通部分がない変数集合のとき、X∪YをX+Yと書く。逆に、X+Yと書い てあったら、XとYが共通部分がないことを前提として含んでいるとする。
X, Y, Uは、変数集合とする。ただし、X∩UもY∩Uも空だとする。XとYはまっ たく任意でX=Yであってもよい。X, Y, Uのいずれか（全部でも）が空であっても よい。式の集合AassとArecが次の条件を満たすとき、 (X, Y, U, Aass, Arec)を‘再帰代入系’と呼ぶ。Aassは‘代入 部’（assignment part）、Arecは‘再帰部’（recursion part）と呼ぶ。
3つの変数集合X、Y、Uをそれぞれ、Aの‘入力変数集合’（input variable set）、‘出力変数集合’（output variable set）、‘作業変数集合’ （working variable set）と呼ぶ。今後、X, Y, Uが有限集合である場合に限 定する。また、変数集合上には、便宜的な順序（例えば、記号の辞書式順序） があり、変数を一列に並べられるとする。その便宜的順序に従って、X={x1, ..., xn}、Y={y1, ..., ym}、U={u1, ..., up}のように書くことに する。
再帰代入系を具体的に書き下すため、記法上の約束をいくつかする。添字を 付けないx, yなどはベクトル変数を表すとする。つまりx=(x1, ..., xn)、 y=(y1, ..., ym)など。ただし、この約束は慣れないと混乱するので、し ばらくはベクトル変数をx、yなどの太字にする（そのうち、太字はや めてしまうが）。
式の集合Aassを次のように書き下す。
これを、ベクトル変数をx、y、uと、TermF(X+U)に属する項達 のベクトルf=(f1, ..., fn)を使って、y=f(x,u)で 示す(*注5)。このベクトル形式の等式がAassを表す。
f(x)という記法は、「f=(f1, ..., fm)であり、各fjが変 数(x1, ..., xn)を含む可能性がある」という程度に解釈しておけばよい だろう。この記法が、厳密に言えば問題を含むことは、「はじめに」、 「記号、表記に関する注意」で指摘したが、まー、便利だからい いとしましょう。
同様に、Arecはu=α(x,u)で示す。
再帰代入系は、代入部Aassと再帰部Arecで決定されるが、1つの式が どちらの部に属するかを明確にするために、代入部に属するときはletを、再 帰部に属するときはrecを式の直前に付けることにする。 よって、y=f(x,u)とu=α(x,u)) で決まる 再帰代入系を書き下すと次の形になる。
X={x}、Y={y}、U={u}として、次は再帰代入系の例である。
この場合、再帰部をなくした次の形と同値である（同値の定義は後に続く記 事で与える）。
つまり、気持ちとしては、y=x+3という関数を表すと思える。
X={x}、Y={y}、U={u, v}として、次は再帰代入系の例である。
この例は、気持ちとしては、y=-x + 1/2 という関数を表す。
X={x1, x2}、Y={y}、U={u1, u2}として、次は再帰代入系の例である。
この例は、気持ちとしては、y=x2;x1?;x2* という正規表現による定義を表し ている。
論理学やモデル論(*注6)では、値やモノを表すつもりの記号的表現を「項」と 呼び、命題や主張を表すつもりの記号的表現を「式（論理式）」と呼ぶのが習 慣である。だが、日常的には、記号的表現はなんでも「式」と呼ぶことが多い から、項と式を区別することは違和感を感じるかもしれないが、「そういう習 慣なのだ」と思って慣れてくださいな(*注7)。
モデル論（model theory）は、“広い意味の論理学”の一部門といえるが、 いまや、それ自体で膨大な内容と固有の方法論を持つ。
変数や項にタイプ（ソート）を導入すると、式（formula）は真偽値をタイプ とする項で、論理結合子も真偽値を引数／値とする関数記号だと解釈できる。 つまり、タイプ付き体系では、項と式の区別をしなくてもよい。
さて、変数と関数記号（定数は引数なしの関数とみなす）の組み合わせが項 であった。関数記号の集合を適当に選ぶと、たいていのモノを項で表すことが できる。たとえば、小学校で習う算術的表現は、定数（0引数関数）として{0, 1, 2, ...}（自然数を表す記号）を採用し、2引数関数記号に{＋, ×}を取れ ば、項として記述できる。
再帰代入系では、式を「変数=項」という特殊な形に限定しているが、 「項=項」の形を許して、式と式を組み合わせるために「∧（and）」「∨（or）」 「¬（not）」などの論理結合子まで入れれば、中学校で習う方程式の議論く らいは、形式的に再現できるだろう（やったことはないから保証はしないが）。
再帰代入系に限定しても、関数記号集合Fの選び方とその解釈を工夫すれば、 けっこうな表現力を持つ。が、（僕にとっては）再帰代入系のもともとの目的 は、文法記述である。そこで、列と右線形文法を、再帰代入系の項と式で記述 してみる。
まず、{a, b, c}という集合を考える。ここで、a, b, cは、ホントに英字ア ルファベットの最初の3文字である。基本記号{a, b, c}から作られる列には、 "ab"、"aaa"、"b"、"cbcba"などがある。列を項として表現するにはいくつか の方法がある。
関数記号を、F0={$}、F1={a, b, c}, Fi={}（i≧2）と選ぶ。この前提 で、a(b($))、a(a(a($)))、b($)、c(b(c(b(a($)))))などは項であるが、これ がそれぞれ、"ab"、"aaa"、"b"、"cbcba"に対応する。
つまり、変数を含まない項が列に対応する。空列は$である。もちろん、変数 を含む a(x)、a(b(x))のような項も存在する。
関数記号を、F0={a, b, c, empty}、F1={}、F2={conc}、 Fi={}（i ≧3）と選ぶ。emptyは空列を表し、concは連接を表すつもりである。この前提 で、conc(a, b)、conc(a, conc(a, a))、b、conc(c, conc(b, conc(c, conc(b, a))))などは項であるが、これがそれぞれ、"ab"、"aaa"、"b"、 "cbcba"に対応する。
ただし、この表現では、"ab"の表現として、conc(a, b)以外に、conc(a, conc(b, empty))、conc(conc(empty, a), b)、conc(conc(empty, a), conc(b, empty))など、いくらでも他の表現がある。よって、標準的な表現に直すため に、正規化手続きが必要になる。
話が単純になるので、以下では、方法1を使うことにする。いま、次のような 右線形文法を考えてみる。x, yは非終端記号（構文変数）で、εは空列を表す。
2番目と3番目の生成規則を「|」を使ってまとめれば次の形になる。
これはもちろん、正規表現を使えば y=a* と書ける定義である。再帰代入系 として表現すれば、入力変数集合が{}（空）、出力変数集合が{y}、作業変数 集合が{u}だとして、次のように書ける。unionは「|」に対応する関数記号で ある。
次の例は、入力変数集合が{y}、出力変数集合が{z}、作業変数 集合が{}（空）の例である。
特別な例を2つ挙げただけだが、基本記号{a, b, c}からできる任意の正規言 語（に対する右線形文法）は、F0={$}、F1={a, b, c}、F2={union}とい う関数記号集合に対する再帰代入系として表現できることはわかるだろう。
Y={y1, ..., ym}だとして、gがTermF(Y)に属する項であるとする。ま た、f1, ..., fmはTermF(X)に属する項であるとする。このとき、gに出 現するすべてのy1をf1で、すべてのy2をf2で、…、 すべてのymをfmで置き換えた結果をg[f1/y1, ..., fm/ym]と書く。 g[f1/y1, ..., fm/ym]は、TermF(X)に属する。 ここで、[f1/y1, ..., fm/ym]を項に作用する演算子とみなし、‘置き 換え’（substitution）と呼ぶ(*注8)。
「（同時）代入」と呼ぶほうが普通だが、letではじまる式を代入と呼ぶので、 混同を避けるために「置き換え」にした。
特に、f1, ..., fmがすべて異なる変数（つまり、Xのメンバー）である ときは、置き換えを‘変数改名’（variable renamer）と呼ぶ。
項gをg(y)、またはg(y1, ..., ym)のように変数付きで書いていると きは、g[f1/y1, ..., fm/ym]を、g(f1, ..., fm)、 あるいはg(f1(x), ..., fm(x))のようにも書く（ベクトル変数 xをさらに展開することもある）。
変数改名の場合は、{1, 2, ..., m}から{1, 2, ..., m}（mは変数集合X、Yの個 数）への写像ρを使って、g[xρ(1)/y1, ..., xρ(m)/ym]と書け るので、g(xρ(1), ..., xρ(m))という表記となる。
置き換えや、その特殊ケースである変数改名については、続く記事で詳しく 調べる。ここでは、g∈TermF(Y)に対して、yjをfjで置き換える場合に 限っている。より一般には、g∈TermF(Y+S)に対しても「yj→fj」とい う置き換えを作用させることができる。このとき、変数集合Sに属する変数は そのまま残ることになる。残ってしまう変数がヤッカイな存在であり、このヤッ カイ者の処理が、置き換えに関する議論の中心となる。
A=(X, Y, U, Aass, Arec)を再帰代入系だとする。 VをUと同じ個数（p個とする）の変数を持つ変数集合で、(X∪Y)∩V=Oである ものとする。このとき、作業変数集合VをUで取り替えてもよい。具体的には、 ρ:{1, ..., p}→{1, ..., p}を双射（1：1の写像）だとして、 Aの代入部y=f(x, u)と 再帰部u=α(x, u)を、次のもので置き換える。
別な書き方をすると、[r]=[vρ(1)/u1, ..., vρ(p)/up]を変数 改名だとして、次のもので置き換える。
右辺に関しては、yj[r]=yj、 uk[r]=uk[vρ(1)/u1, ..., vρ(p)/up]=vρ(k)である。
さらに簡略な言い方をすると、代入部／再帰部に出現するuiをvρ(i) によって、全部置換してしまうことである。一般的定義は多少ややこしいが、 具体的なケースでは、変数改名は単純な機械的な操作である。
A=(X, Y, U, Aass, Arec)に対して、上記の手続きでUをVに取り替えた 再帰代入系A'=(X, Y, V, A'ass, A'rec)は、もとのAと区別しない ことにする。つまり、作業変数の名前だけが異なるような2つの再帰代入系は、 同じものとみなす(*注9)。
すべての再帰代入系の集合に、作業変数の取り替えにより同値関係を導入し て、この同値関係による商集合を対象にするということ。
例えば、{u, v}と{s, t}の違いだけしかない次の2つの再帰代入系は同じもの である。
A=(X, Y, U, Aass, Arec)が再帰代入系のとき、入力変数集合Xと出 力変数集合Yの組をAの‘プロファイル’と呼ぶ。プロファイルはX→Yの形で書 く。再帰代入系Aが、プロファイルX→Yであることを、A:X→Yと書く。
A=(X, Y, U, Aass, Arec)、B=(Y, Z, V, Bass、Brec)を2つ の再帰代入系だとする。つまり、プロファイルはA:X→Y、B:Y→Zとなっている。 このようなとき（かつ、このようなときに限って）AとBの結合A;Bが定義でき る。
A;Bの定義を具体的に与えるため、AとBを次の形で書き下す。
A:
B:
変数集合UとVの共通部分は空だとする。この仮定が 満たされないときは、UとVのどちらか（あるいは両方）を共通部分がないよう な別な作業変数集合に取り替えておく。作業変数集合の取り替えを行っても再 帰代入系としては同じなので、問題にはならない。ただし、結合の定義が作業 変数集合の取り替えにより影響を受けないことを確認する必要はある(*注10)。
続き記事で実際に確認することにする。
AとBの（この順での）‘結合’（composition）A;Bは次の形で与えられる。
ベクトル記法を使えば、次のように簡略化される。
A={let y=f(x, u), rec u=α(x, u)}、 B={let z=g(y, v), rec v=β(y, v)}とす れば、A;B=B・Aは次のように書ける。
また、置き換え[f1/y1, ..., fm/ym]を使って書けば次のようになる。
ベクトル記法を使えば、次のように簡略化される。
第8節に出てきた2つの文法記述を、それぞれ次の形で書いておく。 「{y}←{}」などは、（便宜上、矢印の向きが逆だが）プロファイルを示して いる。
プロファイルは、A:{}→{y}、B:{y}→{z}であり、作業変数集合も分離してい る（片一方が空だ）から、結合できる。その結果は次のとおり。
B・Aの内容は、正規表現を使えば、z=bca* という定義となる。
この記事では、変数の集合Kと関数（記号）の集合Fを固定して、K、Fによる 再帰代入系の定義と、2つの再帰代入系の結合の定義を与えた。
続く記事（のどれか）では、ここで与えた結合以外に、もう1つの演算として集約 （aggregation）を定義する(*注11)。結合と集約に関して、再帰代入系の全体が対称 モノイド圏になることを確かめる。これはつまり、 再帰代入系に関してETBダイヤグラムを描けることを 意味する。さらに、トレースにあたる演算Recを導入する。Recは、代入部の等 式を、再帰部に移動するような操作である。Recが存在する点が、再帰性の本 質である。
ごく小数の人のためにコメントしておくと、集約とは、僕がかつて（1955年 から2000年くらい）「マージ」と呼んでいた演算である。「集約」のほうが一 般的（慣例的）なようなので、この呼び名にした。
KとF上に定義された再帰代入系の全体をRAS(K, F)と書くと、KとFがパラメー タになっている。Kを固定してFを動かす、Fを固定してKを動かす、あるいはK とFの両方を動かすと、indexed categoryが現れる。再帰代入系に適当な意味 論を与えれば、その全体はインスティチューション（institution）類似 な構造になる（通常のインスティチューションになるかどうかは、まだわから ない）。このようなindexed categories（またはファイブレーション）、イン スティチューションの構造も調べる必要がある。
再帰代入系が、ソフトウェア的に実現できることも保証しなくてはならない から、再帰代入系の圏からJanusコンポネントの圏への埋め込みを構成しなく てはならない。このへんに関しては、以前、小さなひな形をいじったことはあ る。たぶん、できるだろう（楽観的:-)）。