Do agda programs neccisarily terminate?
It has been stated a few places that all agda programs terminate. However
I can construct a function like this:
stall : Í n ¨ ℕ
stall 0 = 0
stall x = stall x
The syntax highlighter doesn't seem to like it, but there are no
compilation errors.
Computing the normal form of stall 0 results in 0. Computing the result of
stall 1 causes Emacs to hang in what looks a lot like a non-terminating
loop.
Is this a bug? Or can Agda sometimes run forever? Or is something more
subtle going on?
No comments:
Post a Comment