Maybe and partial functions
Neil Mitchell wrote:
I suggest you try rewriting this program to be complete:
http://darcs.haskell.org/nofib/imaginary/digits-of-e2/Main.lhs
(if you do, please post the result to the list)
As Gen Zhang noted, the problem seems to be quite straightforward: just express in types the fact that we deal with infinite streams and so Nil just cannot happen. One way of doing this as follows. Showing totality (that is, termination of recursion in carry propagate) is harder. But re-writing the program so to avoid head/tail on the empty list is easy: module E where import Prelude hiding (head, tail, map, iterate, take) data I a = C a (I a) deriving Show -- these are total functions: they give WHNF in one step provided non-bottom -- arguments head (C a _) = a tail (C _ l) = l map f (C a l) = C (f a) (map f l) rept a = C a (rept a) take n (C a l) | n > 0 = a:take (n-1) l take _ _ = [] iterate f z = C z (iterate f (f z)) -- There are no pattern-matching failures here. -- The totality is harder to see: all digits are roughly of the same range, -- but each recursive call increments base. Eventually, base becomes bigger -- than d+9 and so the first alternative will be selected, which is in the -- WHNF and so recursion terminates. carryPropagate base (C d ds) | carryguess == (d+9) `div` base = C carryguess (C (remainder+nextcarry) fraction) | otherwise = (C (dCorrected `div` base) (C (dCorrected `mod` base) fraction)) where carryguess = d `div` base remainder = d `mod` base C nextcarry fraction = carryPropagate (base+1) ds dCorrected = d + nextcarry e = map (show.head) $ iterate (carryPropagate 2 . map (10*) . tail) $ C 2 (rept 1) en n = "2." ++ concat (take n (tail e))
Hi
-- There are no pattern-matching failures here. -- The totality is harder to see: all digits are roughly of the same range, -- but each recursive call increments base. Eventually, base becomes bigger -- than d+9 and so the first alternative will be selected, which is in the -- WHNF and so recursion terminates. carryPropagate base (C d ds) | carryguess == (d+9) `div` base = C carryguess (C (remainder+nextcarry) fraction) | otherwise = (C (dCorrected `div` base) (C (dCorrected `mod` base) fraction)) where carryguess = d `div` base remainder = d `mod` base C nextcarry fraction = carryPropagate (base+1) ds dCorrected = d + nextcarry
e = map (show.head) $ iterate (carryPropagate 2 . map (10*) . tail) $ C 2 (rept 1)
en n = "2." ++ concat (take n (tail e))
You still have div and mod, which are partial functions. Thanks Neil
On Tue, 13 Mar 2007 10:17:05 +0000
"Neil Mitchell"
Hi
-- There are no pattern-matching failures here. -- The totality is harder to see: all digits are roughly of the same range, -- but each recursive call increments base. Eventually, base becomes bigger -- than d+9 and so the first alternative will be selected, which is in the -- WHNF and so recursion terminates. carryPropagate base (C d ds) | carryguess == (d+9) `div` base = C carryguess (C (remainder+nextcarry) fraction) | otherwise = (C (dCorrected `div` base) (C (dCorrected `mod` base) fraction)) where carryguess = d `div` base remainder = d `mod` base C nextcarry fraction = carryPropagate (base+1) ds dCorrected = d + nextcarry
e = map (show.head) $ iterate (carryPropagate 2 . map (10*) . tail) $ C 2 (rept 1)
en n = "2." ++ concat (take n (tail e))
You still have div and mod, which are partial functions.
Surely we can assume them total given that base is never zero? Gen
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
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
Hi Nicolas,
It seems like we could refine the first parameter of carryPropagate just as the second: make an= type N1 that only admits values [1..].
How? newtype N1 = N1 Int (put that in a module and don't export N1) define the constant 2, define the increment operator, change div and mod. Now we've mainly got a proof in the type checker, but we still don't actually have a proof for our core N1 definition - but I think that is probably ok, provided it is a common core which can be reused and is minimal.
Would not that suffice to prove that base is never 0 and not have to go beyond the type-checker for a proof?
We've now encoded some properties in the type checker, changed most of the code, and still don't actually have a complete proof. Maybe the type checker isn't a proof tool ;) Thanks Neil
participants (4)
-
Gen Zhang -
Neil Mitchell -
Nicolas Frisby -
oleg＠pobox.com