[Haskell-cafe] Help with Bird problem 3.3.3
Ryan Ingram
ryani.spam at gmail.com
Tue Feb 24 21:28:13 EST 2009
Try starting with
(m * n) / m = n -- given m /= 0
Then do case analysis on n.
I found this process quite enlightening, thanks for posting.
-- ryan
2009/2/24 Peter Hilal <peter at hilalcapital.com>:
> I'm working my way through Bird's _Introduction to Functional Programming
> Using Haskell_. I'd appreciate any help with problem 3.3.3, which is:
> "Division of natural numbers can be specified by the condition (n * m) / n =
> m for all positive n and all m. Construct a program for division and prove
> that it meets the specification."
> The required construction relies on the following definitions:
>
> data Nat = Zero| Succ Nat
> (+) :: Nat -> Nat
> m + Zero = m
> m + Succ n = Succ (m + n)
> (*) :: Nat -> Nat
> m * Zero = Zero
> m * Succ n = m * n + m
> Proceeding as Bird does in Sec. 3.2.2, where he derives the definition of
> "-" from the specification "(m + n) - n = m", I've so far gotten the first
> case, in which m matches the pattern "Zero", simply by (i) substituting Zero
> for m in the specification, (ii) substituting Succ n for n in the
> specification (solely because n is constrained to be positive), and (iii)
> reducing by applying the first equation of "*":
> Case Zero:
>
> (Succ n * Zero) / Succ n = Zero
> ≡ {first equation of "*"}
> Zero / Succ n = Zero
> Easy enough, and completely intuitive, since we expect Zero divided by any
> non-Zero finite number to be Zero. The next case, in which m matches the
> pattern "Succ m", is where I get stuck, and I really have no intuition about
> what the definition is supposed to be. My first step is to substitute "Succ
> m" for "m" in the given specification, and to substitute Succ n for n in the
> specification (for the same reason, as above, that n is constrained to be
> positive), and then to use the definition of "*" to reduce the equation:
> Case Succ m:
> Succ n * Succ m / Succ n = Succ m
> ≡ {second equation of "*"}
> (Succ n * m + Succ n) / Succ n = Succ m
> Where do I go from here? Thank you so much.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
More information about the Haskell-Cafe
mailing list