[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Dan Weston
westondan at imageworks.com
Thu Oct 18 16:59:49 EDT 2007
> The function needs to be total. You seem to be using Haskell to execute
> a function to see if it terminates as a proof of totality. Is that
> fair? This approach might work for some simple examples, but if the
> function doesn't terminate immediately then what? I would assume that
> proof of
> totality would be an obligation of the person who constructed the
> function.
>> thm2 :: (Prop a -> Prop a) -> Prop a
>> thm2 f = Prop undefined
Prop is not total, but thm2 is (if I am not mistaken) total. Every
non-_|_ f results in a non-bottom result (namely, Prop _|_).
My (still hesitant) assertion is that the totality must be transitive to
all sub-expressions for the function to be considered a valid proof. The
easiest way to get Haskell to do this work for you is to make everything
strict and just evaluate the function.
Tim Newsham wrote:
> I'm fairly new to this and struggling to follow along so I might
> be a little off base here...
>
>> I assume you mean then that it is a valid proof because it halts for
>> *some* argument? Suppose I have:
>>
>> thm1 :: (a -> a) -> a
>> thm1 f = let x = f x in x
>>
>> There is no f for which (thm1 f) halts (for the simple reason that _|_
>> is the only value in every type), so thm1 is not a valid theorem.
>>
>> Now we reify our propositions (as the tutorial does) in a constructor:
>>
>> data Prop a = Prop a
>>
>> thm2 :: (Prop a -> Prop a) -> Prop a
>> thm2 f = Prop undefined
>>
>> fix :: (p -> p) -> p
>> fix f = let x = f x in x
>>
>> instance Show (Prop a) where
>> show f = "(Prop <something>)"
>>
>> *Prop> :t thm2
>> thm2 :: (Prop a -> Prop a) -> Prop a
>>
>> *Prop> thm2 (fix id)
>> (Prop <something>)
>>
>> Wow! thm2 halts. Valid proof. We have a "proof" (thm2 (fix id)) of a
>> "theorem" (((Prop a) -> (Prop a)) -> (Prop a)), assuming that can
>> somehow be mapped isomorphically to ((a -> a) -> a), thence to
>> intuitionist logic as ((a => a) => a).
>
> The function needs to be total. You seem to be using Haskell to execute
> a function to see if it terminates as a proof of totality. Is that
> fair? This approach might work for some simple examples, but if the
> function doesn't terminate immediately then what? I would assume that
> proof of
> totality would be an obligation of the person who constructed the
> function. Using Haskell to prove termination for some simple cases might
> be fair (in which case I see your point about avoiding a non-lazy
> constructor), but it doesn't seem to be very general anyway. If you're
> relying on the programmer to provide proof of totality, then I don't
> see the harm in using "Prop a" instead of "a".
>
>> That "somehow" in the tutorial seems to be an implied isomorphism from
>> Prop a to a, so that proofs about (Prop a) can be interpreted as
>> proofs about a. I hope to have shown that unless without constructors
>> strict in their arguments that this is not valid.
>>
>> My hypothesis was that
>>
>> data Prop a = Prop !a
>>
>> justified this isomorphism. Or am I still just not getting it?
>
> That would allow you to use the dynamic property (I observed termination)
> to verify the static property (the function is total) in some situations,
> right? But the static property of totality shouldn't rely on evaluation
> strategy, right?
>
>> Dan
>
> Tim Newsham
> http://www.thenewsh.com/~newsham/
>
>
More information about the Haskell-Cafe
mailing list