[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Stefan O'Rear]

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/da268e54/attachment.bin