http://nineties.github.io/category-seminar/3#/

いいねいいねー。知らない事もいっぱいだ。ただ、圏論やっているんだから論理の推論については『積み上げ』じゃなくて『段階的詳細化』の方向で行かないと行き詰まると思われ。

→http://www.amazon.co.jp/dp/4817161124 （論理との関連についてはカリー＝ハワード同型対応を手がかりに適時読み替えるべし）

最終的にソフトウェア設計の話になるのでオススメ。

関数型プログラミングなる体系だったパラダイムというのは実のところ存在しない。構造化プログラミングとバッカスのFPを聞きかじってほぼでっち上げられたもののようだ。悲惨な事にならないように、オブジェクト指向、プログラム検証などをやりたいひとは関数型プログラミングとかいわれるものなんかではなく構造化プログラミングをしっかりやった方が比較にならないくらい良い。

普遍代数

普遍代数（ふへんだいすう、universal algebra）とは代数系に共通する性質を扱う・・・

概要

?

定義とその例

普遍代数（universal algebra）

普遍代数（universal algebra）または簡潔に代数（algebra）とは空ではない集合 A と有限アリティを持つ A 上演算の族 F との組＜A；F＞のことである。F は無限集合でもよい。F が有限集合すなわち F = { f₁ , f₂ , ... , f_n } であるとき、＜A； f₁ , f₂ , ... , f_n＞と書く。

半群（semigroup）＜G；・＞

モノイド（monoid）＜M；・ , 1＞

群（group）＜G；・, ^-1 , 1＞

環（ring）＜R；＋,・, 0＞

１や０は０項演算

束（lattice）

冪等律、交換律、結合律及び吸収律を満たす２項演算 ∧ 交わり（meet）、∨ 結び（join）からなる代数＜L；∧ , ∨＞を束（lattice）と呼ぶ。

（冪等律）a ∧ a = a = a ∨ a
（交換律）a ∧ b = b ∧ a , a ∨ b = b ∨ a
（結合律）a ∧ (b ∧ c) = (a ∧ b) ∧ c , a ∨ (b ∨ c) = (a ∨ b) ∨ c
（吸収律）a ∨ (a ∧ b) = a = a ∧ (a ∨ b)

半順序集合（partial order set）

半順序集合とは、反射律、反対称律、推移律を満たす２項関係 ≦ をもつ任意の集合 P のことである。

a ≦ b（b は a を含むと読む）に対し、a < b とは a ≦ b かつ a ≠ b と定義する。また、a < b でありかつ、a < x < b となる x が存在しないとき、 b は a を覆う（cover）と呼ぶ。

順序関係 ≦ , ≧ は交わり ∧ , ∨ から定義可能。

a ≦ b は a ∧ b = a

b ≧ c は b ∨ c = b

a ∧ b ≦ a は常に真か？

a ∧ b ≦ a ＝＞ (a ∧ b) ∧ a = a ∧ b を示せばよい

(a ∧ b) ∧ a = (b ∧ a) ∧ a = b ∧ (a ∧ a) = b ∧ a = a ∧ b

よって真

逆に交わり ∧ は順序関係 ≦ から定義できる？

a ∧ b は...

普遍性

?

デカルト積（Cartesian product）

参考文献

George Grätzer (1979). Universal Algebra (2nd ed.)
大熊正『圏論（カテゴリー）』槙書店、1979年。
Garrett Birkhoff (1979). Lattice Theory (3rd ed.)
Dana Scott (1976), Data types as lattices
ガーレット・バーコフ, ソンダース・マクレーン『現代代数学概論』（改訂第３版）白水社、1967年。

利用者:I.hidekazu/sandbox