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

psykotic

By: a guest on Aug 11th, 2009  |  syntax: None  |  size: 11.73 KB  |  hits: 432  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
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
  26. > addN (Succ m) n = Succ (addN m n)
  27.  
  28. This makes N into a monoid.
  29.  
  30. > instance Monoid N where
  31. >     mempty = Zero
  32. >     mappend = addN
  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
  123. >     mappend = addZ
  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.