From: monnier@iro.umontreal.ca   
      
   > Tha halting problem is solvable for linearly bounded automata.   
      
   The halting problem is also trivially solvable for languages such as   
   Coq and Agda: in those languages, all functions terminate.  Of course,   
   they may take centuries to run to completion, so knowing that they   
   will eventually terminate may not be nearly as useful as one might   
   think.   
      
           Stefan   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)