[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

It would seem that this induction on SN requires strictness at every 
stage. Or am I missing something?

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