Email Gateway (Aug 18 2022 at 10:04): Email Gateway (Aug 18 2022 at 10:04):From: Yevgeniy Makarov <emakarov@gmail.com>
Hello,
I am wondering how easy it is to change the representation of numbers
in Isabelle. If I understand correctly, currently natural numbers are
represented as a datatype that has zero and successor, integers are
represented as equivalence classes of pairs of natural numbers, and
rationals are equivalence classes of fractions. Moreover, when
Isabelle specifications are translated into ML, natural numbers are
again represented as a datatype, and integers are converted into the
type int of ML. As was pointed out in couple of days ago in this list,
rational numbers in the development snapshot may be represented as
triples (sign, enumerator, denominator). There is also a module that
maps natural numbers to ML's int. Of course, providing ML types as
counterparts for Isabelle ones raises efficiency and clarity of
programs; however, one has to trust that facts about types proved in
Isabelle hold for the implementation.
Changing number representation is important for code generation. For
example, one may want to produce a program that works with natural
numbers in binary representation or a representation based on an array
of digits instead of a datatype. Of course, it is desirable that the
number of properties proved manually for the new representation is
minimal.
Isabelle library contains definitions and properties for semirings,
rings, and fields, and many lemmas are proved for those abstract
structures. However, there are dozens of statements proved
specifically for natural numbers as a datatype, such as statements
about the successor, order, and truncated subtraction. Some lemmas are
also proved specifically for integers, e.g., facts that the order on
int is not dense and properties of absolute value.
Isabelle also has internal binary representation of integers given by
numerals as well as simplification rules for operations on such
integers, but this seems unrelated to number representation in
Isabelle and extracted programs.
I'd like to ask the following questions:
(1) Was there any attempt to characterize different classes of numbers
(naturals, integers, rationals) purely axiomatically in order to
minimize the number of facts one has to prove for a new
representation?
(2) What is the best way in Isabelle to change the representation of
naturals or integers? I am not just talking about types_code
directive, which maps an Isabelle type into an unrelated ML type, but
a representation whose properties (like commutativity of addition) can
be proved in Isabelle.
Thank you,
Yevgeniy
Email Gateway (Aug 18 2022 at 10:04):From: Tobias Nipkow <nipkow@in.tum.de>
If you want to use a different representation in the logic but retain
all the theorems that you have for the old representation, you
essentially have to reprove them. The only way to automate this to a
large degree is by factoring out a common axiomatic basis. Then you can
use Isabelle's proof terms to reply the old proof but plugging in the
new basis. The AWE project may provide the necessary automation:
http://www.informatik.uni-bremen.de/~cxl/awe/
If you are "only" interested in code generation, you could use
types_code in a disciplined manner: if you want to implement t by t',
you describe t' and its operations in HOL and show (roughly speaking)
that there is a homomorphism from t' to t. This is not completely
foundational because you could make a mistake when writing down the
necessary homomorphism conditions.
Tobias
Email Gateway (Aug 18 2022 at 10:04):From: Lawrence Paulson <lp15@cam.ac.uk>
On 15 Jan 2007, at 12:07, Yevgeniy Makarov wrote:
(1) Was there any attempt to characterize different classes of numbers
(naturals, integers, rationals) purely axiomatically in order to
minimize the number of facts one has to prove for a new
representation?
My paper "Organizing Numerical Theories Using Axiomatic Type Classes"
may be relevant: http://www.cl.cam.ac.uk/~lp15/papers/Reports/
TypeClasses.pdf
(2) What is the best way in Isabelle to change the representation of
naturals or integers? I am not just talking about types_code
directive, which maps an Isabelle type into an unrelated ML type, but
a representation whose properties (like commutativity of addition) can
be proved in Isabelle.
Can't you just prove that the old and new representations are
isomorphic? Properties should then be easy to transfer from the old
representation to the new one.
Larry Paulson
Email Gateway (Aug 18 2022 at 10:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
(1) Was there any attempt to characterize different classes of numbers
(naturals, integers, rationals) purely axiomatically in order to
minimize the number of facts one has to prove for a new
representation?
Indeed, HOL contains a rich theory of abstract algebra: see theories
Orderings.thy, Lattices.thy, OrderedGroup.thy and Ring_and_Field.thy.
However, internal representation of numerals is implemented completely
independent from that.
(2) What is the best way in Isabelle to change the representation of
naturals or integers? I am not just talking about types_code
directive, which maps an Isabelle type into an unrelated ML type, but
a representation whose properties (like commutativity of addition) can
be proved in Isabelle.
Concerning code generation, the default HOL setup for code generator
framework leaves nats as datatypes and maps ints to machine ints.
Technically, it is hard to change without patching the HOL/Main theories
themselves. In any case, you will have to reprove theorems on
fundamental operations in order to get it really working. Though this
demands some effort, there are no fundamental issues to prevent somebody
from doing this. Can you provide me with a little more context, i.e.
which particular representation you want to use for with numeric
datatype for what particular reason etc.?
Cheers,
Florian
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 04:19 UTC