HaltingProblem in Agda?

3
votes

I am working through a paper trying to implement their Haskell code in Agda. They want to formulate the halting problem by saying let bot be a program such that for any data type a:

bot :: a
bot = bot

They go on to define 

data S = T

so the Halting problem is said as:

The function diverges : S → S defined by

diverges(T)= bot
diverges(bot)= T

is not computable and hence is not definable in our language

I tried implementing this in Agda as:

data S : Set where
  ⊤ : S

⊥ : _
⊥ = ⊥

diverges : S → S
diverges ⊤ = ⊥
diverges ⊥ = ⊤

and when I tried to load it, Agda said diverges ⊥ = ⊤ is an unreachable clause. Is this the error I am supposed to get or did I just implement the Haskell code incorrectly?

1
haskellprogramming-languagesagdahalting-problemcomputability
Okay good, that's where some of my confusion came from. Right now it is just underlining the diverges ⊥ part and saying unreachable clause. Any ideas on how to fix this? If it helps, the source I am looking at is: cs.bham.ac.uk/~mhe/papers/entcs87.pdf bottom of page 22 to page 25 (sections 2.4 and 2.5). – user2154420
Termination checking happens quite late in Agda's process of loading a file. The unreachable clause error will be noticed first. Just to clarify what's going on, the type S has one constructor, "top", so the first equation for diverges covers all possible inputs. In the second equation, the argument "bottom" is taken to mean a fresh pattern variable, shadowing the defined "bottom". But there's no situation where that equation can be invoked: if its argument gets stuck, then diverges gets stuck; if its argument gives a value, then that value is "top". The error message is correct. – pigworker
That makes sense. One last question: What exactly does ⊥ mean (if that question makes sense)? Is it like an infinite loop? Also what do you mean by "stuck"? Sorry for all the questions, I just really want to get this down. – user2154420
The "bottom" symbol is just an ordinary identifier. It means whatever you make it mean. In the code above, you seem to be attempting to "define" it to compute recursively for ever: Agda will not accept such a definition. Meanwhile, an expression "gets stuck" if its evaluation terminates without giving a top-level constructor. Open expressions (which involve free variables) can get stuck (for want of knowing the values of the variables), but expressions with no free variables should never get stuck. Pattern matching on something stuck will itself get stuck. Stuckness snowballs. – pigworker

1 Answers

-2
votes

Your project probably isn't going to work, because Agda is not a Turing-complete language. For one thing, it only allows total functions, so it can't model any computation that might not halt. This means it can't even model full computations on Turing machines, for example, since Turing machines can fail to stop. So it's very unlikely that all the programs in the paper can be implemented in Agda.

In fact, it's not even possible to code all total computations in Agda, by a simple diagonal argument. Imagine the following algorithm: "Examine a text file and determine whether it's legal Agda. If it's not, output the empty string; if it is, run that Agda program on that very same text file, and add a space to the end of the output." This is a well-defined algorithm; most of the complexity is in "determine whether it's legal Agda" and "run that Agda program", and programs that do these certainly exist. But no Agda program can implement it, because any candidate would give different output when run on its own source code. Any total language is subject to a similar argument.

Weird circular-with-a-twist arguments like this are at the core of understanding the Halting Problem, so the paper you're reading will probably contain many of them.

Incidentally, the function diverges is not definable in Haskell. Computable functions in Haskell must give more defined outputs for more defined inputs, and ⊤ is considered more defined than ⊥ (it's an actual value, as opposed to the symbol for "this is undefined").