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

半環の定義

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

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

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

半環 の元 と の微分 に対して、可算個の の元の列

を の による極限と呼び、

と書くことにします。

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

ブール代数の定義

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

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

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

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

吸収法則

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

分配束 に元 と と単項演算 が存在して任意の の元 と に対して

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

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

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