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:
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
