It seems like we could refine the first parameter of carryPropagate
just as the second: make an= type N1 that only admits values [1..].
Would not that suffice to prove that base is never 0 and not have to
go beyond the type-checker for a proof?
On 3/13/07, Neil Mitchell
Hi
Note: Total = total ignoring non-termination, for this post
Surely we can assume them total given that base is never zero?
They are not total, they are called in a manner which does not cause them to raise an error. If you want every function to be total, you need to fix div.
If you are happy with individual functions being partial, provided the program as a whole is total, that's fine (and I'd agree with you!). However, in this case you need to either prove that the program won't crash, or stop calling it total. This corresponds to proving that base is never zero.
Of course, if you're going to just accept a proof that base is never zero, why not just accept a proof that head/tail are called on an infinite list? It says you defining codata, and your own versions of head/tail/drop etc
I have a machine checkable (and machine generated) proof that base is never zero, and the list is infinite.
Thanks
Neil _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe