二項クリーネ・スター

二項演算としてのクリーネ・スターを調べている。以下a*bは、(a^*)・bのことではなくて、aとbに二項演算*を施した結果。感じとしては、不定の述語pに対して、while(p){a};b のこと。

不動点帰納法による定式化は次のようだろう。

1. b + a(a*b) = a*b （または b + a(a*b) ≦ a*b）
2. b + ay ≦ y ⇒ y≦a*b

CWIのワン・フォッキンク（Wan Fokkink）が等式的な公理化を2種類提案していて、簡単なほうは、

1. a(a*b) + b = a*b
2. a*(a*b) = a*b

もうひとつは：

1. x(x*y) + y = x*y
2. (x*y)z = x*(yz)
3. x*(y（(x+y)*z） + z) = (x+y)*z

下の複雑な公理系から a*(a*b) = a*b を導くには：

   a*b

 ↓ ベキ等性より a = a + a

 = (a + a)*b

 ↓ 公理3で展開

 = a*[a（(a+a)*b） + b]

 ↓ ベキ等性より a + a = a

 = a*[a(a*b) + b]

 ↓ 公理1

 = a*[a*b]