[Haskell-cafe] Tutorial: Curry-Howard Correspondence
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
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
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