2020-09-21

半環上のフラクタル代数(9)

論理プログラミングとシークエント計算

集合の記法

集合 $X$ に対して $R = \mathcal{F}(X)$ は半環(単位元を持つ自明ではない冪等可換半環)となります。

$S$ を単位元を持つ自明ではない半環とし、 $f: X \to S$ とします。 $x \in R$ は
$x = x_{11} x_{12} \cdots x_{1m_1} + x_{21} x_{22} \cdots x_{2m_2} + \cdots + x_{n1} x_{n2} \cdots x_{nm_n}$ $(x_{ij} \in X)$
と順序を除いて一意的に表すことができます。よって $f^*: R \to S$ を
$f^*(x) = f(x_{11}) f(x_{12}) \cdots f(x_{1m_1}) + f(x_{21}) f(x_{22}) \cdots f(x_{2m_2}) + \cdots + f(x_{n1}) f(x_{n2}) \cdots f(x_{nm_n})$
と定義することができます。 $f^*$ は半環の準同型となります。

集合 $X$ から集合 $Y$ への写像 $f: X \to Y$ に対して $f: X \to \mathcal{F}(X)$ と考えると半環の準同型 $f^* : \mathcal{F}(X) \to \mathcal{F}(X)$ を定義することができます。

$X$ を集合、 $R = \mathcal{F}(X)$ 、 $f: X \to R$ とします。 $Y \subseteq X$ 、 $r \in R$ に対して、 $\rho_{f,Y,r}: X \to R$ を $x \in Y$ のとき $\rho_{f,Y,r}(x) = f(x)$ 、 $x \notin Y$ のとき $\rho_{f,Y,r}(x) = r$ と定義します。

集合 $X$ と $Y$ に対して、 $X$ と $Y$ の直和を $X + Y$ 、 $X$ と $Y$ の直積を $X \times Y$ と書きます。 $X$ の $n$ 個の直積( $n$ は自然数)を $X^n$ と書きます。 $0$ 個の直積も考えます。 $X^* = X^0 + X^1 + X^2 + \cdots X^n$ と書きます。

論理プログラミング

論理プログラミングのデータ

$C$ (Prolog の定数名に対応)、 $F$ (Prolog の関数名に対応)、 $P$ (Prolog の述語名に対応)を有限集合、 $V$ (Prolog の変数名に対応)を可算集合とします。

$f \in F$ に対して $f$ のアリティという自然数 $n = a_F(f)$ が決まっているとします。 $f$ のアリティは $f$ の引数の個数を表します。アリティの異なる元は異なる元とします。 $F_n = \{ f \in F \mid a_F(f) = n \}$ とおくと $F = F_0 + F_1 + \cdots$ となります。 $F_0$ はなくても良いのですが含めることにします。

$p \in P$ に対して $p$ のアリティという自然数 $n = a_P(p)$ が決まっているとします。 $p$ のアリティは $p$ の引数の個数を表します。アリティの異なる元は異なる元とします。 $P_n = \{ p \in P \mid a_P(p) = n \}$ とおくと $P = P_0 + P_1 + \cdots$ となります。 $P_0$ はなくても良いのですが含めることにします。

$T = V + C + F_0 +F_1 \times T + F_2 \times T^2 + \cdots$ (Prolog の項に対応)、
$S = P_0 + P_1 \times T + P_2 \times T^2 + \cdots$ (Prolog の述語の項に対応)、
$Q = S^* \times S$ (Prolog のホーン節に対応)、
$D = Q^*$ (Prolog のプログラムに対応)、
$E = S \times S$ (Prolog の述語の項が一致することを表すものに対応)、
$U = E + S$ (Prolog の述語の項が一致することを表すもの、または述語の項に対応)

とします。

論理プログラミングのプログラム微分

$\lambda: Q \times S \to \mathcal{F}(U)$ を $( (s_1, s_2, \cdots , s_n), h) \in Q$ $(s_1, s_2, \cdots , s_n, h \in S)$ と $x \in S$ に対して $\lambda( ( (s_1, s_2, \cdots , s_n), h), x) = e(h, x) s_1, s_2, \cdots , s_n$ と定義します。 $e(h, x) \in E$ は $h$ と $x$ が一致することを表すものとします。

$\gamma: D \times S \to \mathcal{F}(U)$ を $( q_1, q_2, \cdots , q_m) \in D$ $(q_1, q_2, \cdots , q_m \in Q)$ と $x \in S$ に対して $\gamma( (q_1, q_2, \cdots , q_m), x) = \lambda(q_1, x) + \lambda(q_2, x) + \cdots + \lambda(q_m, x)$ と定義します。ただし $q_i$ と $q_j$ $(i \ne j)$ に現れる変数は重複しないものとします。 $q_i$ に現れる変数は $V_i$ に含まれるとし、 $V^+_0 = V_1 + \cdots + V_m \subseteq V$ とします。

$p \in D$ に対して $\delta_p: U \to \mathcal{F}(U)$ を $x \in S$ のとき $\delta_p(x) = \gamma(p, x)$ 、 $x \in E$ のとき $\delta_p(x) = x$ と定義します。

$\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ となります。 $\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ を $n$ 回繰り返したものを $\delta_p^{*n}: \mathcal{F}(U) \to \mathcal{F}(U)$ とします。ただし $i$ 回目の $p$ ( $p_i$ とします)と $j$ 回目の $p$ ( $p_j$ とします) $(i \ne j)$ に現れる変数は重複しないものとします。 $V^+_i$ は $V^+_0$ と元の個数が同じ集合とします。 $p$ に現れる変数をそれに対応する $V^+_i$ の元で置き換えたものを $p_i$ とおきます。 $V$ は可算集合としたので $V = V^+_1 + V^+_2 + \cdots$ とすることができます。

論理プログラミングの代入

論理プログラミングの変数を含まないデータを定義します。

$T_C = C + F_0 +F_1 \times T_C + F_2 \times T_C^2 + \cdots$ (Prolog の変数を含まない項に対応)、
$S_C = P_0 + P_1 \times T_C + P_2 \times T_C^2 + \cdots$ (Prolog の変数を含まない述語の項に対応)、
$Q _C= S_C^* \times S_C$ (Prolog の変数を含まないホーン節に対応)、
$D_C = Q_C^*$ (Prolog の変数を含まないプログラムに対応)、
$E_C = S_C \times S_C$ (Prolog の変数を含まない述語の項が一致することを表すものに対応)、
$U_C = E_C + S_C$ (Prolog の変数を含まない述語の項が一致することを表すもの、または変数を含まない述語の項に対応)

とします。

$\sigma: V \to T_C$ を代入と呼びます。代入全体の集合を $\Sigma$ とおきます。変数以外は保存されるものとして、 $\sigma: V \to T_C$ を $\bar{\sigma}: U \to U_C$ に拡張することができます。

$\iota: U \to U$ を恒等写像とします。

$\bar{\sigma}(\rho_{\iota,E,0}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在するとき $(p, x)$ は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E,1}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在しないとき $(p, x)$ は $n$ 回で失敗

ということにします。

シークエント計算

これをシークエント計算に対応させます。

シークエント計算のデータ

論理プログラミングのデータからシークエント計算のデータを作ります。

各 $f \in F$ に対して $n = a_F(f)$ とするとき述語 $r_f(x_1, \cdots , x_n, y)$ を $P$ に追加します。すべての $r_f$ を $P$ に追加したものを $P'$ とおきます。

$C'_0 = C$ 、 $C'_{k+1} = C'_k + \{ f(c_1, \cdots , c_n) \mid f \in F_n; \ c_1, \cdots , c_n \in C'_k \}$ $(k = 0, 1, 2, \cdots)$ 、 $C' = C'_0 + C'_1 + C'_2 +\cdots$ とおきます。

$q \in Q = S^* \times S$ (Prolog のホーン節に対応)、 $q = ( (s_1, s_2, \cdots , s_n), h)$ $(s_1, s_2, \cdots , s_n, h \in S)$ とします。

$q$ に関数が現れるごとにそれに対応した変数を追加します。 $q$ に関数 $f(t_1, t_2,\cdots , t_n)$ が現れたとします。その $f(t_1, t_2,\cdots , t_n)$ の出現を、この出現に対応する変数 $v_f$ で置き換えます。そして $s_1, s_2, \cdots , s_n$ の列に $r_f(t_1, t_2,\cdots , t_n, v_f)$ を追加します。この変形によって関数の出現が1つ減ります。よってこの変形を繰り返すことにより、 $q$ に関数が現れないように変形することができます。すべての $v_f$ を $V$ に追加したものを $V'$ とおきます。

関数が現れないように変形した $q = ( (s_1, s_2, \cdots , s_n), h)$ に対して $\forall x_1 \cdots \forall x_m (s_1 \land s_2 \land \cdots \land s_n \implies h)$ を $\bar{q}$ とおきます。ここで $x_1, \cdots , x_m$ は $q$ に現れるすべての変数とします。

$p = (q_1, \cdots , q_k) \in D$ に対して $\bar{q_1} \land \cdots \land \bar{q_k}$ を $\bar{p}$ とおきます。

同様に $u \in S$ を関数が現れないように変形します。 $\exists v_1 \cdots \exists v_c u$ を $\bar{u}$ とおきます。ここで $v_1, \cdots , v_c$ は $u$ に現れるすべての変数とします。

すべての $c_1, \cdots , c_n \in C_k$ の組み合わせに対する $r_f(c_1, \cdots , c_n, f(c_1, \cdots , c_n))$ の全体を $r_1, \cdots , r_l$ とし、 $\bar{r}_k = r_1 \land \cdots \land r_l$ とおきます。

論理プログラミングが $n$ 回で成功するとするとき、適当な $C_\nu$ をとり $C_\nu = \{ c_1, c_2, \cdots , c_k \}$ とすると $\exists c_1 \exists c_2 \cdots \exists c_k ( \bar{r}_\nu \land \bar{p} \implies \bar{u} )$ を証明する図を書くことができます。

LK の記法を一部使って書きます。簡単に書くために $\bar{r}_\nu$ を $r$ と書きます。
$\hspace{4em} \begin{eqnarray*} & \vdash & \exists c_1 \exists c_2 \cdots \exists c_k ( r \land \bar{p} \implies \bar{u} ) \\ & \Uparrow & (右 \exists の繰り返し) \\ & \vdash & r \land \bar{p} \implies \bar{u} \\ & \Uparrow & (右 \implies) \\ r \land \bar{p} & \vdash & \bar{u} \\ & \Uparrow & (右 \exists の繰り返し) \\ r \land \bar{p} & \vdash & \bar{u}' \\ & \Uparrow & (左 \forall の繰り返し) \\ r \land \bar{p}' & \vdash & \bar{u}' \\ & \Uparrow & (左減少) \\ r \land \bar{p}' , r \land \bar{p}' & \vdash & \bar{u}' \\ & \Uparrow & (左 \land の繰り返し) \\ r , \bar{p}' & \vdash & \bar{u}' \\ \end{eqnarray*}$
ここで $\bar{p}'$ は $\bar{p}$ の先頭の $\forall$ をすべて取り除いたもの、 $\bar{u}'$ は $\bar{u}$ の先頭の $\exists$ をすべて取り除いたものとします。

簡単に書くために $\bar{p}'$ を $p$ 、 $\bar{u}'$ を $u$ と書きます。 $p = q_1 \land \cdots \land q_n$ のとき
$\hspace{4em} \begin{array}{c} r , q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ ( r , q_1 \vdash u ) \sqcup \cdots \sqcup ( r , q_n \vdash u ) \\ \end{array}$
となります。ここで $q_i = s_1 \land \cdots \land s_n \implies h$ のとき
$\hspace{4em} \begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash u \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash u) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r, h \vdash u) \\ \end{array}$
となります。ここまでが論理プログラミングの $1$ 回分となります(記法の説明は後述)。

$T' = V' + C'_\nu + F_0 +F_1 \times T' + F_2 \times {T'}^2 + \cdots$ (Prolog の項に対応)、
$S' = P'_0 + P'_1 \times T' + P'_2 \times {T'}^2 + \cdots$ (Prolog の述語の項に対応、 $P'_n$ は $P'$ の元のうちアリティが $n$ であるもの全体)、
$Q' = {S'}^* \times S$ (Prolog のホーン節に対応)、
$D' = {Q'}^*$ (Prolog のプログラムに対応)、
$Z = {S'}^* \times S$ ( $r \vdash u$ の形のシークエントを表す)、
$E' = S' \times S'$ ( $h \vdash u$ の形のシークエントを表す)、
$W = E' + S'$ ( $r \vdash u$ または $h \vdash u$ の形のシークエントを表す)

とします。

シークエント計算の推論ブロック

論理プログラミングの $1$ 回分に相当するシークエント計算の推論を推論ブロックと呼ぶことにします。

$\mathcal{F}(W)$ (シークエントで生成される半環を表す)の計算を考えます。

$\mathcal{F}(U)$ の加法を $\lor$ 、乗法を $\land$ 、 $\mathcal{F}(W)$ の加法を $\sqcup$ 、乗法を $\sqcap$ と書くことにします(上記の説明でこの記法を使っています)。

$\Gamma_{r}: D' \times S' \to \mathcal{F}(W)$ を以下の変換とします。
$\hspace{4em} \begin{array}{c} r , q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ ( r , q_1 \vdash u ) \sqcup \cdots \sqcup ( r , q_n \vdash u ) \\ \end{array}$

$p \in D'$ に対して $\Delta_{r,p}: W \to \mathcal{F}(W)$ を以下の変換とします。
$\hspace{4em} \begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash u \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash u) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r, h \vdash u) \\ \end{array}$

$p \in D'$ に対して $\Delta_{r,p}: W \to \mathcal{F}(W)$ を $x \in S'$ のとき $\Delta_{r,p}(x) = \Gamma_r(p, x)$ 、 $x \in E'$ のとき $\Delta_{r,p}(x) = x$ と定義します。

$\Delta_{r,p}^*: \mathcal{F}(W) \to \mathcal{F}(W)$ となります。 $\Delta_{r,p}^*: \mathcal{F}(W) \to \mathcal{F}(W)$ を $n$ 回繰り返したものを $\Delta_{r,p}^{*n}: \mathcal{F}(W) \to \mathcal{F}(W)$ とします。ただし $i$ 回目の $p$ ( $p_i$ とします)と $j$ 回目の $p$ ( $p_j$ とします) $(i \ne j)$ に現れる変数は重複しないものとします。 $p_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + V_2 + \cdots$ とします(論理プログラミングの場合と同様)。

シークエント計算の代入

$\bar{\sigma}(\rho_{\iota,E',0}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在するとき $p \vdash x$ のシークエント計算は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E',1}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在しないとき $p \vdash x$ のシークエント計算は $n$ 回で失敗

ということにします。

論理プログラミングの $(p, x) \in D \times S$ に上記の変換をしたシークエント計算の $(p', x') \in D' \times S'$ を対応させることによって
$\bar{\sigma}(\rho_{\iota,E,0}^*(\delta_p^{*n}(x))) = 1 \iff \bar{\sigma}(\rho_{\iota,E',0}^*(\Delta_{r,p}^{*n}(x))) = 1$
となるので

論理プログラミングが $n$ 回で成功 $\iff$ シークエント計算は $n$ 回で成功
論理プログラミングが $n$ 回で失敗 $\iff$ シークエント計算は $n$ 回で失敗

が成り立ちます。シークエント計算が $n$ 回で失敗のとき、否定を表す図を書くことができます。

この項は以前書いたものを修正したものです。定数に必要なものをすべて付け加えれば良いと書いていたのに付け加えていなかった点を修正しました。ただしすべて付け加えると無限になってしまって、何も条件のない論理式として書くことができないので、個々の場合に分けて有限個で書くようにしています。

他にも間違っているところがあるかもしれないので、後で検討します。

その前に、この議論は書き方が複雑すぎるので、式を簡単に書くためにPrologのような書き方で書く方法について検討します。

2020-09-15

中間報告(3)

中間報告

論理プログラミング

「論理プログラミング」と「論理計算と随伴関手」のシリーズでは、ブラウザで行われるような無限に続く入出力を、論理プログラミングを使って極限として記述する方法を考えています。しかし実行順序を表す方法がなければ適切に表すことができるのかどうかはわからないと考えています。無限の実行順序なので何かの方法で指定する必要があります。極限として表すことができるということは言えるのですが、実行順序の指定についてはできていないので、わかりやすい説明ができていない状況です。

「半環上のフラクタル代数」では、論理プログラミングのデータを半環と考えて、それを環または体に対応させることを考えています。半環に順序を導入して、それを環または体に対応させてその極限を考えることによって実行順序を表すことを目標としています。環に関する形式的冪級数は極限として定義することができるのでその類似のものについて調べてみようとしています。そしてその順序を定義するために、数式の変形を使うことができないかと考え、その動画によって実行順序を定義する方法を考えています。

現在は、論理プログラミングと半環の対応について調べているところです。一階述語論理についても調査中です。とくにスコーレム標準形について調べています。

「フラクタル代数言語 Fractal」では論理プログラミング言語であるPrologのような言語に、そのような実行順序を指定する機能を追加する方法を考えていますが、まだ何もできていません。

圏論

「斜めの線を使わない圏論」は、このブログでは斜めの線を使った可換図式を書くことができないので、極限を数式の変形で表すことができないかということで始めたものです。極限がどんなものかというぐらいはわかるのですが、圏論についてはよく知らないので極限について調べる前にいろいろ知っていた方が良いので調べている段階です。

圏論の本でHaskellのことが書いてあるものがあったのでHaskellについても調べてみたいと思います。Haskellでは写像の合成によって実行順序が決まっているのではないかと思われるのですが、そのあたりをよく知らないので調べてみたいと思います。

関数プログラミング

「関数プログラミング」では論理プログラミングと関数プログラミングを対応させて、関数プログラミングの実行順序について調べようとしているのですが、何もできていません。Prolog的な計算方法と関数プログラミングとの関係についても調べてみたいのですが、今のところ何もやっていません。

群論の計算

「群論の計算」は代数方程式の冪根による解法の理論が体の同型の群と体上の多項式環の同型の群の計算の理論と考えていたので、体の計算のヒントになるのではないかと思って書いています。定理の証明のところまでは書いたのですが、まだうまく計算する方法はありません。証明を書いてみると知らないこと(忘れていたこと)がけっこうあってもう少し調べないといけないのかもしれません。群の計算を使って証明を書いている例は知らないので、全部を書くことはできないと思いますが部分的には群の計算でできるところもあるのではないかと思います。「3次方程式の冪根による解法」、「対称式の基本定理」はできるかもしれませんが今のところできていません。

今後の予定

極限に関する数式の変形を中心に調べていきます。Prolog のような計算方法で極限の計算ができないかということを考えていきます。

いろいろな数学の問題がヒントにならないかと考えています。絶対数学の本があって、これは体の計算に使えるかもしれないので調べてみる予定です。ABC予想の本の中で絶対数学に関連することが書いてあってこれは関係あるのかどうか調べてみる予定です。

ミレニアム問題の中に、問題を理解するために計算をやってみることができるものがあるかもしれません。フェルマーの最終定理、四色問題なども説明しようとしたことがありますがうまくいかなかったのですが、やり方によってはヒントがあるかもしれません。これらは本があるので調べやすいということは言えます。

2020-09-15

一階述語論理(1)

「論理計算と随伴関手」と「半環上のフラクタル代数」の中でプログラミング言語 Prolog のプログラムを論理計算 LK に変換しようとしていましたが、間違っていました。Prolog のプログラムが証明に対応しているのは事実で、最終的に LK に変換できればどのような対応なのかわかると思うのですが、変換が失敗しています。これは後で書き直すことにします。

ここでは数理論理学と Prolog の対応を考えます。数理論理学の中で変換に必要と思われる部分を Prolog のような計算でやってみることにします。

「数理論理学―合理的エージェントへの応用に向けて」と「数理論理学 (コンピュータ数学シリーズ)」という本を参考にします。Prolog に必要な部分だけを見たいので本をじっくり読むことはできないため、以下のサイトも参考にします。ただし記法は LK がわかりやすいという気がするので基本的には LK に従いますが、ここでは書くのが難しい記法もあるのでその場合は独自の記法で書きます。LK の記法にもいろいろあるようなので基本的には Wikipedia に従います。

Prolog の説明のために数理論理学の理論のどこまで必要なのか調べています。ある論理式とスコーレム標準形の関係がわかれば良いと思うのですが、そのために何が必要なのかまだよく知らないので調べています。

「数理論理学―合理的エージェントへの応用に向けて」によると「スコーレム標準形への変換は、充足不能性のみを保存する変換になります。」スコーレム標準形への変換は「逆変換は不可能」となります。充足不能性とは、「どのような解釈の下でも真になる論理式は恒真な論理式、ある解釈の下で真になる論理式を充足可能な論理式、どのような解釈の下でも偽になる論理式は充足不能な論理式といいます。」

「数理論理学 (コンピュータ数学シリーズ)」によると「ある式が恒真的であることと、そのスコーレム標準形が恒真的であることとは同値である。(定理5.1)」「任意の $D, M, \rho$ に対して $M[[A]]_\rho$ が true となるとき $A$ は恒真的であるという。 $A$ が恒真的でないとき、すなわち、ある $D, M, \rho$ に対して $M[[A]]_\rho$ が false となるとき、反証可能という。また、ある $D, M, \rho$ に対して $M[[A]]_\rho$ が true となるとき、充足可能という。(定義2.4)」

Prolog からシークエント計算への変換は、スコーレム標準形への変換の逆と考えられ、逆変換は決まらないということなので何か1つ変換方法を決めれば良いということだと考えられます。

cai3.cs.shinshu-u.ac.jp
www2.yukawa.kyoto-u.ac.jp

数理論理学―合理的エージェントへの応用に向けて

作者:加藤暢
発売日: 2014/10/01
メディア: 単行本

数理論理学 (コンピュータ数学シリーズ)

作者:晋, 林
発売日: 1989/12/20
メディア: 単行本

2020-09-08

半環上のフラクタル代数(8)

Prolog の動作を説明するため、集合 $X$ に対して $\mathcal{S}(X) = S(S(X))$ と $\mathcal{F}(X) = F(F(X))$ を考えました。 $\mathcal{S}(X)$ は Prolog のデータの「標準形」を作るためのもので、 $\mathcal{F}(X)$ は理論的な論理プログラミングのデータの「標準形」を作るためのものです。

$\mathcal{F}(X)$ は半環になっています。半環の場合は「選言標準形」に変形することができるので「標準形」を作る議論は必要ないのですが、Prolog と対応させるために定義してあります。

理論的な論理プログラミングは証明に対応しています。Prolog のデータはそれを非可換にしたものと考えられ、演算の順序が実行順序に対応しています。ここでは、理論的な論理プログラミングの実行順序を決める方法を考えるため、Prolog と関連付けて議論しています。これは Prolog と関連付ける方がわかりやすいかもしれないためですが、本来はこの議論は不要かもしれません。

論理プログラミングと証明の関係について「論理計算と随伴関手(13)」で説明していたのですが、説明が間違っていました。関数名と述語名は有限個しかないのでそれらの関係を全部付け加えればできると簡単に考えていたのですが、そんなに簡単ではないようです。今回説明をやり直します。

まず $\mathcal{F}(X)$ の「プログラム微分」と「代入」について考えます。「プログラム微分」は Prolog のプログラムの基本的な単位を1回だけ実行することに対応したものです。

論理プログラミングのプログラム微分

集合 $X$ に対して $R = \mathcal{F}(X)$ は半環(単位元を持つ自明ではない冪等可換半環)となります。

論理プログラミングのデータ

$C$ (Prolog の定数名に対応)、 $F$ (Prolog の関数名に対応)、 $P$ (Prolog の述語名に対応)を有限集合、 $V$ (Prolog の変数名に対応)を可算集合とします。

$T = V + C + F \times T^*$ (Prolog の項に対応)、
$S = P \times T^*$ (Prolog の述語の項に対応)、
$Q = S^* \times S$ (Prolog のホーン節に対応)、
$P = Q^*$ (Prolog のプログラムに対応)、
$E = S \times S$ (Prolog の述語の項が一致することを表すものに対応)、
$U = E + S$ (Prolog の述語の項が一致することを表すもの、または述語の項に対応)

とします。これらのもののうち変数を含まないものを

$T_C = C + F \times T_C^*$ (Prolog の変数を含まない項に対応)、
$S_C = P \times T_C^*$ (Prolog の変数を含まない述語の項に対応)、
$Q _C= S_C^* \times S_C$ (Prolog の変数を含まないホーン節に対応)、
$P_C = Q_C^*$ (Prolog の変数を含まないプログラムに対応)、
$E_C = S_C \times S_C$ (Prolog の変数を含まない述語の項が一致することを表すものに対応)、
$U_C = E_C + S_C$ (Prolog の変数を含まない述語の項が一致することを表すもの、または変数を含まない述語の項に対応)

とします。

論理プログラミングの定義

$\gamma: P \times S \to \mathcal{F}(U)$ を $( q_1, q_2, \cdots , q_m) \in P$ $(q_1, q_2, \cdots , q_m \in Q)$ と $x \in S$ に対して $\gamma( (q_1, q_2, \cdots , q_m), x) = \lambda(q_1, x) + \lambda(q_2, x) + \cdots + \lambda(q_m, x)$ と定義します。ただし $q_i$ と $q_j$ $(i \ne j)$ に現れる変数は重複しないものとします。 $q_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + \cdots + V_m$ とします。

$p \in P$ に対して $\delta_p: U \to \mathcal{F}(U)$ を $x \in S$ のとき $\delta_p(x) = \gamma(p, x)$ 、 $x \in E$ のとき $\delta_p(x) = x$ と定義します。

$\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ となります。 $\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ を $n$ 回繰り返したものを $\delta_p^{*n}: \mathcal{F}(U) \to \mathcal{F}(U)$ とします。ただし $i$ 回目の $p$ ( $p_i$ とします)と $j$ 回目の $p$ ( $p_j$ とします) $(i \ne j)$ に現れる変数は重複しないものとします。 $p_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + V_2 + \cdots$ とします。 $V$ は可算集合としたので可算回繰り返すことができます。変数以外は同じものとします。

論理プログラミングの代入

$\iota: U \to U$ を恒等写像とします。

$\bar{\sigma}(\rho_{\iota,E,0}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在するとき $(p, x)$ は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E,1}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在しないとき $(p, x)$ は $n$ 回で失敗

ということにします。

シークエント計算

これをシークエント計算に対応させます。シークエント計算の $n$ 回はプログラム微分の $n$ 回に対応するものとします。

$p \in P$ 、 $x \in S$ とし、 $(p, x)$ は $n$ 回で成功とします。このときシークエント計算の図を書くことができることを示します。これを $n$ 回の図ということにします。

まず $n = 1$ のときを考えます。

ホーン節に対応する論理式を考えます。

$T = V + C + F \times T^*$ (Prolog の項に対応)の元が $(f, (t_1, t_2, \cdots , t_n)) \in F \times T^n$ $(f \in F, t_1, t_2, \cdots , t_n \in T)$ のとき $n$ を関数 $f$ の引数の個数と呼び $a(f)$ と表すことにします( $n$ -ary ( $n$ 項の)を表す)。引数の個数が異なる関数は異なる関数とします(Prolog では関数名は同じものにできるが関数としては異なるものとする)。

各 $f \in F$ に対して $n = a(f)$ とするとき述語 $r_f(x_1, \cdots , x_n, y)$ を追加し、 $\forall x_1 \cdots \forall x_n \exists y \ r_f(x_1, \cdots , x_n, y)$ を証明の前提に追加します。

$q \in Q = S^* \times S$ (Prolog のホーン節に対応)、 $q = ( (s_1, s_2, \cdots , s_n), h)$ $(s_1, s_2, \cdots , s_n, h \in S)$ とします。

$p = (q_1, \cdots , q_k) \in P$ に対して $\bar{q_1} \land \cdots \land \bar{q_k}$ を $\bar{p}$ とおきます。

上で追加した $\forall x_1 \cdots \forall x_n \exists y \ r_f(x_1, \cdots , x_n, y)$ の全体を $r_1, \cdots , r_l$ とし、 $\bar{r} = r_1 \land \cdots \land r_l$ とおきます。

すると $\bar{r} \land \bar{p} \implies \bar{u}$ を証明する図を書くことができます。

LK の記法を一部使って書きます。
$\begin{eqnarray*} & \vdash & \bar{r} \land \bar{p} \implies \bar{u} \\ & \Uparrow & (右 \implies) \\ \bar{r} \land \bar{p} & \vdash & \bar{u} \\ & \Uparrow & (右 \exists の繰り返し) \\ \bar{r} \land \bar{p} & \vdash & \bar{u}' \\ & \Uparrow & (左 \forall の繰り返し) \\ \bar{r}' \land \bar{p}' & \vdash & \bar{u}' \\ \end{eqnarray*}$
ここで $\bar{r}'$ は $\bar{r}$ の先頭の $\forall$ をすべて取り除いたもの、ここで $\bar{p}'$ は $\bar{p}$ の先頭の $\forall$ をすべて取り除いたもの、ここで $\bar{u}'$ は $\bar{u}$ の先頭の $\exists$ をすべて取り除いたものとします。

簡単に書くために $\bar{r}'$ を $r$ 、 $\bar{p}'$ を $p$ 、 $\bar{u}'$ を $u$ と書きます。 $p = q_1 \land \cdots \land q_n$ のとき
$\begin{array}{c} r \land q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ r , q_1 , \cdots , q_n \vdash u \\ \Uparrow (左増加の繰り返し) \\ ( r , q_1 \vdash u ) \sqcup \cdots \sqcup ( r , q_n \vdash u ) \\ \end{array}$
となります。ここで $q_i = s_1 \land \cdots \land s_n \implies h$ のとき
$\begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash u \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash u) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r, h \vdash u) \\ \end{array}$
となります。ここまでが1回目とします。 $n = 0$ のとき1回で成功とします。

2回目からは $u$ の代わりに $s_i$ として $r, p \vdash s_i$ から続けます。

$p$ を途中で増やすことはできないものとして、 $r, p, \cdots , p \vdash u$ ( $p$ の個数は $n$ 個、 $p^n$ と書きます)の図を書くことができるとき $n$ 回の図を書くことができるとします。

論理プログラミングの $\delta_p^{*n}$ に対応する「 $n$ 回までの図」を考えることができます。 $r, p^n \vdash u$ から始めて $n$ 回まで書いたものを $\Delta_{r, p,n}(u)$ とします。

$e'(x, y)$ を $x = y$ のとき $e'(x, y) = 1$ 、 $x \ne y$ のとき $e'(x, y) = 0$ とします。定数は有限個なので定義できます。

論理プログラミングの述語の項に対応するものを、シークエントでも述語の項と呼ぶことにします。述語の項 $p(x_1, \cdots , x_m)$ と $q(y_1, \cdots , y_n)$ に対して、 $p(x_1, \cdots , x_m) \equiv q(y_1, \cdots , y_n)$ を

$p = q$ のとき(このとき $m = n$ としました) $e'(x_1, y_1) \land \cdots \land e'(x_m, y_m)$ 、
$p \ne q$ のとき $0$

と定義します。

あまりうまく書けていないので、この項は後でちゃんと書き直すことにします。

シークエント計算の半環

$Z = P \times S$ (シークエントを表す)、 $E' = T \times T$ ( $e(x, y)$ を表す)とします。 $W = Z + E'$ とおいて $\mathcal{F}(W)$ (シークエントで生成される半環を表す)の計算を考えます。

$Q \times S \subseteq W$ と考えて、 $\Lambda_{r}: Q \times S \to \mathcal{F}(W)$ を $( (s_1, s_2, \cdots , s_n), h) \in Q$ $(s_1, s_2, \cdots , s_n, h \in S)$ と $x \in S$ に対して $\Lambda_{r}( ( (s_1, s_2, \cdots , s_n), h), x) = (h \equiv x) s_1, s_2, \cdots , s_n$ と定義します。

この場合も、先頭の $\forall$ と $\exists$ を取り除いたものから始めます。

$\mathcal{F}(U)$ の加法を $\lor$ 、乗法を $\land$ 、 $\mathcal{F}(W)$ の加法を $\sqcup$ 、乗法を $\sqcap$ と書くことにして、「LKの変形版」で書くと
$\begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash x \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash x) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r \vdash h \equiv x) \\ \end{array}$
のように書けます。ここから $r$ を取り除いて書くこととし、 $\vdash s_i$ を $s_i$ と書くと $(h \equiv x) s_1, s_2, \cdots , s_n$ となります。(さらに進めると $e(t_1, t'_1) e(t_2, t'_2) \cdots e(t_k, t'_k) s_1, s_2, \cdots , s_n$ ( $h$ と $x$ の述語名が一致するとき、各 $t_i, t'_i$ は引数の項)、または $0$ ( $h$ と $x$ の述語名が一致しないとき)となります。この説明もわかりにくいので後で考えることとします。)

$\Gamma_{r}: P \times S \to \mathcal{F}(W)$ を $( q_1, q_2, \cdots , q_m) \in P$ $(q_1, q_2, \cdots , q_m \in Q)$ と $x \in S$ に対して $\Gamma_{r}( (q_1, q_2, \cdots , q_m), x) = \Lambda_{r}(q_1, x) + \Lambda_{r}(q_2, x) + \cdots + \Lambda_{r}(q_m, x)$ と定義します。ただし $q_i$ と $q_j$ $(i \ne j)$ に現れる変数は重複しないものとします。 $q_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + \cdots + V_m$ とします。

これを「LKの変形版」で書くと
$\begin{array}{c} r \land q_1 \land \cdots \land q_n \vdash x \\ \Uparrow (左 \land の繰り返し) \\ r , q_1 , \cdots , q_m \vdash x \\ \Uparrow (左増加の繰り返し) \\ ( r , q_1 \vdash x ) \sqcup \cdots \sqcup ( r , q_m \vdash x ) \\ \end{array}$
となります。

$p \in P$ に対して $\Delta_{r,p}: W \to \mathcal{F}(W)$ を $x \in S$ のとき $\Delta_{r,p}(x) = \Gamma_r(p, x)$ 、 $x \in E$ のとき $\Delta_{r,p}(x) = x$ と定義します。

シークエント計算の代入

$E'$ は $e(x,y)$ 全体の集合とします。

$\bar{\sigma}(\rho_{\iota,E',0}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在するとき $p \vdash x$ のシークエント計算は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E',1}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在しないとき $p \vdash x$ のシークエント計算は $n$ 回で失敗

ということにします。

論理プログラミングの $e(x,y)$ とシークエント計算の $x \equiv y$ は対応しているので

論理プログラミングが $n$ 回で成功 $\iff$ シークエント計算は $n$ 回で成功
論理プログラミングが $n$ 回で失敗 $\iff$ シークエント計算は $n$ 回で失敗

が成り立ちます。

この項はうまく説明できていないので後で書き直すことにします。

2020-08-28

半環上のフラクタル代数(7)

次に可換の場合を考えます。

モノイドから作られる半環(1)

$M$ をモノイドとします。 $N(M)$ に加法( $+$ )と乗法( $\cdot$ )を定義します。乗法は加法に優先するものとします。以下に示すように $N(M)$ は半環となります。

加法の定義

$N(M)$ のモノイドとしての演算を加法とします。

すなわち $N(M)$ のモノイドとしての演算が $\lor$ であるとき、 $N(M)$ の加法の演算 $+$ を $u = u_1 \lor \cdots \lor u_l \in N(M)$ $(u_i \in M)$ と $v = v_1 \lor \cdots \lor v_m \in N(M)$ $(v_i \in M)$ に対して $u + v = u_1 \lor \cdots \lor u_l \lor v_1 \lor \cdots \lor v_m$ と定義します。

$(N(M), \lor)$ が可換モノイドであることから $N(M)$ は加法に関して可換モノイドとなります。

乗法の定義

モノイド $M$ の演算を $\land$ とします。 $\land$ は $+$ に優先するものとします。

$a_i$ 個の和 $u_i + \cdots + u_i$ を $a_i u_i$ と書くことにします。 $u \in N(M)$ は $u = a_1 u_1 + \cdots + a_l u_l$ $(a_i \in \mathbb{N}, u_i \in M)$ と順序を除いて一意的に表すことができます。

$u = a_1 u_1 + \cdots + a_l u_l \in N(M)$ $(a_i \in \mathbb{N}, u_i \in M)$ と $v = b_1 v_1 + \cdots + b_m v_m \in N(M)$ $(b_j \in \mathbb{N}, v_j \in M)$ に対して乗法を $\displaystyle u \cdot v = \sum_{i=1}^{l} \sum_{j=1}^{m} a_i b_j (u_i \land v_j)$ と定義することができます。

乗法の結合法則

$u = a_1 u_1 + \cdots + a_l u_l \in N(M)$ $(a_i \in \mathbb{N}, u_i \in M)$ 、 $v = b_1 v_1 + \cdots + b_m v_m \in N(M)$ $(b_j \in \mathbb{N}, v_j \in M)$ 、 $w = c_1 w_1 + \cdots + c_n w_n \in N(M)$ $(c_k \in \mathbb{N}, w_k \in M)$ に対して $\displaystyle (u \cdot v) \cdot w = u \cdot (v \cdot w) = \sum_{i=1}^{l} \sum_{j=1}^{m} \sum_{k=1}^{n} a_i b_j c_k (u_i \land v_j \land w_k)$ となるので乗法の結合法則が成り立ちます。

乗法の単位元

$M$ の単位元 $1$ を $1 \in N(M)$ と見ることができます。 $u = a_1 u_1 + \cdots + a_l u_l \in N(M)$ $(a_i \in \mathbb{N}, u_i \in M)$ に対して $u \cdot 1 = a_1 (u_1 \land 1) + \cdots + a_l (u_l \land 1) = a_1 u_1 + \cdots + a_l u_l = u$ 、 $1 \cdot u = a_1 (1 \land u_1) + \cdots + a_l (1 \land u_l) = a_1 u_1 + \cdots + a_l u_l = u$ となるので $1$ は $N(M)$ の乗法の単位元となります。

よって $N(M)$ は情報に関してモノイドとなります。

乗法の加法に対する分配法則

$u = a_1 u_1 + \cdots + a_l u_l \in N(M)$ $(a_i \in \mathbb{N}, u_i \in M)$ 、 $v = b_1 v_1 + \cdots + b_m v_m \in N(M)$ $(b_j \in \mathbb{N}, v_j \in M)$ 、 $w = c_1 w_1 + \cdots + c_n w_n \in N(M)$ $(c_k \in \mathbb{N}, w_k \in M)$ に対して
$\hspace{4em} \begin{eqnarray*} (u + v) \cdot w & = & \left( \sum_{i=1}^{l} a_i u_i + \sum_{j=1}^{m} b_j v_j \right) \cdot \left( \sum_{k=1}^{n} c_k w_k \right) \\ & = & \left( \sum_{i=1}^{l} a_i u_i \right) \cdot \left( \sum_{k=1}^{n} c_k w_k \right) + \left( \sum_{j=1}^{m} b_j v_j \right) \cdot \left( \sum_{k=1}^{n} c_k w_k \right) \\ & = & u \cdot w + v \cdot w \end{eqnarray*}$
$\hspace{4em} \begin{eqnarray*} u \cdot (v + w) & = & \left( \sum_{i=1}^{l} a_i u_i \right) \cdot \left( \sum_{j=1}^{m} b_j v_j + \sum_{k=1}^{n} c_k w_k \right) \\ & = & \left( \sum_{i=1}^{l} a_i u_i \right) \cdot \left( \sum_{j=1}^{m} b_j v_j \right) + \left( \sum_{i=1}^{l} a_i u_i \right) \cdot \left( \sum_{k=1}^{n} c_k w_k \right) \\ & = & u \cdot v + u \cdot w \end{eqnarray*}$
より乗法の加法に対する分配法則が成り立ちます。

よって $N(M)$ は半環となります。

集合 $X$ に対して $N(N(X))$ 、 $N(S(X))$ は半環となります。

モノイドから作られる半環(2)

$B$ を1つの元 $\varepsilon$ からなる集合 $E = \{ \varepsilon \}$ の冪集合 $B = \{ \varnothing , E \}$ とおきます。 $B$ は和集合関してモノイドとなります。

集合 $X$ に対して $F(X) = FM(X, B, \varnothing)$ は $f \in F(X)$ を $\{ x \in X \mid f(x) \ne \varnothing \}$ と同一視することにより $X$ の有限部分集合全体の集合と考えることができます。 $F(X)$ は集合 $X$ で生成される自由冪等可換モノイドとなります。

モノイド $M$ に対して $N(M)$ と同様に $F(M)$ に乗法を定義すると、 $F(M)$ は半環となります。

集合 $X$ に対して $F(F(X))$ は半環となります。

2020-08-27

半環上のフラクタル代数(6)

ブール代数(可補分配束)の非可換であるようなものを考えます。

自由モノイド

集合 $X$ で生成される自由モノイドを $X^*$ または $S(X)$ とします。 $S(X)$ は文字の集合 $X$ から作られる文字列全体の集合と見ることができます。空文字列が単位元となります。 $X$ の元を1つの文字からなる文字列と考えると、 $X \subseteq S(X)$ と考えることができます。

$f$ を $X$ からモノイド $M$ への写像 $f: X \to M$ とします。 $M$ の演算を $\times$ 、 $S(X)$ の演算(文字列の連結)を $*$ で表すことにします。 $S(X)$ は $x_1 * \cdots * x_n$ $(x_1,\cdots , x_n \in X)$ という形の列全体の集合となります。 $S(X)$ の元 $x_1 * \cdots * x_n$ に $M$ の元 $f(x_1) \times \cdots \times f(x_n)$ を対応させる写像は、モノイドの準同型 $f^*: S(X) \to M$ となります。

モノイド $M$ に対する $S(M)$ を考えます。 $M$ の演算を $\times$ 、 $S(M)$ の演算(文字列の連結)を $*$ で表すことにします。 $S(M)$ は $x_1 * \cdots * x_n$ $(x_1,\cdots , x_n \in M)$ という形の列全体の集合となります。

$S(M)$ の元 $x_1 * \cdots * x_n$ に $M$ の元 $x_1 \times \cdots \times x_n$ を対応させる写像は、 $S(M)$ から $M$ へのモノイドの準同型となります。

自由半環

集合 $X$ で生成される自由モノイドを $S(X)$ とします。この演算子を $\land$ と書くことにします。空文字列は単位元となります。これを $1$ と書きます。

$S(X)$ で生成される自由モノイドを $S^2(X)$ とします。この演算子を $\lor$ と書くことにします。空文字列は単位元となります。これを $0$ と書きます。

$\land$ は $\lor$ に優先されるものとします。

$S(X) \subseteq S^2(X)$ と考えます。 $S^2(X)$ に二項演算 $+$ (加法)と $\cdot$ (乗法)を定義します。 $\cdot$ は $+$ に優先されるものとします。

加法の定義

$u = u_1 \lor \cdots \lor u_k \in S^2(X)$ 、 $v = v_1 \lor \cdots \lor v_l \in S^2(X)$ に対して $u + v = u_1 \lor \cdots \lor u_k \lor v_1 \lor \cdots \lor v_l$ と定義します。

この加法は $\lor$ と同じなので、 $S^2(X)$ は $+$ (加法)に関してモノイドとなります。

乗法の定義

$x \in S^2(X)$ は
$\hspace{4em} \begin{eqnarray*} x & = & x_{11} \land x_{12} \land \cdots \land x_{1m_1} \\ & \lor & x_{21} \land x_{22} \land \cdots \land x_{2m_2} \\ & \lor & \\ & \vdots & \\ & \lor & x_{n1} \land x_{n2} \land \cdots \land x_{nm_n} \\ \end{eqnarray*}$
と表すことができます $(x_{ij} \in X)$ 。 $x$ に対して $f_x : S(X) \to S^2(X)$ を $y = y_1 \land \cdots \land y_k \in S(X)$ $(x_{ij} \in X)$ に対して
$\hspace{4em} \begin{eqnarray*} f_x(y) & = & x_{11} \land x_{12} \land \cdots \land x_{1m_1} \land y_1 \land \cdots \land y_k \\ & \lor & x_{21} \land x_{22} \land \cdots \land x_{2m_2} \land y_1 \land \cdots \land y_k \\ & \lor & \\ & \vdots & \\ & \lor & x_{n1} \land x_{n2} \land \cdots \land x_{nm_n} \land y_1 \land \cdots \land y_k \\ \end{eqnarray*}$
とすると、モノイドの準同型 $f_x^* : S^2(X) \to S^2(X)$ を定義することができます。 $S^2(X)$ の乗法を $x \cdot y = f_x^*(y)$ と定義します。

乗法の結合法則

上記のように $x \in S^2(X)$ からモノイドの準同型 $f_x^* : S^2(X) \to S^2(X)$ を定義することができます。 $S^2(X)$ から $S^2(X)$ へのモノイドの準同型全体の集合 $\operatorname{End} S^2(X)$ は写像の合成に関してモノイドとなります。 $\varphi : S^2(X) \to \operatorname{End} S^2(X)$ を $\varphi(x) = f_x^*$ とすると $\varphi(x \cdot y) = f_{x \cdot y}^* = f_{x}^* \circ f_{y}^*$ $(x, y \in S^2(X))$ となるのでモノイドの準同型となります。

$S(X)$ の単位元は空文字列なのですが空文字列は書き表しにくいのでこれを $1$ と書き、 $S(X) \subseteq S^2(X)$ と見ることにより $1 \in S^2(X)$ と考えます。
$\hspace{4em} \begin{eqnarray*} f_x(1) & = & x_{11} \land x_{12} \land \cdots \land x_{1m_1} \land 1 \\ & \lor & x_{21} \land x_{22} \land \cdots \land x_{2m_2} \land 1 \\ & \lor & \\ & \vdots & \\ & \lor & x_{n1} \land x_{n2} \land \cdots \land x_{nm_n} \land 1 \\ \end{eqnarray*}$
より $f_x(1) = x$ 、 $f_x^*(1) = x$ $(x \in S^*(X))$ となります。

$x, y, z \in S^2(X)$ に対して
$\varphi( (x \cdot y) \cdot z) = f_{(x \cdot y) \cdot z}^* = f_{x \cdot y}^* \circ f_{z}^* = (f_{x}^* \circ f_{y}^*) \circ f_{z}^*$
$\varphi( x \cdot (y \cdot z)) = f_{x \cdot (y \cdot z)}^* = f_{x}^* \circ f_{y \cdot z}^* = f_{x}^* \circ (f_{y}^* \circ f_{z}^*)$
$(x \cdot y) \cdot z = \varphi( (x \cdot y) \cdot z)(1) = f_{x}^* ( f_{y}^* ( f_{z}^* (1))) = \varphi( x \cdot (y \cdot z))(1) = x \cdot (y \cdot z)$
となるので乗法の結合法則が成り立ちます。

乗法の単位元

上に述べたように $f_x^*(1) = x$ $(x \in S^*(X))$ となります。

$f_1(y) = 1 \land y _i= y_i$ $(y_i \in S(X))$ より $f_1^*(y_1 \lor \cdots y_n) = y_1 \lor \cdots y_n$ $(y_1 \lor \cdots y_n \in S^2(X))$ となって $f_1^*(y) = y$ $(y \in S^*(X))$ となります。よって $x \cdot 1 = 1 \cdot x = x$ $(x \in S^*(X))$ となって $1$ は乗法の単位元となります。

分配法則

$f_x^*$ は準同型なので $f_x^*(y+z) = f_x^*(y) + f_x^*(z)$ より $x \cdot (y + z) = x \cdot z + x \cdot z$ $(x, y, z \in S^*(X))$ が成り立ちます。

$x, y \in S^2(X)$ とします。 $z_i \in S(X)$ とすると定義より $(x + y) \cdot z_i = x \cdot z_i + y \cdot z_i$ が成り立ちます。

$z = z_1 + \cdots + z_n \in S^2(X)$ $(z_i \in S(X))$ とします。 $(S^2(X), \lor)$ が可換モノイド(すなわち $(S^2(X), +)$ が可換モノイド)であるとすると
$\hspace{4em} \begin{eqnarray*} (x + y) \cdot z & = & (x + y) \cdot (z_1 + \cdots + z_n) \\ & = & (x + y) \cdot z_1 + \cdots + (x + y) \cdot z_n \\ & = & (x \cdot z_1 + y \cdot z_1) + \cdots + (x \cdot z_n + y \cdot z_n) \\ & = & (x \cdot z_1 + \cdots + x \cdot z_n) + (y \cdot z_1 + \cdots + y \cdot z_n) \\ & = & x \cdot z + y \cdot z \end{eqnarray*}$
が成り立ちます。

よって $(S^2(X), \lor)$ が可換モノイドならば、乗法の加法に対する分配法則が成り立ちます。よって $(S^2(X), \lor)$ が可換モノイドならば、 $S^2(X)$ は半環となります。

$(S^2(X), \lor)$ は可換ではないので以下では可換になるものについて考えます。

$X$ 、 $Y$ を集合、 $e$ を $Y$ の元とします。 $FM(X, Y, e)$ を $X$ から $Y$ への写像 $f$ で、 $f(x) \ne e$ となる $x \in X$ の個数が有限であるもの全体の集合とします。 $\mathbb{N}$ を自然数全体の集合とします。 $N(X) = FM(X, \mathbb{N}, 0)$ は $X$ で生成される自由可換モノイドとなります。 $S(X)$ の元に、その中に現れる文字 $x \in X$ にその文字の現れる個数を対応させる写像を対応させると、その写像は $S(X)$ から $N(X)$ へのモノイドの準同型となります。よって $N(S(X))$ は半環となります。

$X$ を集合、 $R$ を単位元を持つ自明ではない半環、 $f : X \to R$ とします。 $X \subseteq N(S(X))$ と考えることができます。 $g: N(S(X)) \to R$ を $g(0) = 0$ 、 $g(1) = 1$ 、
$\hspace{4em} \begin{eqnarray*} x & = & k_1 x_{11} x_{12} \cdots x_{1m_1} \\ & + & k_2 x_{21} x_{22} \cdots x_{2m_2} \\ & + & \\ & \vdots & \\ & + & k_n x_{n1} x_{n2} \cdots x_{nm_n} \in N(S(X)) \\ \end{eqnarray*}$
$(k_i \in \mathbb{N}, x_{ij} \in X)$ に対して
$\hspace{4em} \begin{eqnarray*} g(x) & = & k_1 f(x_{11}) f(x_{12}) \cdots f(x_{1m_1}) \\ & + & k_2 f(x_{21}) f(x_{22}) \cdots f(x_{2m_2}) \\ & + & \\ & \vdots & \\ & + & k_n f(x_{n1}) f(x_{n2}) \cdots f(x_{nm_n}) \in R \\ \end{eqnarray*}$
と定義することができます。 $g$ が加法を保存することは定義からわかります。 $u = u_1 \cdots u_l$ $(u_{i} \in X)$ に対して $g(xu) = g(x)g(u)$ であることは定義からわかります。 $y = y_1 + \cdots + y_r$ $(y_{i} \in S(X))$ に対して
$\hspace{4em} \begin{eqnarray*} g(xy) & = & g(x (y_1 + \cdots + y_r)) \\ & = & g(x y_1 + \cdots + x y_r ) \\ & = & g(x y_1) + \cdots + g(x y_r ) \\ & = & g(x) g(y_1) + \cdots + g(x) g( y_r ) \\ & = & g(x) (g(y_1) + \cdots + g( y_r )) \\ & = & g(x) g(y_1 + \cdots + y_r) \\ & = & g(x)g(y) \end{eqnarray*}$
が成り立つので $g$ が乗法を保存することがわかります。よって $g$ は半環の準同型になります。

よって $N(S(X))$ は $X$ で生成された自由半環となります。

2020-08-25

半環上のフラクタル代数(5)

ここでは環上の多項式環に対応するものについて考えてみます。これは Prolog の実行順序の説明で必要となります。まず「群論の計算」の記事で説明した環上のモノイド代数についてもう一度説明します。

環上のモノイド代数

ここでは半環の場合も含めて考えます。半環の場合は半環上のモノイドフラクタル代数と呼ぶことにします。

$R$ を単位元を持つ自明ではない半環、 $M$ をモノイドとします。
$R[M] = \{ \xi : M \to R \ | \ 有限個の x \in M を除いて \ \xi(x) = 0 \}$
とおきます。
$R[M]$ に二項演算、加法 $+: R[M] \times R[M] \to R[M]$ と乗法 $\cdot: R[M] \times R[M] \to R[M]$ ( $\xi \cdot \eta$ を $\xi \eta$ と書くこともあります)を

$(\xi + \eta) (x) = \xi(x) + \eta(x)$
$\displaystyle (\xi \eta) (x) = \sum_{x=yz} \xi(y) \eta(z)$

と定義します。乗法は $\xi(y) \ne 0$ 、 $\eta(z) \ne 0$ であるものの和として定義します。以下のように $R[M]$ は単位元を持つ自明ではない半環となります。

加法の結合法則、交換法則

加法の結合法則、交換法則は、 $R$ が加法に関して可換モノイドであることからわかります。

加法の単位元

$\psi_0 \in R[M]$ を任意の $x \in M$ に対して $\psi_0(x) = 0$ であるような写像とすると $\psi_0$ は加法の単位元となります。

以上により $R[M]$ は加法に関して可換モノイドとなります。

加法の逆元

$R$ が環であるときは加法の逆元が存在するので、 $\xi \in R[M]$ に対して $-\xi \in R[M]$ を任意の $x \in M$ に対して $(-\xi)(x) = -\xi(x)$ であるような写像とすると $-\xi$ は $\xi$ の加法の逆元となります。

以上により $R$ が環であるとき $R[M]$ は加法に関してアーベル群となります。

乗法の結合法則

$\xi, \eta, \zeta \in R[M]$ に対して
$\displaystyle (\xi \eta) (u) = \sum_{u=xy} \xi(x) \eta(y)$ より
$\displaystyle ( (\xi \eta) \zeta ) (v) = \sum_{v=uz} (\xi \eta)(u) \zeta(v) = \sum_{v=uz} \left(\sum_{u=xy} \xi(x) \eta(y)\right) \zeta(z)$
$\displaystyle = \sum_{v=uz} \sum_{u=xy} \left(\xi(x) \eta(y)\right) \zeta(z) = \sum_{v=xyz} \left(\xi(x) \eta(y)\right) \zeta(z)$ 、
$\displaystyle (\eta \zeta) (w) = \sum_{w=yz} \eta(y) \zeta(z)$ より
$\displaystyle (\xi ( \eta \zeta) ) (v) = \sum_{v=xw} \xi(x) (\eta \zeta)(w) = \sum_{v=xw} \xi(x) \left(\sum_{w=yz} \eta(y) \zeta(z) \right)$
$\displaystyle = \sum_{v=xw} \sum_{w=yz} \xi(x) \left(\eta(y) \zeta(z)\right) = \sum_{v=xyz} \xi(x) \left(\eta(y) \zeta(z\right))$
となるので $(\xi \eta) \zeta = \xi (\eta \zeta)$ となります。よって $R$ の乗法の結合法則から $R[M]$ の乗法の結合法則が成り立ちます。

乗法の単位元

$\psi_1 \in R[M]$ を $M$ の単位元 $1$ に対して $\psi_1(1) = 1$ 、 $1$ 以外の任意の $x \in M$ に対して $\psi_1(x) = 0$ であるような写像とします。
$\xi, \eta \in R[M]$ に対して $\displaystyle (\xi \eta) (u) = \sum_{u=xy} \xi(x) \eta(y)$ より
$\displaystyle (\xi \psi_1) (u) = \sum_{u=xy} \xi(x) \psi_1(y) = \sum_{u=x} \xi(x) \psi_1(1) = \xi(u) \cdot 1 = \xi(u)$ 、
$\displaystyle (\psi_1 \xi) (u) = \sum_{u=xy} \psi_1(x) \xi(y) = \sum_{u=y} \psi_1(1) \xi(u) = 1 \cdot \xi(u) = \xi(u)$
となって $\xi \psi_1 = \psi_1 \xi = \xi$ となります。よって $\psi_1$ は乗法の単位元となります。

以上により $R[M]$ は乗法に関してモノイドとなります。

乗法の加法に対する分配法則

$\xi, \eta, \zeta \in R[M]$ に対して
$\displaystyle (\xi (\eta + \zeta)) (u) = \sum_{u=xy} \xi(x) (\eta(y) + \zeta(y)) = \sum_{u=xy} (\xi(x) \eta(y) + \xi(x) \zeta(y))$
$\displaystyle = \sum_{u=xy} \xi(x) \eta(y) + \sum_{u=xy} \xi(x) \zeta(y) = (\xi \eta)(u) + (\xi \zeta)(u)$
となって $\xi (\eta + \zeta) = \xi \eta + \xi \zeta$ となります。
$\displaystyle ( (\xi + \eta) \zeta) (u) = \sum_{u=xy} (\xi(x) +\eta(x)) \zeta(y) = \sum_{u=xy} (\xi(x) \zeta(y) + \eta(x) \zeta(y))$
$\displaystyle = \sum_{u=xy} \xi(x) \zeta(y) + \sum_{u=xy} \eta(x) \zeta(y) = (\xi \zeta)(u) + (\eta \zeta)(u)$
となって $(\xi + \eta) \zeta = \xi \zeta + \eta \zeta$ となります。
よって乗法の加法に対する分配法則が成り立ちます。

以上により $R[M]$ は単位元を持つ半環となります。 $R$ が自明ではないならば $R[M]$ は単位元を持つ自明ではない半環となります。 $R$ が可換ならば $R[M]$ も可換となります。 $R$ が環ならば $R[M]$ も環となります。

$r \in R$ と $\xi \in R[M]$ の乗法 $\cdot : R \times R[M] \to R[M]$ ( $\cdot$ は省略することもあります)を $(r \xi)(x) = r \xi(x)$ と定義します。

$R$ が環であるとき、 $R[M]$ を $R$ 上のモノイド代数と呼びます。 $M$ が可換のときは環上の結合代数となります。

$R$ が環で、 $M$ が $\{X_1, X_2, \cdots , X_n\}$ で生成された自由可換モノイドであるとき $R[M]$ は多項式環 $R[X_1, X_2, \cdots , X_n]$ となります。

$\alpha : R \to R[M]$ を $\alpha(r) = r \cdot 1_M$ とおくと $\alpha$ は単射の半環の準同型となります。 $\beta : M \to R[M]$ を $\beta(x) = 1_R \cdot x$ とおくと $\beta$ は単射のモノイドの準同型となります( $R[M]$ は乗法に関するモノイド)。任意の $r \in R$ と $x \in M$ に対して $\alpha(r) \beta(x) = \beta(x) \alpha(r)$ となります。