@@ -1,11 +1,8 @@
11module Control.Algebra
22
3−import Data.Heap
4−
5−-- XXX: change?
63infixl 6 <->
7−infixl 6 <.>
8−infixl 5 <#>
4+infixl 7 <.>
5+
96
107||| Sets equipped with a single binary operation that is associative, along with
118||| a neutral element for that binary operation and inverses for all elements.
@@ -40,7 +37,6 @@ class Monoid a => Group a where
4037||| forall a, inverse a <+> a == neutral
4138class Group a => AbelianGroup a where { }
4239
43−
4440||| Sets equipped with two binary operations, one associative and commutative
4541||| supplied with a neutral element, and the other associative, with
4642||| distributivity laws relating the two operations. Must satisfy the following
@@ -64,7 +60,6 @@ class Group a => AbelianGroup a where { }
6460class AbelianGroup a => Ring a where
6561 (<.>) : a -> a -> a
6662
67−
6863||| Sets equipped with two binary operations, one associative and commutative
6964||| supplied with a neutral element, and the other associative supplied with a
7065||| neutral element, with distributivity laws relating the two operations. Must
@@ -91,137 +86,10 @@ class AbelianGroup a => Ring a where
9186class Ring a => RingWithUnity a where
9287 unity : a
9388
94−
95−||| Sets equipped with a binary operation that is commutative, associative and
96−||| idempotent. Must satisfy the following laws:
97−|||
98−||| + Associativity of join:
99−||| forall a b c, join a (join b c) == join (join a b) c
100−||| + Commutativity of join:
101−||| forall a b, join a b == join b a
102−||| + Idempotency of join:
103−||| forall a, join a a == a
104−|||
105−||| Join semilattices capture the notion of sets with a "least upper bound".
106−class JoinSemilattice a where
107− join : a -> a -> a
108−
109−instance JoinSemilattice Nat where
110− join = maximum
111−
112−instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
113− join = merge
114−
115−||| Sets equipped with a binary operation that is commutative, associative and
116−||| idempotent. Must satisfy the following laws:
117−|||
118−||| + Associativity of meet:
119−||| forall a b c, meet a (meet b c) == meet (meet a b) c
120−||| + Commutativity of meet:
121−||| forall a b, meet a b == meet b a
122−||| + Idempotency of meet:
123−||| forall a, meet a a == a
124−|||
125−||| Meet semilattices capture the notion of sets with a "greatest lower bound".
126−class MeetSemilattice a where
127− meet : a -> a -> a
128−
129−instance MeetSemilattice Nat where
130− meet = minimum
131−
132−
133−||| Sets equipped with a binary operation that is commutative, associative and
134−||| idempotent and supplied with a unitary element. Must satisfy the following
135−||| laws:
136−|||
137−||| + Associativity of join:
138−||| forall a b c, join a (join b c) == join (join a b) c
139−||| + Commutativity of join:
140−||| forall a b, join a b == join b a
141−||| + Idempotency of join:
142−||| forall a, join a a == a
143−||| + Bottom (Unitary Element):
144−||| forall a, join a bottom == a
145−|||
146−||| Join semilattices capture the notion of sets with a "least upper bound"
147−||| equipped with a "bottom" element.
148−class JoinSemilattice a => BoundedJoinSemilattice a where
149− bottom : a
150−
151−
152−instance BoundedJoinSemilattice Nat where
153− bottom = Z
154−
155−
156−||| Sets equipped with a binary operation that is commutative, associative and
157−||| idempotent and supplied with a unitary element. Must satisfy the following
158−||| laws:
159−|||
160−||| + Associativity of meet:
161−||| forall a b c, meet a (meet b c) == meet (meet a b) c
162−||| + Commutativity of meet:
163−||| forall a b, meet a b == meet b a
164−||| + Idempotency of meet:
165−||| forall a, meet a a == a
166−||| + Top (Unitary Element):
167−||| forall a, meet a top == a
168−|||
169−||| Meet semilattices capture the notion of sets with a "greatest lower bound"
170−||| equipped with a "top" element.
171−class MeetSemilattice a => BoundedMeetSemilattice a where
172− top : a
173−
174−
175−
176−||| Sets equipped with two binary operations that are both commutative,
177−||| associative and idempotent, along with absorbtion laws for relating the two
178−||| binary operations. Must satisfy the following:
179−|||
180−||| + Associativity of meet and join:
181−||| forall a b c, meet a (meet b c) == meet (meet a b) c
182−||| forall a b c, join a (join b c) == join (join a b) c
183−||| + Commutativity of meet and join:
184−||| forall a b, meet a b == meet b a
185−||| forall a b, join a b == join b a
186−||| + Idempotency of meet and join:
187−||| forall a, meet a a == a
188−||| forall a, join a a == a
189−||| + Absorbtion laws for meet and join:
190−||| forall a b, meet a (join a b) == a
191−||| forall a b, join a (meet a b) == a
192−class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
193−
194−
195−instance Lattice Nat where { }
196−
197−||| Sets equipped with two binary operations that are both commutative,
198−||| associative and idempotent and supplied with neutral elements, along with
199−||| absorbtion laws for relating the two binary operations. Must satisfy the
200−||| following:
201−|||
202−||| + Associativity of meet and join:
203−||| forall a b c, meet a (meet b c) == meet (meet a b) c
204−||| forall a b c, join a (join b c) == join (join a b) c
205−||| + Commutativity of meet and join:
206−||| forall a b, meet a b == meet b a
207−||| forall a b, join a b == join b a
208−||| + Idempotency of meet and join:
209−||| forall a, meet a a == a
210−||| forall a, join a a == a
211−||| + Absorbtion laws for meet and join:
212−||| forall a b, meet a (join a b) == a
213−||| forall a b, join a (meet a b) == a
214−||| + Neutral for meet and join:
215−||| forall a, meet a top == top
216−||| forall a, join a bottom == bottom
217−class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
218−
219−
220−-- Fields.
221−||| Sets equipped with two binary operations, both associative and commutative
222−||| supplied with a neutral element, with
223−||| distributivity laws relating the two operations. Must satisfy the following
224−||| laws:
89+||| Sets equipped with two binary operations – both associative, commutative and
90+||| possessing a neutral element – and distributivity laws relating the two
91+||| operations. All elements except the additive identity must have a
92+||| multiplicative inverse. Must satisfy the following laws:
22593|||
22694||| + Associativity of `<+>`:
22795||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
@@ -238,34 +106,24 @@ class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a w
238106||| + Unity for `<.>`:
239107||| forall a, a <.> unity == a
240108||| forall a, unity <.> a == a
241−||| + InverseM of `<.>`:
242−||| forall a, a <.> inverseM a == unity
243−||| forall a, inverseM a <.> a == unity
109+||| + InverseM of `<.>`, except for neutral
110+||| forall a /= neutral, a <.> inverseM a == unity
111+||| forall a /= neutral, inverseM a <.> a == unity
244112||| + Distributivity of `<.>` and `<->`:
245113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
246114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
247115class RingWithUnity a => Field a where
248− inverseM : a -> a
249−
116+ inverseM : (x : a) -> Not (x = neutral) -> a
250117
251−||| A module over a ring is an additive abelian group of 'vectors' endowed with a
252−||| scale operation multiplying vectors by ring elements, and distributivity laws
253−||| relating the scale operation to both ring addition and module addition.
254−||| Must satisfy the following laws:
255−|||
256−||| + Compatibility of scalar multiplication with ring multiplication:
257−||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
258−||| + Ring unity is the identity element of scalar multiplication:
259−||| forall v, unity <#> v = v
260−||| + Distributivity of `<#>` and `<+>`:
261−||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
262−||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
263−class (RingWithUnity a, AbelianGroup b) => Module a b where
264− (<#>) : a -> b -> b
118+sum : (Foldable t, Monoid a) => t a -> a
119+sum = foldr (<+>) neutral
265120
121+product : (Foldable t, RingWithUnity a) => t a -> a
122+product = foldr (<.>) unity
266123
267−||| A vector space is a module over a ring that is also a field
268−class (Field a, Module a b) => VectorSpace a b where {}
124+power : RingWithUnity a => a -> Nat -> a
125+power _ Z = unity
126+power x (S n) = x <.> (Algebra.power x n)
269127
270128
271129-- XXX todo: