Let's be careful here: decidability is only relevant if you want to *automatically* prove calls to filter correct. It is certainly possible to give a type system/specification logic for reasoning about all functions written in a Turing-complete language (e.g., all Haskell functions). In such a type system/logic, you will be able to prove that particular functions have particular results (e.g., "that function f over there maps 4 to true"). If you give filter the type/specification that Henning wants, you may not be able to get a computer to automatically validate all "correct" calls to filter, where "correct" means that I can prove, in the specification logic, that the predicate is satisfiable. However, you can get a computer to validate some calls to filter, and a human may be able to validate others by hand.
I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the "only if" below. -Dan On Feb06, Bulat Ziganshin wrote: > Hello Henning, > > Wednesday, February 6, 2008, 6:09:28 PM, you wrote: > > >> it's another question: you can describe trivial values using type > >> system, but can't prohibit them using it - it's impossible because you > >> can't check for arbitrary algorithm whether it will be finally stopped > > > I could consider the function buggy, if it does not terminate on the given > > example. > > it's impossible to check for *arbitrary* function call whether it will be > terminated. seems that you don't have formal CS education? :) > > so one can develop set of functions that are guaranteed to be > terminated or guaranteed to be non-trivial. but it's impossible to > check for arbitrary function whether it's trivial and even whether it > will terminate for particular data > > this means that answer to original question - one can ensure that > argument for filter is non-terminating function only if these > functions are written using some special notation which doesn't allow > to write arbitrary turing-complete algorithms > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe