Email Gateway (Aug 22 2022 at 13:57): Email Gateway (Aug 22 2022 at 13:57):From: Ken Kubota <mail@kenkubota.de>
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
Email Gateway (Aug 22 2022 at 13:57):From: Lawrence Paulson <lp15@cam.ac.uk>
It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103
Larry Paulson
Email Gateway (Aug 22 2022 at 13:59):From: Ken Kubota <mail@kenkubota.de>
Dear Members of the Research Community,
Please allow me to add a few comments.
What Gordon calls "'second order' [lambda]-terms like \a. \x:a. x, [which]
perhaps [...] should be included in the HOL logic" at
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 22)
is implemented in R0 as the main feature of dependent type theory (i.e., the
binding of type variables with lambda) and called "type abstraction" there:
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 356 ff.)
It might be worth considering publishing this 2001 version of Gordon's paper
within the technical report series in order to ensure long-term (online)
availability of the currently only cached document. In addition, online
availability of the 1985 version (UCAM-CL-TR-68) is desirable, as it is still
of historical interest.
Also, I would like to thank Tom Melham for bringing to my attention his
approach of implementing in the HOL logic the idea of explicit quantification
over type variables as presented by Andrews in 1965: "I have found Andrews'
book [1] invaluable in working out many of the technical details of the
extension to HOL proposed here."
http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf (p. 15)
I have addressed this issue and discussed details in my draft: "It has to be
noted that already in his PhD thesis 'A Transfinite Type Theory with Type
Variables' published in 1965 Andrews is very near to developing a dependent
type theory. [...] In the system Q with type variables the universal quantifier
(∀) becomes a true variable binder in the case of types, but in the case of
terms (objects) a definition depending on λ." [Kubota, 2015, p. 31] However,
for some reason Andrews refrained from directly using lambda as type variable
binder, which would exhibit the reducibility of the variable binders to a
single one, as was done in R0.
Is it possible to figure out the author of this sentence? I am considering
quoting it and would like to credit authorship in such a case.
For this reason, and for other reasons, such as not constraining expressiveness
of the system, instead of postulating a (non-logical) Axiom of Infinity
(usually over the type of individuals), the Peano axioms should be part of the
definition of natural numbers (which can be expressed without axioms quite
simply and naturally in dependent type theory), that guarantees the set to be
infinite: "Actually, any set satisfying postulates P1-P4 must be infinite."
[Andrews, 2002, p. 259] Then there is no need to add an Axiom of Infinity as
Axiom 6, which extends Q0 to Q0^inf [cf. Andrews, 2002, p. 259].
For the same reasons, the use of language elements which make implicit use of
axioms should be avoided. Gordon correctly states: "The inclusion of
[epsilon]-terms into HOL 'builds in' the Axiom of Choice [...]." Somewhat
earlier on the same page, he quite frankly confesses: "It must be admitted that
the [epsilon]-operator looks rather suspicious."
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24)
Implicit use of the Axiom of Choice can be avoided by using the description
operator instead, like in Q0 and R0, where it is the counterpart to identity
(equality) [cf. Andrews, 2002, pp. 211, 213; Kubota, 2015].
For example, the "conditional term Cond t t_1 t_2 (meaning 'if t then t_1 else
t_2')" "defined using the [epsilon]-operator" at
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24)
can be defined using the description operator [cf. Andrews, 2002, pp. 235 f.
(5313)]; software verification of the formal proof has been provided in
[Kubota, 2015, pp. 165-174]. The (verification of the) formal proof and the
axioms for R0 have now been made available online at:
http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf
Please note that in Axiom 5 (Axiom of Descriptions) and throughout the whole
system the primitive symbol for identity (equality) 'Q' used in Q0 [cf.
Andrews, 2002, pp. 211, 213] was eliminated and replaced by the identity symbol
'=' in R0, as the symbol 'Q' syntactically doesn't have an own independent
function:
http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (pp. 351 f.)
It then becomes even more obvious that description is the counterpart to
identity, extracting the single element from a singleton (unit set), and
eliminating the identity symbol '='.
Technically, both Rule R and Rule R' are implemented in the dependent type
theory R0 as two different routines due to the access to different parts of the
formulae, but both routines then use the same subroutine. Rule R and Rule R'
are called §s and §s' in R0, where the section sign (§) indicates a rule, and
's' stands for substitution:
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 362 f.)
Rule §\ ('\' stands for lambda) denotes lambda-conversion (or more
specifically, beta-conversion), which in Andrews' Q0 is obtained as theorem
5207 [cf. Andrews, 2002, p. 218 f.] from Axiom Schemata 4_1 - 4_5. Since some
of the Axiom Schemata 4_1 - 4_5 contain restrictions, lambda-conversion was
implemented as a rule in R0. As the active elements, rules may contain
restrictions, but not theorems (including axioms/axiom schemata), which are
passive elements. This alternative method of implementing lambda-conversion was
already considered by Andrews in a paragraph to which he directed my attention
when I met him and which is already contained in the first edition (1986):
"5207 could be taken as an axiom schema in place of 4_1 - 4_5, and for some
purposes this would be desirable, since 5207 has a conceptual simplicity and
unity which is not apparent in 4_1 - 4_5." [Andrews, 1986, p. 165; Andrews,
2002, p. 214]
The fact that lambda-conversion is actually a process (i.e., active, dynamic,
and hence, a rule), and not only a (passive, static) theorem, axiom, or axiom
schema, becomes obvious in the online presentation of Q0, where Axiom Schemata
4_1 - 4_5 are replaced by 5207 as new Axiom Schema 4 which makes use of a
function "SubFree" denoting the process of substitution (of all free
occurrences of a variable):
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu
Similarly, in Church's simple theory of types, lambda-conversion
(beta-conversion) is implemented as the second (beta-reduction, also called
beta-contraction) and third (beta-expansion) of altogether six rules of
inference [cf. Church, 1940, p. 60].
Kind regards,
Ken Kubota
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.
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] (p. 1, 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.
Kub
[message truncated]
Last updated: Apr 25 2024 at 20:15 UTC