「正規(regular)」とは何なんだ 3
補足、実例など

檜山正幸 (HIYAMA Masayuki)
Wed Apr 20 2005:start
Tue Apr 26 2005:draft

再帰テンプレート、ミュー項、それによる表現力の増強(代数系の拡大に対応す る)などの実例を挙げる。例には、極端に単純化したXML風データ Tiny Toy XML を用いる。

目次

1. はじめに

正規性という概念を探ろうとした記事:「『正規 (regular)』とは何なんだ」は、まーまーな記事かと思います(キマイラ・ サイト内では、ね)。それに続く「『正規(regular)』 とは何なんだ 2 正規構造」は、長すぎましたね。未整理でゴチャゴチャな 感じ。正規性は、再帰代入系とも深く関係するのだけど、 「再帰代入系 1」「再帰代入系 2」も読みやすくは なく、しかも、まだ再帰代入系の話は全然完了してません。

と、そういう状態で、同じ話題でさらに記事を追加するのもどうか? とも感 じます -- 宙ぶらりん状態の続きを先に書くべきだろう、とかね。が、キマイ ラ・サイトは素材置き場であり、体系性、一貫性、完成度は目的ではないので、 ひらきなおることにしました(つまり、「順序はどうでもいい」、「質より量」 だ!と)。

で、この記事は、引き続き再帰(recursion)や正規性(regularity)を話題 にしますが、、副題のとおり、Tiny Toy XMLを素材とした実例を中心にしてい ます。あまり厳密ではありませんが、正規構造の感じをつかむにはいいかもし れません。

2. Tiny Toy XMLと構文パターン

「『正規(regular)』とは何なんだ」の第8節で も「『正規(regular)』とは何なんだ 2 正 規構造」の第16節でも「XMLの事例」を取り上げてます。その素材は、雑誌 に書いたことがあるTiny Toy XMLです。ここで一応、‘Tiny Toy XML’の構文 を定義しておきましょう。

「名前」と「空白文字」は前もって決まっているとします(その定義は、常 識の範囲内なら適当でいいです)。

 空白 ::= 空白文字+
 要素 ::= '<' 名前 '/>' 
        | '<' 名前 '>' 内容 '</' 名前 '>'  /* 条件:名前が一致 */
 内容 ::= (空白? 要素)* 空白?

もちろん空白は無視可能で、 <名前/><名前></名前> の略記とみな します。“正規化”されれば、空白は削除され、略記は展開されます。インス タンスの同値性は“正規形の同一性”(*注1)で判断され、マークアップの “ゆれ”は考慮しないことにします。

注1

同一性は「一字一句違わない」ことです。ただしこの定義は、インスタンス がキャラクタ・シーケンスにシリアライズできることを仮定してます。

今までの記事では、ほんとのリテラル(Tiny Toy XMLインスタンスそのもの) と、変数(プレイスホルダー)を含む“Tiny Toy XML パターン”を構文的に は区別せず、説明(地の文)で構文的パターンであることを指摘してきました。 これでは面倒だし間違えることもありそうなので、この記事では、パターン変 数には必ず'$'を付けて識別することにしましょう。 <a/> はリテラルだけ ど、 <$a/> はパターンになります。(リテラルも変数を持たない特別なパ ターンとみなせるけどね。)

NOTE: 用語法で苦しむ!

上で「パターン」と書いたものは、「テンプレート」と呼んだほうがいいと 思うでしょ。そのとおりなんですが、 しかし! 後で「『正規(regular)』とは何なん だ 2 正規構造」で導入した「再帰テンプレート」という用語が出てくるの で、それとの混同を避けるためにパターンと呼んだわけです。

再帰テンプレートは、最初は「再帰スキーム」と呼んでいたのですね、個人 的に。しかし、「スキーム」はいろいろな所で使うし、「テンプレート」の ほうが親しみやすかろうと「スキーム」から「テンプレート」に変更したので す。(正規構造を定義するスキームを正規スキームと呼ぶと、代数幾何の用 語ともろにバッティングするのもイヤだった。)

ところがそうすると、今度は、一般的にテンプレートと呼ばれている対象を 呼ぶ言葉がなくなってしまうという事態。いったいどうしたらいいの? 再帰 テンプレートに類似の概念で再帰子(recursor)ってのがあるから、再帰テン プレートを再帰子って呼んでしまってもいいかもしれない。が、となると、算 術テンプレートはどう呼ぶ? 算術子?これは変だ。 ウーン。

パターン変数には型があり、型ごとに出現してよい場所も決まってます。型 はName, Tree, Listであり、Tree型はList型の文脈に出現可能で、自動的に (暗黙の)型変換がされるとしましょう。例えば、$xがTree型のとき、 <a>$x</a> は合法で、$xは長さ1のリスト(を表す変数)として解釈されま す。

念のために言っておきますが、ドル記号による変数識別は僕の好みじゃあり ません。ドル記号が散らばると、なんか汚い感じがしてイヤ。だけど、世 間では、ドル記号が圧倒的によく使われるから迎合した。僕は原理主義者じゃ なくて迎合主義者だからね。

3. ソート付きの形式的体系

「『正規(regular)』とは何なんだ」の第8節の 内容を、もっとちゃんと述べるには、形式的体系に「ソート」(sort)を導入 しないといけませんね。ここで言うソートってのは、順序よく並べる(整列) のことではありません、「型識別子」とでも訳せばいいのか? まー、いっ そ「型」(タイプ)と言ってしまってもいいのだけど、伝統的にソートと呼ぶ のだな。そのココロは、単なる名前/記号であることを強調したいから、であ ろう。つまり、型概念の定式化ではあるのだが、あくまで形式的体系内に記 号として存在するのがソートなんでしょう、たぶん。

ソート付きの形式的体系では、まずソート(あくまで記号です!)の集合Sを 準備して、さらに、s1, s2, ..., sn, s ∈Sを使って s1, s2, ..., sn->s のような複合記号(これもあくまで記号!)を考える。この複合 記号もソートと呼ぶことが多いが、ランクとかアリティとかプロファイルとも いいます。僕は、プロファイルと呼びます。プロファイルのココロ(インフォー マルな意味)は、関数の型(プロトタイプ)宣言ですね。

プロファイル記号 s1, s2, ..., sn->s は、n個の引数の型がそれぞれ s1, s2, ..., sn であり、戻り値の型がsであることを示します(イン フォーマルには)。->s というプロファイル記号は、ソート記号sと事実上同 じ。なぜなら、 プロファイル ->s は戻り値がsであり引数を持たない関数を表すけど、それは sの値といっても同じだからね。矢印「->」の左に何もないのがさびしいなら、 空を表す「ε」とかを書いておいてもいいけど、僕は面倒だから何も書かない。

関数記号はプロファイルごとに準備されるので、今までみたいに F=(F0, F1, F2, ...)という列ではなくて、F = {Fp : pはプロファイ ル} という感じです。つまり、“プロファイルで添字付けられた記号集合の族”と して関数記号レパートリを準備するのです。

例えば、S={s, v}として、ソートsがスカラー、vがベクトルだとして次の記 号を考えましょう。(ベクトル計算の用途を想定。)

  1. スカラー定数の0
  2. スカラー定数の1
  3. スカラーの足し算 +
  4. スカラーの掛け算 *
  5. ベクトル定数のO
  6. ベクトルの足し算 + (オーバーロード)
  7. スカラーとベクトルの乗法 ・

これらの記号をソートごとに分類して振り分けると:

  1. F->s = {0, 1} (スカラー定数)
  2. F->v = {O} (ベクトル定数)
  3. Fs,s->s = {+, *} (スカラー演算)
  4. Fv,v->v = {+} (ベクトル演算)
  5. Fs,v->v = {・} (スカラーとベクトルが混じった演算)
  6. その他のFp は {}

関数記号にソートが付くと、変数もソートごとに準備する必要があります。 今の例なら、スカラー変数の集合Xs とベクトル変数の集合Xv ですね (*注2)。習慣では、スカラー変数とベクトル変数は書体を変えますね、ベクト ル変数はボールドとか。あるいは、ベクトル変数(定数でも)は上に矢印を引 くとか。こういうふうに明示的に変数を分けないときは、「文脈から推測して ね」という約束があります(*注3)(人間が型推論するのだ)。

注2

実用上は、ソートが指定されてない変数の集合Xを準備して、変数のソート (型)宣言によりローカルなソート付き変数環境を作って使う、という流儀が 多いようです。自然言語による説明文でも、(インフォーマルに)ローカルな 環境を作り、その環境内で説明を書きますよね。

注3

変数などの記号を、ソート(型)ごとにちゃんと書き分けるかどうかは大 問題です。many many sortedになると、書体とか文字飾りでは区別がつけら れなくなります。仮にたくさんの書体/飾りを使い分けても煩雑になるだけで 逆効果。結局、文脈/環境により、同じ記号をいろいろな目的に使い回す(オー バーロードする)ことになるのですが、これもやりすぎると「何がなんだかわから ない」ことになります。

関数記号、変数記号にソートが付けば、当然に項にもソートが付く。s∈Sご とに、ソートsの項が定義できます。ちなみに、今使った「s」は、 ソートを表す変数、さっきの例に出てきた「s」はスカラーという特定の ソートを示す定数、ややこしいですね、これぞ形式的体系を説明するとき に出会う困難。で、以下の「s」はソートを一般的に表す変数だと思って読ん でね。

  1. F->sに属する関数(実は定数)記号はソートsの項。
  2. Xsに属する変数記号はソートsの項。
  3. t1, ..., tn がそれぞれソートs1, ..., snの項であり、aがプロ ファイルs1, ..., sn->sの関数記号のとき、a(t1, ..., tn)はソー トsの項。
  4. 以上の手順により得られたものだけが、ソートsの項。

実は、ソートsの項よりは、プロファイルが s1, ..., sn->s の項を考え た方が整合的になるのだけど、世間では「ソートsの項」で済ませちゃう例が 多いので、これでいいとします、今回は(*注4)

注4

s∈Sに対して「ソートsの項」が使えれば、たいていは間に合うので、まー別 にいいのですが、「s1, ..., sn->s の項」、さらには、 「s1, ..., sn->t1, ..., tm の項」まで考えた方が視野が開けます から、そのような構成法についての記事を書くかもしれません。

4. Tiny Toy XMLを記述する形式的体系

言い忘れた:ソートなしの形式的体系は、実は単一のソートがあるとも思え る。よって、Sが単元集合のとき(単一ソートのソート付き体系)はソートが ないに等しい。Sが2つ以上のメンバーを含むときソートが問題となるので、ソー ト付き体系は‘多ソート’(many-sorted)体系とも呼ぶ。

さらに、ソート集合S内に順序があるときは‘順序ソート’(order sorted) 体系です。この順序とは何かというと、s < s' のときはsからs'への暗黙の型 変換ができるってことね。

ふー、これで話が先に進む。

実は、Tiny Toy XMLの構文記述システム(「『正規 (regular)』とは何なんだ」の第8節)は、順序ソート体系なんです。ま ずソートの集合は{Name, Tree, List}という3つのソートを含む集合。これに は順序 Tree < Listがある。

ソート付きの関数記号集合は次のとおり(*注5)

  1. F->Name = 名前リテラル全部
  2. F->List = {empty}
  3. FList,List->List = {concat, choice}
  4. FName,List->Tree = {surround}
注5

choiceやconcatをオーバーロードするのは止めて、型変換で済ませることに した。例えば、Tree型の項tとsに対するchoice(t, s)は、tとsをList型に自動 型変換して考えます。このほうがスッキリしている。

変数記号の集合はXName、XList、XTreeの3種が必要だが、次の ようなイイカゲンな約束でお茶を濁します、とりあえず。

  1. 英字アルファベット小文字の前のほうの文字(a, b, cなど)からはじま る名前はXNameに属する変数。
  2. 英字アルファベット小文字の後のほうの文字(u, v, x, yなど)からはじ まる名前はXListに属する変数。
  3. 英字アルファベット文字からはじまる名前はXTreeに属する変 数。

なお、名前リテラルは、'a'とか'foo'のごとく一重引用符で囲む。あ、それ と、上のようなイイカゲンな約束では「あんまりだ」ってときは、ちゃんと変 数の型(ソート)宣言をすることもあります(*注6)。何の宣言もないときは、イイカ ゲン・ルールで型推論してください。

注6

結局この記事の中では、一回も宣言を使っていない。

さーこれで、surround('a', concat(X, u)) がTree型の項だってことが合理化 できた。先に進みましょう。

5. 項のパターン表現

前の節で定義した順序ソート付きの形式的体系に名前(固有名詞)を付けて おきます。Tiny Toy XML の構文記述(syntax description)体系だから、 TTX-SD1とでもしましょう(あまりにも芸がないネーミング)。お尻の「1」 は、「最初のもの」という程度。

TTX-SD1には、Name, Tree, Listのソート(型)がありますから、ソートごと に項が定義されますね。念のため、各ソートに対する項の定義を具体的に書き 下しておきましょう。(以下の説明で出てくる n, x, yは、説明のために使う メタ変数で、形式的体系に含まれる変数ではありません。)


・ Name項

  1. ソートがNameである定数(名前リテラル)はName項である。例:'a', 'foo'
  2. ソートがNameである変数(名前変数)はName項である。例:a, b
  3. 以上により得られるものだけがName項である。

・ Tree項

  1. ソートがTreeである変数(ツリー変数、要素変数)はTree項である。例:E, T
  2. nがName項で、xがList項であるとき、surround(n, x)はTree項である。例: surround('a', empty)
  3. 以上により得られるものだけがTree項である。

・ List項

  1. emptyはList項である。
  2. ソートがListである変数(リスト変数、列変数)はList項である。例:u, v
  3. すべてのTree項は、(自動型変換により)List項である。
  4. x, yがList項であるとき、concat(x, y)はList項である。例:concat(empty, u)
  5. x, yがList項であるとき、choice(x, y)はList項である。例:choice(u, v)
  6. 以上により得られるものだけがList項である。

例えば、surround('foo', concat(surround(a, empty), surround('bar', x))) はTree項です。ただし、aはName変数で、xはList変数だとする。(ここ で出てきた a, xは、形式的体系に含まれる変数です。いいすっか?)

関数記号の入れ子である項は見にくいから、もっと見やすくなるように、項 にパターンを対応させましょう。いま例に出した項なら、次のパターンに なります。

<foo>
 <$a/>
 <bar>$x</bar>
</foo>

項からパターンへの翻訳規則を厳密に述べることもできるけど、面倒だから おおよその方針だけを次に記します。

  1. 変数にはドル記号を付ける。変数のソートは、暗黙または明示的な宣言で 示す。(暗黙のイイカゲン約束は既に述べた。)
  2. 空白はどうせ無視するので、適当に入れてよい。
  3. まとまりを付けるために、適宜丸括弧(「(」と「)」)を使う。
  4. emptyは、何も書かないか、またはEMPTYで示す。
  5. choiceは「|」で示す。
  6. concatは特に演算記号(メタ文字)を使わない。
  7. surroundはタグ形式で書く。

もうひとつ例をあげましょう。次の項(インデントしてもやっぱり見にくい) は、その下に書いたパターンに翻訳されます。

concat(x, 
       concat(surround('foo', 
                       choice(empty, 
                              surround(a, x))),
              surround('bar', empty)))
($x (<foo>(EMPTY | <$a>$x</$a>)</foo> <bar/>))

「パターンもXML構文で書く」という提案(下はその例)はごもっともだし僕 好みでもあるが、見やすさに関してはたいして貢献しないから(今の文脈では) 却下。

<p:list xmlns:p="PatternNamespaceURI">
 <p:variable name="x" type="list" />
 <p:list>
   <foo>
    <p:choice>
      <p:empty/>
      <p:tree>
       <p:variable name="a" type="name"/>
       <p:variable name="x" type="list"/>
      </p:tree>
    </p:choice>
   </foo>
   <bar/>
 </p:list>
</p:list>

6. 基礎パターンと単純パターン、マッチング

変数を含まない項は‘基礎項’(ground term)といいます。これに倣って、 パターン変数を含まないパターンを‘基礎パターン’と呼びましょう。当然に、 基礎パターンとTiny Toy XMLインスタンスは事実上同じ概念です。事実上同じ なら区別しなくもよさそうですが、基礎パターンはパターンの世界の住人であ り、インスタンスの世界の住人とは区別することもあるのです。

ここだけの用語ですが、演算記号「|」を含まない項を‘単純項’(simple term)、それに対応するパターンを‘単純パターン’と呼ぶことにします。

パターンとインスタンスが「マッチする」ということをちゃんと定義してま せんが、それは常識と直観に頼ることにして、マッチングに関して次が成立す ることを注意しておきます。

  1. インスタンスが、基礎パターンとマッチする ⇔ インスタンスが、基礎パター ンと(構文的に)一致する。
  2. インスタンスが、単純パターンとマッチする ⇔ インスタンスが、単純パター ンに出現する変数を適切に具体化したものと一致する。
  3. インスタンスが、n個の単純パターンp1, ..., pnを使って (p1 | ... | pn) と書けるパターンとマッチする ⇔ インスタンスが、p1, ..., pnの少なくともどれか1つとマッチする。
  4. どんなパターンも、n個の単純パターンp1, ..., pnを使って (p1 | ... | pn) と書ける。

最後の命題は説明が必要でしょう。「と書ける」とは何かというと、同値な パターンで、(p1 | ... | pn) の形のものがあることで、同値とは、マッ チングの能力がまったく同じことです。これを示すには、構文的な議論だけで は辛いので、surroundに対応するホントの演算(仮に★としよう)が次の性質 (ある種の分配性)を持つことを利用すると楽でしょう。

これらの事実から言えることは、いままでに導入したパターンの“表現力” は、「単純パターンの有限集合」の程度であることです。単純パターンは、そ の名の通り、非決定性や条件分岐を持たない(so-called)テンプレートです から、具体化もマッチングも容易です。その代わり、表現力(生成力)はもの 足りないと言えます。

7. 伝統的繰り返し「*」の導入

項でもそれに対応するパターンでも、構文的演算は、concat, choice, surroundの3つしかありません。そして、その表現力(生成力)がイマイチで あることは前節で指摘したとおりです。ここで、 「『正規(regular)』とは何なんだ 2 正規構造」で説明したミュー項により、 繰り返し「*」を導入しましょう。ミュー項は、項の表現力を劇的に高めます。

「『正規(regular)』とは何なんだ 2 正規構造」では、 テンプレート変数 と束縛変数を、普通の変数とは全然別ものとしたけど、ここでは、テンプレート変数は 普通の変数を流用しちゃいましょう。例えば、choice(empty, x) のxは普通の 変数だけど、これをテンプレート変数とみなせば、この項は(束縛変数を含まないけど)再帰テンプレートです。

また、束縛変数はアンダスコアからはじまる名前を使い、次のように固定し てしまいましょう。

束縛変数はせいぜい1個しか出現しないので、ミュー項は束縛変数を明示せず 「μ[項]」の形で書くことにします。

さてそれで、ミュー項μ[choice(empty, concat(t, _z))]を考えると、これが実 は repeat(t)、よりお馴染みの形なら t* に対応するのでした。ミュー項をパター ンで書けば多少は見やすいでしょう。やってみます:μ[EMPTY | t _z] です ね。さらに項tを具体化した例は、μ[EMPTY | <a/> _z] とか。この例で、こ のミュー項(ミュー・パターンと言ったほうがいいかな)が実際に (<a/>)* であること を見てみましょう。

ミュー項の定義から、μ[EMPTY | <a/> _z]は次の再帰方程式の最小解です。

_zの初期値をNONE(空集合)として始める逐次近似で最小解を求めることが できるので(厳密には示してないけど、信じてちょうだい)(*注7)、次のよ うな近似列が構成できます。

  1. EMPTY
  2. (EMPTY | <a/> EMPTY) = (EMPTY | <a/>)
  3. (EMPTY | <a/> (EMPTY | <a/>)) = (EMPTY | <a/> | <a/><a/>)
  4. (EMPTY | <a/> (EMPTY | <a/> | <a/><a/>)) = (EMPTY | <a/> | <a/><a/> | <a/><a/><a/>)
  5. ...(続く)
注7

「『正規(regular)』とは何なんだ 2 正規構造」の第15節に正規構造の意味パートの条件が載っています。Tiny Toy XMLインスタンス(と関係する名前や列)の言語を考えると、それらの言語の 全体が作る順序集合はしかるべき性質を持っていて、確かに正規構造になって いるのです。

これらを(結果だけ)集合記法で書くなら:

  1. {EMPTY}
  2. {EMPTY, <a/>}
  3. {EMPTY, <a/>, <a/><a/>}
  4. {EMPTY, <a/>, <a/><a/>, <a/><a/><a/>}
  5. ...(続く)

これで、μ[EMPTY | <a/> _z]が (<a/>)* と同じってことは、いいですよね (了解していただけたでしょうか?)。

8. 縦方向の繰り返し「#」

前節で導入した繰り返し「*」は、列言語で既に登場しているので特に目新し いものではありません。再帰テンプレートとミュー項を利用すれば、さまざまな (無限の)繰り返し演算が定義できます。

例えば、再帰テンプレート (surround(n, empty) | surround(n, _U)) を考 えてみます。変数nはソート(型)がNameであるテンプレート変数で、_Uはソー ト(型)がTreeである束縛変数です。このテンプレートを具体化(テンプレー ト変数に実際の項を代入)してみると、例えば、(surround('a', empty) | surround('a', _U))となり、さらにμオペレータで束縛するとミュー項μ[surround('a', empty) | surround('a',_U)]ができあがります(パターンで表現するならμ [<a/> | <a>_U</a>])。このミュー項の意味を考えましょう。

定義により、ミュー項(パターン表現)μ[<a/> | <a>_U</a>]は次の再帰方程式 の最小解を意味します。

_Uの初期値をNONE(空集合)から初めての解の近似列は次のようになります。

  1. {<a/>}
  2. {<a/>, <a><a/></a>}
  3. {<a/>, <a><a/></a>, <a><a><a/></a></a>}
  4. {<a/>, <a><a/></a>, <a><a><a/></a></a>, <a><a><a><a/></a></a></a>}
  5. ...(続く)

ミュー項μ[choice(empty, concat(t, _z))]を t* と書いたのと同じように、 Name項tに対して、μ[surround(t, empty) | surround(t ,_U)]を t# と書く ことにしましょう。例えば、'a'# は今例にしたμ[surround('a', empty) | surround('a',_U)]のことです。

Name項は名前リテラルか、ソートがNameである変数(a, b, nなど)なので、 演算子「#」を含む項の形は、「名前リテラル#」、「名前変数#」の2種類です。 「名前リテラル#」は、'a'# のごとくに、“縦方向”にどんどん伸びていく無 限個のTiny Toy XMLインスタンス(基礎項または基礎パターンと言っても同じ) の集合を表します。「名前変数#」は、名前変数を含む単純パターンの無限集 合を表すと解釈できます。

9. 2項の繰り返し演算「%」

別な再帰テンプレートを使って、もうひとつ別な繰り返し演算を定義してみ ましょう。使う再帰テンプレートは (surround(n, empty) | surround(n, concat(x, _U)) です。これは2つのテンプレート変数n, xを含み ます。

まずは、テンプレート変数n(ソートはName)とx(ソートはList)を具体化 してみましょう。例えば(パターン表現で)、(<a/> | <a><b/><c/> _U</a>) は具体化のひとつです。さらにμオペレータで束縛すれば、μ[<a/> | <a><b/><c/> _U</a>]となります。その意味は(もうわかると思いますが)次 の近似列で与えられます。

  1. {<a/>}
  2. {<a/>, <a><b/><c/><a/></a>}
  3. {<a/>, <a><b/><c/><a/></a>, <a><b/><c/><a><b/><c/><a/></a></a>}
  4. {<a/>, <a><b/><c/><a/></a>, <a><b/><c/><a><b/><c/><a/></a></a>, <a><b/><c/><a><b/><c/><a><b/><c/><a/></a></a></a>}
  5. ...(続く)

今度の再帰テンプレートには、2つのテンプレート変数が入っていたので、ミュー 項を作る前に、2箇所具体化する場所があります。つまり、 ミュー項μ[surround(n, empty) | surround(n, concat(x, _U)]は、2つのパ ラメータを持つと考えていいわけです。したがって、このミュー項を適当な演 算子で略記するときは2項演算子を使うことになります。いま仮に「%」をその 2項演算子の記号として採用すると、'a'%(<b/><c/>) という演算子を含む式が μ[<a/> | <a><b/><c/> _ U</a>] の略記となります。'a' % empty は 'a'# と同値であることを確認してみてください。

10. おわりに

この記事は実例に終始したので、最後に少しだけ一般論をしておきます。お おざっぱな話なので、フォローしきれなくても気にする必要はありません。

Aがある再帰構造の領域(のひとつ)だとします。Aを変域とする束縛変数 (*注8)だけを含む項は、λオペレータで束縛すれば A→Aという写像を定義し ます。つまり、束縛変数だけを含む項の“意味”は写像の集合 Mpa(A, A) の 中(*注9)に存在するとみてもいいでしょう。

注8

「Aを変域とする束縛変数」の正確な意味は、変数zのソートがsであり、ソー トsに対して割り当てられた領域がAであることです。

注9

Mpa(A, A)は、すべての写像を含むわけではありません。何らかの基準で“タ チが良い”写像だけを集めたものです。

さて、一般的な再帰テンプレートはいくつかのテンプレート変数を含みます。 それらテンプレート変数の変域をB1, ..., Bnとすると、再帰テンプレー トはおおよそ(細かいことは端折って) B1, ..., Bn → Map(A, A) とい う写像とみなせるでしょう。f∈Map(A, A)に対してlfp(f)が、fの最小不動点 だとすると、テンプレートによる写像T:B1, ..., Bn → Map(A, A) と lfp:Map(A, A) → A を結合すると、 B1, ..., Bn → A という写像が定 義できます。再帰テンプレートが定義する演算の意味とは、このような写像で す。

「正規」とは、“再帰方程式の最小解=最小不動点”を求める操作を適宜追加 して代数系を拡張することだと解釈するなら、正規であることをささえている のは、最小不動点を返す写像(不動点演算子)lfp:Map(A, A) → A だと言え ますね。