[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Stefan O'Rear]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20071017/a91b396d/attachment.bin