On Wed, Oct 17, 2007 at 06:49:24PM -0700, Dan Weston wrote: > It would seem that this induction on SN requires strictness at every stage. > Or am I missing something?
Yes you are missing something. Whether it exists in my message is less certain. First, note that the elements of SN[a] are lambda-terms, like (\x -> x) (\x -> x). Second, strong normalization means that *every* reduction sequence terminates. E.g. that term is strongly normalizing, since the only possible reduction leads to \x -> x, from which no further reductions apply. Third, by inhabit...when passed, I mean that if TERM1 inhabits SN[a -> b], and TERM2 inhabits SN[a], then (TERM1) (TERM2) inhabits SN[b]. No mention of evaluation required. Is it clear now? Stefan > Stefan O'Rear wrote: >> 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