項代数

普遍代数学と数理論理学において、代数とは、与えられた署名上の自由に生成された代数構造を指す。^[1]^[2]例えば、単一の二項演算からなる署名において、変数集合X上の代数とは、Xによって生成される自由マグマそのものを指す。この概念の同義語には、絶対自由代数や無政府代数などがある。^[3]

圏論の観点から見ると、項代数とは、同じ署名を持つすべての X生成代数の圏の初期オブジェクトであり、同型性を除いて一意であるこのオブジェクトは初期代数と呼ばれ、準同型射影によって圏のすべての代数を生成する。 ^[4]^[5]

同様の概念として、論理におけるエルブラン宇宙があります。これは通常、論理プログラミングにおいてこの名称で用いられます。^{[6]これは、}節集合内の定数と関数記号の集合から（完全に自由に）定義されます。つまり、エルブラン宇宙はすべて基底項、つまり変数を含まない項から構成されます。

原子式またはアトムは、一般的に、項の組に適用される述語として定義されます。基底アトムは、基底項のみが現れる述語です。エルブラン基底とは、エルブラン宇宙における元の節と項の集合に含まれる述語記号から形成できるすべての基底アトムの集合です。^[7]^{[8]これら2つの概念は、}ジャック・エルブランにちなんで名付けられました。

項代数は、抽象データ型のセマンティクスでも役割を果たします。抽象データ型の宣言は、複数のソートされた代数構造のシグネチャを提供し、項代数は抽象宣言の具体的なモデルです。

普遍代数

型とは関数シンボルの集合であり、それぞれには対応するアリティ（つまり入力数）が関連付けられています。任意の非負整数について、はアリティの関数シンボルを表します。定数はアリティ 0 の関数シンボルです。 $\tau$ $n$ $\tau _{n}$ $\tau$ $n$

を型とし、を変数シンボルを表す空でないシンボルの集合とします。（簡単のため、とは互いに素であると仮定します。）すると、上の型の項の集合は、の変数シンボルとの定数および演算を用いて構築できるすべての整形式の文字列の集合です。正式には、は次を満たす最小の集合です。 $\tau$ $X$ $X$ $\tau$ $T(X)$ $\tau$ $X$ $X$ $\tau$ $T(X)$

$X\cup \tau _{0}\subseteq T(X)$ — の各変数記号はの項であり、の各定数記号もの項です。 $X$ $T(X)$ $\tau _{0}$
すべての関数記号および項について、文字列が得られます。項が与えられた場合、それらに-ary 関数記号を適用すると、再び項が表されます。 $n\geq 1$ $f\in \tau _{n}$ $t_{1},...,t_{n}\in T(X)$ $f(t_{1},...,t_{n})\in T(X)$ $n$ $t_{1},...,t_{n}$ $n$ $f$

型代数とは、要約すると、各式をその文字列表現に写像する型の代数である。正式には、次のように定義される。^[9] ${\mathcal {T}}(X)$ $\tau$ $X$ $\tau$ ${\mathcal {T}}(X)$

のドメインはです。 ${\mathcal {T}}(X)$ $T(X)$
の各 nullary 関数に対して、は文字列として定義されます。 $f$ $\tau _{0}$ $f^{{\mathcal {T}}(X)}()$ $f$
すべてのおよびの各n項関数、および定義域内の要素に対して、は文字列として定義されます。 $n\geq 1$ $f$ $\tau$ $t_{1},...,t_{n}$ $f^{{\mathcal {T}}(X)}(t_{1},...,t_{n})$ $f(t_{1},...,t_{n})$

項代数は絶対的に自由であると言われる。なぜなら、型の任意の代数、および任意の関数に対して、は一意の準同型に拡張され、各項を対応する値に単純に評価するからである。正式には、各に対して： ${\mathcal {A}}$ $\tau$ $g:X\to {\mathcal {A}}$ $g$ $g^{\ast }:{\mathcal {T}}(X)\to {\mathcal {A}}$ $t\in {\mathcal {T}}(X)$ $g^{\ast }(t)\in {\mathcal {A}}$ $t\in {\mathcal {T}}(X)$

もしなら、。 $t\in X$ $g^{\ast }(t)=g(t)$
もしなら、。 $t=f\in \tau _{0}$ $g^{\ast }(t)=f^{\mathcal {A}}()$
かつの場合にはとなります。 $t=f(t_{1},...,t_{n})$ $f\in \tau _{n}$ $n\geq 1$ $g^{\ast }(t)=f^{\mathcal {A}}(g^{\ast }(t_{1}),...,g^{\ast }(t_{n}))$

例

例として、整数演算からヒントを得た型は、各に対して、、、によって定義できます。 $\tau _{0}=\{0,1\}$ $\tau _{1}=\{\}$ $\tau _{2}=\{+,*\}$ $\tau _{i}=\{\}$ $i>2$

最もよく知られている型の代数は、自然数を定義域として持ち、、、を通常の方法で解釈します。これをと呼びます。 $\tau$ $0$ $1$ $+$ $*$ ${\mathcal {A}}_{nat}$

変数セットの例については、上の型の項代数を調べます。 $X=\{x,y\}$ ${\mathcal {T}}(X)$ $\tau$ $X$

まず、型の項の集合について考察する。その要素は構文形式が一般的ではないため、赤色で表示することで識別しにくくなる可能性がある。例えば、 $T(X)$ $\tau$ $X$

${\color {red}x}\in T(X)$ は変数シンボルなので、 $x\in X$
${\color {red}1}\in T(X)$ は定数記号なので、 $1\in \tau _{0}$
${\color {red}+x1}\in T(X)$ は2項関数記号なので、 $+$
${\color {red}*+x1x}\in T(X)$ は2項関数シンボルです。 $*$

より一般的には、の各文字列は、許容される記号から構築され、ポーランド語の接頭辞記法で書かれた数式に対応します。例えば、項は通常の接頭辞記法の式に対応します。ポーランド語の記法では曖昧さを避けるために括弧は必要ありません。例えば、接頭辞式は項に対応します。 $T(X)$ ${\color {red}*+x1x}$ $(x+1)*x$ $x+(1*x)$ ${\color {red}+x*1x}$

反例をいくつか挙げると、例えば

${\color {red}z}\not \in T(X)$ は変数記号としても定数記号としても認められていないため、 $z$
${\color {red}3}\not \in T(X)$ 同じ理由で、
${\color {red}+1}\not \in T(X)$ は2 項関数記号ですが、ここでは 1 つの引数項 (つまり) のみで使用されています。 $+$ ${\color {red}1}$

項集合が確立されたので、型の項代数について考察します。この代数はを定義域として用いており、この定義域上で加算と乗算を定義する必要があります。加算関数は2つの項とを取り、項を返します。同様に、乗算関数は与えられた項とを項に写像します。例えば、は項に評価されます。非公式には、との演算はどちらも、実際に計算を行うのではなく、実行すべき計算を記録するだけという点で「怠け者」です。 $T(X)$ ${\mathcal {T}}(X)$ $\tau$ $X$ $T(X)$ $+^{{\mathcal {T}}(X)}$ $p$ $q$ ${\color {red}+}pq$ $*^{{\mathcal {T}}(X)}$ $p$ $q$ ${\color {red}*}pq$ $*^{{\mathcal {T}}(X)}({\color {red}+x1},{\color {red}x})$ ${\color {red}*+x1x}$ $+^{{\mathcal {T}}(X)}$ $*^{{\mathcal {T}}(X)}$

準同型写像の一意な拡張可能性の例として、とによって定義されるを考えてみましょう。非公式には、は変数記号への値の割り当てを定義しており、これが完了すると、のすべての項はにおいて一意に評価できるようになります。例えば、 $g:X\to {\mathcal {A}}_{nat}$ $g(x)=7$ $g(y)=3$ $g$ $T(X)$ ${\mathcal {A}}_{nat}$

{\begin{array}{lll}&g^{*}({\color {red}+x1})\\=&g^{*}({\color {red}x})+g^{*}({\color {red}1})&{\text{ since }}g^{*}{\text{ is a homomorphism }}\\=&g({\color {red}x})+g^{*}({\color {red}1})&{\text{ since }}g^{*}{\text{ coincides on }}X{\text{ with }}g\\=&7+g^{*}({\color {red}1})&{\text{ by definition of }}g\\=&7+1&{\text{ since }}g^{*}{\text{ is a homomorphism }}\\=&8&{\text{ according to the well-known arithmetical rules in }}{\mathcal {A}}_{nat}\\\end{array}}

同様の方法で、が得られます。 $g^{*}({\color {red}*+x1x})=...=8*g({\color {red}x})=...=56$

エルブラン基地

言語のシグネチャ σ は、定数 O 、関数記号 F 、述語 P のアルファベットからなる三つ組 < O 、 F 、 P > である。シグネチャσ のエルブラン基底[ 10 ]は、 σの すべての基底アトム、すなわち形式 R ( t 1 、 ...、 t n ) のすべての式から構成される。^ここで、 t 1 _、 ... 、_t nは変数_を含まない_項(つまりエルブラン宇宙の要素) であり、Rはn項関係記号 (つまり述語)である。等式を含む論理の場合、形式t ₁ = t ₂のすべての方程式も含まれる。ここで、t ₁とt ₂には変数が含まれない。

決定可能性

項代数は量指定子除去を用いて決定可能であることが示される。二項構成子は単射であり、したがって対関数であるため、決定問題の複雑さは非基本的である。 ^[11]

参照

参考文献

^ ウィルフリッド・ホッジス(1997). 『短縮モデル理論』ケンブリッジ大学出版局. pp. 14. ISBN 0-521-58713-1。
^ フランツ・バーダー、トビアス・ニプコウ(1998). 『用語の書き換えとそのすべて』ケンブリッジ大学出版局. p. 49. ISBN 0-521-77920-0。
^ クラウス・デネケ、シェリー・L・ウィスマス (2009). 普遍代数と余代数. World Scientific . pp. 21– 23. ISBN 978-981-283-745-5。
^ TH Tse (2010).構造化分析・設計モデルのための統一的枠組み：初期代数意味論と圏論を用いたアプローチ.ケンブリッジ大学出版局. pp. 46– 47. doi :10.1017/CBO9780511569890. ISBN 978-0-511-56989-0。
^ Jean-Yves Béziau (1999). 「論理構文の数学的構造」. Carnielli, Walter Alexandre; D'Ottaviano, Itala ML (編). 『現代論理とコンピュータサイエンスの進歩：第11回ブラジル数学論理会議議事録』（1996年5月6日～10日、ブラジル、バイーア州サルバドール） .アメリカ数学会. 9頁. ISBN 978-0-8218-1364-5. 2011年4月18日閲覧。
^ ダーク・ヴァン・ダーレン (2004)。ロジックと構造。スプリンガー。 p. 108.ISBN 978-3-540-20879-2。
^ M. Ben-Ari (2001). 『コンピュータサイエンスのための数理論理学』Springer . pp. 148– 150. ISBN 978-1-85233-319-5。
^ モンロー・ニューボーン (2001). 『自動定理証明：理論と実践』シュプリンガー43ページ. ISBN 978-0-387-95075-4。
^ スタンレー・バリス、H・P・サンカッパナヴァール (1981). 『普遍代数学講座』シュプリンガー. pp. 68– 69, 71. ISBN 978-1-4613-8132-7。{{cite book}}: CS1 maint: multiple names: authors list (link)
^ Rogelio Davila. 回答セットプログラミングの概要。
^ Jeanne Ferrante; Charles W. Rackoff (1979).論理理論の計算複雑性. Springer , 第8章, 定理1.2.

さらに読む

ジョエル・バーマン (2005). 「自由代数の構造」. 『オートマトン、半群、普遍代数の構造理論』シュプリンガー. pp. 47–76. MR 2210125.

外部リンク

ワイスタイン、エリック・W.「ヘルブランド・ユニバース」。マスワールド。

[1] ウィルフリッド・ホッジス(1997). 『短縮モデル理論』ケンブリッジ大学出版局. pp. 14. ISBN 0-521-58713-1。

[2] フランツ・バーダー、トビアス・ニプコウ(1998). 『用語の書き換えとそのすべて』ケンブリッジ大学出版局. p. 49. ISBN 0-521-77920-0。

[DeneckeWismath2009-3] クラウス・デネケ、シェリー・L・ウィスマス (2009). 普遍代数と余代数. World Scientific . pp. 21– 23. ISBN 978-981-283-745-5。

[Tse2010-4] TH Tse (2010).構造化分析・設計モデルのための統一的枠組み：初期代数意味論と圏論を用いたアプローチ.ケンブリッジ大学出版局. pp. 46– 47. doi :10.1017/CBO9780511569890. ISBN 978-0-511-56989-0。

[CarnielliD'Ottaviano1999-5] Jean-Yves Béziau (1999). 「論理構文の数学的構造」. Carnielli, Walter Alexandre; D'Ottaviano, Itala ML (編). 『現代論理とコンピュータサイエンスの進歩：第11回ブラジル数学論理会議議事録』（1996年5月6日～10日、ブラジル、バイーア州サルバドール） .アメリカ数学会. 9頁. ISBN 978-0-8218-1364-5. 2011年4月18日閲覧。

[Dalen2004-6] ダーク・ヴァン・ダーレン (2004)。ロジックと構造。スプリンガー。 p. 108.ISBN 978-3-540-20879-2。

[Ben-Ari2001-7] M. Ben-Ari (2001). 『コンピュータサイエンスのための数理論理学』Springer . pp. 148– 150. ISBN 978-1-85233-319-5。

[Newborn2001-8] モンロー・ニューボーン (2001). 『自動定理証明：理論と実践』シュプリンガー43ページ. ISBN 978-0-387-95075-4。

[Burris1981-9] スタンレー・バリス、H・P・サンカッパナヴァール (1981). 『普遍代数学講座』シュプリンガー. pp. 68– 69, 71. ISBN 978-1-4613-8132-7。{{cite book}}: CS1 maint: multiple names: authors list (link)

[10] Rogelio Davila. 回答セットプログラミングの概要。

[11] Jeanne Ferrante; Charles W. Rackoff (1979).論理理論の計算複雑性. Springer , 第8章, 定理1.2.