Re: [isabelle] Need a "What's the foundation of Theory.thy" utility



On 7/9/2013 9:21 AM, Ramana Kumar wrote:
In HOL4, every theorem (a value of type thm in ML), can be inspected to see
the axioms used in its production.

Moreover, all the theorems about any constant (such as might appear in the
conclusion of a theorem) can be retrieved, to help gain confidence in how
the constant was defined. (For example, you could easily check that all the
constants in some theorem were defined in standard HOL4 libraries.)

I'd be surprised if analogous facilities didn't exist in Isabelle already..

If it's easy, and a single, automated process, then I definitely want to know about it. But if I have ten theorems in a theory that give me 10 final results, rather than one final result, then it's not easy if I have to manually find those 10 theorems, and type in a command, and look at the results. I like the idea of automation, as we all do.

I keep using the phrase "or can't be determined to be axiomatic". I say that because I don't assume that with ML used in a THY it's quick and easy to automate listing any statement in the ML that's axiomatic, but it could be easy. I try to assume less than more.

What is axiomatic in logic is so important, the first thing that the software should provide for a THY is what axiomatic statements get used in the THY, and anything axiomatic that the THY imports. I want to know what others are getting for free, and I want others to know what I'm getting for free, and I want it all to be listed by an official utility so we all know it's legit and official.

I shouldn't have to have any expertise to answer the question, "What's the axiomatic foundation of Theory.thy?" The software should immediately be able to tell me, whether I understand what it tells me or not.

When you study a book on axiomatic set theory, you get the axioms up front. You don't understand them at first, but getting them up front categorizes the logic you're using. We're not really interested in ZFC+Falso. It's different. We immediately skip past those theories in the AFP that tell us Falso is used. When they don't tell us up front they use Falso, we end up looking at something we're not interested in.

I'm making a request which now sounds like a demand, but I just use what's available, and a lot is available. On a private level, I don't need this at all.

What I'm asking for will eventually become a priority. If thousands of people are using proof assistants, and they're not from some circle of trusted professionals, if you don't know a person, and you don't know what's in their THY, you want to know immediately and effortlessly what they're using axiomatically, and you want the software to tell you that, and do with automation.

On 7/9/2013 8:02 AM, Ramana Kumar wrote:
OpenTheory does allow new axioms. (OpenTheory only checks that some conclusions follow from some axioms; you're free in the choice of conclusions and axioms, as long as you provide the proof.)

Dedukti should work both for new axioms and for type classes. It does an encoding into a rich type theory that should support most logical features... (I'm not so sure about the details).

The lack of one feature can make a big difference, like automatic type coercion, not to mention getting heavily tied into a particular library of theorems, used with a particular proof assistant.

But it's good to know that OpenTheory allows new axioms, and that Dedukti has type classes. Maybe in two years I'll be looking for some extra verification, and by then there should be more documentation.

It's hard enough to learn the language of one proof assistant. A simple utility to report the foundation of a THY would probably satisfy me. Like I said. I say this now just to plant a seed. And maybe someone will say, "Dude, just type in print_foundation."

Regards,
GB






On Tue, Jul 9, 2013 at 3:10 PM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:

On 7/9/2013 5:13 AM, "Mark" wrote:

Hi Gottfried,

So you are advocating a utility that would reveal the "foundation" in a
theory.  Do you envisage that this utility would have a human aspect to
its
usage, reviewing that the reported foundation is good, e.g. that the "+"
operator really is the intended "+" operator, etc? By saying a "10 second
check", it suggests not, although maybe I'm missing your point.

Mark,

No, it's only to list anything that's being used in the theory and
language that's either axiomatic, or might be axiomatic.  Also, it would do
some easy checks to rule out the possibility of a person doing sneaky
things, like doing checksum comparisons on third-party files a person is
distributing with their theory, where the local third-party files would be
obtained from the original source.

If someone writes 100,000 lines of source and at the end claims to prove
the Riemann Conjecture, the first thing you want to know is what's in their
THY that's axiomatic, or can't be determined to be axiomatic. The utility
is to give you that information fast.

If someone's not using anything axiomatic beyond what Complex_Main gives
them in Isabelle, then their doing stupid stuff like trying to fool people
with deceptive notation still  wouldn't allow them to prove something
that's not true. It would just appear to be something different on the
surface. The statement of a theorem after 50,000 lines of source is always
going to take some effort to figure out what it proves. The utility is to
let you know what the limitations there are to the foundation.


  Also, are
you suggesting that the utility would do some form of automated check on
the
foundation of a theory, or would it just report what the foundation is?

No, it would just tell me what the axiomatic foundation is for a
particular THY, or what can't be determined in a THY to be axiomatic.

Some things can't be hacked easily. Most people use distribution sources
they've gotten from the official web sites, so you can't hack the
distribution sources and fool anyone but people using local sources. I do
want the utility to tell me what foundation Complex_Main gives me, but I'd
think it's mostly about the utility reporting what people have done to
extend Complex_Main, or done to modify third-party files that aren't part
of the official distribution sources.

The simple part would be listing the axioms used. You might think all I
need to do is grep on "axiomatization", but in Isar, there are more than
"axiomatization". The latest axiomatic command in Isar I've learned about
is "arities". It's not obvious at all it's an axiomatic command.

Right now I'm speculating that when ML is used in Isar, it can't be
determined that the ML does something axiomatic unless you inspect the ML,
but I wouldn't know, which is the purpose of the utility, to get an
official report on what the foundation is.

The purpose is to make it fast, easy, and official what axiomatic
foundation is being used in a THY. For the case where we're not interested
in any logic proved other than what can be proved by importing
Complex_Main, the first thing we would do is run the utility on a THY to
see if that's the case.

I was vague on the details because it's the Isabelle foundation people who
know what possibly can be done axiomatically, but I came up with a scenario:

1) Person 3 releases Theory3.thy. It's distributed with Theory1.thy and
Theory2.thy, which have been released by Persons 1 and 2.

2) I download Person 3's theory, and I run the Isabelle foundation utility
on it. It does a checksum comparison on Theory1.thy and Theory2.thy with
the original files which I obtained. It tells me everything that's in
Theory3.thy that's axiomatic, or can't be determined to be axiomatic.
Additionally, it tells me what's axiomatic beyond what's axiomatic in
Theory1.thy and Theory2.thy

Now, having obtained all that information in a couple of minutes, I can
make an informed decision about whether I want to look at Theory1.thy. If
I'm a professor, and Person 3 wasn't supposed to add anything axiomatic,
and they  did, they get bad grade. If I'm an employer, and Person 3 wasn't
supposed to use anything axiomatic, and they did, they get fired.

Some of that I could do myself, but then it's not official, and I don't
know all the details about what can be axiomatic in Isabelle, or what can't
be determined to be axiomatic.

It's not just about checking others, I want the ability to say to people,
"Here's an official report on the foundation I'm using, so you can know up
front what logic my theory is based on."

Like I said to Ramana, even a third-party verifier like yours needs to be
able to give a basic report on what foundation is being used. If all I'm
interested in is standard HOL, then I want to know as fast as possible
whether someone's using standard HOL.

Regards,
GB



Mark.

on 9/7/13 8:41 AM, Gottfried Barrow<gottfried.barrow at gmx.**com<gottfried.barrow at gmx.com>>
  wrote:

  Hi,
I don't need this now, but in a year or two, I'd like to have a Isabelle
utility that I run on a theory which tells me what the "foundation" is,
and that also can take a Thy1.thy as the base "foundation", and given
Thy2.thy, the utility reports what additional "foundation" Thy2.thy adds
to Thy1.thy.

The foundation would be anything in a theory which would be axiomatic in
nature, and maybe some kind of checksum on things.

Different people are motivated by Isabelle for different reasons. A big
part of my interest in Isabelle is that it's a tool which, at the very
least, replaces the function of peer reviewed journals, to the extent
that it can. That means, at the very least, it's a huge preliminary
vetting of logic in Theory.thy that announces to anyone interested, "The
logic in Theory.thy has been vetted by Isabelle as being correct. It
most likely will not be a waste of anyone's time to wade through 20,000
lines of source in Theory.thy to figure out what it is, and to find out
if it really is correct."

On a personal level, by all appearances, Isabelle can take the place of
peer reviewed journals, to the extent that it can give you confidence
that you're not producing a bunch of logical nonsense. What Isabelle
doesn't do is solve the "person X is trustworthy and competent" problem
on a community level.

I could dig through the mailing list archives and find where Larry has
said something like, "You have to use Isabelle intelligently." And a
while back, on the HOL4 list, there was a discussion about the
possibilities of people getting proof assistants to do something wrong
for either devious reasons or non-devious reasons. And most recently, on
this very list, Falso was presented as a great logical break through,
where, no doubt, still today, many verifiers, formalizers, and sourcers,
not to be confused with sorcerers, are now full of themselves, mistaking
their own logical prowess with the success that always comes with Falso.


  https://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-**
users/2013-March/msg00165<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00165>
.

html

Anyway, a "what's the foundation" utility would allow people to do a 10
second check on a theory as a first step, to make sure nothing obvious
is wrong, and to increase the trust factor, and even good people mess up
bad some times.

I assume that there are much more complex problems involved in proof
assistants being completely secure from being hacked, or messed up
unintentionally, but I think it would be good for a person to get a
basic rubber stamp from an official utility that generates a basic
report on what the foundation of a theory is, and that can compare the
foundation of two theories.

No one needs to respond to this. I'm putting it out so maybe in a year
or two there's an Isabelle foundation report utility.

Regards
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.