On Fri, Mar 4, 2011 at 8:45 AM, Markus Läll
<markus.l2ll@gmail.com> wrote:
Would this also have an uncomputable order type? At least for comparing tuples you'd just:
You can tell if an enumeration will have an uncomputable order type by whether or not your enumeration has to "count to infinity" before it can continue. For example, let's use top-left to bottom-right diagonals. Then you would have to "count infinitely many steps" (0,0), (1,1), (2,2), (3,3) ... before you could go to the next diagonal. This excludes an enumeration from being computable in the usual sense (or having a computable order type). As Daniel pointed out, every countable set can be put in some computable order, since it can inherit the order of the naturals through the enumeration.
lt :: (Integer,Integer) -> (Integer,Integer) -> Bool
(a,b) `lt` (c,d) = let
sum1 = (a + b)
sum2 = (c + d)
in if sum1 == sum2
then a < c
else sum1 < sum2
The order you impose is a bit broken, but the principle of using diagonals is sound. (Consider (1,2) and (2,1): under this order, (1,2) `lt` (2,1) and (2,1) `lt` (1,2), so (1,2) == (2,1))
Indeed, the diagonal construction is how an enumeration of the rationals is demonstrated.