Email Gateway (Aug 22 2022 at 13:40): Email Gateway (Aug 22 2022 at 13:40):From: Ken Kubota <mail@kenkubota.de>
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00070.html
Thank you for bringing this to my attention. Let me first comment on the
manuals before getting back to the type system.
It would be desirable to have such information - on the nature of the
"datatype" declarations - as well as on the low-level routines for type
inference and type introduction available in the manuals. Also, in order to
avoid misunderstanding, it should be pointed out that "BNF" is an abbreviation
of "Bounded natural functor" and not "Backus-Naur form".
For any type theory, including Isabelle/HOL, the type system is essential.
Hence, one would wish for a concise specification of the logical core, i.e.,
both the type system and the rules of inference. For example, Andrews' system
Q0 - the type system, symbols, wffs, axioms, and the single rule of inference -
is fully specified in a very precise manner on only a few pages [cf. Andrews,
2002, pp. 210-215].
Moreover, one would wish for a tutorial on how to inspect both the types
introduced by the datatype declarations as well as the type of any well-formed
formula, such that the user can look behind the surface and examine the
(actual) type system. In my R0 implementation, it is possible to display the
fully typed expression of any wff (including that of any primitive or derived
type), e.g., the logical AND (&), with a simple print command, which yields the
type (e.g., o -> o -> o [written as "{{o,o},o}", lambda is denoted by '\', and
lambda application is denoted by '_']):
":print &
g{{{o,o},o}}{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}]{@}){{o,@}}_[\g{{{o,o},o}}{{{o,o},
o}}.((g{{{o,o},o}}{{{o,o},o}}_x{o}{o}){{o,o}}_y{o}{o}){o}]{@}){o}]{{o,o}}]
type # 0: {{o,o},o} = 35"
For a formatted PDF version, see
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 356)
Concerning the type system, the most informative explanation I could find in
the documentation was at the very beginning of Part III (Isabelle/HOL) of The
Isabelle/Isar Reference Manual (February 17, 2016):
"Andrews'[ ] book [1] is a full description of the original Church-style
higher-order logic, with proofs of correctness and completeness wrt. certain
set-theoretic interpretations. The particular extensions of Gordon-style HOL
are explained semantically in two chapters of the 1993 HOL book [50]."
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf (p. 236)
Again, a brief description of the type system in the online documentation,
instead of only literature references, would be desirable.
Please allow me a minor correction here. In both the first edition [Andrews,
1986] referenced by the manual as well as the current second edition [Andrews,
2002] Andrews does not only provide a "full description of the original
Church-style higher-order logic", but, more exactly, a description of his own
system Q0, which is roughly equivalent, but much more elegant. For example, in
Church's simple type theory, Modus Ponens is a primitive rule (the fifth of
altogether six rules) [cf. Church, 1940, p. 60; Andrews, 2014, available online
at
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#AxiRulInf
], whereas in Andrews' Q0, Modus Ponens is a derived rule [cf. Andrews, 2002,
p. 224 (5224)] obtained from the single rule of inference of Q0. The type
system is identical, allowing only 'i' (iota) and 'o' (omicron), and
combinations of them (i.e., simple type theory, having no type variables).
In the dependent type theory R0, not only type variables, but also an
additional type inference mechanism is implemented, which seems to resemble
"Gordon['s] [...] facility to introduce new types as semantic subtypes from
existing types"
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf (p. 261)
: "Whenever a sentence of the form p_(oα)c_(α) is inferred [...], type p is
added to c, such that c_p becomes a well-formed formula." [Kubota, 2015, p. 32]
If it isn't already, p becomes (also) a type, by additionally assigning the
type of types (tau) to it.
The abstract of the article by Traytel et al. you referred to via the DOI link
http://dx.doi.org/10.1109/LICS.2012.75
starts as follows: "Interactive theorem provers based on higher-order logic
(HOL) traditionally follow the definitional approach, reducing high-level
specifications to logical primitives." This elegant formulation on the
"definitional approach" coincides with what Andrews calls "expressiveness"
[Andrews, 2002, p. 205], except that the reduction (or, in turn, the
expressiveness of the few primitive symbols and rules) does not only apply to
symbols, but also to the rules, such that the basis of Q0 consists of only
two primitive type symbols (the type of propositions 'o' and the type of
individuals 'i'),
and only a single rule of inference (substitution),
from which everything can be expressed (within the limits of simple type
theory).
For extending expressiveness to dependent type theory, in R0, type iota ('i')
is replaced by type omega (the universal type), and type tau (the type of
types) is introduced. Furthermore, it is possible to bind type variables with
lambda.
If one consequently follows Andrews' approach of expressiveness at all levels,
then Hilbert-style deductive systems are preferred, since they allow the rules
to be reduced to a single rule of inference. An extra rule for induction such
as that given at
https://www4.in.tum.de/~wenzelm/papers/lausanne2009.pdf (p. 5)
can be avoided by making induction part of the definition of N [cf. Andrews,
2002, p. 260]. In the same spirit, a primitive type for natural numbers can be
avoided by using a combination of 'i' and 'o' as carrier type ( nat := (o(oi))
) [cf. ibid.].
The pairing operation used by Andrews [cf. Andrews, 2002, p. 208] (see also the
definition of the logical AND (&) above, wff 47) is better suited for lambda
calculus than the one suggested at
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 13),
and in R0, it can be used to form both a type restricted as well as a
polymorphic pairing operator (by the use of type omega).
According to this approach, a proliferation of primitive types and type
inference mechanisms should be avoided, and rules should be kept as simple as
possible, e.g., as quoted above: "Whenever a sentence of the form p_(oα)c_(α)
is inferred [...]."
In one of the manuals it is stated:
"If you introduce a new type axiomatically, i.e. via typedecl and
axiomatization (§5.5), the minimum requirement is that it has a non-empty
model, to avoid immediate collapse of the logical environment."
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf (p. 115)
But what does this mean exactly, having "a non-empty model"? Is this the same
as the existence of a proven theorem of the form "p_(oα)c_(α)", which shows
that p is non-empty?
It will take some time until I am able to read through the article by Traytel
et al., but at first glance a more complex semantic reasoning seems to be
behind it:
"An inductive definition specifies the least predicate or set R closed under
given rules: applying a rule to elements of R yields a result within R. For
example, a structural operational semantics is an inductive definition of an
evaluation relation.
[...]
Both inductive and coinductive definitions are based on the Knaster-Tarski
fixed-point theorem for complete lattices. The collection of introduction rules
given by the user determines a functor on subsets of set-theoretic relations."
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf (p. 238)
Please allow me, where appropriate, to postpone answers, as I would like to
focus on my forthcoming publication of R0 [Kubota, 2015].
Kind regards,
Ken Kubota
References
Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type
Theory: To Truth Through Proof. Orlando: Academic Press.
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] (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
Last updated: Apr 26 2024 at 20:16 UTC