Hi Bulat, Once again, let's be careful about what "check arbitrary functions for termination/non-trivialness" means. If you mean, "decide via an algorithm whether a function is terminating on all inputs", then yes, you need to restrict the class of functions. If you mean "prove in some logic that a function is terminating on all inputs", then there is no reason to restrict the class of functions. (Think of it this way: the truth of propositions in that logic may not be decidable, so the existence of a proof of termination in that logic does not imply an algorithm for deciding termination.)
ACL2 and Twelf are practical systems built around this second kind of reasoning. In these systems, you write down partial functions (in a functional notation in ACL2, in a logic programming notation in Twelf) and then prove that they are terminating, and therefore total. Both systems permit the definition of all computable functions on the natural numbers (worst comes to worst, you can write an interpreter for the untyped lambda-calculus). So in neither system is it *decidable* whether a function is terminating. However, both provide helpful tools for proving that individual functions are terminating, and in both systems you can help these tools along yourself when the automated reasoning doesn't do the job. Many dependently typed programming languages have this flavor, in that you can prove propositions that are not decidable. Propositions are represented by types, and proofs by programs, so the truth of a proposition comes down to the existence of a term of a particular type. There is no reason that type inhabitation (and therefore all propositions) needs to be decidable. So it is perfeclty possible to have a dependent type system where you give filter the type "for all satisfiable f" where f ranges over all computable functions of the appropriate type, even though this proposition is not decidable. -Dan On Feb07, Bulat Ziganshin wrote: > Hello Henning, > > Thursday, February 7, 2008, 4:27:30 PM, you wrote: > > >> ok, read this as "computer can ensure...", because it was exactly the > >> original question - "can computer check that any given function in > >> turing-complete language is non-trivial?" > > > My original question according to > > > > http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html > > was "Is Haskell's type system including extensions strong enough for > > describing a function, that does not always return a trivial value?" > > where Haskell is *turing-complete* *computer* language > > this allows to answer to your question that you need to use special, > non-turing language if you want to check arbitrary functions for > non-trivialness. one example of such language: > > data Func = ConstTrue | ConstFalse > > and dependent-typed languages provides you (afaiu) much richer > facilities to describe functions for which you still may prove > something useful > > so, if you term "function" includes the Func type, the answer is > "yes", but if you mean usual haskell functions, the answer is no > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe