エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理プログラミング(3)

半環の定義

集合  R に2つの二項演算、加法  + と乗法  \cdot が定義されていて、加法に関しては可換なモノイド、乗法に関してはモノイドで、乗法が加法に対して分配法則を満たすとき、 R は半環であると言います。乗法が可換であるとき  R は可換であると言います。加法が冪等であるとき  R は冪等であると言います。

 R が半環、 d が  R から  R への加法を保存する写像で、任意の  R の元  x y に対して

 \displaystyle d(xy) = d(x)y + xd(y)

が成り立つとき  d を  R微分と呼ぶことにします。

半環  R の元  x R微分  d に対して、可算個の  R の元の列

 \displaystyle x, d(x), d2(x), \cdots

 x d による極限と呼び、

 \displaystyle exp(d, x)

と書くことにします。

この定義は無限に動くプログラムを定義するときに使う予定です。今後定義を変更することがあるかもしれません。

 

ブール代数の定義

集合  R に2つの二項演算結び  \lor と交わり  \land が定義されていて、

結びと交わりは結合的、可換、冪等であり、

結びが交わりに対して分配的であり、 

交わりが結びに対して分配的であり、

吸収法則

 \displaystyle (x \land y) \lor x = x, (x \lor y ) \land x = x

を満たすとき  R分配束であると言います。

分配束  R に元  0 1 と単項演算  \lnot が存在して任意の  R の元  x y に対して

 \displaystyle x \land \lnot x = 0, x \lor \lnot x = 1

を満たすとき、 Rブール代数であると言います。

 

PLP は否定を含まないので PLP のデータは分配束として定義することができます。分配束は結びに関する単位元  0 と交わりに関する単位元  1 が存在するとき可換な冪等半環となります。

これらの定義を使って PLP を数学的に定義していきます。プログラムを実行してみることができるサイトを作る予定です。動画も作る予定です。