[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Dan Weston
westondan at imageworks.com
Thu Oct 18 15:13:35 EDT 2007
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
More information about the Haskell-Cafe
mailing list