[Haskell-cafe] Tutorial: Curry-Howard Correspondence

Stefan O'Rear stefanor at cox.net
Wed Oct 17 21:33:32 EDT 2007

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


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.

-------------- 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

More information about the Haskell-Cafe mailing list