ちなみに，公理化するときの代数的な意味と論理学的な意味

代数にも論理学にも公理という概念がある．

正確に言うと，代数構造を設計すると言うのは，公理系を設計することである．例えば，Bool 代数とか，・・・とか．

それらのソフトウェア開発におけるプログラミング・モデリングの際の意味の違いは以下の通り．

代数学の観点から公理化をおこなうとは，結果的にデータ型としての「公理系によって定められた演算によって閉じた”集合”」を定義することである．これはパターンマッチなどの適用に便利である．

論理学の観点から公理化をおこなうとは，「形式証明」をおこなうためである．公理によって定められた規則にしたがって，与えられた命題が真であるか偽であるかを定めるためのものとして定められる．

これらより，例えば，代数仕様では公理化は証明による検証のためにものであるから，これは代数と呼びつつも，論理学的な側面を用いているような気がする．一方で，データ型の基礎理論としての代数は，証明というよりも、パターンマッチの使用など，代数的な使用を想定しているように思う．