[Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

[Ken K. <ma...@ke...>]

Dear Roger Jones,
Dear Tom,

Thank you very much for your hints.
Let me first pick up Tom's suggestion, and copy to the Isabelle mailing list, as it also affects Isabelle/HOL.


For HOL, now the "definability of new types" is named as the main feature at
	http://dx.doi.org/10.4444/100.111
as it is clearly the most important newness for classical higher-order logic, which doesn't exist
in Church's STT or Andrews' Q0. In order to preserve the information that HOL is implemented in ML, 
Stanford and Edinburgh LCF is distinguished, as Edinburgh LCF seems to mark the birth of ML,
according to Gordon's historical account.

I can't help emphasizing the clarity and precision of [Gordon and Melham, 1993],
in particular the logic part by Andrews Pitts.
If one takes the LCF approach of a small trusted logical kernel for serious, the logic has to be described in
a separate and clearly identifiable part, as the kernel should be a verified and therefore trusted, not a blindly trusted kernel.
Further, the extensions are clearly marked as "extensions" in the table of contents, and the use of
axioms ("Asserting an axiom", section 2.5.4 Extension by type definition) is clearly named:
	http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf

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
With a structure of the documentation similar to that of HOL, it would have become obvious that the
introduction of overloaded constant definitions for axiomatic type classes is not only a new feature or an
extension of the logic, but even a modification of the core of the logic itself, as something in between
a variable and a constant is introduced, which caused an inconsistency:
	http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3)
In their paper "A Consistent Foundation for Isabelle/HOL", Ondřej Kunčar and Andrei Popescu then
found a way to solve the problem, however, I have the feeling that their efforts are not honored
appropriately, as the discussion on the Isabelle mailing list about the reason for the inconsistency
ended up in nowhere.
Note that in HOL, extensions of the logic were made with the highest care, and an analysis
was made before, and not after an extension (or even a modification of the core) of the logic:
“[...] Dr Andrew Pitts was commissioned to validate HOL’s definitional principles.
He produced informal proofs that they could not introduce inconsistency
[Gordon and Melham, 1993, Chapter 16].” [Gordon, 2000, p. 175]

In R0, the interpretation of types is that of (nonempty) sets. Naturally, one would see, for example,
the number 3 as a natural number, and therefore has its type:
	3 : N   (or "3_N" in Tex/LaTeX notation)
If one defines the set of all numbers smaller than 5
	S5 := [\x.x<5]
then
	(S5 3)
is a provable theorem, and hence 3 has type S5 (= is element of the set of the numbers smaller than 5).
The consequence is, of course, that a mathematical entity may have several types, as naturally
one would like to express 3 : N, 3 : S5, or 3 : R (three is a real number).
PVS seems to allow this, too, as we also would have 3 : nonzero, in order to avoid division by zero:
	http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf (p. 715)
Since terms like [\x.x<5] (S5, the set of the numbers smaller than 5), can become a type, the strict
distinction between terms and types is removed, as when a theorem like
	(S5 3)
is obtained, S5 becomes a type by adding the types of types (tau) to it, and
to the number 3 the new type S5 is added.
Somewhere in [Gordon and Melham, 1993], it is written that in higher-order logic, unlike in first-order logic,
logical connectives are not a separate syntactic category anymore, but also become terms.
Similarly, with the mechanism described above, types are not a separate syntactic category anymore,
but terms of type tau, see for example the definitions with type abstraction at:
	http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf
Also, with type abstraction, axiomatic type classes can be expressed in a very natural way, without
having to modify the logic as done in Isabelle/HOL. The concept of axiomatic type classes
seems to be identical with what I tried to show with my definition of groups by proving a property
on groups, and then transferring that property to an entitiy which fulfils the definition of groups.
Note that the definition of groups in R0 doesn't need any axiom.
The only axioms required are the five axioms of Q0 (slightly modified: with type abstraction).


Concerning Roger Jones' remarks, let me first note that a legend ("significance of the shape of boxes")
can be found on top of the 2nd page, as it doesn't fit on the first anymore.

Please also note the arrow from lambda calculus (LC) to simple type theory (STT), narrowing the
interest to theories based on LC. The purpose is mainly to distinguish the logics based on LC
by their expressiveness in terms of their syntactic features, where STT is characterized by having no
type variables in their object language at all. From this perspective, the very early developments
prior to LC can be neglected, as Church's 1940 paper is the today's standard reference.
For me, even Church's 1940 logic is baroque, as I grew up with Andrews' Q0, which is much more
elegant, cleaner, and natural.
However, for historical accuracy, I already considered adding a quote mentioning Ramsey and Chwistek from
	http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf (p. 12)
in the Historical Notes section. Note that Church mentions both, and Carnap, in the first footnote
of his 1940 article.


Best regards,

Ken

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100


> Am 18.10.2016 um 15:34 schrieb Roger Bishop Jones <rb...@rb...>:
> 
> This is a bit of input to Ken Kubota's research, which has resulted in ProofPower appearing
> on his nice little genealogical diagram as "by Roger Jones", due to a bit of overgenerous
> credit given by Rob Arthan.
> 
> Rob and I usually describe each other in this kind of context as "co-architects" of ProofPower,
> which is a pretty weak characterisation of our relationship and contributions, but saves
> boring all with too much detail, which I am now going to do.
> 
> The story of ProofPower begins in 1986 when I was asked by Roger Stokes at ICL to join a
> new team set up to apply formal methods to the design and verification of highly secure
> computer systems.
> GCHQ/CESG had by then already decided that they wanted their contractors to work
> with the Z specification language and Roger Stokes was looking at Boyer-Moore and HOL
> as possible tools to use for reasoning about Z specifications.
> I pretty quickly decided that HOL was the better bet and set about making that work,
> initially using manual transcriptions from Z into HOL.
> 
> A couple of years later I had been put in charge of the "High Assurance" team, and
> an opportunity arose to undertake a collaborative R&D project part-funded by the UK
> government.
> I recommended that we put together a project under which ICL could develop a proof
> tool for Z working by semantic embedding of Z into HOL, and that to provide a stable
> basis for this work which would underpin the future business of the team we would
> do a new implementation of a HOL proof tool.
> This eventually was called "ProofPower" (primarily for marketing reasons, ICL then had
> several products with names ending in "Power" of which the most important was OfficePower).
> 
> So I put together a collaboration which included Cambridge University
> (actually the maths department doing some logical theory), Kent University (Keith Hanna)
> and Program Validation Limited (a Southampton University spin-off with a set of tools
> for static analysis and verification of programs in the SPARK subset of the Ada
> programming language).
> The idea to include the CU maths department was Mike Gordon's who was engaged by
> ICL as a consultant for the duration of the project, even though the Cambridge Computer
> Labs did not have a formal involvement.
> 
> So ProofPower was by baby, it was my idea, I put together the project, bid for the funding
> and most importantly, knowing that a full-time team leader was needed and that I could
> not devote all my time to it, I invited Rob Arthan to join us and lead the team.
> 
> In terms of contributions to that first project, Rob was the main force.
> I did not contribute a single line of code, but I was involved in all the design reviews
> that took place and some of the original features of the ProofPower implementation
> were suggested by me.
> My most substantial technical contribution was probably the design of the Z embedding,
> working out how the derived rules for reasoning with Z would work, and in some of the
> changes to the inference rules, tactics, and goal package which made the system sensitive
> to the characteristics of the embedded language, and made it possible to reason in Z
> without necessarily having to understand the mapping into HOL.
> (ProofPower was designed from the start to support logical pluralism via semantic embedding).
> 
> That's just about the original 3-year project which created ProofPower, in the subsequent history
> my own involvement has been very small.
> 
> If any single person should have the ProofPower by-line, then it should certainly be Rob,
> but I naturally prefer Arthan/Jones or some other joint attribution, because I still think
> of ProofPower as "my baby", in contexts where the entire team cannot be credited.
> 
> But this isn't one of them so here, for the record is the list of contributors:
> 
> Mark Adams
> Rob Arthan
> Kevin Blackburn
> Phil Clayton
> Adrian Hammon
> Adrian Hayward
> Roger Bishop Jones
> Dave King
> Gill Prout
> Geoff Scullard
> Roger Stokes
> Piotr Trojanek
> 
> My biggest regret is the divergence of ProofPower from the rest of the HOL community,
> though I don't know how we could then have prevented that from happening.
> "Open-source" was a pretty new idea then, particularly as far as industry was concerned.
> 
> 
> Credit for the Simple Theory of Types
> =======================
> 
> Ken's diagram makes it look like this theory begins with Church.
> 
> Its not entirely uncontroversial as to who should have credit for devising this system.
> Most frequently credit has been given to Ramsey, but though he seems to have had the
> idea pretty early on, he never formulated the logical system in detail (and one might think
> that the idea of simplifying Russell's ramified theory would have occurred to others).
> 
> Recent scholarship suggests that the first fully detailed account of STT as a formal
> system is due to Rudolf Carnap, who, in the course of writing a logistics textbook
> to facilitate the application of formal logic in mathematics and science, decided to
> base it around the simplified rather than the ramified type theory.
> I think this particular formulation may have escaped attention because the book
> "Abriss der Logistik" was written in German and has never been translated into
> English.
> Until recently the more widely know text by Hilbert and Ackermann was thought
> to be the first formal account of the simple theory of types.
> STT appears I  believe, only in the second edition of their text, so though the
> first edition (1928) precedes Carnap's (1929) text, he still was in first with STT.
> There were many later textbooks which presented this version of STT
> (not based on the lambda-calculus and having "power set" as the primitive
> type constructor), which was probably the dominant conception of STT
> (and may still be, among logicians) until Mike Gordon adopted
> and adapted Church's version for HOL.
> 
> So maybe a little circle with "(Ramsey/Carnap)" at the top of the STT box?
> 
> I wondered what the significance of the shape of boxes in the diagram was.
> It looked like most of the rectangles were proof tools and the elipses
> were theories, but that seems not quite consistent.
> 
> Roger Jones