日々の流転

λ. 群の公理の問題

群の公理

• ∀x. 1 x = x
• ∀x. x^-1 x = 1
• ∀x,y,z. (x y) z = x (y z)

から

• ∀x. x 1 = x

を証明せよ。

以前にやったことあるし、とりあえず証明はすぐに出来た。

この群の公理の話はKnuth-Bendixの完備化手続きの例として良く出てくる*1のだが、実際に手で完備化をしようとしたら、規則がオーバーラップする場合を全て列挙する方法が良くわからなくて困ってしまった。俺駄目すぎ。また、列挙する順序によっては本来不要な規則を追加することになってしまうような……