Email Gateway (Aug 22 2022 at 13:04): Email Gateway (Aug 22 2022 at 13:04):From: Makarius <makarius@sketis.net>
I have nothing against just one high-quality Rat module in Isabelle/ML,
one that takes all previous experience into account and uses the current
possibilities of Poly/ML and Isabelle/ML.
Looking briefly through the sources raises the following questions:
* Is MyRat based on the existing Rat, or an independent development?
* What is the relation of Integer.lcm/gcd, PolyML.IntInf.lcm/gcd versus
MyRat.gcd? Could it be all based on PolyML.IntInf.lcm/gcd (taking care
about the proper sign)? PolyML.IntInf.lcm/gcd might lead to much
better performance, because it uses GMP operations directly.
* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are
these actually correct?
How about a formally specified and verified implementation? It should be
mostly trivial with all the algebraic tools in Isabelle/HOL.
Some of the authors of the existing rat.ML should get involved.
Makarius
Email Gateway (Aug 22 2022 at 13:04):From: Makarius <makarius@sketis.net>
a theorem prover.
It would be great to see a fully verified CakeML compiler + runtime system
As a start, someone could put the old Isabelle/OpenTheory implementation
by Brian Huffman into shape.
Makarius
Email Gateway (Aug 22 2022 at 13:04):From: Makarius <makarius@sketis.net>
There are two syntax questions here:
* Overloaded +, -, *, / etc. as for the other SML Basis number
implementations. Poly/ML provides an internal operation for that,
which happens to be publicly available, at least during Isabelle/Pure
bootstrap.
* Notation for literals. We have already antiquotations in Isabelle/ML,
even short forms with control symbols and cartouches. This could be
probably stretched one step further to introduce the following syntax:
#DIGITS/DIGITS or #~DIGITS/DIGITS
As abbreviation for @{rational ...} with the usual meaning of
antiquotations. In particular, a "value" antiquotation produces
results as static values only once at compile-time.
Such advanced ML surface syntax requires a truely advanced implementation
behind it, beyond any doubts about correctness and performance.
Makarius
Email Gateway (Aug 22 2022 at 13:04):From: Manuel Eberl <eberlm@in.tum.de>
* Is MyRat based on the existing Rat, or an independent development?
It's independent; I only found out that there was one in Isabelle after
I'd written my own. I didn't think to look in "src/Tools".
* What is the relation of Integer.lcm/gcd, PolyML.IntInf.lcm/gcd versus
MyRat.gcd? Could it be all based on PolyML.IntInf.lcm/gcd (taking
care
about the proper sign)? PolyML.IntInf.lcm/gcd might lead to much
better performance, because it uses GMP operations directly.
Probably. I didn't know Poly/ML already had GMP bindings; in that case,
one could probably use GMP rationals directly, which might increase
performance further. This is probably something that we could suggest to
David Matthews.
* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are
these actually correct?
There is a ~ missing in MyRat.inv. That code should definitely receive a
thorough review before it goes anywhere. Rat.inv looks fine to me.
How about a formally specified and verified implementation? It should
be mostly trivial with all the algebraic tools in Isabelle/HOL.
Well, we have a rational number type in Isabelle/HOL with working code
equations. If I recall correctly, the performance was almost as good as
Haskell's (unverified) rational number implementation. (modulo using the
unverified gcd operation from GMP). However, I would imagine that the
exported could would be quite ugly.
Manuel
Email Gateway (Aug 22 2022 at 13:05):From: Manuel Eberl <eberlm@in.tum.de>
However, I would imagine that the exported could would be quite ugly.
*The exported /code/
Also, I just remembered another issue that should be taken care of: As
far as I'm aware, there is currently no way to convert HOL rational
numbers to Isabelle/ML rational numbers and the other way round. (like
what I do in MyRat)
Email Gateway (Aug 22 2022 at 13:05):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 2 Apr 2016, at 10:58 PM, Makarius <makarius@sketis.net> wrote:
On Sat, 2 Apr 2016, Lawrence Paulson wrote:
CakeML illustrates the advantages of a formal definition. It is a subset of standard ML with substantially the same semantics. Without a formal semantics, the very idea of a verified compiler is meaningless. Others have also noticed the benefits of using a formally defined language for coding
a theorem prover.It would be great to see a fully verified CakeML compiler + runtime system
+ proof checker, and Isabelle export to that for independent checking.As a start, someone could put the old Isabelle/OpenTheory implementation by Brian Huffman into shape.
We (Sydney team, including Ramana and Michael on the HOL4 side) are interested in working on that in the medium term, i.e. in a few months to a year or so.
If anyone else is interested as well, let us know, more than happy to collaborate on it!
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:05):From: Makarius <makarius@sketis.net>
I did not mean to use exported code, but just to make a demo theory with
all the definitions and maybe some simple proofs (e.g. in HOL/ex). The
idea is just to make certain intentions and invariants explicit, notably
the sign of certain parts.
A related question is about sign in lcm/gcd: in structure Integer,
PolyML.IntInf, and the HOL definitions. There is also a connection of
PolyML.IntInf operations with the code generator in AFP Gauss_Jordan and
Echelon_Form.
Makarius
Email Gateway (Aug 22 2022 at 13:05):From: Manuel Eberl <eberlm@in.tum.de>
That should be quite possible, and I expect the proofs to be very easy,
if not completely automatic.
Manuel
Email Gateway (Aug 22 2022 at 13:06):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I noticed that there is an ML implementation of rational numbers in the
Isabelle distribution (~~/src/Tools/rat.ML).
There are a few issues with this:
– for some reason, it does not use operator overloading for
addition/multiplication/equality/etc. on rational numbers, but
introduces a "+/", "*/" etc. syntax for it.
– pretty printing displays 1/3 and 1 as "Rat (1, 3)" and "Rat (1, 0)",
respectively instead of "1 / 3" and "1". One could argue that "Rat (1,
3)" is the better choice since that means one can copy-paste output
directly back as ML source again; however, it also makes output more
difficult to read, in my opinion. At the very least, there should be a
function that converts a rational number to such a string.
– there is no functionality for parsing rational numbers at all (at
least I couldn't find something like that)
I have already implemented all of these things in my own little version
of rational numbers (see attachment) and could merge any of them into
the distribution if there is a consensus that that should be done.
Any opinions?
Cheers,
Manuel
rat.ML
Email Gateway (Aug 22 2022 at 13:07):From: Makarius <makarius@sketis.net>
On Fri, 1 Apr 2016, Manuel Eberl wrote:
I noticed that there is an ML implementation of rational numbers in the
Isabelle distribution (~~/src/Tools/rat.ML).
I don't think this is relevant to isabelle-users. Rat is just one of many
auxiliary modules in the implementation. I will nonetheless continue here,
to avoid cross-mailing list confusion wrt. isabelle-dev.
There are a few issues with this:
– for some reason, it does not use operator overloading for
addition/multiplication/equality/etc. on rational numbers, but introduces a
"+/", "*/" etc. syntax for it.
This follows Standard ML. Adhoc overloading is not defined by the language
and works differently in each implementation.
Since SML/NJ has been discontinued after Isabelle2016 (see
http://sketis.net/2016/isabelle-no-longer-supports-smlnj) and old versions
of Poly/ML as well, we can in principle become more specific to a
particular Poly/ML version. This means that standard-ness is given up, and
the game becomes more like that of OCaml (or Scala, even Haskell/GHC). I
am myself still unsure if this is good or bad.
I have already implemented all of these things in my own little version
of rational numbers (see attachment) and could merge any of them into
the distribution if there is a consensus that that should be done.
There is no need for "consensus" for Isabelle development, but a need for
a critical mass of people (1-3) who understand a certain module or part of
the system.
The Mercurial history is the first place to look:
http://isabelle.in.tum.de/repos/isabelle/log/471b576aad25/src/Pure/General/rat.ML
http://isabelle.in.tum.de/repos/isabelle/log/1948d555a55a/src/Tools/rat.ML
It shows that Florian Haftmann has done the main work in putting and
keeping this in shape.
The history also shows exposes various "fixes" and other amendments. It is
important to check that there is no regression. In half-forgotten Isabelle
jargon, "new" means a failed attempt to do something old in a better way.
Just some formal notes on Isabelle/ML usage:
* Const names etc. should be always used with proper antiquotations;
lack of that is legacy (unmaintainable).
* Option.map is the only canonical operation from that structure,
everything else should be ignored.
Makarius
Email Gateway (Aug 22 2022 at 13:08):From: Christine Sherif Rizkallah <christine2711987@gmail.com>
Thanks for sharing Manuel. I'm sure I can benefit from the pretty printing.
Email Gateway (Aug 22 2022 at 13:10):From: Manuel Eberl <eberlm@in.tum.de>
I don't think this is relevant to isabelle-users. Rat is just one of
many auxiliary modules in the implementation.
I have one entry in the AFP already that uses rational numbers in ML,
and another AFP submission is in preparation. I think this is definitely
relevant to some Isabelle users (e.g. for automatically providing
witnesses for certain things; in my case, solutions to linear programs
and adequate interval splittings for Sturm's method).
This follows Standard ML. Adhoc overloading is not defined by the
language and works differently in each implementation. […] we can in
principle become more specific to a particular Poly/ML version. […]
I don't really have any opinion on this. Uniform notation for addition
etc. is nice to have, but I cannot say whether it is worth it. This is
one of the reasons why I wrote that email, to collect some more opinions
on the issue.
* Option.map is the only canonical operation from that structure,
everything else should be ignored.
All right, then what is the canonical way to do things like that? Nested
case statements? Those can get very ugly and unreadable very fast.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:11):From: Makarius <makarius@sketis.net>
There is nothing wrong with case expressions. Isabelle/ML is not as
point-free as Haskell.
See also the "implementation" manual about "Options":
Apart from @{ML Option.map} most other operations defined in structure
@{ML_structure Option} are alien to Isabelle/ML and never used. The
operations shown above are defined in @{file
"~~/src/Pure/General/basics.ML"}.
Here is a general note from the manual about the basis library from NJ:
The basis library proposal of SML97 needs to be treated with caution.
Many of its operations simply do not fit with important Isabelle/ML
conventions (like ``canonical argument order'', see
\secref{sec:canonical-argument-order}), others cause problems with the
parallel evaluation model of Isabelle/ML (such as @{ML TextIO.print} or
@{ML OS.Process.system}).
Makarius
Email Gateway (Aug 22 2022 at 13:12):From: Makarius <makarius@sketis.net>
It would be certainly nice to have +, -, *, / on type rat.
Looking at the Poly/ML sources, its internal addOverload operation has a
comment as follows:
(* This goes in RunCall since it's only for the basis library. *)
In Isabelle/bb29cc00c31f I have already removed that critical bootstrap
structure from the ML environment: it contains other things that may
disrupt the ML system in a bad way (similar to Obj.magic in OCaml).
So if the overloaded syntax should be used, it needs to be part of the
Isabelle/Pure bootstrap environment. In that case one could also invent
separate notation for rat literals and make that an integral part of
Isabelle/ML.
Isabelle/ML is an "embrace and extend" version of Standard ML -- what SML
could have been if it had not been hindered by SML/NJ. Nonetheless, adding
new things to Isabelle/ML requires some care.
Makarius
Email Gateway (Aug 22 2022 at 13:13):From: Lawrence Paulson <lp15@cam.ac.uk>
I would say bad, and we should try to limit our deviations from Standard ML to what is essential. If there ever is further evolution of Standard ML, we should try to bring our own ideas into it.
CakeML illustrates the advantages of a formal definition. It is a subset of standard ML with substantially the same semantics. Without a formal semantics, the very idea of a verified compiler is meaningless. Others have also noticed the benefits of using a formally defined language for coding
a theorem prover. We have been forced to stretch things a bit, due to the lack of other competitive implementations, but we must hope that this situation doesn't last forever.
Larry Paulson
Last updated: Apr 19 2024 at 20:15 UTC