[Haskell-cafe] Signature for non-empty filter

[Dan Licata]

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
> 
>