[Haskellcafe] Tutorial: CurryHoward 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
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 nontext attachment was scrubbed...
Name: not available
Type: application/pgpsignature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskellcafe/attachments/20071017/da268e54/attachment.bin
More information about the HaskellCafe
mailing list