Email Gateway (Aug 19 2022 at 09:51): Email Gateway (Aug 19 2022 at 09:51):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people,
I hope my question won't look too much stupid to logics gurus.
Reading at Wikipedia's page about HOL, something tackled me a bit:
http://en.wikipedia.org/wiki/Higher-order_logic
“HOL with standard semantics is more expressive than first-order logic.
For example, HOL admits categorical axiomatizations of the natural
numbers, and of the real numbers, which are impossible with first-order
logic. However, by a result of Gödel, HOL with standard semantics does
not admit an effective, sound and complete proof calculus.”
There's also a criticism section on the same page.
Well, I'm not sure to understand what it really means and would like to
know if there are good pointers to understand how and when difference
between HOL and FOL matters, and when and how Isabelle has to do with it.
The quote from Wikipedia looks weird to me, as it seems to say they may be
soundness issue with HOL? Is that really it? I've never heard about any
such assertion before…
Email Gateway (Aug 19 2022 at 09:51):From: Ramana Kumar <rk436@cam.ac.uk>
The Wikipedia article is referring to the fact that there will always be
true statements in HOL that are not the conclusion of any derivation in a
proof calculus.
(This can be contrasted with FOL: there is a sound proof calculus for FOL
with the property that every true FOL statement can be proved in it.)
(The problem in HOL, as I understand it, is that there are too many true
statements, more than could be all the conclusions from a proof calculus.)
It does not say that there cannot be a sound proof calculus for HOL.
Indeed, we think Isabelle/HOL implements one such calculus.
As for how to learn this stuff... I'm sure someone on list will be able to
recommend a good textbook.
Personally I think Wikipedia is OK, but you have to be patient and willing
to read carefully and follow links... and sometimes it may be wrong, so
discussing with others helps :)
Email Gateway (Aug 19 2022 at 09:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote:
Hi people,
I hope my question won't look too much stupid to logics gurus.
Yannick,
I collect books written by the logic gurus, and occasionally read the
introductions, so I am qualified to provide links to books.
The standard text that keeps getting mentioned by the logic gurus here
is Andrews' text, which starts with propositional logic and FOL, and
then covers type theory, where types would be the beginning of the
foundation of HOL in general:
http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theory/dp/1402007639
FOL begins with the standard logic operators as its primitives, or a few
of them from which the others can be derived, as shown by Definitions
5.1, 5.2, and 5.3 of Bilaniuk's book:
http://euclid.trentu.ca/math/sb/pcml/
FOL is reasonably fixed in stone and standardized.
HOL begins with variables, functions, and function application as
primitives, as shown by Paulson's "Foundations of Functional
Programming" Definition 1, page 2:
http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf
From there (or somewhere else) HOL diverges, where the two biggest
camps would be Coq's higher-order logic, and the HOL family, where HOL
is not to be confused with the general phrase "higher-order logic", and
where John Harrison gives a diagram showing the HOL family of products
on page 9 of "HOL Light Tutorial":
http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
Alfio recently pointed me to "Introduction to Type Theory" by Geuvers
which makes comparisons between type theory and set theory:
http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf
Because ZFC sets reigns as King and Queen in the world of mathematics,
and is a FOL language, then HOL vs. FOL is largely "types vs. ZFC sets",
at least for those who even know about the comparison, where education
about types is near non-existence in formal, mathematics education, even
though Church and Curry had their formal degrees in mathematics.
To compare the two, the problem is understanding what HOL is, not what
FOL is, at least for me, since FOL is much simpler, even though HOL
starts with a simple set of primitives.
I shared a list of the books I'd collected on trying to get up to speed
with Isabelle/HOL:
http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00024.html
http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00003.html
Fortunately, I've decided I probably will be able to be live more
normally, which is to occasionally ponder questions about foundational
logic, but not have to completely understand it all to work at a higher
level. It's a very healthy place to be.
Regards,
GB
Reading at Wikipedia's page about HOL, something tackled me a bit:
http://en.wikipedia.org/wiki/Higher-order_logic
“HOL with standard semantics is more expressive than first-order
logic.
For example, HOL admits categorical axiomatizations of the natural
numbers, and of the real numbers, which are impossible with
first-order
logic. However, by a result of Gödel, HOL with standard semantics
does
not admit an effective, sound and complete proof calculus.”There's also a criticism section on the same page.
Well, I'm not sure to understand what it really means and would like
to know if there are good pointers to understand how and when
difference between HOL and FOL matters, and when and how Isabelle has
to do with it. The quote from Wikipedia looks weird to me, as it seems
to say they may be soundness issue with HOL? Is that really it? I've
never heard about any such assertion before…
Email Gateway (Aug 19 2022 at 09:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
When I'm only qualified to provide links, and I start speaking
authoritatively, then I quickly get in trouble.
Lambda calculus would be the beginning, and types comes next. I was
speaking of lambda calculus and types as being monolithic. In my mind,
it must be that lambda calculus and types are part of the same
foundation. That perception might be eliminated if I read more of the
books, or it might become stronger.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:52):From: Alfio Martini <alfio.martini@acm.org>
Hi Yannick,
Adding to Gottfried´s selected readings, I strongly recommend the highly
readable
"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.
Best!
Email Gateway (Aug 19 2022 at 09:52):From: "\"Mark\"" <mark@proof-technologies.com>
You might find my glossary of HOL terminology useful. It includes various
entries about mathematical logic.
www.proof-technologies.com/misc/Glossary.txt
Mark.
on 31/1/13 3:52 PM, Alfio Martini <alfio.martini@acm.org> wrote:
Hi Yannick,
Adding to Gottfried´s selected readings, I strongly recommend the highly
readable"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.Best!
On Thu, Jan 31, 2013 at 12:04 PM, Gottfried Barrow
<gottfried.barrow@gmx.comwrote:
On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote:
Hi people,
I hope my question won't look too much stupid to logics gurus.
Yannick,
I collect books written by the logic gurus, and occasionally read the
introductions, so I am qualified to provide links to books.The standard text that keeps getting mentioned by the logic gurus here is
Andrews' text, which starts with propositional logic and FOL, and then
covers type theory, where types would be the beginning of the foundation
of
HOL in general:http://www.amazon.com/**Introduction-Mathematical-**Logic-Type-Theory/dp/*
*1402007639<http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theor
y/dp/1402007639>FOL begins with the standard logic operators as its primitives, or a few
of them from which the others can be derived, as shown by Definitions
5.1,
5.2, and 5.3 of Bilaniuk's book:http://euclid.trentu.ca/math/**sb/pcml/<http://euclid.trentu.ca/math/sb/pcml
/>FOL is reasonably fixed in stone and standardized.
HOL begins with variables, functions, and function application as
primitives, as shown by Paulson's "Foundations of Functional Programming"
Definition 1, page 2:http://www.cl.cam.ac.uk/~lp15/**papers/Notes/Founds-FP.pdf<http://www.cl.cam
.ac.uk/~lp15/papers/Notes/Founds-FP.pdf>From there (or somewhere else) HOL diverges, where the two biggest camps
would be Coq's higher-order logic, and the HOL family, where HOL is not
to
be confused with the general phrase "higher-order logic", and where John
Harrison gives a diagram showing the HOL family of products on page 9 of
"HOL Light Tutorial":http://www.cl.cam.ac.uk/~**jrh13/hol-light/tutorial_220.**pdf<http://www.cl.
cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf>Alfio recently pointed me to "Introduction to Type Theory" by Geuvers
which makes comparisons between type theory and set theory:http://www.cs.ru.nl/~herman/**PUBS/IntroTT-improved.pdf<http://www.cs.ru.nl/
~herman/PUBS/IntroTT-improved.pdf>Because ZFC sets reigns as King and Queen in the world of mathematics,
and
is a FOL language, then HOL vs. FOL is largely "types vs. ZFC sets", at
least for those who even know about the comparison, where education about
types is near non-existence in formal, mathematics education, even though
Church and Curry had their formal degrees in mathematics.To compare the two, the problem is understanding what HOL is, not what
FOL
is, at least for me, since FOL is much simpler, even though HOL starts
with
a simple set of primitives.I shared a list of the books I'd collected on trying to get up to speed
with Isabelle/HOL:users/2012-June/msg00024.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabel
le-users/2012-June/msg00024.html>users/2012-June/msg00003.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabel
le-users/2012-June/msg00003.html>Fortunately, I've decided I probably will be able to be live more
normally, which is to occasionally ponder questions about foundational
logic, but not have to completely understand it all to work at a higher
level. It's a very healthy place to be.Regards,
GBReading at Wikipedia's page about HOL, something tackled me a bit:
http://en.wikipedia.org/wiki/**Higher-order_logic<http://en.wikipedia.org/wi
ki/Higher-order_logic>“HOL with standard semantics is more expressive than first-order
logic.
For example, HOL admits categorical axiomatizations of the natural
numbers, and of the real numbers, which are impossible with
first-order
logic. However, by a result of Gödel, HOL with standard semantics
does
not admit an effective, sound and complete proof calculus.”There's also a criticism section on the same page.
Well, I'm not sure to understand what it really means and would like to
know if there are good pointers to understand how and when difference
between HOL and FOL matters, and when and how Isabelle has to do with
it.
The quote from Wikipedia looks weird to me, as it seems to say they may
be
soundness issue with HOL? Is that really it? I've never heard about any
such assertion before…
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
Email Gateway (Aug 19 2022 at 09:52):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi Alfio!
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)
Still looking at Gottfried's list.
Email Gateway (Aug 19 2022 at 10:00):From: Makarius <makarius@sketis.net>
This is indeed a very nice overview, I need to study this further.
Particularly notable is Theorem 11 / Virtue 6 about the completeness of
HOL, which goes back to Henkin 1950, published shortly after the famous
Church 1940 paper.
More than 60 years after it, there are still occasional rumors about HOL
being incomplete. Farmer gives some nice explanations about the overall
situation.
Makarius
Email Gateway (Aug 19 2022 at 10:01):From: Freek Wiedijk <freek@cs.ru.nl>
Hi Larry,
I gather that the Coq kernel also contains a big chunk of
C code. Surprising, to say the least.
Not if you consider Coq to be a functional language that
you want to execute as fast as possible.
Freek
Email Gateway (Aug 19 2022 at 10:01):From: Makarius <makarius@sketis.net>
This seems to refer to the virtual machine that runs at the bottom of Coq.
(We would need some Coq experts here, or move that thread to coq-club, if
anybody dares to do it.)
Looking the problem from a higher level, it is the old debate how you make
the prover: LCF-style to run through the inference kernel at run-time, or
somehow native as part of the computational part of the logic. This also
means the logic is made in a way to have a computational part in the first
place (like Coq, Agda, etc.).
My impression is that the LCF-style run-time interpretation turns out as
surprisingly fast in many practical applications, both relatively and
absolutely compared to the Coq computation model. In a system like
Isabelle/HOL you are not limited to a single built-in computational model,
you can do things with different formal status (say HOL specifications vs.
emitted code in other languages). In principle, Coq does not limit you
either, but the traditional way is to assimilate everything within its one
big formal system.
Incidently, a Coq user has explained to me just last weak, that the
notable Isabelle application IsaFoR/CeTA performs best in its category.
The code that does the actual work in the end is native in Haskell,
without the prover preventing it from being really fast.
Makarius
Email Gateway (Aug 19 2022 at 10:03):From: "\"Mark\"" <mark@proof-technologies.com>
I think it can get quite confusing because different people use the same
names for different things, and different names for the same things, and
sometimes the same people do this too!
"HOL" can mean "higher-order logic" (referring to one or more of various
logics that are higher-order), or it can mean "the HOL logic" (Mike Gordon's
particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL Light,
ProofPower and HOL Zero). Other theorem provers such as Coq, PVS and IMPS
implement other higher-order logics. So the logic described in the HOL4
logic manual really is the same as HOL Light's, etc, the only difference
being that they are built up in different ways (i.e. they start with a
different initial set of axioms and primitive inference rules, but these
axiomatisations are just different ways of defining the same logic).
Does that clear anything up?
Mark.
on 1/2/13 2:23 PM, Gottfried Barrow <gottfried.barrow@gmx.com> wrote:
On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".If you keep talking long enough, another one might pop in and throw in
the term "type classes".Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types
Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:http://hol.sourceforge.net/documentation.html
For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:simply-typed : (adj) Relating to type systems that are relatively simple
and
are not, for example, dependently-typed. There is considerable variation
in
the
precise intended meaning of "simply-typed" in contemporary usage: in some
usages
polymorphism is not a disqualifying factor, in other usages polymorphism
is
only
a disqualifying factor if it caters for the quantification of type
variables,
and in other usages still any form of polymorphism is a disqualifying
factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.Still looking at Gottfried's list.
In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.Regards, GB
http://www.phil.cmu.edu/~avigad/formal/
http://www.andrew.cmu.edu/user/avigad/isabelle/
http://www4.in.tum.de/~ballarin/belgrade08-tut/
http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php
http://isabelle.in.tum.de/coursematerial/IJCAR04/
http://archiv.infsec.ethz.ch/education/permanent/csmr.html
http://isabelle.in.tum.de/exercises/
http://www.irisa.fr/celtique/genet/ACF/
http://dream.inf.ed.ac.uk/projects/isabelle/
http://isabelle.in.tum.de/coursematerial/PSV2009-1/
http://www21.in.tum.de/teaching/logik/SS12/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/
http://www.cs.colorado.edu/~siek/7000/spring07/
http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html
http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php
http://www.lri.fr/~wenzel/Isar2010-Orsay/
http://www.lri.fr/~wenzel/Isabelle2011-Paris/
Email Gateway (Aug 19 2022 at 10:10):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/1/2013 3:41 PM, "Mark" wrote:
Does that clear anything up?
Mark,
I was sort of speaking of maybe where I was a year ago, but "the
problem" is still there to a certain extent.
So I count 30 folders for the "HOL section" of books, then there's the
non-HOL logic folders, where I count 49 folders, along with the ML
folders, 14 of those, and the Isabelle section with about 14 top level
folders, but many subfolders by author or web page.
Before tying into the last paragraph, in the document
kanaskskis-8-logic.pdf, I point out the semi-formal BNF grammar
describing a HOL4 type, page 11, and then the first BNF grammar
describing a term, page 15, followed by the second BNF grammar of a term.
I now ask, "Where is the semi-formal definition of a Isabelle type and
term?"
If you said, "If you understand the HOL4 definitions of a type and term,
then you basically understand Isabelle's".
To that I would reply, "But I'm not interested in studying 2 or 3 or 4
other HOL's to get a general understanding of Isabelle's logic, I'm
interested in studying one logic to get a precise understanding of the
one logic that I'm using."
"The problem" is represented by another question. "What is the clear
learning path for learning about a particular HOL so that a person can
use that HOL in a theorem assistant, and do that within a reasonable
period of time, and not just end up with a foggy notion of ideas?"
The answer is that, for self-education, there is no clear path. It's not
clear what is essential, and what is an unneeded tangent. But that's not
anyone's fault. It just indicates that the market is not mature.
In a mature market, speaking analogously, you don't have to learn C, to
learn C++, to learn Java, when it's Java that you're going to be using.
In a mature market, people have written lots of books to start you
wherever you want to start.
Now to something of a positive nature. The name for your HOL Zero site
on my hard drive is "hoZ", and I downloaded the latest glossary, which
is now named "hoZ__Glossary 130202.pdf".
It occurred to me that I can tweak it to fit my own preferences, so I
saved it to PDF, and with Acrobat, I can add a bookmark entry for each
of the terms, and make them sub-bookmarks of their first character.
Doing that, I'll be able to see the trees, and not just the forest.
There are many mini-lessons in there that don't demand a big investment
of time, so thanks for that.
Regards,
GB
I think it can get quite confusing because different people use the same
names for different things, and different names for the same things, and
sometimes the same people do this too!"HOL" can mean "higher-order logic" (referring to one or more of various
logics that are higher-order), or it can mean "the HOL logic" (Mike Gordon's
particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL Light,
ProofPower and HOL Zero). Other theorem provers such as Coq, PVS and IMPS
implement other higher-order logics. So the logic described in the HOL4
logic manual really is the same as HOL Light's, etc, the only difference
being that they are built up in different ways (i.e. they start with a
different initial set of axioms and primitive inference rules, but these
axiomatisations are just different ways of defining the same logic).
Does that clear anything up?Mark.
on 1/2/13 2:23 PM, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:
On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)
There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".If you keep talking long enough, another one might pop in and throw in
the term "type classes".Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types
Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:http://hol.sourceforge.net/documentation.html
For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:simply-typed : (adj) Relating to type systems that are relatively simple
and
are not, for example, dependently-typed. There is considerable variation
in
the
precise intended meaning of "simply-typed" in contemporary usage: in some
usages
polymorphism is not a disqualifying factor, in other usages polymorphism
is
only
a disqualifying factor if it caters for the quantification of type
variables,
and in other usages still any form of polymorphism is a disqualifying
factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.Still looking at Gottfried's list.
In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.Regards, GB
http://www.phil.cmu.edu/~avigad/formal/
http://www.andrew.cmu.edu/user/avigad/isabelle/
http://www4.in.tum.de/~ballarin/belgrade08-tut/
http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php
http://isabelle.in.tum.de/coursematerial/IJCAR04/
http://archiv.infsec.ethz.ch/education/permanent/csmr.html
http://isabelle.in.tum.de/exercises/
http://www.irisa.fr/celtique/genet/ACF/
http://dream.inf.ed.ac.uk/projects/isabelle/
http://isabelle.in.tum.de/coursematerial/PSV2009-1/
http://www21.in.tum.de/teaching/logik/SS12/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/
http://www.cs.colorado.edu/~siek/7000/spring07/
http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html
http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php
http://www.lri.fr/~wenzel/Isar2010-Orsay/
http://www.lri.fr/~wenzel/Isabelle2011-Paris/
Email Gateway (Aug 19 2022 at 10:11):From: "\"Mark\"" <mark@proof-technologies.com>
Yes, I agree it's very difficult. When I started in theorem proving I was
also struck by the lack of a clear learning path. Isabelle is I think one
of the most difficult to really understand how everything works. You have
to understand each of the many layers of Isabelle. I'm afraid I don't
understand these layers, although I would like to at some stage, but more
seem to be getting added as the years go by! But the main priorities for
the implementors of Isabelle, as I understand it, have been usability and
power, and having an understandable implementation comes way down the list.
In HOL Zero, trustworthiness and understandable implementation are top of
the list (they go hand-in-hand in my opinion), but of course it is very
basic and no good for creating proofs. So I think an important part of the
issue here is about priorities.
Mark.
on 2/2/13 9:04 PM, Gottfried Barrow <gottfried.barrow@gmx.com> wrote:
On 2/1/2013 3:41 PM, "Mark" wrote:
Does that clear anything up?
Mark,I was sort of speaking of maybe where I was a year ago, but "the
problem" is still there to a certain extent.So I count 30 folders for the "HOL section" of books, then there's the
non-HOL logic folders, where I count 49 folders, along with the ML
folders, 14 of those, and the Isabelle section with about 14 top level
folders, but many subfolders by author or web page.Before tying into the last paragraph, in the document
kanaskskis-8-logic.pdf, I point out the semi-formal BNF grammar
describing a HOL4 type, page 11, and then the first BNF grammar
describing a term, page 15, followed by the second BNF grammar of a term.I now ask, "Where is the semi-formal definition of a Isabelle type and
term?"If you said, "If you understand the HOL4 definitions of a type and term,
then you basically understand Isabelle's".To that I would reply, "But I'm not interested in studying 2 or 3 or 4
other HOL's to get a general understanding of Isabelle's logic, I'm
interested in studying one logic to get a precise understanding of the
one logic that I'm using.""The problem" is represented by another question. "What is the clear
learning path for learning about a particular HOL so that a person can
use that HOL in a theorem assistant, and do that within a reasonable
period of time, and not just end up with a foggy notion of ideas?"The answer is that, for self-education, there is no clear path. It's not
clear what is essential, and what is an unneeded tangent. But that's not
anyone's fault. It just indicates that the market is not mature.In a mature market, speaking analogously, you don't have to learn C, to
learn C++, to learn Java, when it's Java that you're going to be using.
In a mature market, people have written lots of books to start you
wherever you want to start.Now to something of a positive nature. The name for your HOL Zero site
on my hard drive is "hoZ", and I downloaded the latest glossary, which
is now named "hoZ__Glossary 130202.pdf".It occurred to me that I can tweak it to fit my own preferences, so I
saved it to PDF, and with Acrobat, I can add a bookmark entry for each
of the terms, and make them sub-bookmarks of their first character.
Doing that, I'll be able to see the trees, and not just the forest.There are many mini-lessons in there that don't demand a big investment
of time, so thanks for that.Regards,
GBI think it can get quite confusing because different people use the same
names for different things, and different names for the same things, and
sometimes the same people do this too!"HOL" can mean "higher-order logic" (referring to one or more of various
logics that are higher-order), or it can mean "the HOL logic" (Mike
Gordon's
particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL
Light,
ProofPower and HOL Zero). Other theorem provers such as Coq, PVS and
IMPS
implement other higher-order logics. So the logic described in the HOL4
logic manual really is the same as HOL Light's, etc, the only difference
being that they are built up in different ways (i.e. they start with a
different initial set of axioms and primitive inference rules, but these
axiomatisations are just different ways of defining the same logic).
Does that clear anything up?Mark.
on 1/2/13 2:23 PM, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:
On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)
There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".If you keep talking long enough, another one might pop in and throw in
the term "type classes".Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types
Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:http://hol.sourceforge.net/documentation.html
For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:simply-typed : (adj) Relating to type systems that are relatively
simple
and
are not, for example, dependently-typed. There is considerable
variation
in
the
precise intended meaning of "simply-typed" in contemporary usage: in
some
usages
polymorphism is not a disqualifying factor, in other usages polymorphism
is
only
a disqualifying factor if it caters for the quantification of type
variables,
and in other usages still any form of polymorphism is a disqualifying
factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.Still looking at Gottfried's list.
In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.Regards, GB
http://www.phil.cmu.edu/~avigad/formal/
http://www.andrew.cmu.edu/user/avigad/isabelle/
http://www4.in.tum.de/~ballarin/belgrade08-tut/
http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php
http://isabelle.in.tum.de/coursematerial/IJCAR04/
http://archiv.infsec.ethz.ch/education/permanent/csmr.html
http://isabelle.in.tum.de/exercises/
http://www.irisa.fr/celtique/genet/ACF/
http://dream.inf.ed.ac.uk/projects/isabelle/
http://isabelle.in.tum.de/coursematerial/PSV2009-1/
http://www21.in.tum.de/teaching/logik/SS12/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/
http://www.cs.colorado.edu/~siek/7000/spring07/
http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html
http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php
http://www.lri.fr/~wenzel/Isar2010-Orsay/
http://www.lri.fr/~wenzel/Isabelle2011-Paris/
Email Gateway (Aug 19 2022 at 10:14):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/2/2013 4:17 PM, "Mark" wrote:
Yes, I agree it's very difficult.
Mark,
But there's still lots of good news, like "the market" is way past
Cambridge LCF, and that low-priced computers now can have 4 cores, 8
GBytes of ram, and run at 2.5GHz or greater, because without fast
computers, functional programming would still be the domain of the
academics. It was only a few years ago that I would rail about Java,
after my computer performance would come to crawl because the browser
was starting up Java.
The docs distributed with HOL Zero have some good tutorial information
in them, like "3_HOL_Language.txt".
I created the file "HOL_Zero_docs.tex". If a person unzips
"holzero-0.6.0.tgz", and puts my .tex file in the folder
"./holzero-0.6.0", then they can produce the PDF file "HOL_Zero_docs.pdf".
I had to add the extension ".txt" to the files without an extension,
otherwise "\VerbatimInput" gave an error.
I attached "HOL_Zero_docs.tex", and I attached ""HOL_Zero_docs.pdf",
where the PDF is for demonstration purposes only. The PDF is to show
what a person would have access to if they were to install Latex on
their machine and compile the .tex file.
Again, the PDF is for demonstration purposes only. It is required that
any student of HOL acquire the sources from the web and compile their
own .tex file. The allotted time for viewing the PDF for demonstration
purposes is an integer m, where m can be greater than or equal to 1, but
less than or equal to 30, where the dimension of m is seconds.
Regards,
GB
When I started in theorem proving I was
also struck by the lack of a clear learning path. Isabelle is I think one
of the most difficult to really understand how everything works. You have
to understand each of the many layers of Isabelle. I'm afraid I don't
understand these layers, although I would like to at some stage, but more
seem to be getting added as the years go by! But the main priorities for
the implementors of Isabelle, as I understand it, have been usability and
power, and having an understandable implementation comes way down the list.
In HOL Zero, trustworthiness and understandable implementation are top of
the list (they go hand-in-hand in my opinion), but of course it is very
basic and no good for creating proofs. So I think an important part of the
issue here is about priorities.Mark.
on 2/2/13 9:04 PM, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:
On 2/1/2013 3:41 PM, "Mark" wrote:
Does that clear anything up?
Mark,I was sort of speaking of maybe where I was a year ago, but "the
problem" is still there to a certain extent.So I count 30 folders for the "HOL section" of books, then there's the
non-HOL logic folders, where I count 49 folders, along with the ML
folders, 14 of those, and the Isabelle section with about 14 top level
folders, but many subfolders by author or web page.Before tying into the last paragraph, in the document
kanaskskis-8-logic.pdf, I point out the semi-formal BNF grammar
describing a HOL4 type, page 11, and then the first BNF grammar
describing a term, page 15, followed by the second BNF grammar of a term.I now ask, "Where is the semi-formal definition of a Isabelle type and
term?"If you said, "If you understand the HOL4 definitions of a type and term,
then you basically understand Isabelle's".To that I would reply, "But I'm not interested in studying 2 or 3 or 4
other HOL's to get a general understanding of Isabelle's logic, I'm
interested in studying one logic to get a precise understanding of the
one logic that I'm using.""The problem" is represented by another question. "What is the clear
learning path for learning about a particular HOL so that a person can
use that HOL in a theorem assistant, and do that within a reasonable
period of time, and not just end up with a foggy notion of ideas?"The answer is that, for self-education, there is no clear path. It's not
clear what is essential, and what is an unneeded tangent. But that's not
anyone's fault. It just indicates that the market is not mature.In a mature market, speaking analogously, you don't have to learn C, to
learn C++, to learn Java, when it's Java that you're going to be using.
In a mature market, people have written lots of books to start you
wherever you want to start.Now to something of a positive nature. The name for your HOL Zero site
on my hard drive is "hoZ", and I downloaded the latest glossary, which
is now named "hoZ__Glossary 130202.pdf".It occurred to me that I can tweak it to fit my own preferences, so I
saved it to PDF, and with Acrobat, I can add a bookmark entry for each
of the terms, and make them sub-bookmarks of their first character.
Doing that, I'll be able to see the trees, and not just the forest.There are many mini-lessons in there that don't demand a big investment
of time, so thanks for that.Regards,
GBI think it can get quite confusing because different people use the same
names for different things, and different names for the same things, and
sometimes the same people do this too!"HOL" can mean "higher-order logic" (referring to one or more of various
logics that are higher-order), or it can mean "the HOL logic" (Mike
Gordon's
particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL
Light,
ProofPower and HOL Zero). Other theorem provers such as Coq, PVS and
IMPS
implement other higher-order logics. So the logic described in the HOL4
logic manual really is the same as HOL Light's, etc, the only difference
being that they are built up in different ways (i.e. they start with a
different initial set of axioms and primitive inference rules, but these
axiomatisations are just different ways of defining the same logic).
Does that clear anything up?Mark.
on 1/2/13 2:23 PM, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:
On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)
There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".If you keep talking long enough, another one might pop in and throw in
the term "type classes".Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types
Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:http://hol.sourceforge.net/documentation.html
For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:simply-typed : (adj) Relating to type systems that are relatively
simple
and
are not, for example, dependently-typed. There is considerable
variation
in
the
precise intended meaning of "simply-typed" in contemporary usage: in
some
usages
polymorphism is not a disqualifying factor, in other usages polymorphism
is
only
a disqualifying factor if it caters for the quantification of type
variables,
and in other usages still any form of polymorphism is a disqualifying
factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.Still looking at Gottfried's list.
In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.Regards, GB
http://www.phil.cmu.edu/~avigad/formal/
http://www.andrew.cmu.edu/user/avigad/isabelle/
http://www4.in.tum.de/~ballarin/belgrade08-tut/
http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php
http://isabelle.in.tum.de/coursematerial/IJCAR04/
[message truncated]
Email Gateway (Aug 19 2022 at 10:17):From: Makarius <makarius@sketis.net>
On Sat, 2 Feb 2013, "Mark" wrote:
Yes, I agree it's very difficult. When I started in theorem proving I
was also struck by the lack of a clear learning path. Isabelle is I
think one of the most difficult to really understand how everything
works. You have to understand each of the many layers of Isabelle.
I'm afraid I don't understand these layers, although I would like to at
some stage, but more seem to be getting added as the years go by!
I don't know anybody who really understands everything of Isabelle. But I
do understand its construction principles, and have a vague idea of the
vast space of possibilities resulting from it. This is just plain-old
modularity taken seriously.
There is no need for users to understand everything. I use Linux everyday
without having a clue how it is done these days, although I know about
certain general principles as a mental model.
But the main priorities for the implementors of Isabelle, as I
understand it, have been usability and power, and having an
understandable implementation comes way down the list.
Understandable implementation is actually the main priority in Isabelle.
Otherwise this vast system could not be managed at all.
The difference you see is that we have made conceptual progress in the
last 20 years how to build a high-end LCF-style system. Progess is not
for free, you have to provide some structure, and that inevitaby
introduces some complexity.
In HOL Zero, trustworthiness and understandable implementation are top
of the list (they go hand-in-hand in my opinion), but of course it is
very basic and no good for creating proofs.
This discussion has bounced between the HOL and Isabelle mailing lists
several times already. HOL Zero is as tiny that you see the problems
inherited from OCaml immediately. I would put more trust on OpenTheory
right now.
But we don't have users in the queue to ask substantially more
trustworthyness than is there in Isabelle already. Most users actually
want less, but I have no inclination to reduce the general robustness of
Isabelle either.
Makarius
Email Gateway (Aug 19 2022 at 10:19):From: Makarius <makarius@sketis.net>
See the Isabelle/Isar implementation manual chapter 2, about Isabelle/Pure
as reduced version of Higher-Order Logic to provide the logical framework.
This is occasionally interesting to know, although just some tiny
foundational bit. From Isabelle/Pure you move on to Isabelle/HOL, then
you add many add-on tools for 'inductive', 'datatype' etc. and lots of
proof tools like Sledgehammer. Then you are quite high above the logical
foundations and don't care much about them.
What is also interesting that the final end-user view tends to converge to
what totally different systems offer here, e.g. Coq with its quite
different foundations, if you take inductive definitions or recursive
functions, for example.
Makarius
Email Gateway (Aug 19 2022 at 10:21):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Mon, 04 Feb 2013 16:16:43 +0100, Makarius
<makarius@sketis.net> a écrit:
On Sat, 2 Feb 2013, Gottfried Barrow wrote:
I now ask, "Where is the semi-formal definition of a Isabelle type and
term?"If you said, "If you understand the HOL4 definitions of a type and
term, then you basically understand Isabelle's".See the Isabelle/Isar implementation manual chapter 2, about
Isabelle/Pure as reduced version of Higher-Order Logic to provide the
logical framework. This is occasionally interesting to know, although
just some tiny foundational bit. From Isabelle/Pure you move on to
Isabelle/HOL,
But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't it?
What is also interesting that the final end-user view tends to converge
to what totally different systems offer here, e.g. Coq with its quite
different foundations, if you take inductive definitions or recursive
functions, for example.
People seems to care, only when they have to port some proof from one
system to another. There seems to be multiple HOL4 to Isabelle papers on
the web, and seems all are concerned with foundations.
Email Gateway (Aug 19 2022 at 10:22):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/4/2013 9:16 AM, Makarius wrote:
On Sat, 2 Feb 2013, Gottfried Barrow wrote:
I now ask, "Where is the semi-formal definition of a Isabelle type
and term?"If you said, "If you understand the HOL4 definitions of a type and
term, then you basically understand Isabelle's".
See the Isabelle/Isar implementation manual chapter 2, about
Isabelle/Pure as reduced version of Higher-Order Logic to provide the
logical framework.
Makarius,
Thanks for the reference. A little guidance can go a long way. But, it
still gets unwieldy, so I quote from a cycling blog article,
http://inrng.com/2013/02/eurosport-david-harmon-interview/
In truth the greatest challenge is from having to deal with
performances unfolding in front of you that are just so astounding
and abnormal that you know precisely what's happening but you just
can't say it straight out. The list is endless; Rasmussen, Armstrong
and the Postals, Sella, Ricco, Mazzoleni... and on. I now confine
myself to saying "that was an unbelievable performance"...
What I know precisely is that the answer is spread out over multiple
documents, which was actually easy to know, just not easy to sort out.
I'm already past my word limit, so I try to implement a form of the
method from the quote.
The augmented question at hand: what is a "more formal" definition of a
Isabelle type, term, and formulae.
We start at the very bottom of page 27 and the first three lines of page
28 of isar-ref.pdf to give us a conceptual view of 3 important
meta-logic types: functions, universal quantification, and implication:
http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/isar-ref.pdf
On page 28, there's reference [5] to Stefan and Tobias' "Proof terms for
simply typed higher order logic", published 2000, where on page 2 of
that, there are semi-formal definitions of types, terms, and formulae,
where two of those important meta-logic types show up again, universal
quantification, and implication.
http://www4.in.tum.de/~berghofe/papers/TPHOLs2000.pdf
There are references [33,34] in isar-ref.pdf and [8,9] in "Proof terms"
to Larry's papers, where the one common reference is most applicable,
"The foundation of a generic theorem prover", published 1989.
http://arxiv.org/ftp/cs/papers/9301/9301105.pdf
Page 4 introduces types, terms, and formulae, along with three important
meta-logic constants, and then on page 7, the three meta-logic constants
are printed on 3 lines to emphasize them.
So, you look at the three different documents, read the three different
descriptions, look at the types of the meta-logic constants, read about
"prop" and "trueprop", and it might make more sense.
Interesting is that they all list implication and quantification, but
only Larry lists meta-logic equality.
But then things are more complex now, right? But another reference out
of those listed above is "Isabelle, a Generic Theorem Prover", published
1994.
http://www.amazon.com/Isabelle-Generic-Theorem-Lecture-Computer/dp/3540582444
And on page 5 they're already talking about type classes.
(Makarius writes)
This is occasionally interesting to know, although just some tiny
foundational bit. From Isabelle/Pure you move on to Isabelle/HOL,
then you add many add-on tools for 'inductive', 'datatype' etc. and
lots of proof tools like Sledgehammer. Then you are quite high above
the logical foundations and don't care much about them.
In another email, you made the analogy to being a Linux user. I think
the better analogy would be where 90% of the code is in C, but then
there's that occasional call into assembly language. If assembly
language is not a total mystery to you, you make tweak here or there.
Or maybe it's the VHDL analogy. You can read schematics, but that VHDL
that the PGA is programmed in, that really stumps you, and you come to a
grinding halt because that's not something you easily learn, and a lack
of understanding really limits your ability to understand the circuit.
Until the book "The Isabelle/Pure and Isabelle/HOL Logic, From Top to
Bottom, as Implemented in ML and Isar" comes out, every 4-6 months
someone will be asking, "Hey, what's Isabelle/Pure all about?"
But there's quite a bit of documentation to all this, or I wouldn't be
messing around with it.
Regards,
GB
What is also interesting that the final end-user view tends to
converge to what totally different systems offer here, e.g. Coq with
its quite different foundations, if you take inductive definitions or
recursive functions, for example.Makarius
Email Gateway (Aug 19 2022 at 10:23):From: "\"Mark\"" <mark@proof-technologies.com>
Makarius,
That was quite an aggressive email. I feel I have to respond to your points
in order to defend my work.
on 4/2/13 3:10 PM, Makarius <makarius@sketis.net> wrote:
I don't know anybody who really understands everything of Isabelle. But I
do understand its construction principles, and have a vague idea of the
vast space of possibilities resulting from it. This is just plain-old
modularity taken seriously.There is no need for users to understand everything. I use Linux everyday
without having a clue how it is done these days, although I know about
certain general principles as a mental model.
Yeah, but I'm talking here about people who, for whatever reason of their
own choosing, want to really understand how Isabelle works. I'm not talking
about "ordinary users".
But the main priorities for the implementors of Isabelle, as I
understand it, have been usability and power, and having an
understandable implementation comes way down the list.Understandable implementation is actually the main priority in Isabelle.
Otherwise this vast system could not be managed at all.
The main priority? I don't believe that! You've already said that you
don't understand everything. The extra layers that have been introduced
massively complicate the implementation, but are done with the good
intention of improving usability (and maybe other reasons as well). So, if
understandable implementation were the main priority then why on Earth
would this have been done?
This discussion has bounced between the HOL and Isabelle mailing lists
several times already. HOL Zero is as tiny that you see the problems
inherited from OCaml immediately.
As far as I understand, the only trustworthiness issue that you have with
HOL Zero is that it is implemented in OCaml. Firstly, HOL Zero addresses
the main OCaml vulnerabilities to do with string and integer representation,
and in any case can be relatively easily ported to SML, and I even intend to
do this at some stage, as you well know, so please stop banging on about
this. Secondly, the implementation language is secondary here. The primary
problem is designing and implementing a system that itself has no intrinsic
trustworthiness-related flaws. All other HOL systems other than HOL Zero
have not managed to do this because they have flaws in their pretty
printer/concrete syntax design. Their implementors either admit these flaws
or brush them under the carpet with "well normal users are not malicious so
would never in practice exploit these". Only HOL Zero has no such known
flaws, and it even has a bounty of $100 for anyone who can find one. So,
please, try to say something positive about HOL Zero's trustworthiness.
I would put more trust on OpenTheory right now.
It is a misconception that HOL Zero is competing with or incompatible with
Open Theory. HOL Zero is a HOL system. OpenTheory is a system for porting
theory and proofs between HOL systems (and perhaps other systems). Someone
could write an Open Theory importer or exporter for HOL Zero just as much as
for any other HOL system. If they did, this would boost the credibility of
OpenTheory.
But we don't have users in the queue to ask substantially more
trustworthyness than is there in Isabelle already. Most users actually
want less, but I have no inclination to reduce the general robustness of
Isabelle either.
Yes, there is no such queue of users. Isabelle quite rightly concentrates
on usability. This does not mean that I am wrong.
Mark.
Email Gateway (Aug 19 2022 at 10:23):From: Steven Ericsson-Zenith <steven@iase.us>
I'd say from the point of view of constructing real proofs this inaccessibility is a real problem. Are there proof statements concerning the formal properties of Isabelle?
Steven
Email Gateway (Aug 19 2022 at 10:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle has been developed over nearly 30 years, but with largely the same formalism; the only real changes have concerned polymorphism and type classes. Thanks to the LCF architecture, only a tiny percentage of the code has to be trusted. There are papers concerning formal properties of the basic calculus and some of its extensions, which should answer many specific questions. I would mention in particular the following papers:
L. C. Paulson.
The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397.
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.html
Markus Wenzel
Type classes and overloading in higher-order logic
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science Volume 1275, 1997, pp 307-322
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
Larry Paulson
Email Gateway (Aug 19 2022 at 10:23):From: Ramana Kumar <rk436@cam.ac.uk>
As someone who once attempted to write an exporter from Isabelle/HOL to
OpenTheory, I have to say that figuring out exactly what the primitive
inference rules for Isabelle/HOL are and how they are used is not an easy
thing.
I would anticipate it to be much easier for HOL Zero, and know it to be
fairly easy for HOL4 and HOL Light.
My attempt in Isabelle is on hold at the moment; the last thought was to
see if I could use the existing proof-recording technology (Berghofer et
al) and translate the proof terms it creates into OpenTheory proofs.
There have been some references and links in this thread that I haven't
examined in detail yet, though, so thanks.
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
On Tue, 5 Feb 2013, "Mark" wrote:
That was quite an aggressive email. I feel I have to respond to your
points in order to defend my work.
I don't know where you see the agression here. I am rather getting tired
about the topic, because it has made so little progress in the past 3
years, where it has occasionally shown up on the mailing lists.
You should also try to get Coq into the whole picture, because its user
base covers all of the HOLs and Isabelle taken together, and the system
and its logic is even more complex. So how about moving this thread to
coq-club as a change?
on 4/2/13 3:10 PM, Makarius <makarius@sketis.net> wrote:
This is just plain-old modularity taken seriously.
The main priority? I don't believe that! You've already said that you
don't understand everything. The extra layers that have been introduced
massively complicate the implementation, but are done with the good
intention of improving usability (and maybe other reasons as well).
It is important to discern complexity vs. complication. Isabelle was not
done the way like "this is a good day to introduce some new layers to
complicate things; we are so smart, and it was hard to write so it should
be hard to read".
On the contrary, the "layers" were always an answer to genuine
complication that had occumulated over time, to rationalize and
systematize concepts etc. Doing this sucessfully then turns complications
into mere complexity. And modularity taken seriously means you only need
to understand layers separately and the principles of composition, but not
the whole of the result.
So, if understandable implementation were the main priority then why
on Earth would this have been done?
To keep the system alive and thriving over a very long time, with ever
growing demands from the applications. Isabelle has an unbroken tradition
of more than 25 years, always with the same code-base. Internally it
looks rather young, fresh, and clean, if you compare it to other systems
of such an age. For example, I am now routinely exposed to Java and its
standard libraries, and that is really complicated, not just complex.
As far as I understand, the only trustworthiness issue that you have with
HOL Zero is that it is implemented in OCaml. Firstly, HOL Zero addresses
the main OCaml vulnerabilities to do with string and integer representation,
and in any case can be relatively easily ported to SML, and I even intend to
do this at some stage, as you well know, so please stop banging on about
this.
The string and int problem is a good example for genuine complication: you
have to "repair" bad effects from OCaml, but you don't want that extra
stuff there. The Coq guys have quite a few such repairs of OCaml in their
code. To make HOL Zero on OCaml really bullet-proof you would probably
have to blow up the kernel by a factor of 2 compared to a pure version,
lets say in SML, or even HOL as specification language.
I have pointed out further nasty tricks of OCaml occasionally, where you
simply cannot trust your eyes reading the OCaml source. Some LRI guys are
particularly good at playing such tricks and proud of it.
The primary problem is designing and implementing a system that itself
has no intrinsic trustworthiness-related flaws. All other HOL systems
other than HOL Zero have not managed to do this because they have flaws
in their pretty printer/concrete syntax design. Their implementors
either admit these flaws or brush them under the carpet with "well
normal users are not malicious so would never in practice exploit
these".
I am one of thos who brush it under the carpet, because it is no real
problem in practice, but there are others. Pinning down parsing / pretty
printing like that is neither necessary nor sufficient for
trustworthiness.
I did see real issues in a different area, e.g. when Oracle (via the JVM)
bombs your GUI display somehow, so that you see an outdated version of
prover output. But the HOL-Zero approach does not cover prover IDE
connectivity at all.
Makarius
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
On Tue, 5 Feb 2013, Ramana Kumar wrote:
As someone who once attempted to write an exporter from Isabelle/HOL to
OpenTheory, I have to say that figuring out exactly what the primitive
inference rules for Isabelle/HOL are and how they are used is not an
easy thing.
It is important to understand Isabelle/HOL as an application of the
Isabelle framework (a very large and important one), not as a variant of
"HOL", like HOL4, HOL-Light, HOL-XYZ. I am not surprised that it was
difficult to see the logical content there in the belly of Isabelle, if
you are expecting it to be just like "HOL".
My attempt in Isabelle is on hold at the moment; the last thought was to
see if I could use the existing proof-recording technology (Berghofer et
al) and translate the proof terms it creates into OpenTheory proofs.
There have been some references and links in this thread that I haven't
examined in detail yet, though, so thanks.
The proof terms by Stefan Berghofer are indeed the main starting point.
This aspect of Isabelle has been refined several times over the years, the
last time in Spring 2010 when we tried hard to make everything exportable
in principle, but the practical proof of it was still missing. Since then
there was a lack of significant applications, to justify spending too much
time there.
Someone interested in Open Theory output should look there again.
Makarius
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
On Mon, 4 Feb 2013, Gottfried Barrow wrote:
The augmented question at hand: what is a "more formal" definition of a
Isabelle type, term, and formulae.We start at the very bottom of page 27 and the first three lines of page 28
of isar-ref.pdf to give us a conceptual view of 3 important meta-logic types:
functions, universal quantification, and implication:http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/isar-ref.pdf
On page 28, there's reference [5] to Stefan and Tobias' "Proof terms for
simply typed higher order logic", published 2000, where on page 2 of that,
there are semi-formal definitions of types, terms, and formulae, where two of
those important meta-logic types show up again, universal quantification, and
implication.http://www4.in.tum.de/~berghofe/papers/TPHOLs2000.pdf
There are references [33,34] in isar-ref.pdf and [8,9] in "Proof terms" to
Larry's papers, where the one common reference is most applicable, "The
foundation of a generic theorem prover", published 1989.http://arxiv.org/ftp/cs/papers/9301/9301105.pdf
Page 4 introduces types, terms, and formulae, along with three important
meta-logic constants, and then on page 7, the three meta-logic constants are
printed on 3 lines to emphasize them.So, you look at the three different documents, read the three different
descriptions, look at the types of the meta-logic constants, read about
"prop" and "trueprop", and it might make more sense.Interesting is that they all list implication and quantification, but only
Larry lists meta-logic equality.
All of the above are important references about Isabelle/Pure.
Generally, you always need to put things into the context of who is
writing when -- there different ways to explain things, which also tend
to change over time. For example, I always follow the advice by Stefan
Berghofer from 2000 to say "logical framework" and not "meta-logic": Pure
gives you so little to speak about other logics, e.g. no induction on the
object-logic formulation.
The == connective of Pure is hardly relevant for users now, it serves
mainly foundational purposes, so it appears later in my exposition in the
"implementation" manual. And there are more important add-on constants in
Isabelle/Pure, like conjunction or funny prop markers.
For users mainly => !! ==> are relevant, to express the structure of your
abstract syntax and rule statements.
But then things are more complex now, right? But another reference out of
those listed above is "Isabelle, a Generic Theorem Prover", published 1994.http://www.amazon.com/Isabelle-Generic-Theorem-Lecture-Computer/dp/3540582444
And on page 5 they're already talking about type classes.
That is now really really old. I feel nostalgic about the "3 standard
Isabelle manuals" that were pasted together for the 1994 LNCS volume.
Things have changed a lot since then, both the system and the way it is
explained. Type classes are not as trivial as they were looking in 1992,
so you can't just introduce them in passing right at the start of an
arbitrary Isabelle manual.
What I sometimes do is to show a canonical application of type classes to
beginners, e.g.
http://isabelle.in.tum.de/dist/library/HOL/Isar_Examples/Group.html
This looks simple and obvious, and people learn something they can re-use
later. It is very far removed from the actual logical foundation of type
classes, though. Lots of "layers" around the raw logic at the bottom.
Makarius
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
On Mon, 4 Feb 2013, Yannick Duchêne (Hibou57) wrote:
See the Isabelle/Isar implementation manual chapter 2, about Isabelle/Pure
as reduced version of Higher-Order Logic to provide the logical framework.
This is occasionally interesting to know, although just some tiny
foundational bit. From Isabelle/Pure you move on to Isabelle/HOL,But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't it?
Isabelle/HOL is an application within Isabelle/Pure. Isabelle/Pure has
some magic bootstrapping to get the core logical framework with lots of
add-on infrastructure for Isabelle/ML in place. This magic stops just
after loading the Pure.thy and shipping the result as "Isabelle/Pure"
image. Then comes HOL and loads tons of conventional Isabelle theories
and tool implementations on top, and ships that as "Isabelle/HOL" image.
So in some sense Isabelle/HOL is indeed derived from Isabelle/Pure, for a
suitable definition of "derived".
What is also interesting that the final end-user view tends to converge
to what totally different systems offer here, e.g. Coq with its quite
different foundations, if you take inductive definitions or recursive
functions, for example.People seems to care, only when they have to port some proof from one
system to another. There seems to be multiple HOL4 to Isabelle papers on
the web, and seems all are concerned with foundations.
These converters usually try to convert the "object-code". There are
interesting ongoing projects like
https://www.rocq.inria.fr/deducteam/Dedukti/ with potentially interesting
applications of moving huge lambda terms back and forth between systems.
The high-level problem of moving huge applications from prover X to prover
Y is not addressed at all.
Makarius
Email Gateway (Aug 19 2022 at 10:25):From: Ramana Kumar <rk436@cam.ac.uk>
On Wed, Feb 6, 2013 at 2:49 PM, Makarius <makarius@sketis.net> wrote:
On Tue, 5 Feb 2013, Ramana Kumar wrote:
As someone who once attempted to write an exporter from Isabelle/HOL to
OpenTheory, I have to say that figuring out exactly what the primitive
inference rules for Isabelle/HOL are and how they are used is not an easy
thing.
It is important to understand Isabelle/HOL as an application of the
Isabelle framework (a very large and important one), not as a variant of
"HOL", like HOL4, HOL-Light, HOL-XYZ. I am not surprised that it was
difficult to see the logical content there in the belly of Isabelle, if you
are expecting it to be just like "HOL".
I was not at all expecting it to be like the other implementations of HOL.
I am aware of the Isabelle framework. However, I was expecting to find
something resembling higher-order logic, that is, the logic Isabelle/HOL
purports to implement. The way that is put together using the framework is
still somewhat obscure to me, and there is no one reference to learn about
it. However there are plenty I should read more of.
My attempt in Isabelle is on hold at the moment; the last thought was to
see if I could use the existing proof-recording technology (Berghofer et
al) and translate the proof terms it creates into OpenTheory proofs.
There have been some references and links in this thread that I haven't
examined in detail yet, though, so thanks.
The proof terms by Stefan Berghofer are indeed the main starting point.
This aspect of Isabelle has been refined several times over the years, the
last time in Spring 2010 when we tried hard to make everything exportable
in principle, but the practical proof of it was still missing. Since then
there was a lack of significant applications, to justify spending too much
time there.Someone interested in Open Theory output should look there again.
Makarius
Email Gateway (Aug 19 2022 at 10:26):From: Makarius <makarius@sketis.net>
On Wed, 6 Feb 2013, Ramana Kumar wrote:
I was not at all expecting it to be like the other implementations of
HOL. I am aware of the Isabelle framework. However, I was expecting to
find something resembling higher-order logic, that is, the logic
Isabelle/HOL purports to implement.
That is in principle src/HOL/HOL.thy, which is based on the original
Cambridge HOL report by Mike Gordon. Note that some of the axiomatic bits
have been moved to other Isabelle theories over the years, such as Hilbert
choice to src/HOL/Hilbert_Choice.thy.
The way that is put together using the framework is still somewhat
obscure to me, and there is no one reference to learn about it.
But this is where things really happen, and what makes the difference.
Rules are specified as "axioms" in user-space, and the system composes
them according to the principles introduced by Larry Paulson 25 years ago.
Makarius
Email Gateway (Aug 19 2022 at 10:26):From: "\"Mark\"" <mark@proof-technologies.com>
on 6/2/13 2:41 PM, Makarius <makarius@sketis.net> wrote:
I don't know where you see the agression here. I am rather getting tired
about the topic, because it has made so little progress in the past 3
years, where it has occasionally shown up on the mailing lists.
But Makarius, I merely mentioned Isabelle's priorities, to help explain some
background about its complexity. You then questioned HOL Zero's
trustworthiness, then I responded. So if you're getting tired of the
trustworthiness issue, then don't bring it up.
So, if understandable implementation were the main priority then why
on Earth would this have been done?To keep the system alive and thriving over a very long time, with ever
growing demands from the applications. Isabelle has an unbroken tradition
of more than 25 years, always with the same code-base. Internally it
looks rather young, fresh, and clean, if you compare it to other systems
of such an age. For example, I am now routinely exposed to Java and its
standard libraries, and that is really complicated, not just complex.
My point is that these changes, with their best of intentions, dominate the
implementation of Isabelle and yet make the implementation harder to
understand. Therefore understandable implementation cannot be Isabelle's
main priority over the years. The main priorities are things that are
driving these changes.
The primary problem is designing and implementing a system that itself
has no intrinsic trustworthiness-related flaws. All other HOL systems
other than HOL Zero have not managed to do this because they have flaws
in their pretty printer/concrete syntax design. Their implementors
either admit these flaws or brush them under the carpet with "well
normal users are not malicious so would never in practice exploit
these".I am one of thos who brush it under the carpet, because it is no real
problem in practice, but there are others. Pinning down parsing / pretty
printing like that is neither necessary nor sufficient for
trustworthiness.
Pretty printing is very strongly related to trustworthiness! If the pretty
printer prints one thing but internally it's something else, then the user
gets misled about what has been proved and/or what has beed defined. I have
known examples on real industrial safety-critical projects where this has
caused problems. It doesn't get much more serious than that.
I did see real issues in a different area, e.g. when Oracle (via the JVM)
bombs your GUI display somehow, so that you see an outdated version of
prover output. But the HOL-Zero approach does not cover prover IDE
connectivity at all.
Because these are all secondary issues, i.e. issue in the programs that fit
around the theorem prover rather in the theorem prover itself. I'll say it
again, the primary trustworthiness issue in theorem prover implementation is
designing and implementing a system that itself has no intrinsic
trustworthiness-related flaws. LCF-style architecture gets us a long way on
this count, but is not the end of the story because it does not address
pretty printer issues.
Mark.
Email Gateway (Aug 19 2022 at 10:26):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
What is “LRI” please?
Email Gateway (Aug 19 2022 at 10:26):From: Yannick <yannick_duchene@yahoo.fr>
Isn't it what OpenTheory is for? Or I may have not understand what it is;
will get time to have a real look at it later.
Email Gateway (Aug 19 2022 at 10:26):From: Makarius <makarius@sketis.net>
French habit of making long complicated expressions short: Laboratoire de
Recherche en Informatique, i.e. the CS lab at Paris Sud.
The coffee room of the lab is sometimes an exchange point for the latest
OCaml tricks -- there are many power users of it. Historically, the lab
was also one of the originators of Coq, but that is now mainly done at LIX
and PPS/Pir2 -- yet more odd abbreviations (you are French yourself, so
you should know).
And of course, Coq is not untrustable just because it is using OCaml.
The French colleagues understand the problems and made their homework, but
it also introduces complexities. People like Bruno Barras could tell you
more.
So maybe that is now the point for Mark Adams to move this never-ending
thread to coq-club to see how they react about high-end provers having to
be simplistic.
Makarius
Email Gateway (Aug 19 2022 at 10:27):From: Lawrence Paulson <lp15@cam.ac.uk>
I gather that the Coq kernel also contains a big chunk of C code. Surprising, to say the least.
Larry
Email Gateway (Aug 19 2022 at 10:27):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:
Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#
(the page also has a link at the top, for a PDF version)
There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".
http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/
When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".
If you keep talking long enough, another one might pop in and throw in
the term "type classes".
Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.
For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.
If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".
https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types
Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.
For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:
http://hol.sourceforge.net/documentation.html
For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:
simply-typed : (adj) Relating to type systems that are relatively simple and
are not, for example, dependently-typed. There is considerable variation in the
precise intended meaning of "simply-typed" in contemporary usage: in some usages
polymorphism is not a disqualifying factor, in other usages polymorphism is only
a disqualifying factor if it caters for the quantification of type variables,
and in other usages still any form of polymorphism is a disqualifying factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.
Still looking at Gottfried's list.
In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.
Regards, GB
http://www.phil.cmu.edu/~avigad/formal/
http://www.andrew.cmu.edu/user/avigad/isabelle/
http://www4.in.tum.de/~ballarin/belgrade08-tut/
http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php
http://isabelle.in.tum.de/coursematerial/IJCAR04/
http://archiv.infsec.ethz.ch/education/permanent/csmr.html
http://isabelle.in.tum.de/exercises/
http://www.irisa.fr/celtique/genet/ACF/
http://dream.inf.ed.ac.uk/projects/isabelle/
http://isabelle.in.tum.de/coursematerial/PSV2009-1/
http://www21.in.tum.de/teaching/logik/SS12/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/
http://www.cs.colorado.edu/~siek/7000/spring07/
http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html
http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php
http://www.lri.fr/~wenzel/Isar2010-Orsay/
http://www.lri.fr/~wenzel/Isabelle2011-Paris/
http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/
http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/
Email Gateway (Aug 19 2022 at 13:06):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I'm adding this one:
“What does one need, when she needs higher‑order logic”?
http://jarda.peregrin.cz/mybibl/PDFTxt/484.pdf
It's about cases where a translation from second/higher order to first
order is possible; which may be seen as a way to get a strict
identification of what's unique to orders above the first.
Unfortunately, it's not easy to read (at least to me), as it refers to
example predicates which seems to be defined elsewhere.
Email Gateway (Aug 19 2022 at 13:08):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
From the same author (W. M. Farmer), an academic course (link below) I
landed into. Its wordings in chapter 5, made me feel I've read something
like this before… indeed, as I checked, this was in the Seven Virtues of
STT.
http://imps.mcmaster.ca/courses/SE-2F03-05/slides/
Chapter 5 concisely explains (to me, even more concisely than in the Seven
Virtues) many of the theoretical concepts found in Isar‑Ref and the
Isabelle Tutorial (for people like me who are not from the academic
world). He's a lot fan of the type theory.
Interestingly, at the end, he suggest an extension of STT, which would
include indefinite expressions, which seems to be the same as what
shown‑up during another topic with references to HOL+LCF as HOLCF (an
Isabelle theory).
Email Gateway (Aug 19 2022 at 13:08):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, the question of whether or not to adopt an explicit logic of “definedness” continues to attract discussion. Most implemented formal systems have only total functions. Then there is PVS and the dependently-typed calculi, which allow partial functions but still don’t formalise the notion of “undefined”. I believe that Farmer advocates such formalisms. LCF and related systems formalise domain theory, in which the concept of definedness induces a partial ordering over all values. As always, increasing the expressiveness of the formalism also increases the difficulty of conducting proofs.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:17):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Fri, 01 Feb 2013 15:22:53 +0100, Gottfried Barrow
<gottfried.barrow@gmx.com> a écrit:
[…]
For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to
learn about HOL4's formal logic:
The one titled “Logic” (file name “kananaskis-8-logic.pdf”) still says in
the preface:
This material was written by Andrew Pitts in 1991, and was
originally part of DESCRIPTION. Because this logic is shared
with other theorem-proving systems (HOL Light, ProofPower),
and is similar to that implemented in Isabelle, where it is
called Isabelle/HOL, it is now presented in its own manual.
Email Gateway (Aug 19 2022 at 13:30):From: IG BI <igbi@gmx.com>
/From/: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr
<mailto:yannick_duchene@DOMAIN.HIDDEN>>
What is perfect will vary according to need. The HOL4 logic manual is
imperfect for a perfect understanding of Isabelle/HOL, and also of
Isabelle/Pure, because HOL4 is only similar to what is implemented in
Isabelle. Significant differences are that with Isabelle there are two
logics, along with type classes.
To set the stage, I repeat a variation of a question I've asked in the
past, and I state a law.
QUESTION_1: Where is the BNF grammar, or similar grammar, that precisely
states what a typed lambda calculus term is in Isabelle/Pure and
Isabelle/HOL?
QUICK_COMMENT: Such a grammar might immediately answer certain
questions, such as whether an Isabelle/Pure term is identical to an
Isabelle/HOL term. Here, I explicitly differentiate between Pure and HOL
because of a paper by Wenzel in which he emphasizes that there are two
HOLs in Isabelle. I reference the paper below.
LAW OF RIGOR: If you don't have the time to treat a formal, mathematical
topic with proper rigor, then do your best to never mention the topic,
lest you be accused of being a non-rigorous arm-waver. If you must
discuss the topic, then give the shortest, possible overview of the
topic, to make it obvious that the overview is not a formal treatment of
the topic.
I assume that the Law of Rigor is one reason why the grammar I mention
above doesn't exist for the current state of the Isabelle art, though
such a thing may actually exist. Simple questions such as "Where is such
and such?", when such and such is somewhere, are many times not
answered. Such is life.
I say here that I've found several, older documents in which a type and
term was defined for the state of the Isabelle art at that time. I
reference those documents below.
COMPLEX TYPED TERMS, NO MOTIVE TO SORT THROUGH A SIMILAR GRAMMAR
Back to the HOL4 logic manual, on page 8 there is the phrase "[a] more
accurate grammar of terms is", and then he gives a grammar which we must
sort through using previously defined grammars, along with more formal
discussion.
It would be doable, if I was willing to expend enough brain waves, but
it would never get me an exact understanding of what an Isabelle/Pure
and Isabelle/HOL term is.
I now use my first-order logic analogy. At the point I understood
Bilaniuk's definitions 5.1, 5.2, and 5.3 to define the symbols, terms,
and formulas of a first-order language, the definition of a first-order
language ceased to be Ph.D. level knowledge for me. If I completely
understand those definitions, how can it be Ph.D. level knowledge? I
don't have a Ph.D.
I bring the first-order logic analogy to an end prematurely to keep
things shorter, lamenting that I must sacrifice what would've been the
most intellectually stimulating rhetoric of my whole life (a joke? no,
no joke), but I also consider the upside of not having to type 800 more
characters. It's six of one, or a half dozen of the other, as they say.
Economically speaking, we can equate the most intellectually stimulating
rhetoric of my whole life with the time I would have spent typing 800
more characters, minus the number of characters in this sentence.
Anyway, I already know that terms have types, and types have types. I
don't see any purpose in straining my brain to study something like the
HOL4 grammar to only end up understanding, a bit better, that terms have
types and types have types. When an authority on Isabelle publishes the
grammar of QUESTION_1 above, then it's worth putting out that kind of
effort.
SOME ISABELLE SOURCE BEFORE SOME ORIGINAL SOURCES
Frequently, I've seen it stated that Isabelle is simply typed lambda
calculus. Here, I'd like to make the point that the definition of a
lambda calculus term is fairly simple, which I do to compare its
simplicity to a typed lambda calculus term, which is not simple.
Consider the following:
term "x::(('a::{type,equal,ord}) list)"
Understanding the typing of concrete examples like this is
straightforward, though partly straightforward because I can use the
PIDE to show me what some of the inferred typing is.
What the example shows is that the general case for a typed term is not
simple at all. There are four things that can vary there: variable, type
variable, type variable type (the type class), and type constructor.
SOME ORIGINAL SOURCES
Your recent question about sorts led to me sorting through some
bibliographies again:
Re: [isabelle] Are sorts of Isabelle the same as what's described for
second order logic?
I've decided the available documentation of Isabelle can be described as
"30 documents spread over 20 years". There is the question of which is
more difficult:
1) Is it more difficult for me to understand involved explanations about
how typing works, where some of the names for the types are outdated,
and the definitions are mainly formatted in paragraph form, rather than
formatted in a BNF grammar type style?
2) Or, is it more difficult for me to remember where the difficult
passages are in the 30 documents spread out over 20 years?
I list in chronological order some documents I've sorted through, and
make some comments:
1987: LOGIC AND COMPUTATION, INTERACTIVE PROOF WITH CAMBRIDGE LCF
By L. C. Paulson
Published by Cambridge Tracts in hardcopy form.
Section 5.1.3 contains a BNF syntax for types, and 5.1.4 has one for
terms. The book is pretty much a textbook style book. The first part of
the book teaches some basic logic, such as natural deduction and sequent
calculus.
I guess after the first time a person does that, the motivation to
repeatedly teach the basics decreases over time.
1994: ISABELLE, A GENERIC THEOREM PROVER
by Lawrence Paulson, with Contributions by Tobias Nipkow
Published by Springer-Verlag in hardcopy form.
This book was broken up into 5 documents, and distributed with the
Isabelle distribution. I looked at Isabelle1999-2 to Isabelle2008. The
PDFs for a long time were intro, logics, logics-HOL, logics-ZF, and ref.
The ref document stayed mostly the same up until 2008, after which it
started to be subsumed by other documents. With Isabelle2013-2, it's
completely gone.
Of note is that the page count of intro.pdf, the old intro, has stayed
at about 77 pages from 1999 to 2013-2:
http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/intro.pdf
Section 1.2 discusses type classes, and even explains the empty sort.
This seems to be an important document.
Possibly, some type names have changed. I've been wondering what the
type of "int" is, because the PIDE doesn't show it has a type with this:
term "a::int"
Section 1.2 tells me that the type of the "int" constructor is "term". I
don't ever see that in the PIDE.
1995: TYPE RECONSTRUCTION FOR TYPE CLASSES
by Tobias Nipkow and Christian Prehofer
http://www21.in.tum.de/~nipkow/pubs/jfp95.html
There's a grammar for a Mini-Haskell on page 3.
If someone told me, "The Mini-Haskell syntax basically describes a
Isabelle/HOL term", I'd say, "Great, so go ahead and modify it so that I
know exactly what a Isabelle/HOL term is, rather than basically know. I
wouldn't understand it at first, but an important starting point is
having a precise definition."
1997: TYPE CLASSES AND OVERLOADING IN HIGHER-ORDER LOGIC
by Makarius Wenzel
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
Here Makarius, in several ways, treats Isabelle/Pure as the HOL to be
considered, rather than Isabelle/HOL. He says,
As a quite harmless simplification, HOL can be identified directly
with Isbelle/Pure.
The consequence for me is that I now want to see a precise definition
for a typed term for both Isabelle/Pure and Isabelle/HOL. It might help
me see a difference that's important, that I otherwise wouldn't see.
In section 3.1 HOL Syntax, he quickly describes the HOL types and terms.
OUTRO
I have a better understanding now that terms have types and types have
types. I'm better now at understanding what I see when I have show_sorts on.
Below, I include some of what I was looking at. I was mainly interested
in looking at the types "type" and "{}".
Regards,
GB
(******************)
theory i140105a
imports Complex_Main
begin
declare[[show_sorts=true]]
declare[[show_brackets=true]]
(*OBJ_EXP_1: lambda calculus terms are simple, but typed Isabelle/HOL
terms are
complex. Four things are involved here: variable, type variable, type
variable
type (the type variable type class), and type constructor. Does the type
constructor 'list' also have a type?
*)
term "x::(('a::{type,equal,ord}) list)"
(*OJB_EXP_2: Do type variable constants such as 'int' have a type? Type
variable constants such as 'int' aren't displayed as having type. But in
Coq,
type constants have a type, such as "nat:Set":
http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C5.pdf
I think that int is a 0-ary type constructor. If so, the basic question
is the
same. Do 0-ary type constructors have a type?
*)
term "x::int" (Displayed: "(x::int)"::int.)
(*EXP_3: Inferred: x::('a::{})
*)
term "x"
term "x::('a::{})"
(*META_EXP_4: Inferred: x::('a::{}).
*)
term "x == x"
theorem "x == x"
by(simp)
theorem "x == (x::('a::{}))"
by(simp)
(*OBJ_EXP_5: Type: x::('a::ab_semigroup_add).
*)
theorem "(x::('a::{type, plus, semigroup_add, ab_semigroup_add})) = x"
by(simp)
(*OBJ_EXP_6: Type: x::('a::{plus,equal}).
*)
theorem "(x::('a::{plus,equal})) = x"
by(simp)
(*META_EXP_7: Inferred: x::prop. There is no type variable.
*)
term "PROP x"
theorem "PROP x == PROP x"
by(simp)
(*OBJ_EXP_8: Inferred: x::('a::type).
*)
term "x = x"
theorem "x = x"
by(si
[message truncated]
Last updated: Apr 24 2024 at 20:16 UTC