In this discussion on the Isabelle mailing list, I am missing the question
of the correctness of the small logical kernel that should guarantee
the correctness of the whole system.
Currently, the arguments presented so far seem to open up a false alternative
between logically correct (reliable) but small theorem provers (e.g., HOL Zero),
and large and practical but less reliable provers (e.g., Isabelle/HOL):
> The other big provers (e.g. Coq) are similar in this respect. […]
> HOL-Zero is a notable exception in targeting a market of potentially
> malicious (ab-)users, but it is not a "big prover".
According to this idea, any reliable prover/checker must be small,
and any practical (and hence, large) prover isn't reliable.
But the concept of a small logical kernel that guarantees
the correctness of the whole system states exactly the opposite,
i.e., no matter how large and practical the software is, it remains reliable.
This concept is given up in arguments like
> We do not have to work on the basis that "X has been proved, therefore X is
> true", but rather "We have been given a proof of X; Is it credible?"
which even seems to rhetorically downplay a desirable must-have (correctness)
as an annoying impediment to get rid of ("do not have to work on the basis").
In particular, transferring the responsibility for providing reliability
(correctness)
from (verifying) the small logical kernel to either examining specific parts of
the formalized proof or estimating the credibility of the supplying person is
questionable,
as even the best mathematicians from time to time fail at complex proofs:
> Then we can look at any part of this proof where we have doubts. […]
> The effort we choose to invest in this would depend on how important X is and
> how much we distrust the person who supplied the proof.
I do not see any alternative to providing a correct small logical kernel.
Preserving logical dependencies is part of (has to be guaranteed by) the
logical kernel.
For this reason, I consider the following phenomenon as highly problematic
(and even as a failure of the logical kernel):
>> found this originally, but you can hide the ‘taint’ of a theorem by
>> going through a type class instantiation:
If a conditional can be stripped off so easily, it might be possible to obtain
from
different conditionals two contradictory theorems, and hence, an inconsistency.
In a related discussion about this question on the Metamath mailing list I
argued
in favor of introducing all non-logical axioms as conditionals (hence, Q0 and
R0 have only five axioms)
in order to make the dependency explicit:
> Third, the dependency is made explicit. If "the software tracks
> axiom usage, as Metamath does", the task of tracking dependencies
> is moved from the logic to the software, which I already, in another
> context, criticized at Kunčar/Popescu's approach (which is
> nevertheless legitimate as an auxiliary approach).
> […] Andrews' exercise X5308 […] stated and
> formalized on pp. 151 ff. of
> http://www.owlofminerva.net/files/formulae.pdf
> is taken as an example where the dependency of the theorem
> is make explicit, assuming the form
> AC => theorem
> since the (non-logical) Axiom of Choice was
> introduced as a conditional, not as an axiom.
https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/VSAVebXPCQAJ
Norman Megill presented a similar example:
> It is certainly possible to prefix every theorem with "ZFC ->"
https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/nvmXHUffCQAJ
I agree with Norman Megill that in certain practical contexts constantly
displaying
the same conditional prefix may be redundant, but this is a question of the
user interface
(which could, for example, replace the default prefix – e.g., "ZFC ->" – by a
star "*"), but not a
matter relevant for the logical kernel, where this dependency should be made
explicit.
As mentioned earlier, the Isabelle concept of axiomatic type classes as
described and discussed in
https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
and introduced in
> Prover-powered type classes were introduced by Nipkow and Snelting [28] in
> Isabelle/HOL
> and by Sozeau and Oury [32] in Coq—they additionally feature verifiability
> of the type-class conditions upon instantiation: a type T is accepted as a
> member
> of the semigroup class only if associativity can be proved for its +
> operation.
http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf (p.
3)
is considered as a preliminary solution by me, since the same fact can be
expressed
very naturally with the means of type abstraction (as suggested by Mike Gordon,
see first quote at
http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/
) and as argued and demonstrated at pp. 12, 362, 420 of
http://www.owlofminerva.net/files/formulae.pdf
Here, the fact that (o,XOR) is a group, formalized as
Grp o XOR
(p. 420) can be stated only after proving the three group axioms for (o,XOR),
and only after that, a general proof on groups (Uniqueness of the Group
Identity Element, pp. 362 ff.)
can be instantiated (transferred) to the specific XOR group without having to
carry out the proof again
(Uniqueness of the Group Identity Element of the XOR Group, pp. 420 ff.).
Coq is not suited for a comparison. It is very expressive (e.g., it has
dependent types),
but there is profound criticism raised by Freek Wiedijk and John Harrison (and
Josef Urban),
see section 3 of
http://doi.org/10.4444/100.111
and for an example the rule on top of p. 54 at
http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf
which is very far from a natural expression of formal logic and mathematics.
The Isabelle documentation is discussed quite often.
> Extensive documentation is available.
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 3)
> The problem remains open: How can true expertise about how Isabelle
> really works be reconstructed? We've seen a slow and steady decline in
> the past 10 years, and myself writing hundreds of pages of documentation
> helped only very little.
It is always claimed that the Isabelle documentation is ample, but
unfortunately,
it is not logically structured, which makes the extent of the documentation
rather a disadvantage than an advantage.
For comparison, the HOL/HOL4 documentation provides a precise and quick
introduction,
which allowed me to fully comprehend the logic, install the software and
carry out proofs very quickly. It has, as one would expect, a separate logic
part
(Part III: The HOL Logic [Gordon and Melham, 1993, pp. 191–232]), available
online at
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf
and a very good guidebook which allows one to inspect the details of the system:
https://hol-theorem-prover.org/guidebook/
I already made suggestions for improvements earlier:
> Although of course Isabelle/HOL is a very good piece of software, this
> precision is currently missing in my opinion.
> The extension from classical HOL to Gordon's HOL can be found in section 11.7
> (p. 261), as well as the
> (single) extension from Gordon's HOL to Isabelle/HOL ("Isabelle/HOL goes
> beyond Gordon-style HOL
> by admitting overloaded constant definitions") within a document of 13
> chapters and 330 pages,
> which makes it practically impossible to identify and locate important
> features and extensions of the core logic
> within a reasonable amount of time:
>
> http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html
Essential information on the logic is hidden somewhere between many technical
details,
and at the first glance I can't even see a reason for why the extension of the
HOL logic is
described in the Isar reference, and not in the Isabelle/HOL reference.
With the HOL/HOL4 documentation, I was able to understand the logic and study
the details of the proof technology within 24 hours (see example files
attached),
but with the Isabelle/HOL documentation, even after many months the details
are obscure. Moreover, the concept of a small logical kernel should be reflected
in the documentation by a separate logic part, as in the HOL/HOL4 documentation.
The Isabelle/HOL documentation currently doesn't conform to this clear standard
established by the original HOL system.
The emails quoted are attached below.
The full discussion is available at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/date.html
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 08.07.2017 um 20:59 schrieb Lawrence Paulson <l...@cam.ac.uk>:
>
> To protect against malicious intentions would turn Isabelle into a form of
> security software. But the guarantees we get from the latter are quite
> different from what we get from a formal proof. Ultimately security claims
> depend upon trusting a lot of complicated mechanisms, such as certificate
> authorities and cryptosystems. We are not a lot better off than when a model
> checker comes back with nothing.
>
> However, we work with formal proofs, which can be examined, even
> interactively. We do not have to work on the basis that "X has been proved,
> therefore X is true", but rather "We have been given a proof of X; Is it
> credible?" Then we can look at any part of this proof where we have doubts. A
> devious user has many ways to try to fool us, but it's not so easy if he has
> to supply the full source code and we insist on legibility throughout. The
> effort we choose to invest in this would depend on how important X is and how
> much we distrust the person who supplied the proof.
>
> Larry Paulson
>
>> On 8 Jul 2017, at 18:12, scott constable <sdcon...@syr.edu> wrote:
>>
>> Isabelle does not protect against malicious intentions. It would require
>> a quite different system to do that, one that you won't like to use.
>>
>> The other big provers (e.g. Coq) are similar in this respect.
> Am 08.07.2017 um 12:46 schrieb Makarius <makar...@sketis.net>:
>
> On 07/07/17 18:37, scott constable wrote:
>>
>> possibly written by other persons with malicious intentions.
>
> Isabelle does not protect against malicious intentions. It would require
> a quite different system to do that, one that you won't like to use.
>
> The other big provers (e.g. Coq) are similar in this respect.
>
> HOL-Zero is a notable exception in targeting a market of potentially
> malicious (ab-)users, but it is not a "big prover".
>
>
> Makarius
> On 08/07/17 13:01, Manuel Eberl wrote:
>> Unfortunately, it is very easy to circumvent this. I don't recall who
>> found this originally, but you can hide the ‘taint’ of a theorem by
>> going through a type class instantiation:
>
> "Found this originally" sounds very funny to me.
>
> Of course, the problem of oracles vs. type classes instantiations is as
> old as oracles and type class instantiations in Isabelle. It is rather
> well-known for insiders.
>
>
> So we are back to the new meta-problem from recent years: even power
> users don't know anymore what Isabelle is and what it does, and
> especially what it does not.
>
>
> Makarius
> Am 08.07.2017 um 16:03 schrieb Makarius <makar...@sketis.net>:
>
> On 08/07/17 15:33, Tobias Nipkow wrote:
>
> […]
>
>> It is usually due to a fanciful interpretation of the documentation. The
>> latter says that "The system always records oracle invocations within
>> derivations of theorems by a unique tag." but does not claim that these
>> tags are also always inherited in the way one is all too likely to
>> assume.
>
> The problem remains open: How can true expertise about how Isabelle
> really works be reconstructed? We've seen a slow and steady decline in
> the past 10 years, and myself writing hundreds of pages of documentation
> helped only very little.
>
>
> Makarius
____________________________________________________
Makefile
____________________________________________________
SRCS = types.sml
OBJS =
TGTS = $(SRCS:.sml=.out)
CC = $(HOME)/HOL/bin/hol
.PHONY: all clean view full edit
all: $(TGTS)
clean:
rm -f $(OBJS) $(TGTS)
view: all
open -t $(TGTS)
full: clean all view
edit:
open -a xcode Makefile $(SRCS)
%.out: %.sml
$(CC) < $< > $@
____________________________________________________
types.sml
____________________________________________________
(* TO DO List
HOL terms vs. types (different syntactical category)
LCF: rules of inference (type thm)
terms as trees?
* type operators: fun, pair, list
* pairs
* 3 extensions
*)
(* prove that a figure - a number from 0 to 9 - exists *)
app load ["Q"]; open arithmeticTheory;
val figure_def = Define `figure a = a < 10`;
g `?x. figure x`;
e (RW_TAC arith_ss [figure_def]);
val FIGURE_EXISTS = top_thm();
drop();
(* create type "figure" (tyfi) and an object (a variable) of that type *)
val figure_axiom = new_type_definition ("tyfi", FIGURE_EXISTS);
(* show new type *) types "-";
val figure_object = ``a:tyfi = a``;
(* show type of object *) set_trace "types" 1; figure_object;
(* show type of object *) set_trace "types" 2; figure_object;
set_trace "types" 0;
(* But figure 3 doesn't have type "tyfi",
which would be desirable, and the following fails:
``3:tyfi``;
The reason is, that in HOL terms can only have a single type.
(Types are disjoint.) *);
type_of ``3``;
(* show universal quantifier *)
dest_comb ``!x.x``;
(* show type of universal quantifier *)
type_of ``$!``;
(* find theory of universal quantifier *)
dest_thy_const ``$!``;
(* show some information about the theory "bool" *)
thy "bool";
axioms "bool";
definitions "bool";
theorems "bool";
constants "bool";
types "bool";
ancestry "bool";
(* show some information about the theory "min" *)
types "min";
constants "min";
(* interactively we could do:
help "arithmeticTheory";
*)
(* find definition in database *)
DB.find "FORALL_DEF";
DB.match ["arithmetic"] ``SUC n * x``;
(* type definition example from kananaskis-10-reference.pdf, p. 630 *)
app load ["PairedLambda", "Q"]; open PairedLambda pairTheory;
val tyax =
new_type_definition ("three",
Q.prove(`?p. (\(x,y). ~(x /\ y)) p`,
Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));
open arithmeticTheory;
val divides_def = Define `divides a b = ?x. b = a * x`;
set_fixity "divides" (Infix(NONASSOC, 450));
val prime_def = Define `prime p = ~(p=1) /\ !x. x divides p ==> (x=1) \/ (x=p)`;
g `!x. x divides 0`;
e (RW_TAC arith_ss [divides_def]);
e (EXISTS_TAC ``0``);
e (RW_TAC arith_ss []);
restart();
e (RW_TAC arith_ss [divides_def] THEN EXISTS_TAC ``0``
THEN RW_TAC arith_ss []);
____________________________________________________
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
