Email Gateway (Aug 19 2022 at 11:45): Email Gateway (Aug 19 2022 at 11:45):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/3/2013 12:04 PM, Makarius wrote:
On Tue, 3 Sep 2013, Gottfried Barrow wrote:
I care about the operator "==", and over the months, Makarius has
made a number of comments deemphasizing it, and the comments below
indicate something similar. I don't see how "==" could be gotten rid
of from Isar, but what do I know?The operator "==" will forever be an Isar operator, won't it?
...What exactly do you mean by "==" as Isar operator? It belongs to
Pure, not Isar. So it is not an Isar operator now, and will never be.
But it is Isar. Anything between "theory" and "end" in a THY is Isar. I
quote from an authority on Isar, you, in
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-August/msg00037.html
:
* The content of a theory file between 'theory' and the final 'end'
is by
definition the Isar source language.
If you mean this Isar command:
def x == "t"
No. What's being talked about on [isabelle-dev] and what I'm thinking
about are apparently two different things. I'd say I'm wasting your
time, but you've belittled "==" almost every time it's listed as one of
the meta-operators in a discussion. Belittling a feature can precede a
feature being eliminated.
To finish this perspective of more flexibile local definitions within
proofs, in conformance to 'definition' for local theories, the general
form would be like this:define f where "f x y z = t" for x y z
I'm wasn't talking about proofs, but having to use any HOL operator,
such as "=", is what I don't want to be forced to use. I'm talking about
using "==" in "definition" and the statement of a theorem with "lemma"
or "theorem".
This next definition is what I'm talking about, which is the one single
definition I need to mess around with meta-logic in Isabelle/HOL, and
keep it separate from the object-logic:
definition MFalse :: "prop" where
"MFalse == (!!P. PROP P)"
Nothing of that old cleanup plan is imminent, not for the coming release.
My paranoia is a result of you telling me several times that I should be
working at the object-logic level, rather than the meta-logic level. I
don't care if you tell me that, but I'd hate to be forced to always work
at the object-logic level soley because that's what you think I should do.
I'm imagining some 2-year plan by the devs to push the meta-logic
operators down and out of Isar. I don't want to put 6 months and more of
work into developing a bunch of meta-logic, if I know it's going away.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:48):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'll generalize this comment thread I started, and here I'll play the
part of Joe User Advocate. The details I was talking about are covered
by this generalization, and after this I'll just take what comes. I
don't expect any changes to be withheld because of me, and I'm basically
going to start making all my plans based on what the next release is.
Maybe two weeks ago, my perception was that Isabelle2012 is a prime-time
product, not a throw-away research product, as it's been described in
the past by one of the primary developers.
Today, I'm thinking about two points, based on how I've seen changes
implemented:
1) For Isabelle/HOL, there is zero commitment to backwards compatibility
by the developers.
2) For Isabelle/HOL, there is no long term, future forecasts published
by the developers so that users can plan for the future, to help users
not get tied into things which are going to disappear.
Here, I'm reminded of an email by a user about three months ago who had
put a lot of work into a version such as Isabelle2009, but who is now
out of luck with the new versions. Change is necessary, but I take that
as a lesson for what's coming down the road for me.
Formalizing math is a multi-year project, like a 10, 20, or 30 year
project. From today, I estimate that in five years, I might have
something that's worthwhile. I don't want to put a year or more of work
into something, and then not be able to use it.
The short story is that I've decided that I could get locked into
Isabelle2012 today, and it would get me through another 20 years,
running either on Windows, Linux, or on VirtualBox. Being prepared to
get locked into any version is my solution to 1) and 2) above.
I would lose the ability to coordinate what I do with others, but I'm my
own highest priority. I don't have to wonder whether the ZFC axioms are
going to be the same in 6 months, so I'm not going to stay in some
constant state of flux as far as the software.
My suggestion is that a running, multi-year forecast of changes be
published, to help other Joe Users get a feel for the future.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:53):From: Makarius <makarius@sketis.net>
On Tue, 3 Sep 2013, Gottfried Barrow wrote:
The operator "==" will forever be an Isar operator, won't it?
...What exactly do you mean by "==" as Isar operator? It belongs to Pure,
not Isar. So it is not an Isar operator now, and will never be.But it is Isar. Anything between "theory" and "end" in a THY is Isar. I quote
from an authority on Isar, you, in
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-August/msg00037.html
:* The content of a theory file between 'theory' and the final 'end'
is by
definition the Isar source language.
That is indeed true for the outermost language of Isabelle/Isar, but there
there are several languages embedded into that (potentially recursively),
e.g. the languages of types, terms, theorems of the logical environment
(Isabelle/Pure or Isabelle/HOL or whatever), or Isabelle/ML, or Isabelle
document source.
I'm wasn't talking about proofs, but having to use any HOL operator,
such as "=", is what I don't want to be forced to use. I'm talking about
using "==" in "definition" and the statement of a theorem with "lemma"
or "theorem".
That was not really on the thread that you have seen on isabelle-dev.
Basic == of Isabelle/Pure is perfectly adequate for situations where you
make Pure definitions, e.g. like this:
definition MFalse :: "prop" where
"MFalse == (!!P. PROP P)"
When you work in Isabelle/HOL, what most users do most of the time, it is
better to use its plain =, though. This helps to make specifications and
proofs uniform and with reduced surprise of proof tools that cannot cope
with pure == (e.g. certain calculation reasoning rules in HOL).
My paranoia is a result of you telling me several times that I should be
working at the object-logic level, rather than the meta-logic level. I
don't care if you tell me that, but I'd hate to be forced to always work
at the object-logic level soley because that's what you think I should
do.
The general principle is: the right tool for the right job. When you work
in Isabelle/Pure directly, without Isabelle/HOL, then == is fine, and in
fact the only option for actual "meta" definitions.
Other object-logics like Isabelle/ZF cannot internalize all definition
forms into their own = and sometimes have to evade into Pure for that, but
this extra complication is not needed in Isabelle/HOL.
Makarius
Email Gateway (Aug 19 2022 at 11:53):From: Makarius <makarius@sketis.net>
On Tue, 3 Sep 2013, Gottfried Barrow wrote:
Maybe two weeks ago, my perception was that Isabelle2012 is a prime-time
product, not a throw-away research product, as it's been described in
the past by one of the primary developers.
Does it mean you are not converted to Isabelle2013 yet? Isabelle release
cycles are done such that the least painful way to upgrade is to do that
continuously. The amount of incompatibilities in each release is usually
limited to something that works out for most applications.
Today, I'm thinking about two points, based on how I've seen changes
implemented:1) For Isabelle/HOL, there is zero commitment to backwards compatibility by
the developers.2) For Isabelle/HOL, there is no long term, future forecasts published by the
developers so that users can plan for the future, to help users not get tied
into things which are going to disappear.
You should say "Isabelle" in general, not Isabelle/HOL (before you have
pointed out an interest to work directly with Isabelle/Pure, ignoring the
huge Isabelle/HOL library).
I am myself involved in Isabelle only since 1993, but I've never seen a
commitment to "backwards compatibility". Instead there has always been a
natural flow of updating the system technically, conceptually, introducing
new things, discontinuing old things (the latter requires a lot of work).
Without that principle, Isabelle2012 would not have been as nice as it was
last year (now Isabelle2013 is nicer). You may also browse through the
recorded history to see yourself if you want to stack back in 1993:
http://isabelle.in.tum.de/repos/isabelle/file/831a9a7ab9f3
or lets say 1998:
http://isabelle.in.tum.de/repos/isabelle/file/be6b5edbca9f
The 1998 vintage was actually an exceptionally good one.
Here, I'm reminded of an email by a user about three months ago who had put a
lot of work into a version such as Isabelle2009, but who is now out of luck
with the new versions. Change is necessary, but I take that as a lesson for
what's coming down the road for me.
Isabelle2009 was a long time ago. People who don't mange to keep
up-to-date all the time can put their material into shape for AFP, where
it usually gets updated "automagically".
My suggestion is that a running, multi-year forecast of changes be
published, to help other Joe Users get a feel for the future.
You can look at Isabelle/NEWS to get a feeling for the continuity of
changes in Isabelle, and project them into the future.
If I compare this to the Java distribution that is even a bit younger than
Isabelle, I wonder which project turns out as more professional and
reliable in the end.
E.g. see http://openjdk.java.net/projects/jdk8/ for the precise forecast
that has been changed so many times. Tomorrow should be the "Developer
Preview" of Java 8, and if it happens I expect it to have most of the
old problems of Java 7 again, in perfect backwards compatibility.
Makarius
Email Gateway (Aug 19 2022 at 11:53):From: Makarius <makarius@sketis.net>
For the full fun of browsing ancient Isabelle/HOL sources, one needs to
include this annex to the history (which was cut out from the CVS tree at
some point): http://isabelle.in.tum.de/repos/Old_HOL/
For example
http://isabelle.in.tum.de/repos/Old_HOL/annotate/14b9286ed036/llist.ML
shows that what is now src/HOL/List.thy has always been "TOO LONG! needs
splitting up" (according to Larry Paulson 1993-09-22).
Makarius
Email Gateway (Aug 19 2022 at 11:53):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
To me, llist.ML looks more like the construction of coinductive lists. This later became
LList.thy in HOL/Induct and has been dropped after Isabelle 2009 in favour of the AFP
entry Coinductive.
Andreas
Email Gateway (Aug 19 2022 at 11:53):From: Makarius <makarius@sketis.net>
On Wed, 4 Sep 2013, Andreas Lochbihler wrote:
On 04/09/13 14:49, Makarius wrote:
On Wed, 4 Sep 2013, Makarius wrote:
or lets say 1998:
http://isabelle.in.tum.de/repos/isabelle/file/be6b5edbca9f
The 1998 vintage was actually an exceptionally good one.
For the full fun of browsing ancient Isabelle/HOL sources, one needs to
include this annex
to the history (which was cut out from the CVS tree at some point):
http://isabelle.in.tum.de/repos/Old_HOL/For example
http://isabelle.in.tum.de/repos/Old_HOL/annotate/14b9286ed036/llist.ML
shows
that what is now src/HOL/List.thy has always been "TOO LONG! needs
splitting up"
(according to Larry Paulson 1993-09-22).
To me, llist.ML looks more like the construction of coinductive lists.
You are right. Strangely I can't see a List.thy in that view of the
history. Here is a more complete one:
http://isabelle.in.tum.de/repos/Old_HOL/file/c3913a79b6ae
This later became LList.thy in HOL/Induct and has been dropped after
Isabelle 2009 in favour of the AFP entry Coinductive.
Which is an excellent library, and it will be yet better in the next
release when the new codatatype package based on "BNFs" is used.
Makarius
Email Gateway (Aug 19 2022 at 11:56):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/4/2013 7:20 AM, Makarius wrote:
* The content of a theory file between 'theory' and the final 'end'
is by
definition the Isar source language.That is indeed true for the outermost language of Isabelle/Isar, but
there there are several languages embedded into that (potentially
recursively), e.g. the languages of types, terms, theorems of the
logical environment (Isabelle/Pure or Isabelle/HOL or whatever), or
Isabelle/ML, or Isabelle document source.
I will, many times, grudgingly conform, but if you make the Latin too
complex, the vulgar masses will corrupt the official Latin either out of
ignorance, or to make it practical to use in everyday conversation.
I can call '==' an Isabelle/Pure operator, but then the emphasis is all
wrong. There are three Isabelle/Pure operators, \<And>, !!, and ==, that
are a seamless part of the Isar language. Because the high-level part of
Isar is the high-level language I want to use, I want vocabulary that
emphasizes that's the level I'm concerned about.
Inside a command ML{...}, I would never call the '=' operator an Isar
operator, even though I've been told that everything between "theory"
and "end" is Isar.
However, given the inner syntax part of the two lines theorem "A == B"
and theorem "A = B", there is nothing special that marks '==' and '='
to differentiate one as a Pure operator, and one as a HOL operator. So,
if '==' is an operator that is seamlessly integrated into Isar, and
high-level Isar is what I care about, rather than the low-level ML that
makes up the bulk of Pure, then I definitely am inclined to call '==' an
Isar operator.
It's Isar. It's an operator that can be used in inner syntax. It's an
Isar operator. That it's also a Pure operator, and a meta-logic
operator, that just reflects complexity and sophistication. It's "Pure
operator" that's going to be neglected, because I only look at the files
that define Pure when I click on something in jEdit that opens up an ML
file.
It's not that important. It's just convenient. Severe torture could be
used to change my mindset.
When you work in Isabelle/HOL, what most users do most of the time, it
is better to use its plain =, though. This helps to make
specifications and proofs uniform and with reduced surprise of proof
tools that cannot cope with pure == (e.g. certain calculation
reasoning rules in HOL).
Trying to do what I'm told not to do can sometimes be an excellent way
to appreciate why I don't want to do what I'm told not to do, and
occasionally it leads to discovery of something good. With software, one
can touch the hot stove and not get burned, if, say, the software is not
running on a server for a large corporation.
Thanks for your time,
GB
Email Gateway (Aug 19 2022 at 11:56):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/4/2013 7:38 AM, Makarius wrote:
Does it mean you are not converted to Isabelle2013 yet? Isabelle
release cycles are done such that the least painful way to upgrade is
to do that continuously. The amount of incompatibilities in each
release is usually limited to something that works out for most
applications.
I'm using Isabelle2013, and looking forward to the locale addition in
2013-1. The years 2012 and 2103 get blurred together for me.
Isabelle2012 was prime-time, and Isabelle2013, with the Poly/ML fix, was
prime-time+.
Today, I'm thinking about two points, based on how I've seen changes
implemented:1) For Isabelle/HOL, there is zero commitment to backwards
compatibility by the developers.2) For Isabelle/HOL, there is no long term, future forecasts
published by the developers so that users can plan for the future, to
help users not get tied into things which are going to disappear.You should say "Isabelle" in general, not Isabelle/HOL (before you
have pointed out an interest to work directly with Isabelle/Pure,
ignoring the huge Isabelle/HOL library).
It becomes a matter of emphasis again. The signs indicate that it is
specifically Isabelle/HOL of Isabelle that is going to rule the world. I
don't ignore the Isabelle/HOL library at all, it's just taking me a
while to get through HOL.thy. The library as part of the distribution is
a big part of what makes Isabelle/HOL convenient to use.
Other practical matters also rule. It's preliminary, but I'm interested
in working up some meta-logic, such as intro and elim rules, along with
pseudo-sequents, but only within Isabelle/HOL. With a little planning, I
can maybe keep things independent, but because it's Isabelle/HOL I'm
working in, everything can potentially be used in Isabelle/HOL, along
with the potential of extracting what's been set up to be independent.
Keeping some logic independent within a locale, that's only dependent on
the independent meta-logic, would again allow it to then be used with
HOL, but yet be extracted. I guess. I'm talking about things I haven't
worked out.
It's not practical to spend years learning formal logic, and then not be
able to use the concepts you've learned.
I am myself involved in Isabelle only since 1993, but I've never seen
a commitment to "backwards compatibility". Instead there has always
been a natural flow of updating the system technically, conceptually,
introducing new things, discontinuing old things (the latter requires
a lot of work).
Consequently, because of your lack of promising to be all things to all
people, to take care of Americans in all ways, and not promising
everyone a small rose garden, the tally of those who vote for you when
you run for political office will be equal to a small integer n.
Without that principle, Isabelle2012 would not have been as nice as it
was last year (now Isabelle2013 is nicer). You may also browse
through the recorded history to see yourself if you want to stack back
in 1993:
I had downloaded 1999-2 to see what users would have had available to
them in that year. The number systems are pretty much non-existent. The
differences are big enough that it makes it too much work to want to
spend any time figuring out what the differences are.
For me, starting with Isabelle2013-1, there is the current version, and
that's all there is. If I don't have a solution to be able to say that,
then it's not worth the risk of continuing. But I do have a solution, to
at least address one scenario.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
On Thu, 5 Sep 2013, Gottfried Barrow wrote:
On 9/4/2013 7:20 AM, Makarius wrote:
* The content of a theory file between 'theory' and the final 'end'
is by
definition the Isar source language.That is indeed true for the outermost language of Isabelle/Isar, but there
there are several languages embedded into that (potentially recursively),
e.g. the languages of types, terms, theorems of the logical environment
(Isabelle/Pure or Isabelle/HOL or whatever), or Isabelle/ML, or Isabelle
document source.I will, many times, grudgingly conform, but if you make the Latin too
complex, the vulgar masses will corrupt the official Latin either out of
ignorance, or to make it practical to use in everyday conversation.
Vulgarisation is indeed a problem. Note that in the best of times of the
Roman Empire, educated people were fluent in Latin, Greek, and probably
Persian (a bit later also Arabic).
In Isabelle we have a similar multilingial environment that poses some
challenges. One needs to try to get at least at a few stable islands of
understanding of "what is what" in Isabelle. To simplify that scheme, I
am using Isabelle/XYZ as uniform terminology to refer to the XYZ aspect of
Isabelle, e.g. Isabelle/Pure, Isabelle/HOL, Isabelle/Isar, Isabelle/ML,
Isabelle/Scala. No "X level" nor "Y layer" as was done occasioanlly in
the past.
Sometimes there are more general expressions like "the logical language"
(which could mean Isabelle/Pure or Isabelle/HOL or both), or "the Prover
IDE" (which could mean Isabelle/Scala or Isabelle/jEdit, or some other
front-end).
I can call '==' an Isabelle/Pure operator, but then the emphasis is all
wrong. There are three Isabelle/Pure operators, \<And>, !!, and ==, that
are a seamless part of the Isar language. Because the high-level part of
Isar is the high-level language I want to use, I want vocabulary that
emphasizes that's the level I'm concerned about.
I don't quite understand that. Maybe the use of "level" causes again
confusion. The Isar language is mostly about so-called "outer syntax":
commands like 'theorem' or 'proof' / 'qed' with a certain token language,
like "..." or {* ... } or ( ... *).
How does '==' from the logical environment get in here? What is your
meaning of "Isar"? If you call it "logical operator" it is all fine: it
is clearly identified as part of the "logical environment".
Inside a command ML{...}, I would never call the '=' operator an Isar
operator, even though I've been told that everything between "theory"
and "end" is Isar.
That should be ML {* ... }. The verbatim token { ... *} is used here
most of the time for convenience, since it allows to use "..." inside
without extra escapes. (Further nesting of languages then requires
slightly awkward backslashed quotes.)
Conceptually, from the Isar language embedding approach, there is no
difference of
ML "fun f x = x + 1" -- "Isabelle/ML as embedded language"
vs.
lemma "xyz" -- "logical proposition as embedded language"
In fact, just a few weeks ago I had some discussion with someone who wants
to do another Isabelle sub-language about that quoting business. I had
some problems explaining {* ... *} vs. "..." apart from history. So if
this would be done afresh, it could be all unified with some nestable
quotes (just one kind of them) and no escapes inside quotes. Then, within
an advanced Prover IDE, the user might not even notice much about quoting
any more.
It's Isar. It's an operator that can be used in inner syntax. It's an
Isar operator.
This is contradictory. A classic simplified view is:
Isar --- "outer syntax"
logical language --- "inner syntax"
Makarius
Email Gateway (Aug 19 2022 at 11:58):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/6/2013 6:58 AM, Makarius wrote:
Vulgarisation is indeed a problem. Note that in the best of times of
the Roman Empire, educated people were fluent in Latin, Greek, and
probably Persian (a bit later also Arabic).
I'll put my most important comment first. I take the view that the
non-structural parts of language, such as spelling, pronunciation, and
word choice, are largely arbitrary in nature. For example, which is it,
welcome, willkommen, or bienvenida? Consequently, I try to be willing to
adopt official, technical vocabulary, but to do that I have to have
something that officially tells me what the official vocabulary is, with
some explanations and examples explaining subtleties.
I have heard that the French work very hard to preserve and protect
their language. There is the reputation of the French, that when an
American goes to Paris and tries to ask questions in English, the French
will act as if they don't know English, when they do (and we know they
all speak English).
There is also the Academie francaise, the spelling of which I, of
course, slaughter, as every mono-lingual English speaker should:
https://en.wikipedia.org/wiki/Acad%C3%A9mie_fran%C3%A7aise
I have no problem with people aggressively trying to protect their language.
As to Isabelle, there should be a section in the Isar reference manual
which gives users something to authoritatively quote to explain to
others how to talk about the different parts of Isabelle.
When there are 10,000 users, I guarantee, you will be overwhelmed if no
such section exists.
If there's something official to quote, then 2,000 experienced users of
the 10,000 can act as the Academy of Isabelle, even if the vocabulary
doesn't always make sense.
In Isabelle we have a similar multilingial environment that poses some
challenges. One needs to try to get at least at a few stable islands
of understanding of "what is what" in Isabelle. To simplify that
scheme, I am using Isabelle/XYZ as uniform terminology to refer to the
XYZ aspect of Isabelle, e.g. Isabelle/Pure, Isabelle/HOL,
Isabelle/Isar, Isabelle/ML, Isabelle/Scala. No "X level" nor "Y
layer" as was done occasioanlly in the past.Sometimes there are more general expressions like "the logical
language" (which could mean Isabelle/Pure or Isabelle/HOL or both), or
"the Prover IDE" (which could mean Isabelle/Scala or Isabelle/jEdit,
or some other front-end).
Context is everything, and you're fighting the traditional and general
use of the word "level". More about "level" below.
...Because the high-level part of Isar is the high-level language I
want to use, I want vocabulary that emphasizes that's the level I'm
concerned about.I don't quite understand that. Maybe the use of "level" causes again
confusion. The Isar language is mostly about so-called "outer
syntax": commands like 'theorem' or 'proof' / 'qed' with a certain
token language, like "..." or {* ... } or ( ... *).
You've now changed what I should or shouldn't say. I was taking as
authoritative the statement "everything between 'theory' and 'end' is by
definition the Isar source language".
Now, you say Isar is "outer syntax", where your use of "mostly" doesn't
help me figure out whether inner syntax can or can't be labeled as Isar.
And there is the general meaning of "level" which is interfering here.
"Level" can commonly mean "level of abstraction".
Hexadecimal machine code is low-level. Assembly language is low-level,
but higher-level than machine code. C language is finally high-level,
but with pointers, not as high-level as Java.
If everything in a THY is Isar, I need to talk about what's in ML{...}
as low-level Isar. Generally speaking, ML is a lower-level language than
much of Isar. The context is merely the level of abstraction of ML
versus the level of abstraction of Isar.
Here, I say this, "Give me an example of a popular programming language
that can't be referred to with just one word or phrase, where, or
course, Isabelle/HOL and Isar are not programming languages, though
there's no official documentation that I can quote from to say that, and
even now, I'm not sure I'm right in saying that about Isabelle/HOL,
because, again, there's no authoritative documentation or book to sort
it all out for me."
Coq has a language, Gallina, but everyone just calls Coq one thing,
"Coq". It's easy to talk about Coq when you want to talk about Coq. You
just talk about Coq.
Calling Isabelle "Isabelle" is way too general. There's the popular
logic Isabelle/HOL, the secondary logic Isabelle/ZF, and then many minor
logics, all composed of languages that elude being given one label.
Wanting to work at a high level of abstraction, I try to use "Isar", but
you contest my use of "Isar".
How does '==' from the logical environment get in here? What is your
meaning of "Isar"? If you call it "logical operator" it is all fine:
it is clearly identified as part of the "logical environment".
My meaning of Isar was your description of Isar, that everything between
"theory" and "end" is Isar. If only outer syntax is Isar, I must
reconsider this matter of correct vocabulary usage, more than I prefer to.
It's Isar. It's an operator that can be used in inner syntax. It's an
Isar operator.This is contradictory. A classic simplified view is:
Isar --- "outer syntax"
logical language --- "inner syntax"
If the phrase Isar --- "outer syntax" is being enforced ex post facto,
it's clear that I'm breaking the law.
I immediately ask, "If inner syntax is not Isar, what one word can I use
to label the language that's being used in inner syntax? 'Syntax'
implies the use of a language."
Suppose I'm told, "It's not a language, but a logic." (Here, others'
past emphasis on the difference between a logic and a programming
language interfered with me focusing on there being "languages of logic".)
I say, "Fine, I can go with logic. The creator gets the liberty to make
the rules axiomatically."
I now immediately ask, "What is the one word I can use to describe the
logic being used in inner syntax?"
If I'm told, "It's not that simple. There are multiple logics being used
in the inner syntax."
I say, "Okay. It is what you say it is. In A = B ==> A = B, it is
clear that '==>' is meta-logic or Pure, and that 'A = B' is HOL logic.
There is a complication, though, because I know that 'A = B' is being
coercied to type prop, so what is the one word to use to emphasize that
A = B is both a meta-logic term and an object-logic term?"
If I'm told. "There is no one word, you must use a lengthy phrase, or a
word that is too general to capture the meaning of what you want to say."
I then say, "It's time to rebel against the creator, at least in my mind."
Regards,
GB
Email Gateway (Aug 19 2022 at 11:58):From: Makarius <makarius@sketis.net>
(In order to avoid the usual chaos of cross-posting between the lists,
I've changed the subject.)
What exactly do you mean by "==" as Isar operator? It belongs to Pure,
not Isar. So it is not an Isar operator now, and will never be.
If you mean this Isar command:
def x == "t"
it does belong to Isar, but it can be better done like 'obtain' as follows
(with the same preprocessing like 'definition'):
define x where "x = t"
Nothing of that old cleanup plan is imminent, not for the coming release.
Makarius
Email Gateway (Aug 19 2022 at 11:58):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I like to try bring to an end my part of these kind of threads as fast
as possible. First, I tell you my plan for the future, and then I try
and explain it.
Unless I brainstorm for a better solution to fit my needs, in my mind,
it's "Isar operator". It's possible that what is in my mind will make
its way into something I put out on the Web, and what I put on the Web,
I will never ask anyone here for any kind of editorial review. That's
the great thing about proof assistants, auto-review is built in. That
the logic is correct, that's the main thing.
I need a language, and I need a name for the language. Here, let me
start by calling it the NN language, for the no-name language.
You have provided many languages, so I pick the four that are most
related to what I'm doing: Isabelle/ML, Isabelle/HOL, Isabelle/Pure, and
Isabelle/Isar.
It's hard not to go on tangents. As to Isabelle/HOL being a language, I
see many places where HOL is called a logic, but there's only the
occasional, half-hearted comment where it's called a language. It
doesn't even sound right to call it a language, but I'll call it a language.
Here I describe the parts of the languages of Isabelle that I'm using:
1) Outer syntax commands to state theorems and to make proof statements.
2) Inner syntax that is mainly formulas made up of meta-logic operators,
HOL operators, and HOL functions.
I don't use any ML. I don't use any Latex. I don't use any annotations.
The inner syntax I'm using consists of item 2 that I've listed. So far,
what I'm doing looks more like the contents of a Mathematica document
than an ML or Coq document. We could call much of it "cryptic
natural-language-like mathematics."
That you've clarified to me that the logic of ML can be used in inner
syntax makes "inner syntax" even less suitable to describe the language
that I'm using. The name of a language doesn't give us exact details,
but it can precisely rule out some things. With Java, we know that
pointers aren't being used.
If inner syntax can be ML as the logical language, and I don't use ML,
then "inner syntax" ends up being too general to describe what I'm doing
in Isar.
Here the imaginary conversation starts:
/Someone/: "You're using the language Pure."
/Me/: "But I'm exclusively working in the logic Isabelle/HOL. I don't
foresee working in any other logic, and I'm using HOL to do the bulk of
what I'm doing."
/Someone/: "Then obviously you're using the language Isabelle/HOL."
/Me/: "Not necessarily. I could be creating some meta-logic in HOL
that's independent of HOL. There's also the issue that the three Pure
operators and the HOL operators have so much in common that they deserve
to be considered as part of the same language."
/Someone/: "Whatever you do, it's clear that 'Isar' can't be the word
you use."
/Me/: "No, of course not, not without at least explaining my specific
use of 'Isar' in the preface of a document."
So, with a name for a language, I can then start modifying it with
things like "NN operator". That's pretty normal, as I see it.
It won't really matter if no one is interested in what I'm doing. If
they are interested, that's good for me, and good for Isabelle.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
On Fri, 6 Sep 2013, Gottfried Barrow wrote:
I have heard that the French work very hard to preserve and protect
their language. There is the reputation of the French, that when an
American goes to Paris and tries to ask questions in English, the French
will act as if they don't know English, when they do (and we know they
all speak English).
The French are generally a bit reluctant to use English, because they
don't know it very well.
There is also the Academie francaise, the spelling of which I, of course,
slaughter, as every mono-lingual English speaker should:https://en.wikipedia.org/wiki/Acad%C3%A9mie_fran%C3%A7aise
I have no problem with people aggressively trying to protect their language.
There are many jokes about that centralized language committee of France,
both inside and outside the country. Sometimes they do some interesting
job. E.g. email is officially called "courriel", while spam is
"pourriel". Unfortunately that ingenious linguistic construction is
hardly ever used in practice: the man on the street just says "email" and
"spam" with a strange French pronounciation. Thus the pop culture from
North America has overcome Central European sophistication.
Anyway, this is getting a bit off-topic.
...Because the high-level part of Isar is the high-level language I want
to use, I want vocabulary that emphasizes that's the level I'm concerned
about.I don't quite understand that. Maybe the use of "level" causes again
confusion. The Isar language is mostly about so-called "outer syntax":
commands like 'theorem' or 'proof' / 'qed' with a certain token language,
like "..." or {* ... } or ( ... *).You've now changed what I should or shouldn't say. I was taking as
authoritative the statement "everything between 'theory' and 'end' is by
definition the Isar source language".
It is definitely Isar (as outer syntax). Then you can embed any other
language inside it (as inner syntax), and repeat or alternate that
principle ad infinitum. After some nesting, it becomes difficult to hold
up the simplifying termninolgy of "outer" vs. "inner", although the
outermost Isar token language always remains as a starting point.
"Level" can commonly mean "level of abstraction".
Hexadecimal machine code is low-level. Assembly language is low-level, but
higher-level than machine code. C language is finally high-level, but with
pointers, not as high-level as Java.If everything in a THY is Isar, I need to talk about what's in ML{...}
as low-level Isar. Generally speaking, ML is a lower-level language than
much of Isar. The context is merely the level of abstraction of ML
versus the level of abstraction of Isar.
This is leading in the wrong direction; the level of abstraction does not
matter here. Isabelle/ML and Isabelle/Isar are both high-level languages,
but of quite different kind and purpose.
Coq has a language, Gallina, but everyone just calls Coq one thing,
"Coq". It's easy to talk about Coq when you want to talk about Coq. You
just talk about Coq.Calling Isabelle "Isabelle" is way too general. There's the popular
logic Isabelle/HOL, the secondary logic Isabelle/ZF, and then many minor
logics, all composed of languages that elude being given one label.
I would say as first approximation it is fine to say "Isabelle source
text" for any of the Isabelle languages. You then become specific
according to the context: Isabelle/ML, Isabelle/HOL etc.
The situation is not fundamentally different in Coq, although they never
worked out the integration of different languages as systematically as was
done in Isabelle in the last 10 years. Moreover there is a cultural
difference: French Type Theorists like to eat everything from one plate,
so there is a tendency to internalize everything into the core logic
(which then becomes huge and hard to manage conceptually).
This is contradictory. A classic simplified view is:
Isar --- "outer syntax"
logical language --- "inner syntax"If the phrase
Isar --- "outer syntax"is being enforced ex post facto, it's
clear that I'm breaking the law.I immediately ask, "If inner syntax is not Isar, what one word can I use to
label the language that's being used in inner syntax? 'Syntax' implies the
use of a language."Suppose I'm told, "It's not a language, but a logic." (Here, others' past
emphasis on the difference between a logic and a programming language
interfered with me focusing on there being "languages of logic".)
A logic is also a language. So if you just say "the logic" or "the
logical language", either for Isabelle/Pure or Isabelle/HOL, it will be
right.
I say, "Okay. It is what you say it is. In
A = B ==> A = B, it is clear
that '==>' is meta-logic or Pure, and that 'A = B' is HOL logic. There is a
complication, though, because I know that 'A = B' is being coercied to type
prop, so what is the one word to use to emphasize thatA = Bis both a
meta-logic term and an object-logic term?"If I'm told. "There is no one word, you must use a lengthy phrase, or a word
that is too general to capture the meaning of what you want to say."
I am a big fan of the distinction of Isabelle/Pure vs. Isabelle/HOL, but
you should not overemphasize Pure as "the meta-logic". There is not much
"meta" going on here: you can't reason about other logics with Pure.
Instead, what really happens is that you use Isabelle/Pure connectives !!
and ==> to outline the structure of natural deduction rules that you want
do use in everyday work in Isabelle/HOL. So Pure is mainly a framework
work higher-order natural deduction, with declarative composition of rules
according to a few principles (notably higher-order unification).
Makarius
Email Gateway (Aug 19 2022 at 11:59):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Makarius,
I assume you read that other email. All that email was is a statement of
my decision to finalize what I'm going to do, with some forewarning, in
case it matters in the grand scheme of things.
Any complaining and arguing I do is indirectly a note of thanks, where
I'm trying to limit how much I thank you. There's like 3 main features
of Isabelle as I see it, jEdit user interface, Isar language syntax, and
a powerful logic engine which allows the control of proof steps from
precise statements all the way to full automation. I don't know what the
limitations of the software are, but there's nothing else on the market
like Isabelle.
You control the distribution, but as far as language, you're not in
complete control of the language.
Most of what I'm saying can be represented by this statement: For me,
there has to be one word for a language, call it "NN", in which I can
say "NN operator", where "NN operator" refers to the three Pure
operators, ==>, !!, and ==, along with any object logic operator in a
THY file.
When you give me one word for your choice of "NN", I'm thinking that's
when I'm ready to start conforming on this matter.
Just consider me a representative of the users to come. I can't lose on
this. The nature of things like art, philosophy, religion, politics, and
general acts of creation is that there's continual evolution and
morphing of one thing to another. People pick and choose what they want.
Right now, I'm refusing to do any work with Isabelle, to force myself to
get up to speed on some audio/video software. If I'm more successful
than you at getting a popular following, then it's possible I'll have
more influence than you on how the word "Isar" is eventually used.
No one can authoritatively correct me if there's nothing authoritative
to quote from. I've tried authoritatively quoting from mailing list
emails. It doesn't work for sorting out the complexities of the
vocabulary of Isabelle. It's regrettable that writing would take up
valuable resources on your part, but I can't help that. However, mere
writing wouldn't solve me not having a "NN operator", as I described.
On 9/10/2013 8:13 AM, Makarius wrote:
This is leading in the wrong direction; the level of abstraction does
not matter here. Isabelle/ML and Isabelle/Isar are both high-level
languages, but of quite different kind and purpose.
So maybe for you, "level" means "level of logic", which you consider
wrong, rather than some common meaning like "level of abstraction". My
main point was that you're fighting other common usages of the word
"level", and I don't see you winning. That {a_i} is notation for a
sequence is messed up, but nothing any time soon is going to change that
it's the dominant notation.
I would say as first approximation it is fine to say "Isabelle source
text" for any of the Isabelle languages. You then become specific
according to the context: Isabelle/ML, Isabelle/HOL etc.
There are many places I could say this, but the vocabulary is too
complex. I don't actually care that the vocabulary is complex. I think I
understand enough for why you require it to be complex. It's too complex
without some document existing to enforce the vocabulary, along with the
vocabulary meeting more than just your needs.
I am a big fan of the distinction of Isabelle/Pure vs. Isabelle/HOL,
but you should not overemphasize Pure as "the meta-logic". There is
not much "meta" going on here: you can't reason about other logics
with Pure.
Many places in all this, we're crossing into Ph.D. logic territory,
where most mathematicians of the world (me not being one) don't
understand Ph.D. level logic anymore than I do, where I'm already above
average as to understanding logic.
As to the "meta" in "meta-logic", I quickly admit that I don't
understand in-depth the connection between meta-languages and
object-languages.
However, with Isabelle, I can take a purely definitional view of
"meta-logic" to mean the three operators ==>, !!, and ==, along with
what I can do with them in a THY file.
I myself, rather than one of the many Ph.Ds here, discovered that I can
define and use meta-false as (!!P. PROP P), along with what I call
hybrid-false, (!!P. P::bool), which end up giving me the standard
connectives, without using ML.
It could be I'm wasting my time pursuing this line of logic. Finding
that out must wait until I work my way through the audio/video software.
Instead, what really happens is that you use Isabelle/Pure connectives
!! and ==> to outline the structure of natural deduction rules that
you want do use in everyday work in Isabelle/HOL. So Pure is mainly a
framework work higher-order natural deduction, with declarative
composition of rules according to a few principles (notably
higher-order unification).
I'm willing to recognize my lack of knowledge, and recognize others'
superior knowledge, but when the student learns enough, the student
begins to challenge the master.
I don't accept at all the limitation of Pure as a framework, with only 3
operators, meant to be used only to defined object-logics. If my view of
Pure is ridiculously narrow and trivializes the bulk of Pure's purpose,
what is that to me? I work in a THY file, see the three operators and
prop as the face of Pure, and have quit wanting to ignore them.
I had asked myself this question, "What are the limitations of using the
standard logic connectives of Pure, without being able to add any axioms?"
I'm past that question.
If I add global axioms to HOL, it's not HOL anymore. There is the
possibility, though, of adding axioms in locales in HOL, and using, as
much as possible, operators which are abbreviations of ==>, !!, ==, and
meta-false. That sounds like more than only using Pure as a framework.
It's actually the concept that's important, not whether there's a fatal
flaw to prevent me from following through.
If I spend a lot of time trying to do these things, and decide you've
been right all along, you're the man, along with many others. If it
leads to something great, you're still the man, along with many others.
I'm doing the easy part.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
To finish this perspective of more flexibile local definitions within
proofs, in conformance to 'definition' for local theories, the general
form would be like this:
define f where "f x y z = t" for x y z
All composed from standard parts that we have elsewhere for many years
already. (When it actually happens, further fine points will come
naturally from "deriving the implementation" properly and carefully from
the existing framework.)
Makarius
Last updated: Apr 26 2024 at 01:06 UTC