Email Gateway (Oct 02 2022 at 14:43): Email Gateway (Oct 02 2022 at 14:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Also an opinion: sdiv and smod being one of the basic operations on
words, I do not consider them particularly 'exotic'.
This is a good opportunity to ask a question about signed division on
words »as it is by now«.
Currently, the characteristic equation is:
‹v {sdiv} w = word_of_int (sint v {sdiv} sint w)›
The sint conversion is of course inherent to »signed« interpretation of
words.
The »signed« integer division on the RHS is characterized as:
‹k {sdiv} l = sgn k * sgn l * (¦k¦ {div} ¦l¦)›
I. e. the pre-existing divison on natural numbers (interpreted as
non-negative integers) is extended to algebraically by factoring out the
signs, and ‹1 div sgn l = sgn l› yields the product we see above.
Is this based on existing literature or folklore or just an historic
artefact, maybe originally induced by the tempting syntactic coincidence
of sdiv on int and word?
Why this doubt? My naive idea of »signed« division on words would
follow other »signed« operations, which interpret word representants
centered around 0 rather than starting with 0. Particulary, I would
expect sth. like
‹signed_take_bit n w = w smod (2 ^ Suc n)› (**)
to hold, which is definitely not that case with current definition, but
which would hold (*) e. g. when using
‹v {sdiv} w = word_of_int (sint v {rdiv} sint w)›
as characteristic equation (c.f. HOL-Library.Rounded_Division).
(Admittedly there is no explicit proof for (*) so far, but it easy to
agree that there is a definition of smod on words from which (**) would
follow)
Any suggestions on this?
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Oct 03 2022 at 08:06):From: Peter Lammich <lammich@in.tum.de>
Hi Florian,
I'm not sure if I understand your wording, but for me it looks like sdiv
is rounding towards zero, while div rounds down.
Division implementations in computers is usually round towards zero.
Including rounded division, we now have 3 names around: div, rdiv, sdiv.
Looks like one too many for me.
Also, I don't know if there are standard naming conventions. In Haskell,
the operations are named quot/rem and div/mod.
https://hackage.haskell.org/package/base-4.17.0.0/docs/Prelude.html#v:quot
Except from rounding down vs. towards zero, are there any other concepts
that we need to map here?
Email Gateway (Oct 03 2022 at 09:01):From: Gerwin Klein <kleing@unsw.edu.au>
The machine word operations were are usually modelled after whatever C does, which tends to be modelled after what the main popular asm instruction sets used to do a few decades ago.
So I suspect this is where the current sdiv/smod behaviour comes from.
Cheers,
Gerwin
Email Gateway (Oct 03 2022 at 11:38):From: Joe Wells <cl-isabelle-users@lists.cam.ac.uk>
the standard reference for pairs of division and modulus operations that
i always give people is:
daan leijen.
division and modulus for computer scientists.
2001.
web search says right now it can be found here:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf
is there something better now?
best wishes,
joe
Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:
1. Heriot-Watt University, a Scottish charity registered under number SC000278
2. Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.
The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.
Email Gateway (Oct 06 2022 at 12:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
thanks for the references and comments.
After a look at it, the situation »as it is« appears to me as follows:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf
(*) defines different kinds of integer division with remainder.
The »common« div/mod operation in HOL on int in terms of (*) is
F-division (rounded towards minus infinity) and is advocated by Knuth.
The sdiv/smod operation in HOL on int in terms of (*) is T-division
(rounded towards zero) or (in my own terminology) the natural algebraic
extension of division on nat to division on int. It is required to
define sdiv/smod on words which by convention follows ISO C99, which in
turn adopted the typical behavior of hardware modern in the beginning of
the 1990ies.
The rdiv/rmod operation is required to define div/mod on Gaussian
numbers (the material is still about to emerge). It is different from
any approach given in (*) since it centers the modulus towards zero, e.
g. _ mod 5 yields {-2, -1, 0, 1, 2}. Lifting that definition to
arbitrary types with bit structure would satisfy
‹signed_take_bit n a = a rmod (2 ^ Suc n)›
analogously to
‹take_bit n a = a mod 2 ^ n›,
(This is just an observation, not a proposal to introduce that
generalization.)
This is to record that…
for any existing variant of div/mod on int, there is a motivation or
application;
the definition of sdiv/smod on words resembles an established
(although somehow accidental) convention;
how our division operations relate to definitions found in literature.
I plan to augment the distribution with references to (*) to clarify the
situation.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Oct 06 2022 at 12:28):From: Peter Lammich <lammich@in.tum.de>
Hi Florian,
thanks for the clarification.
I will now add regression tests into my developments, just in case
someone should change the current meanings of sdiv/smod in the future:
This might silently break trusted code bases of PL semantics formalizations.
Email Gateway (Oct 08 2022 at 12:44):From: Joe Wells <cl-isabelle-users@lists.cam.ac.uk>
hi florian,
if your goal is to put the various div/mod definitions in context, you might (or might not) want to look at these references:
* a list of many variations (including some not already mentioned) that are used by various languages, standards, machines: What A Stray Mind Coughed Up: A survey of 'divmod'<https://straymindcough.blogspot.com/2012/02/survey-of-divmod.html>
* an attempt (possibly successful, i have not carefully inspected it) to generalize over all div/mod definitions: divmod.pdf<http://www.math.bas.bg/bantchev/articles/divmod.pdf>
* modulus of intervals (instead of single numbers) which generalizes over many of these ideas: [PDF] Modulo intervals: a proposed notation | Semantic Scholar<https://www.semanticscholar.org/paper/Modulo-intervals%3A-a-proposed-notation-Dershowitz-Reingold/ab9794bb2ec68576d4e2f3830ba35de5fe08e747>; Modulo.pdf<http://www.cs.tau.ac.il/~nachumd/papers/Modulo.pdf>
* a predecessor of the paper i mentioned in previous email with more details: The Euclidean definition of the functions div and mod - 452146.pdf<https://biblio.ugent.be/publication/314490/file/452146.pdf>
i do not know if the rdiv/rmod you mention is an instance of any of the above.
are you saying that the "euclidean division" in isabelle/hol is not an instance of leijen/boute's euclidean division, and also that leijen/boute's euclidean division is not an instance of "euclidean division" in isabelle/hol?
with my best wishes,
joe
Email Gateway (Oct 08 2022 at 13:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joe,
Am 08.10.22 um 14:43 schrieb Joe Wells:
hi florian,
if your goal is to put the various div/mod definitions in context, you
might (or might not) want to look at these references:
[...]
thanks for the references, I will have a look at it occassionally.
are you saying that the "euclidean division" in isabelle/hol is not an
instance of leijen/boute's euclidean division, and also that
leijen/boute's euclidean division is not an instance of "euclidean
division" in isabelle/hol?
To clarify, AFAIU leijen/boute speak about division on integers.
Whereas the type class »euclidean_semiring« in Isabelle/HOL can be
instantiated
to a variety of different types including naturals, integers,
polynomials over fields
and gaussian numbers, using an abstract euclidean norm to constrain the
modulus, which
is the primary motivation for its name.
The concrete existing traditional instantiation of this type class for
integers
implements F-division, although I guess in theory there would be enough
freedom
to choose another variant, including leijen/boute's euclidean division.
Hope this helps,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Oct 11 2022 at 17:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joe,
I managed to have a look at those references:
They augment the picture but do IMHO not fundamentally change it.
While reading, the following insights came to my mind:
A variant of what I have called »rounded division« (rdiv) is mentioned
in (*) p. 131 as »f = round« –
instead rounding .5 towards plus infinity, it rounds .5 towards the even
neighbor. Not clear whether this
is just an aspect of »fairness« or has algebraic implications.
Wikipedia calls (rdiv) »centered division«,
without explicit reference. Not sure whether this justifies a renaming
from (rdiv) to (cdiv).
The proper »euclidean« division with 0 <= k mod l < abs l has the nice
property that the modulus is equivalent
modulo algebraic units, abstractly (**): a mod (b * c) = a mod b if c is
an algebraic unit.
* For nat, this is trivial since 1 is the only algebraic unit.
* For poly it holds, although there is no explicit theorem yet in the
distribution.
* For gauss quickcheck finds counter examples; it is not clear to me
whether the now-existing definition (in post-Isabelle2022 (!)) can be
tweaked to avoid this.
* For int which is defined as F-division, it does obviously not hold.
Why is (**) a desirable property? If we compute whole equivalence
classes, both _ mod b and _ mod (b * c)
yield the same equivalence class if c is an algebraic unit. Hence it is
strange to postulate that the
operations a mod b and a mod (b * c) would yield different representants.
So far for this evening,
cheers,
Florian
Last updated: Jan 04 2025 at 20:18 UTC