On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: > 2) the function must halt for all defined arguments > > fix :: forall p . (p -> p) -> p > fix f = let x = f x in x
consider: foo :: ((a -> a) -> a) -> a foo x = x id foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'. - An effective approach for handling this was found long ago in the context of prooving the strong normalization of the simply typed lambda calculus. Define a category of terms SN[a] for each type a by recursion on a. SN[a], for atomic a, consists of terms that halt. SN[a -> b] consists of functions that inhabit SN[b] when passed an argument in SN[a]. With that definition, prooving that every term of the STLC of type a inhabits SN[a], and thus halts, becomess a trivial induction on the syntax of terms. Stefan
signature.asc
Description: Digital signature
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
