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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
