Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon



It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103

Larry Paulson


> On 8 Aug 2016, at 12:13, Ken Kubota <mail at kenkubota.de> wrote:
> 
> Dear Members of the Research Community,
> 
> As part of my efforts to try to understand the type system of Isabelle/HOL, I 
> have gathered the references from the mails written by Corey Richardson and 
> Michael Norrish and from The Isabelle/Isar Reference Manual, especially from
> 	a) Chapter 10: Higher-Order Logic (pp. 236 f.)
> 	b) Â 11.7 Semantic subtype definitions (pp. 260-263)
> 	c) Â 11.8 Functorial structure of types (pp. 263 f.).
> 
> In all cases, with one exception, I was able to obtain either the link to the 
> online version or the ISBN number.
> 
> 
> The exception is Mike Gordon's text "HOL: A machine oriented formulation of 
> higher order logic" (Technical Report 68, University of Cambridge Computer 
> Laboratory), registered at
> 	http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-68.html
> 
> As Isabelle is provided by the University of Cambridge Computer Laboratory, 
> among others, would it be possible for the Isabelle developers to make this 
> technical report available online as a PDF file? This was done for the first 
> five reports listed at
> 	http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-table.html
> 
> According to the references supplied with the traditional (Mike Gordon's) HOL 
> variant, a revised version exists: "Technical Report No.\ 68 (revised 
> version)", quoted from
> 	https://github.com/HOL-Theorem-Prover/HOL/blob/master/Manual/Description/references.tex
> Either both versions or the revised version should be made available.
> 
> 
> I would like to take this opportunity to thank Michael Norrish for his advice. 
> The LOGIC part of HOL4 system's documentation at
> 	http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
> is the kind of short and precise formulation of the logical core I recently 
> proposed for Isabelle/HOL, too:
> 	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00105.html
> 
> In this HOL4 document, it is stated: "From a logical point of view it would be 
> better to have a simpler substitution primitive, such as 'Rule R' of Andrews' 
> logic Q0, and then to derive more complex rules from it." (p. 27)
> This is exactly the same idea that I presented recently: "The main criterion is 
> expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility of 
> mathematics to a minimal set of primitive rules and symbols. [...] For the 
> philosopher it is not proof automation but expressiveness that is the main 
> criterion, such that the method with the least amount of rules of inferences, 
> i.e., a Hilbert-style system, is preferred, and all other rules become derived 
> rules."
> 	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00028.html
> 
> Similarly, the HOL4 document argues in favor of definitions instead of 
> introducing new axioms: "The advantages of postulation over definition have 
> been likened by Bertrand Russell to the advantages of theft over honest toil. 
> As it is all too easy to introduce inconsistent axiomatizations, users of the 
> HOL system are strongly advised to resist the temptation to add axioms, but to 
> toil through definitional theories honestly." [p. 33]
> In the same manner, I wrote: "One consequence [...] is to avoid the use of 
> non-logical axioms. [...] The appropriate way to deal with objects of certain 
> properties is to create a set of objects with these properties." [Kubota, 2015, 
> p. 29]
> For this reason, in the R0 implementation, the group axioms are expressed not 
> as axioms, but as properties in the definition of "Grp" (wff 266):
> 	http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 359)
> 
> 
> Kind regards,
> 
> Ken Kubota
> 
> 
> 
> Sources
> 
> [S1] The Isabelle/Isar Reference Manual (February 17, 2016)
> 	http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf
> 
> [S2] Reference in the e-mail written by Corey Richardson
> 	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00070.html
> 
>    Dmitry Traytel / Andrei Popescu / Jasmin C. Blanchette, Foundational, 
> Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to 
> Theorem Proving
> 	http://dx.doi.org/10.1109/LICS.2012.75
> 	https://www21.in.tum.de/~traytel/papers/lics12-codatatypes/codat.pdf
> 
> [S3] Reference in the e-mail written by Michael Norrish
> "The chapters from the HOL book mentioned above are available as part of the 
> HOL4 system's documentation at:
> 	http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf/download
> See Â2.5.4 in particular for a discussion of how the system can be extended 
> with new types."
> 
>    The HOL System: LOGIC (November 6, 2014)
> 	http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
> 
> 
> Derived References (from [S1], pp. 260-263)
> 
> [15] W. M. Farmer. The seven virtues of simple type theory. J. Applied Logic, 
> 6(3):267-286, 2008.
> 	http://imps.mcmaster.ca/doc/seven-virtues.pdf
> 
> [18] M. J. C. Gordon. HOL: A machine oriented formulation of higher order 
> logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985.
> 
> [50] A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, 
> Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 
> pages 191-232. Cambridge University Press, 1993.
> 	ISBN 0-521-44189-7
> 
> [57] M. Wenzel. Type classes and overloading in higher-order logic. In E. L. 
> Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs 
> '97, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997.
> 	http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
> 
> [22] F. Haftmann and M. Wenzel. Constructive type classes in Isabelle. In T. 
> Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES 2006, 
> volume 4502 of LNCS. Springer, 2007.
> 	http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf
> 
> [27] O. Kuncar and A. Popescu. A consistent foundation for Isabelle/HOL. In C. 
> Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International 
> Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume 
> 9236 of Lecture Notes in Computer Science. Springer, 2015.
> 	http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf
> 	http://andreipopescu.uk/pdf/ITP2015.pdf
> 
> 
> Standard References
> 
> Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type 
> Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9 
> (Hardcover). ISBN 0-12-058536-7 (Paperback).
> 
> Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type 
> Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: 
> Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.
> 
> Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of 
> Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at 
> http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 2, 
> 2016).
> 
> Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: 
> Journal of Symbolic Logic 5, pp. 56-68.
> 
> 
> Further References
> 
> Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, 
> 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 
> 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 
> 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: 
> http://dx.doi.org/10.4444/100.10
> 
> Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and 
> pp. 754-755). Available online at 
> http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf 
> (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c 
> 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 
> 3d1047d1831bc357eb57b263b44c885b.
> 
> ____________________
> 
> Ken Kubota
> doi: 10.4444/100
> http://dx.doi.org/10.4444/100
> 
> 





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