半環の定義
集合 に2つの二項演算、加法
と乗法
が定義されていて、加法に関しては可換なモノイド、乗法に関してはモノイドで、乗法が加法に対して分配法則を満たすとき、
は半環であると言います。乗法が可換であるとき
は可換であると言います。加法が冪等であるとき
は冪等であると言います。
が半環、
が
から
への加法を保存する写像で、任意の
の元
と
に対して
が成り立つとき を
の微分と呼ぶことにします。
半環 の元
と
の微分
に対して、可算個の
の元の列
を の
による極限と呼び、
と書くことにします。
この定義は無限に動くプログラムを定義するときに使う予定です。今後定義を変更することがあるかもしれません。
ブール代数の定義
集合 に2つの二項演算結び
と交わり
が定義されていて、
結びと交わりは結合的、可換、冪等であり、
結びが交わりに対して分配的であり、
交わりが結びに対して分配的であり、
吸収法則
を満たすとき は分配束であると言います。
分配束 に元
と
と単項演算
が存在して任意の
の元
と
に対して
を満たすとき、 はブール代数であると言います。
PLP は否定を含まないので PLP のデータは分配束として定義することができます。分配束は結びに関する単位元 と交わりに関する単位元
が存在するとき可換な冪等半環となります。
これらの定義を使って PLP を数学的に定義していきます。プログラムを実行してみることができるサイトを作る予定です。動画も作る予定です。