Thank you for that clarification, and I hope you will have patience for a follow-up question. I am really eager to fully understand this correspondence and appreciate any help. Your strong normalization induction does deconstruct function application but seemingly not constructor application, which I guess halts in System F at weak head normalization, so a theorem (Prop p) does not prove a theorem p. You said that:
foo is a valid proof of a true theorem, but does not halt for the defined argument 'fix'.
I assume you mean then that it is a valid proof because it halts for *some* argument? Suppose I have: thm1 :: (a -> a) -> a thm1 f = let x = f x in x There is no f for which (thm1 f) halts (for the simple reason that _|_ is the only value in every type), so thm1 is not a valid theorem. Now we reify our propositions (as the tutorial does) in a constructor: data Prop a = Prop a thm2 :: (Prop a -> Prop a) -> Prop a thm2 f = Prop undefined fix :: (p -> p) -> p fix f = let x = f x in x instance Show (Prop a) where show f = "(Prop <something>)" *Prop> :t thm2 thm2 :: (Prop a -> Prop a) -> Prop a *Prop> thm2 (fix id) (Prop <something>) Wow! thm2 halts. Valid proof. We have a "proof" (thm2 (fix id)) of a "theorem" (((Prop a) -> (Prop a)) -> (Prop a)), assuming that can somehow be mapped isomorphically to ((a -> a) -> a), thence to intuitionist logic as ((a => a) => a). That "somehow" in the tutorial seems to be an implied isomorphism from Prop a to a, so that proofs about (Prop a) can be interpreted as proofs about a. I hope to have shown that unless without constructors strict in their arguments that this is not valid. My hypothesis was that data Prop a = Prop !a justified this isomorphism. Or am I still just not getting it? Dan Stefan O'Rear wrote:
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:
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'.
On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote: - 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