Email Gateway (Aug 18 2022 at 13:08): Email Gateway (Aug 18 2022 at 13:08):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,
I noticed the definition to minus today (Isabelle2008):
primrec minus_nat
where
diff_0: "m - 0 = (m::nat)"
| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
I was expecting it to be:
primrec
diff_0: "0 - m = 0"
| diff_Suc: "(Suc m) - n = (case n of 0 => (Suc m) | Suc k => m - k)"
which I think would produce better code and seems more "natural" to
me... so I thought I was probably missing some subtlety... I'd be
interested in any reasons for the Isabelle definition.
thanks,
lucas
Email Gateway (Aug 18 2022 at 13:08):From: Lawrence Paulson <lp15@cam.ac.uk>
We use the traditional definition, which embodies the principle that
subtraction consists of repeated application of the predecessor
function. Yours does have advantages, however. For example, it is tail
recursive. When this work was done, code generation was not even
envisaged.
Larry
Email Gateway (Aug 18 2022 at 13:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
it is important to note that specifications are mainly for *definitional
construction* of things; rules for generic tools (simplifier, code
generator) can be proven arbitrarily, which happens in this case abundantly.
Florian
signature.asc
Last updated: May 03 2024 at 04:19 UTC