Hilbert-Post Completeness of BoolState

gistfile1.txt

以下は Lecture 1: Algebraic Effects I （Gordon Plotkin） - Exercise 5 の解である。
http://cs.ioc.ee/ewscs/2015/plotkin/plotkin-slides-exercises1.pdf

p. 31 の等式理論 BoolState より、いかなる式に対しても
read(write_b1(x), write_b2(y))  (x, yは変数)
という形の normal form が自然に与えられる。

以下のように、2つの異なる normal form に関する等式を仮定する:
read(write_b1(x), write_b2(y)) ＝ read(write_b1'(x'), write_b2'(y'))  (b1 ≠ b1' ∨ x ≠ x' ∨ b2 ≠ b2' ∨ y ≠ y')

このとき、b1 ≠ b1' ∨ x ≠ x' の場合は write_true、b2 ≠ b2' ∨ y ≠ y' の場合は write_false を上に示した等式の外側に付け、公理に従って式変形し、代入を行うことで
write_b3(z) = write_b3'(z')  (b3 ≠ b3' ∨ z ≠ z')
が導ける。ここから、いかなる b, w, w' についても write_b(w) = write_b(w') が成り立つことを導く。

- b3 = b3' かつ z ≠ z' の場合:
  各変数への代入(b3 = b3' = b, z = w, z' = w')により目的の式が導ける。
- b3 ≠ b3' の場合:
  必要に応じて対称律を用いることで write_true(z) = write_false(z') が導ける。この両辺に z = z' = read(write_b(w), write_b(w')) を代入すると、
  write_true(z) ＝ write_true(read(write_b(w), write_b(w'))) ＝ write_true(write_b(w)) = write_b(w),
  write_false(z') = write_false(read(write_b(w), write_b(w'))) ＝ write_false(write_b(w')) = write_b(w')
  となるので、write_b(w) = write_b(w')。

上に示したように、任意の b, w, w' について write_b(w) = write_b(w') が成り立つので、任意の x, y について
read(write_true(x), write_false(x)) = read(write_true(y), write_false(y))
が導ける。この式と
read(write_true(x), write_false(x)) = read(x, x) = x,
read(write_true(y), write_false(y)) = read(y, y) = y
より、x = y。

2つの異なる normal form に関する等式が成り立つと仮定し、BoolState の公理を用いて任意の x, y について x = y であることを示したので、等式理論 BoolState は Hilbert-Post complete である。