Email Gateway (Aug 19 2022 at 11:00): Email Gateway (Aug 19 2022 at 11:00):From: Makarius <makarius@sketis.net>
Here are some more Q&A threads on nat vs. int, and the natural
construction of int via quotients:
http://cstheory.stackexchange.com/questions/3772/why-naturals-instead-of-integers
http://mathoverflow.net/questions/29090/direct-construction-of-the-integers
Makarius
Email Gateway (Aug 19 2022 at 11:00):From: Makarius <makarius@sketis.net>
I agree with that, although the "marketing" of proof assistants in the
last 10 years or so has moved in a different direction. Today most people
think of Coq as some dependently typed functional programming language,
and the Agda is emphasizing the programming aspect even more.
My own terminology is mainly about "formal languages" and "formalization"
of any kind. For example, the formal proof language of Isar is used to
write formal proofs, not to "program" nor to "implement" proofs.
Isabelle/ML and Isabelle/Scala happen to be programming languages just by
accident, so you can use them to program things. The Isabelle document
preparation language (formal latex) also happens to be computationally
complete, but nobody would say to "program" / "implement" / "code" some
text for a paper or book.
Interestingly, the computational or non-computational aspect of languages
often causes additional confusion for licensing. E.g. see the discussion
in the paper about "Licensing the Mizar Mathematical Library"
http://arxiv.org/abs/1107.3212
To my taste, the attempt to see Mizar articles as potentially
computational is even more artificial for that particular proof checker.
Makarius
Email Gateway (Aug 19 2022 at 11:00):From: Makarius <makarius@sketis.net>
You need to be specific what you mean by "Isabelle". Maybe Isabelle/HOL?
In some sense, generic "Isabelle" is a framework (or playground) for a
multitude of formal languages of different use and purpose: Isabelle/ML,
Isabelle/Scala, Isabelle/Pure, Isabelle/HOL, Isabelle/Isar, Isabelle/XYZ.
See also
https://sites.google.com/site/isabelleedinburgh2013/Slides_makarius.pdf?attredirects=0
notably slide 4 about some languages of Isabelle.
Makarius
Email Gateway (Aug 19 2022 at 11:01):From: Lawrence Paulson <lp15@cam.ac.uk>
If people want to prove theorems, they had better turn to us :-)
Larry
Email Gateway (Aug 19 2022 at 11:08):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I want to recover the ordered pair part of an int. I actually have a
simple solution like this:
definition myI :: "int => nat * nat" where
"myI x = (nat x, nat (-x))"
In the process of getting to the above definition, I was trying to get
the ordered pair using lower level methods. Even though I have a
solution, I ask about these other methods in case there's something
useful there for me to use.
In Int.thy, on line 20, int is defined as a quotient_type:
(020) quotient_type int = "nat * nat" / "intrel"
(021) morphisms Rep_Integ Abs_Integ
The type of Rep_Integ is (int => (nat * nat)), so I try to use it with
something like "Rep_Integ 3", but I can't ever get it to return an
ordered pair like (3,0).
QUESTION: Is there a way for me to get "Rep_Integ 3" to return (3,0)?
I try to do some lifting, like on line 208:
(208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
of_nat j"
However, on line 1661, there's this:
(1661) declare Quotient_int [quot_del]
In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
try to enable it blindly like,
setup_lifting Quotient_int,
but I get a warning, and lifting doesn't work for me.
QUESTION: Can I enable lifting for int?
Thanks,
GB
Email Gateway (Aug 19 2022 at 11:08):From: Lawrence Paulson <lp15@cam.ac.uk>
The simple answer is no. What your request is impossible. The integers are constructed as a quotient and therefore the representation of an integer is an equivalence class, in this case a set of pairs of natural numbers. The construction does not give you a map from integers to some distinguished element of this set. Of course, nothing stops you from writing your own function from integers to pairs of natural numbers.
Some time ago I wrote a paper on such matters, which you may find useful:
http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses.pdf
Larry Paulson
Email Gateway (Aug 19 2022 at 11:09):From: Ondřej Kunčar <kuncar@in.tum.de>
On 05/21/2013 05:22 AM, Gottfried Barrow wrote:
I try to do some lifting, like on line 208:
(208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
of_nat j"However, on line 1661, there's this:
(1661) declare Quotient_int [quot_del]
In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
try to enable it blindly like,setup_lifting Quotient_int,
but I get a warning, and lifting doesn't work for me.
I guess "lifting doesn't work for me" means this:
Lifting failed for the following term:
Term: λ(i∷nat, j∷nat). of_nat i - of_nat j
Type: nat × nat ⇒ ?'b∷{minus,semiring_1}
Reason: The type of the term cannot be instantiated to "nat × nat ⇒
'a∷type".
And this gives you a hint where the problem is:
you cannot instantied 'a::type for ?'b::{minus, semiring_1}.
The original definition of of_int in Int.thy is done in a context ring_1.
Try this:
lift_definition of_int :: "int => 'a::ring_1" is "%(i,j). of_nat i -
of_nat j"
QUESTION: Can I enable lifting for int?
Yes, by the command you used:
setup_lifting Quotient_int
or even better together with the reflexivity theorem:
setup_lifting Quotient_int int_equivp[THEN equivp_reflp2]
Ondrej
Email Gateway (Aug 19 2022 at 11:09):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Larry,
Alright, your paper will be the explanatory comments to Int.thy that
everyone forgot to put in. Your slides will also be useful:
http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses-slides.pdf
<http://www.cl.cam.ac.uk/%7Elp15/papers/Reports/equivclasses-slides.pdf>
I just need to match up a little of your notation in the paper with the
newer Isar that's in Int.thy, and a lot of the naming is the same.
It'd be interesting to know if it's common these days for other
languages to use the classic definition of the integers as equivalence
classes like you did with Int.thy:
https://en.wikipedia.org/wiki/Integer#Construction
It seems it's common for the natural numbers to be built using the
successor function, but I'm guessing it's not so common for the integers
to be equivalence classes.
I only need one representation of an integer, like (3,0) for 3, which I
can use to tie into an equivalence class of my own, if that's the way I
should do things, and it will work out.
Thanks for the help,
GB
Email Gateway (Aug 19 2022 at 11:09):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Ondřej,
One thing led to another, and I did a bunch of searches, and it turns
out you would be one of the two to ask for a tutorial on lifting, but
I'm sure you don't have time.
I found this:
http://www4.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf
<http://www4.in.tum.de/%7Ekuncar/documents/huffman-kuncar-itp2012.pdf>
And it turns out you have connections to Josef Urban.
I got rid of my setup_lifting warning by importing Quotient_Product.thy,
from a tip of yours here:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-January/msg00127.html
Now, I do setup_lifting, and the line of code you gave me works, so I'm
at an error for a simple thing I want to do, which will show you that I
have a fundamental misunderstanding of how to use lifting:
setup_lifting Quotient_int
lift_definition of_int :: "int => 'a::ring_1" is "%(i, j). of_nat i
- of_nat j"
by(metis int.abs_eq_iff of_int.abs_eq)
lift_definition foo45 :: "int => nat * nat" is "%(x,y). (nat x, nat y)"
The last line gives this error:
Lifting failed for the following types:
Raw type: int
Abstract type: nat
Reason: No quotient type "Nat.nat" found.
But my "foo45" represents what I want, but you'll have to tell me
exactly what I have to do to get something like that.
I've attached a screenshot which shows the four lines of code above,
with the error.
Thanks for the help,
GB
130521a__lifting_attempt.png
Email Gateway (Aug 19 2022 at 11:09):From: Johannes Hölzl <hoelzl@in.tum.de>
In my experience it is quite the other way round. The first semesters
mathematics course I attended introduced the integers, the rational
numbers and the real numbers as equivalence classes. Only the natural
numbers and the complex numbers where introduced like a datatype.
- Johannes
Email Gateway (Aug 19 2022 at 11:10):From: Lawrence Paulson <lp15@cam.ac.uk>
My slides briefly hint at the reason why the integers and rationals are almost invariably defined using equivalence classes and not using particular representations such as signed natural numbers or reduced fractions. It is simply that equivalence classes make everything much easier.
Imagine defining addition on signed natural numbers. You will need at least three cases: (1) the signs agree (2) left operand is greater (3) right operand is greater. To prove the associative law, you will have four occurrences of the addition operator and therefore 81 separate cases. With equivalence classes, there is only one case and it is shown in full on one of the slides.
For fractions in reduced form, the situation is even worse, because you're constantly reasoning about greatest common divisors. With equivalent classes, there is no need for that.
Larry Paulson
Email Gateway (Aug 19 2022 at 11:10):From: Ondřej Kunčar <kuncar@in.tum.de>
The term "(nat x, nat y)" has type "int * int" and you want to lift it
to a term of the type "nat * nat". That's not possible because there is
not registered any such quotient (or subtype) (i.e., using integers to
represent natural numbers).
What you probably meant (but I don't know I am just guessing your
intentions), is this definition:
lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"
This is type correct but you can't prove the respectfulness theorem
since this theorem implies that each equivalence class in a definition
of integers contains exactly one element. That's not true.
You need some kind of a normalization function that picks up one element
for each class. For example:
lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" by auto
This gives you for each positive integer x a pair (x, 0) and for each
negative integer (0, 0).
For deep understanding I recommend read the paper that Brian and I wrote
about Lifting/Transfer and it is also good to know how typedef works.
You can also read a paper by Kaliszyk, Urban
(http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).
Ondrej
Email Gateway (Aug 19 2022 at 11:10):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Johannes,
Thanks for your comment. I was comparing the formal, textbook
construction of the integers, as in what you're listing, to concrete
implementations of integers in programming languages, such as Coq,
Isabelle/HOL, Haskell, or any other language, old or new, but especially
new.
I'm speculating that this ability of Isabelle/HOL to define integers as
equivalence classes is special, and that it takes a special foundation
in a language to be able to do it, and that most languages don't have
the foundation to be able to do it in a practical way.
But I wouldn't know. This is the first time I've ever delved into the
low-level internals of a programming language, but defining an integer
as a set, in particular as an equivalence class, seems like it requires
some clever and sophisticated foundational code.
First, a person would simply know how it could be done at all. But
that's not enough; their code would have to perform reasonably fast.
I wouldn't know where to begin, and I'm sure any initial discovery of
mine on how to do it would be so slow, it would be useless.
All that to say, I'm guessing that Isabelle/HOL is pretty special in
this ability to achieve a textbook definition of the integers. But I try
not to become dogmatic about things I don't know about, and it could be
that it's very common for programming languages to implement integers as
equivalence classes.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:10):From: Lawrence Paulson <lp15@cam.ac.uk>
Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.
Larry Paulson
Email Gateway (Aug 19 2022 at 11:10):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-05-22 14:26 Lawrence Paulson:
Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.
Well, but there _is_ a notion of "programming" in Isabelle, given that
it is based on a functional programming language, isn't it? I recall
this earlier discussion on the title of the "programming and proving"
tutorial:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:10):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 5/22/2013 8:26 AM, Lawrence Paulson wrote:
Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.
Larry Paulson
Larry,
My general rule is to never use emoticons, but rules have their exceptions.
You gave me that idea :). As to acronyms such as "lol", even under these
circumstances, they're still unacceptable.
This is the specific email:
http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00034.html
This will contain the thread:
http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html>
I was just starting to decide that under certain contexts, I could refer
to Isabelle/HOL as a programming language, because it's just a lot
easier to use that phrase sometimes, whereas, according to your specific
clarification in the email linked to above, Isabelle/Pure and
Isabelle/Isar are never to be called programming languages, so I try to
use "proof language" or "source language" when referring to them, even
when I know others might not get my point.
One of my other recent emails to the list spawned some private chatter
in which I referred to HOL as a programming language, which resulted in
a similar response to yours, which paraphrased would be, "What is this
programming language you're talking about in reference to HOL?"
That's why I had easy access to the links above, because I thought I had
the perfect, authoritative reference to explain that Isabelle/HOL is a
programming language, where Pure and Isar aren't.
In an attempt to use safe, correct vocabulary, I've resorted to using
"coding language" when trying to refer to the whole Isabelle family of
languages. At some point, there's a need for phrases, like, "I'm
programming with Isabelle/HOL", or, "I'm coding with Isabelle". Like I
say, "coding" has become my word of choice to replace "programming".
Anyway, I'm happy to try and use the official vocabulary correctly.
There are a ton of interwined languages with Isabelle, so I give up and
get lazy sometimes, and just say "programming language".
As to Coq, it seems to me if I can call Isabelle/HOL a programming
language, then I can call Coq a programming language. That's just an
aside. I'd be happy to use any official Coq vocabulary to use to refer
to Coq.
Regards,
GB
On 22 May 2013, at 14:16, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:
Thanks for your comment. I was comparing the formal, textbook construction of the integers, as in what you're listing, to concrete implementations of integers in programming languages, such as Coq, Isabelle/HOL, Haskell, or any other language, old or new, but especially new.
Email Gateway (Aug 19 2022 at 11:10):From: Ramana Kumar <rk436@cam.ac.uk>
On Wed, May 22, 2013 at 2:45 PM, Christoph LANGE <
math.semantic.web@gmail.com> wrote:
2013-05-22 14:26 Lawrence Paulson:
Coq and Isabelle/HOL are proof assistants, not programming languages. I
can't imagine what gave you that idea. In Coq and Isabelle/HOL you write
specifications, not code.Well, but there _is_ a notion of "programming" in Isabelle, given that
it is based on a functional programming language, isn't it?
I would not put it that way.
Both Isabelle/HOL and <your favourite functional programming language> are
based on some flavour of lambda calculus. That's the connection.
However, there is no evaluation strategy specified for Isabelle/HOL terms,
and several constants don't have reducible definitions.
It's possible (and even common) to write uncomputable specifications in HOL
whereas you can't write anything uncomputable in a programming language.
I recall
this earlier discussion on the title of the "programming and proving"
tutorial:https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html
Cheers,
Christoph
--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
Work-in-progress deadline 7 June; http://cicm-conference.org/2013/
→ OpenMath Workshop, 10 July, Bath, UK.
Submission deadline 7 June; http://cicm-conference.org/2013/openmath/
Email Gateway (Aug 19 2022 at 11:11):From: Lawrence Paulson <lp15@cam.ac.uk>
You can call anything anything, but you are only complicating things for yourself. To my mind, asking why Isabelle/HOL has equivalence classes when Haskell doesn't and they are both programming languages is a bit like asking why a Boeing can fly and a Ford cannot when they are both cars.
Perhaps the term you are looking for is "formal language". Programming languages are formal, and higher-order logic is also a formal language. Just as Boeings and Fords are both vehicles.
Larry Paulson
Email Gateway (Aug 19 2022 at 11:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Ondřej,
What you probably meant (but I don't know I am just guessing your
intentions), is this definition:lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"
Yes.
This is type correct but you can't prove the respectfulness theorem
since this theorem implies that each equivalence class in a definition
of integers contains exactly one element. That's not true.You need some kind of a normalization function that picks up one
element for each class. For example:lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" by
auto
And so telling me that I need to prove "respectfulness" represents this
big need of people like me to have some understanding of what's going on
under the hood of the engine. Things like "fun" and lifting are great
because they take care of a lot of overhead, until I stray outside of
some example/template I have.
This gives you for each positive integer x a pair (x, 0) and for each
negative integer (0, 0).
This is one more time in which lifting appears to not be the best
solution. I think it'll be hard to beat the simple definition that I
came up with. But the value in these attempts to use lifting is in
getting closer to knowing what lifting is.
For deep understanding I recommend read the paper that Brian and I
wrote about Lifting/Transfer and it is also good to know how typedef
works. You can also read a paper by Kaliszyk, Urban
(http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).
And so I have 3 papers to pull from now, yours, Peter's and this one you
just listed. All along it's been, "Something's being lifted from
somewhere, to some thing, but what's being lifted is not clear to me,
and neither are the restrictions on what the some thing can be."
It looks like Urban and Kaliszyk's paper provides a good conceptual
overview. From section 5:/
/
/The main benefit of a quotient package is to lift automatically
theorems over raw types to theorems over quotient types. We will
perform this lifting in three phases, called regularization,
injection and cleaning according to procedures in Homeier’s ML-code./
So I was asking myself, "What's this Homeier's ML-code?"
And then I replied, "Oh, that would be Peter Homeier, who sent me a link
to his paper on quotients earlier in the day, in response to my global
request for docs on quotients and lifting."
With quotients and lifting, it appears that if you learn the one, you
learn the other.
Thanks,
GB
Email Gateway (Aug 19 2022 at 11:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Larry,
I was going to let your email be the end, a decision which actually
resulted in me culling out every point I thought about making, except
for trying to make a point with your transportation analogy.
To summarize the point to begin with, so you don't have to actually read
the analogy, it's just a variation of my past "Isabelle is awesome"
statements.
So Isabelle/HOL is a Boeing airplane, though a special model that's
configurable, and Haskell is a Ford car.
In regards to transportation, it appears not to make sense for a person
to make anything but the broadest of generalizations when comparing the two.
That's because, Isabelle, being a Boeing airplane, is certainly a means
of transportation, but the maintenance and fuel costs are extraordinary,
and so on the surface, to point out that Haskell, a Ford car, hasn't
implemented certain theoretical, engineering concepts when Isabelle has,
can appear to be dumb, especially, because practically speaking, as far
as transportation the advanced features are of no use.
However, the proper context is my use of the special, configurable
Boeing airplane. It happens to be that I have almost no interest in
traveling, I only care to theorize about traveling, in particular,
theorizing about air travel.
At this time, I don't have the money to even have the Boeing started up,
but then again, at this point, I only have a need to look at the Boeing,
and take a few measurements for certain parts that aren't completely
documented.
Now, I would hope that in several years, I'm doing something more than
what has already been done in regards to theorizing about air travel, to
the point to where I have a need to do more than just look at the
airplane, but in two years time, manufacturing costs being what they
are, there's some chance it will be affordable for me to pay some per
minute charge to reconfigure the special Boeing, where simply
reconfiguring it should answer some question I'll have.
So forth and so on. As times passes, what was once not affordable
becomes affordable, in regards to testing my theories. The upside is
that I may never have to resort to buying a Ford car, which is
accessible to the masses, but still costs a lot of money, and is a waste
if I don't have to do it.
And there's the possibility, if I can keep postponing the need for a
Ford car, that at some point, the configurable Boeing has ceased to be
leading edge technology, for near exclusive use by academics and
researchers, but the costs have dropped so much that it has become
commodity technology, and things have evolved for me to the where I now
have a need to travel, but not simply on the ground, like with the Ford
car, but in the air.
Do the designers intend for a person like me to use the Boeing in this
way? Probably not. Most likely, the configurable Boeing is meant as an
ends to a mean for professionals who work in the aerospace industry.
But instead of of using the configurable Boeing as an ends to a means, I
use it as an ends in itself, and because it can be used like that, it's
awesome.
Well, because I have no desire to ever work outside the realm of the
configurable Boeing, certain vocabulary doesn't fit my use of the Boeing
as good as it fits the designers use, but that idea is not to be pursued
here.
Regards,
GB
Last updated: Apr 25 2024 at 04:18 UTC