> 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/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
