This time I will write about a way to construct fields from integral domains using Haskell. It will use the structures from my previous post. But first a comment on that post. When discussing integral domains I said that it was hard to test the property that there should be no zero divisors. A friend of mine asked me why I did not test the contrapositive instead. That is, I should use to convert into which should be easier to test…
Now let’s consider how to turn integral domains into fields. This construction is called field of fractions and is denoted by where A is an integral domain. It is a generalization of the construction of from . An element of is a pair with and . This pair should be interpreted as . This could be represented straight forwardly in Haskell as a pair. But I want to work with reduced expressions, that is I want the extra constraint that . To guarantee this I need to consider a more specialised structure than integral domains called GCD domains. This is a structure in which any pair of nonzero elements has a greatest common divisor. This is represented as:
class IntegralDomain a => GCDDomain a where gcd' :: a -> a -> (a,a,a)
Here gcd’ take nonzero and and compute such that , and . That is, it computes the greatest common divisor of and plus witnesses that it actually divides both and . This can be specified as:
propGCD :: (GCDDomain a, Eq a) => a -> a -> Property propGCD a b = a /= zero && b /= zero ==> a == g <*> x && b == g <*> y where (g,x,y) = gcd' a b
Now we are ready to represent the field of fractions over a GCD domain:
newtype GCDDomain a => FieldOfFractions a = F (a,a)
Now can be embedded in by
toFieldOfFractions :: GCDDomain a => a -> FieldOfFractions a toFieldOfFractions a = F (a,one)
Since we are working over a GCD domain we can compute reduced expressions:
reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a reduce (F (a,b)) | b == zero = error "reduce: Division by 0" | a == zero = F (zero,one) | otherwise = F (x,y) where (g,x,y) = gcd' a b
Using this we can define a function from to A.
fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a fromFieldOfFractions x | b' == one = a' | otherwise = error "fromFieldOfFractions: Denominator is not 1" where F (a',b') = reduce x
To test equality the underlying ring need to have decidable equality (i.e. it should be discrete). and are equal iff which give:
instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a) where (F (a,b)) == (F (c,d)) = a <*> d == b <*> c
We can also implement all the operations needed for showing that the constructed field of fractions is in fact a field.
instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a) where (F (a,b)) <+> (F (c,d)) = reduce (F (a <*> d <+> c <*> b,b <*> d)) (F (a,b)) <*> (F (c,d)) = reduce (F (a <*> c,b <*> d)) neg (F (a,b)) = reduce (F (neg a,b)) one = toFieldOfFractions one zero = toFieldOfFractions zero instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a) instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a) instance (GCDDomain a, Eq a) => Field (FieldOfFractions a) where inv (F (a,b)) | a == zero = error "inv: Can't invert 0" | b == zero = error "inv: Division by 0" | otherwise = reduce $ F (b,a)
Finally we can construct from by just writing:
type Q = FieldOfFractions Z *Algebra.Q> quickCheck (propField :: Q -> Q -> Q -> Property) +++ OK, passed 100 tests. *Algebra.Q> 3*(1/2)^3 :: Q 3/8
Where the last computation is possible by adding suitable Num, Fractional and Show instances. I really like this way of constructing fields. For instance I used this to implement the field of rational functions using my implementation of polynomials.
Of course I don’t need the GCDDomain constraint for any function except fromFieldOfFractions, so it would be very easy to generalize this for any integral domain. But it proved useful when implementing a proof for constructing interesting Prüfer domains, so I added the constraint everywhere. It also look more appealing with reduced expressions and I have only had to consider and the field of rational functions so far.
Finally I would like to write a little about GCD domains. It is possible to prove that they are non-Noetherian analogues of unique factorization domains (UFDs), that is, one gets UFDs by taking GCD domains and adding the ascending chain condition on ideals. The reason for not having Noetheriannity is that it gives constructive versions of classical notions. So instead of UFDs we get GCD domains and instead of PIDs we get Bézout domains in constructive mathematics. The problem with Noetheriannity is quite intricate and I have not fully grasped it yet. As far as I know there is no consensus about what a constructive version should be. I plan to write more about this in some upcoming posts.