Pastebin launched a little side project called HostCabi.net, check it out ;-)Don't like ads? PRO users don't see any ads ;-)

# psykotic

By: a guest on Aug 11th, 2009  |  syntax: None  |  size: 11.73 KB  |  hits: 432  |  expires: Never
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
1. Grothendieck Completion
2.
3. > {-# OPTIONS -XNoMonomorphismRestriction -XExistentialQuantification #-}
4. > import Data.Monoid
5. > import Data.Set
6.
7. One of the experiences of learning mathematics is climbing the ladder
8. of numbers from natural numbers to complex numbers:
9.
10.     N < Z < Q < R < C
11.
12. Here I'll review how Z may be constructed from N by a general algebraic
13. method and then see what that same method yields when applied to more
14. arbitrary data types.
15.
16. We define natural numbers as Peano numerals.
17.
18. > data N = Zero | Succ N deriving (Eq, Show)
19.
20. A mathematician would say that we have made a free monoid on one
21. generator (the Succ constructor).
22.
23. Addition is a simple matter of combining all the generators.
24.
25. > addN Zero     n = n
27.
28. This makes N into a monoid.
29.
30. > instance Monoid N where
31. >     mempty = Zero
33.
34. As a matter of syntactic convenience, we'll use an infix operator for
35. the monoid operation and use a shorthand for the unit.
36.
37. > e = mempty
38. > (>>>) = mappend
39.
40. The left-to-right bias of >>> is intended. Later we will be working with
41. non-commutative monoids.
42.
43. The e is shorthand for Einheit, meaning unit, and is a common abbreviation
44. in the literature. If you don't like it, tough! Blame Germany for producing
45. so many influential algebraists and settling countless conventional one-letter
46. abbreviations like K for fields (K for Körper).
47.
48. We'd like for N to be an instance of Num so we can use fromInteger. We don't
49. care about the rest, so we leave them undefined.
50.
51. > instance Num N where
52. >     fromInteger n = iterate Succ Zero !! fromInteger n
53. >
54. >     (+) = undefined
55. >     (*) = undefined
56. >     abs = undefined
57. >     signum = undefined
58.
59. Most of us are used to thinking of the integers Z as natural numbers with a
60. sign prefixed. To construct Z from N, your first instinct is probably to define
61.
62.   data Sign = Minus | Plus
63.   data Z = Z Sign N
64.
65. Indeed, that is one possible way to go. The only hitch is that you have to
66. ensure that Z Plus Zero and Z Minus Zero are considered equal. The easiest
67. way to achieve that is to use some consistent normalization:
68.
69.   normalizeZ (Z Minus Zero) = Z Plus Zero
70.   normalizeZ n              = n
71.
72. All functions that construct new integers must then call normalizeZ.
73.
74. However, there is also an alternative construction of Z from N. The idea is
75. this: Rather than view the sign (plus or minus) as a prefix, we can view it
76. as an infix between two numbers. That is, we know that every integer can be
77. expressed as the difference of two naturals, so we should be able to represent
78. integers as pairs of naturals (m, n), corresponding to the integer m - n.
79.
80. The mathematician Grothendieck invented a more general version of this
81. construction to define the K_0 groups of K theory, and therefore it generally
82. bears his name. You see variations on "Grothendieck construction", "Grothendieck
83. completion" and "K-completion" thrown around. Here I'll refer to it as the
84. Grothendieck completion as best describes its purpose of completing (in the
85. sense of filling or perfecting) a monoid by adjoining formal inverses.
86.
87. > data Z = Z N N deriving Show
88.
89. With the sign-based representation, the only redundantly represented number
90. was zero, expressible as either plus or minus zero. With this pair-based
91. representation, there are far more redundancies. For example, 2 - 3 and
92. 1 - 2 both represent the same number. More generally,
93.
94.     m - n = m' - n'
95.
96. if and only if
97.
98.     m + n' = m' + n
99.
100. As an aside, note how this looks like the rule for comparing fractions
101. if you replace + and - by * and /. The only difference is that we allow
102. our "denominators" to be zero.
103.
104. > instance Eq Z where
105. >     (Z m n) == (Z m' n') = (m >>> n') == (m' >>> n)
106.
107. Addition is now defined by simply adding entrywise, much like how fractions
108. are multiplied by multiplying numerators and denominators separately.
109.
110. > addZ (Z m n) (Z m' n') = Z (m >>> m') (n >>> n')
111.
112. If no for other reason, this simple implementation of integer addition should
113. make us appreciate this pair-based construction.
114.
115. Addition for sign-based integers is less symmetric and messier. It corresponds
116. to addition in the pair-based representation, where Plus n and Minus n are
117. interpreted as (n, Zero) and (Zero, n), followed by a normalization step that
118. shifts all the Succ occurrences to one side or the other, depending on which is
119. larger.
120.
121. > instance Monoid Z where
122. >     mempty = Z Zero Zero
124.
125. Everything should far should have been pretty simple. I hope you're convinced
126. that this pair-based representation indeed produces a structure isomorphic to
127. integers. However, let's review what we did in more general terms in an attempt
128. to identify the assumptions that made it work out so well.
129.
130. We started with N, a free monoid on one generator. Because it only has a single
131. generator, N is automatically commutative. While the monoidal operation (addition)
132. is not generally invertible, N's freeness as a monoid does have a related
133. property: If a >> b = a >> c then a = b. This makes N a cancelative monoid.
134.
135. Let's say we want to extend or complete N to make its operation invertible.
136. That is, we want to make N a group. A group is just a monoid with a way of
137. computing inverses for every element.
138.
139. > class Monoid g => Group g where
140. >     inverse :: g -> g
141.
142. For a Group instance to represent an actual group, the defining property
143. of inverses must hold:
144.
145.   x >>> inverse x = e
146.   inverse x >>> x = e
147.
148. This is easily implemented for our integer type Z. It's just a matter of
149. swapping the entries in a pair.
150.
151. > instance Group Z where
152. >     inverse (Z m n) = (Z n m)
153.
154. As an aside, it's curious to see that the involution property of inverses
155. follows from the fact that swapping pair entries twice does nothing!
156.
157. The group completion of N is a new algebraic object K N with a map
158.
159.   inject :: N -> K N
160.
161. It is injective and therefore paired with a projection:
162.
163.   project :: K N -> Maybe K
164.
165. Projection is the left inverse of injection:
166.
167.   project . inject = Just
168.
169. Whatever else its properties, a basic requirement is that the injective image
170. of N inside of K N should behave identically to N on its own. That is, if
171. we zoom in on the part of K N that is the injective image of N then the
172. dynamics should be indistinguishable from N's own dynamics. This is another
173. way of saying that the injection is a monoid homomorphism:
174.
175.   inject (x >>> y) = inject x >>> inject y
176.
177. The >>> on the left side is in N and the one on the right side is in K N.
178.
179. Let's return to the cancelation property and consider a general monoid M.
180. We saw earlier that in the case of N, a cancelative monoid, we successfully
181. got Z, a group, as the completion. What would happen if M were not cancelative?
182.
183. One case would be the natural numbers, this time with multiplication instead of
184. addition. We can cancel most of the time but not when the multiplier is zero.
185. Certainly 0 * 1 = 0 * 3 does not imply 1 = 3. In attempting to complete this M to
186. K M the requirement that 'inject' is a homomorphism means that n * 0 = 0 for all n
187. must also hold true in K M as well. But since every element, including 0, must have
188. an inverse, we can take the equality like 0 * n = 0 and multiply both sides by the
189. inverse of 0 to get n = 0. That is, the image of M inside K M is 0, so 'inject'
190. certainly cannot be injective!
191.
192. Thus we see that a monoid must be cancelative to have a group completion.
193.
194. The other special fact about N is that it is a free monoid, and in particular it
195. is a free monoid on one generator ("one-dimensional") and therefore commutative.
196. What about free monoids on more generators, which would be non-commutative?
197.
198. For any type X we can consider the free monoid F X with a generator for every element
199. in X. An element of F X is a word (possibly empty) drawn from the alphabet X and
200. the monoid operation is concatenation. The free monoid construction is a functor,
201. meaning every map X -> Y can be lifted to a map F X -> F Y on the free monoids.
202.
203. This F is of course none other than the type constructor for lists! The monoid operation
204. is list concatenation and the identity element is the empty list. The lifting is our
205. familiar friend map :: (a -> b) -> ([a] -> [b]).
206.
207. We have said multiple times that N is a free monoid on one generator. With this
208. identification of the free monoid construction F with the type constructor for lists,
209. this is simply a way of saying that N is isomorphic to [()] since () is the canonical
210. type inhabited by a single value, also denoted ().
211.
212. What happens when we transfer our pairing construction to arbitrary free monoids?
213. It's a straightforward matter of taking our code from Z and replacing every occurrence
214. of N with an abstract type parameter:
215.
216. > data K m = K m m deriving Show
217. >
218. > instance Monoid m => Monoid (K m) where
219. >     mempty = K e e
220. >     mappend (K x y) (K x' y') = K (x >>> x') (y >>> y')
221. >
222. > instance Monoid m => Group (K m) where
223. >     inverse (K x y) = (K y x)
224. >
225. > instance (Monoid m, Eq m) => Eq (K m) where
226. >     (K x y) == (K x' y') = (x >>> y') == (x' >>> y)
227.
228. Injection and projection is now a simple matter:
229.
230. > inject x = (K x e)
231. >
232. > project (K x e) = Just x
233. > project _       = Nothing
234.
235. It's easy to see that project . inject = Just. What about the homomorphism property?
236. Can you prove that?
237.
238. We defined an instance of Group for K m but is it actually a group? So far we've only
239. verified that directly for the type N, or equivalently [()]. Let's tackle the next
240. simplest case, where the value type has two elements. We might as well pick the standard
241. type Bool.
242.
243. *Main> let x = inject [True]
244. *Main> x
245. K [True] []
246. *Main> inverse x
247. K [] True
248. *Main> x >>> inverse x
249. K [True] [True]
250. *Main> x >>> inverse x == e
251. True
252.
253. Cool! But so far we have only used lists of one kind of value. Let's try more.
254.
255. *Main> let x = inject [True, False]
256. *Main> x
257. K [True,False] []
258. *Main> inverse x
259. K [] [True,False]
260. *Main> x >>> inverse x == e
261. True
262.
263. It seems to work alright. Let's try some experiments with an infinite value type. We'll
264. use the integers.
265.
266. *Main> let a = inject [1]
267. *Main> let b = inject [2]
268. *Main> let c = inject [3]
269. *Main> a >>> (b >>> inverse b)
270. K [1,2] [2]
271. *Main> a >>> (b >>> inverse b) >>> c
272. K [1,2,3] [2]
273.
274. We would expect (b >>> inverse b) to be not only equal to e in the sense of the (==)
275. equality function we defined but to be interchangeable with all e in all contexts,
276.
277. *Main> a >>> e >>> c
278. K [1,3] []
279. *Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
280. False
281.
282. Damn! That's definitely not right!
283.
284. The problem stems from the lack of commutativity, so it seem that the commutativity of N
285. that may have seemed incidental to our success in constructing Z is not so incidental
286. after all.
287.
288. To verify that the construction indeed works for commutative monoids other than N, let's
289. explore some related examples. It turned out that lists (free mononoids) did not work due
290. to the non-commutativity of list concatenation. What are the closest thing to lists
291. while having a commutative kind of concatenation? Sets of course! The Set type constructor
292. in fact corresponds to the free commutative monoid construction. Given a type X that acts
293. as a generating set, Set X is the freest possible commutative monoid with X as generators.
294.
295. Let's replay the failing example with sets instead of lists.
296.
297. *Main> let a = inject (singleton 1)
298. *Main> let b = inject (singleton 2)
299. *Main> let c = inject (singleton 3)
300. *Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
301. True
302.
303. Yay! It worked!
304.
305. If K N were the integers then what is K (Set X)? Because of the commutativity, the different
306. generators don't really interact, so you'd expect it to be a product of integers, one copy
307. for each value in X. That is, K (Set X) is isomorphic to the function type X -> Z.