項代数
普遍代数学および数理論理学において、項代数(こうだいすう、テンプレート:Lang-en-short)は、与えられたシグネチャ上に自由に生成される代数的構造である[1][2]。たとえば、1 つの二項演算のみからなるシグネチャにおいては、変数の集合 X 上の項代数は正確に、X により生成されるテンプレート:仮リンクに等しい。他の同義語として、絶対自由代数(absolutely free algebra)やアナーキー代数(anarchic algebra)が用いられる[3]。
圏論の観点からは、項代数は、同一シグネチャをもつ X 生成代数全体からなる圏の始対象である。この対象は同型を除いて一意であり、始代数と呼ばれる。項代数は圏内のすべての代数を準同型的な射影によって生成する[4][5]。
これに類似した概念として、論理におけるテンプレート:仮リンクがある。この用語は通常論理プログラミングにおいて用いられ[6]、節の集合に含まれる定数と関数記号の集合から出発して(絶対的自由に)定義される。すなわち、エルブラン領域は、すべてのテンプレート:仮リンク――変数を全く含まない項――から構成される。
項代数は、抽象データ型の意味論にも重要な役割を果たす。すなわち、抽象データ型の宣言は多ソート代数的構造のシグネチャを与え、項代数はその抽象宣言の具体的モデルとなる。
普遍代数学における定式化
型 とは関数記号の集合であり、各関数記号にそれぞれアリティ(すなわち入力の個数)が付随している。任意の非負整数 に対し、 中のアリティ の関数記号を と表す。定数とはアリティ 0 の関数記号である。
を型とし、 を変数記号を表す空でない記号の集合とする(簡単のため と は互いに素であるとする)。このとき、X 上の型 のテンプレート:仮リンクの集合 は、 の変数記号と の定数および演算を用いて構成できるすべての整形式の文字列の集合である。形式的には、 は次を満たす最小の集合として定義される。
- — の各変数記号は の項であり、 の各定数記号もまた項である。
- すべての 、すべての関数記号 、および項 について、文字列 — 個の項 が与えられれば、 項関数記号 をこれらに適用したものもまた項となる。
X 上の型 の項代数 とは、要するに、各式にその文字列表現を対応付ける型 の代数である。形式的には、 は次のように定義される[7]。
- の領域は である。
- 中の各 0 項関数 について、 は文字列 として定義される。
- すべての と、 中の各 n 項関数 および領域の元 について、 は文字列 として定義される。
項代数が絶対自由(absolutely free)と呼ばれるのは、型 の任意の代数 と任意の関数 に対して、 が一意な準同型 に拡張されるためである。この準同型は、単に各項 を対応する値 に評価する。形式的には、各 について:
- もし ならば 。
- もし ならば 。
- もし で かつ ならば、。
例
整数演算に着想を得た型の例は、、、、および各 に対して と定義できる。
型 の最もよく知られた代数は自然数を領域とし、、、、 を通常の意味で解釈するものである。これを と呼ぶことにする。
変数集合の例として を取り、X 上の型 の項代数 を調べる。
まず、X 上の型 の項の集合 を考える。通常見慣れない構文形式のため識別しづらいことがあるため、その要素をテンプレート:Colorで表す。たとえば、次が得られる:
- ( は変数記号だから)
- ( は定数記号だから)
- ( は 2 項関数記号だから)
- ( は 2 項関数記号だから)
より一般に、 中の各文字列は、許容された記号から構築されポーランド前置記法で書かれた数式に対応する。たとえば、項 は通常の中置記法における式 に対応する。ポーランド記法では曖昧さを避けるための括弧は不要である。たとえば中置式 は項 に対応する。
反例をいくつか挙げる:
- ( は許容された変数記号でも定数記号でもないから)
- (同じ理由)
- ( は 2 項関数記号だが、ここでは項を 1 つ()しか伴っていないから)
項集合 が確立されたので、次に X 上の型 の項代数 を考える。この代数は領域として を用いる。この上に加算と乗算を定義する必要がある。加算関数 は 2 つの項 と を受け取り、項 を返す。同様に、乗算関数 は与えられた項 と を項 に写す。たとえば は項 に評価される。非形式的にいえば、演算 と はいずれも「怠け者」で、実際の計算を行うのではなく、どんな計算をすべきかを記録するだけである。
準同型が一意に拡張可能な例として、、 で定義される を考える。非形式的にいえば、 は変数記号への値の割り当てを定めており、これが定まれば の任意の項は において一意な方法で評価できる。たとえば、
ここで、各ステップの等号は上から順に以下の理由によって成り立つ。
- は準同型であるため。
- は 上で に一致するため。
- の定義による。
- 再び、 は準同型であるため。
- 最後に、 における周知の算術規則を適用した。
同様にして、 が得られる。
エルブラン基底
テンプレート:Main 言語のシグネチャ σ は、定数のアルファベット O、関数記号 F、および述語 P からなる三つ組 <O, F, P> である。原子式(atomic formula)は通常、項のタプルに述語を適用したものとして定義され、テンプレート:仮リンクは基底項のみを引数にとる原子式として定義される。
シグネチャ σ のエルブラン基底(Herbrand base)[8] は、σ のすべての基底原子式からなる[9][10]。すなわち、R(t1, ..., tn) の形の式であって、t1, ..., tn が変数を含まない項(すなわちエルブラン領域の元)であり、R が n 項関係記号(すなわち述語)であるようなものである。等号を含む論理の場合には、t1 = t2 の形のすべての等式(t1 と t2 は変数を含まない)も含まれる。これらエルブラン領域およびエルブラン基底の概念は、いずれもジャック・エルブランにちなんで名付けられた。
決定可能性
任意の項代数の一階理論はテンプレート:仮リンクを用いて決定可能であることを示せる。決定問題の計算量はテンプレート:仮リンクに属する。これは 2 項構築子が単射で、したがって対関数となるためである[11]。
関連項目
- テンプレート:仮リンク
- テンプレート:仮リンク
- 議論領域 / 宇宙 (数学)
- テンプレート:仮リンク(無限テンプレート:仮リンクのモナディック理論は決定可能である)
- 始代数
- 抽象データ型
- テンプレート:仮リンク
出典
参考文献
- Joel Berman (2005). "The structure of free algebras". In Structural Theory of Automata, Semigroups, and Universal Algebra. Springer. pp. 47–76. テンプレート:MR.
外部リンク
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ テンプレート:Cite book
- ↑ Rogelio Davila. Answer Set Programming Overview.
- ↑ テンプレート:Cite book
- ↑ Jeanne Ferrante; Charles W. Rackoff (1979). The Computational Complexity of Logical Theories. Springer, Chapter 8, Theorem 1.2.