Why I Don't Love Gödel, Escher, Bach

of course I do - I misspoke after I missed your reference to prime numbers in the list of open/hard problems. I get why you're including it, but if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" so I don't see your point.

That's lovely, but didn't answer the question. But I can see that perhaps I offended you, I was just curious, so sorry.

You posted something inaccurate and chasing offered a correction. Instead of e-pretending to miss the point, accept the correction as you did with ramblerman.

A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop:

  loop = loop

What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`:

  loop : forall t. t
  loop = loop

Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values!

    data Empty where
      -- This page intentionally left blank

    loop : forall t. t
    loop = loop

    myEmptyValue : Empty
    myEmptyValue = loop

In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested):

    -- Peano arithmetic
    data Natural where
      Zero : Natural
      Succ : Natural -> Natural

    one = Succ Zero

    halve : Natural -> Natural
    halve Zero            = Zero
    halve (Succ Zero)     = Succ Zero  -- Should never reach this; included for completeness
    halve (Succ (Succ n)) = Succ (halve n)

    threeTimes : Natural -> Natural
    threeTimes Zero     = Zero
    threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n)))

    data Boolean where
      True  : Boolean
      False : Boolean

    not : Boolean -> Boolean
    not True  = False
    not False = True

    ifThenElseNat : Boolean -> Natural -> Natural -> Natural
    ifThenElseNat True  x y = x
    ifThenElseNat False x y = y

    isEven : Natural -> Boolean
    isEven Zero     = True
    isEven (Succ n) = not (isEven n)

    collatzStep : Natural -> Natural
    collatzStep Zero     = one  -- Again, only for completeness
    collatzStep (Succ n) = ifThenElseNat (isEven (Succ n))
                                         (halve (Succ n))
                                         (Succ (threeTimes (Succ n)))

    -- This won't be allowed by Agda/Idris since it may or may not halt ;)
    collatzLoop : Natual -> Natural
    collatzLoop Zero            = collatzLoop (collatzStep Zero)  -- For completeness
    collatzLoop (Succ Zero)     = Succ Zero  -- Halt
    collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n)))

We can then define the Collatz conjecture, using a standard encoding of equality:

    data Equal : Natural -> Natural -> Type where
      reflexivity : (n : Natural) -> Equal n n

    CollatzConjecture : Type
    CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one

    proofOfCollatzConjecture : CollatzConjecture
    proofOfCollatzConjecture = ?

    disproofOfCollatzConjecture : CollatzConjecture -> Empty
    disproofOfCollatzConjecture purportedProof = ?

The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong).

The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them!

    proofOfCollatzConjecture : CollatzConjecture
    proofOfCollatzConjecture = loop

    disproofOfCollatzConjecture : CollatzConjecture -> Empty
    disproofOfCollatzConjecture purportedProof = loop

The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter).

For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well.

One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ):

    data Delayed : Type where
      Now   : Natural -> Delayed
      Later : Delayed -> Delayed

    collatzLoop : Natural -> Delayed
    collatzLoop Zero            = Later (collatzLoop (collatzStep Zero))  -- For completeness
    collatzLoop (Succ Zero)     = Now (Succ Zero)  -- Halt
    collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n))))

This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get:

    collatzLoop 6
    Later (collatzLoop 3)
    Later (Later (collatzLoop 10))
    Later (Later (Later (collatzLoop 5)))
    Later (Later (Later (Later (collatzLoop 16))))
    Later (Later (Later (Later (Later (collatzLoop 8)))))
    Later (Later (Later (Later (Later (Later (collatzLoop 4))))))
    Later (Later (Later (Later (Later (Later (Later (collatzLoop 2)))))))
    Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1))))))))
    Later (Later (Later (Later (Later (Later (Later (Later (Now 1))))))))

We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`):

    unwrap : Natural -> Delayed -> Delayed
    wrap Zero     x         = x
    wrap (Succ n) (Now   y) = Now y
    wrap (Succ n) (Later y) = unwrap n y

    data DelayEqual : Delayed -> Delayed -> Type where
      delayedReflexivity : (d : Delayed) -> DelayEqual d d

    -- The notation `(x : y *** z)` is a dependent pair, where the first element has
    -- type `y` and the second element has type `z` which may refer to the first
    -- value as `x`
    CollatzConjecture : Type
    CollatzConjecture = (boundFinder : Natural -> Natural ***
                         (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

    proofOfCollatzConjecture : CollatzConjecture
    proofOfCollatzConjecture = ?

    disproofOfCollatzConjecture : CollatzConjecture -> Empty
    disproofOfCollatzConjecture (boundFinder, purportedProof) = ?

With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type:

    (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

This says that given any `n : Natural`, we can return a proof that:

    DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`.

To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!).

The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)

Metamagical Thomas