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

```