[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

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