[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] notes on isabelle vs. mizar


Hi Makarius,

On Thu, 7 Feb 2008, Makarius wrote:


On Thu, 7 Feb 2008, Josef Urban wrote:


someone here might be interested a couple of fairly raw (and sometimes
probably incorrect) notes comparing some features of isabelle and mizar:
http://www.google.com/notebook/public/13713103740520825807/BDQ7EQwoQw4TZgfwi .


Just some notes on this from the Isabelle perspective.


thanks


* Semantics:

Isabelle/Pure (the logical framework) and Isabelle/HOL (a major
application within that) should not be confused, as appears to be done in
the discussion about axiomatic vs. definitional extensions.
it is about I/HOL; I obviously was interested in I/ZF, but e.g. sledgehammer (ATP) is now only implemented for I/HOL (Larry says that nobody uses I/ZF, and there is no library communication between I/HOL and I/ZF (hence also my interest in I/HOLZF)) 


Starting from the Pure theory, initial extensions are usually axiomatic
(declaring types, consts, axioms), in order specify an object-logic (say
FOL, ZF, HOL, HOLCF).  Normal applications never do this -- it would
require to reconsider the whole logical foundations of axiomatizations.
Isabelle does provide proper definitional elements that are also
explicitly checked, similar to HOL4 and HOL-Light (although the latter is
much more picky about this).

At times, some adventurous individuals do extend an existing logical base
by new axioms, as has been done for HOLCF (HOL + Scott domain theory) and
HOLZF (HOL + ZF axioms).

If you look at regular applications within Isabelle/HOL or Isabelle/ZF it
is all just definitions and proofs, as in Mizar.


yes, that's what I was told later too by Tom & Mike (for HOL)


* Locales, type classes vs. structures: It would be *very* interesting to
look more closely at this.  I would also like to understand Mizar
aggregates better, especially the version that has been presented at MKM
2007.
the two things are quite close; ATCs can have axioms packed with them, and existence does not have to be proved, while for structures one adds axioms later (usually via Mizar attributes), and has to prove non-emptiness of such "axiomatic types"; also ATCs are higher-order, while structures can only contain "small" things, i.e. sets; so ATCs are probably also close to IMPS' little theories 


* Set theory in Isabelle/HOL:

You write "I wonder how one gets around the limitation that sets is
defined as a predicate on a particular type".  Well you just suffer, and
restrict yourself to applications where this does not matter, or is even
quite natural in the first place (e.g. modeling programming-style
concepts, similar to ML or Haskell).

Personally, I would like to move on to full set-theory in the style of
Isabelle/ZF.  But this would need a layer for proper syntactic type
checking, similar to the present one in HOL, but without the theoretical
limitations.  In his paper on TPHOLs 2007, Freek makes a point about a
type-system being either "foundational" (as in HOL or Coq) or just a
convenience for the user, claiming that the latter is what you want.
yet that presentation looks quite "foundational" :-) ; yes, I think this is an old Mizar opinion (be practical and not dogmatic about the type system). On the other hand, I am hoping to provoke more opposition/explanation from "type fundamenta"-lists about this: first, because one chooses foundations also for practical reasons, second, because the Mizar type system is much less theoretically explored and could use some streamlining (IMHO) 


* Automation:

You say "automation much better in Isabelle".  Well, Isabelle/Pure merely
provides higher-order unification, which is nice but not so much
automation.  Everything else is implemented on top of the existing system.


yes, I meant the top layer


The important point here is that this can be done, i.e. Isabelle is an
open system, unlike Mizar.
Isabelle is open and much better documented; on the other hand, there are at least three open interfaces for doing things with Mizar (XML, MML Query, and MPTP exports) which can be used for producing interesting tools. And it's unfortunately quite fruitless to get started on this forum again on the necessity of openness and peer review of academic software intended to check mathematical proofs. 


You say "large parts of the library are not distributed with Isabelle only
available through http://afp.sourceforge.net/ this will eventually lead to
their incompatibility with the system and distributed library".

AFP is surprisingly easy to maintain.  We do it continously as we go on
modifying the main Isabelle distribution.  So these two are practically in
sync all the time.  There are official AFP distributions corresponding to
official Isabelle releases.


I sse, very good.


You say "Browsing of Isabelle formalizations sucks".


sorry, I should have toned down that bit before publishing


 I basically agree,
but nobody really browses the sources or HTML pages.
I think HTML (just browser) is very useful for many people. And it's not much work to have the code HTML-ized (I did a crude perl hack for HOL Light a while ago (http://lipa.ms.mff.cuni.cz/~urban/hol_light_html/) and it helped me alot to learn about it). ML-hackers should be able to re-use the ML parser and produce good HTML quite easily. 


Did you try
find_theorems within the live Isabelle session?
Yes, it is nice and useful, but (AFAIK) it does not let you to click on a symbol and go to its definition. 


You say "some Isabelle formalization have ML code in them this should be
completely hidden from mathematicians, Mizar seems to be better just for
browsing formal mathematics".  I disagree with that.  While ML is harder
to read than common Isabelle/Isar source specifications, it is an integral
part in building up the library, enabling almost arbitrary extensions to
the system as you move on.
OK, that's your choice. Mathematicians certainly can learn programming languages, but I still think they shouldn't be scared away by their inclusion into "normal mathematical presentations". 


Some details can be still improved, but we
have gone a far way from the traditional ``LCF'' approach of ML-only
theories that is still present in HOL / HOL-Light (here even basic
specifications and proofs are all in ML).  Isabelle has always tried to
minimize ML, but not to abolish it.  Recently we have even started to
integrate ML into Isar more seriously.
This certainly also depnds on the intended applications of the proof assistant. 


* Isar vs. Mizar:

I would say you can practically forget about "thus" and "hence" in Isar --
today I would prefer to get rid of these slightly odd abbreviations of
"then show" and "then have" altogether.  Apart from the shared "assume",
this makes the keywords of both proof languages almost disjoint, which is
adequate, as the exect meaning is quite different.


OK


* Proof General:

You write "It is a nuisance that Proof General has to stop Isabelle
running for one buffer". Most users just invoke several isabelle-interface
processes at the same time as required, e.g. when porting existing
libraries from one version of Isabelle to another.
Yes but this is not good when I just want to browse the library and have to start a new instance each time I want to (have to) use "find_theorems" for another theory. 


This does not mean
that Proof General is the last word on user interfaces for theorem
provers.

The interaction model of Proof General is that of traditional interactive
proof checkers (LCF, HOL, Coq etc.).  Isabelle/Isar also emulates this,
because of its heritage, but it is much more flexibile inside.  At the
TYPES workshop at Edinburgh last fall, I've proposed an interaction model
that is essentially a synthesis of Mizar-style whole-text processing with
traditional LCF-style interaction, see also
http://homepages.inf.ed.ac.uk/rpollack/mathWiki/slides/Wenzel.pdf
I also think that even the interactive provers are pretty fast today. I used Proof General in the "block checking mode" ("go to point") all the time - not much difference to working with Mizar. 

Josef