[isabelle] Specification of the type system of Isabelle/HOL, expressiveness (was: Declaration of (co)datatypes)



> The datatype declarations written in theory files is surface syntax for
> the underlying datatype package which handles proving non-emptiness
> among many other properties. The ML-style declaration is a convenient
> abstraction that is easy to use. The following paper explains the
	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 &
# wff      47 :  [\x.[\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])]]
#                                                           :=  &
# w typd   47 :  [\x{o}{o}.[\y{o}{o}.((={{{o,@},@}}_[\g{{{o,o},o}}{{{o,o},o}}.((
g{{{o,o},o}}{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}]{ at }){{o,@}}_[\g{{{o,o},o}}{{{o,o},
o}}.((g{{{o,o},o}}{{{o,o},o}}_x{o}{o}){{o,o}}_y{o}{o}){o}]{ at }){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 symbols (identity and description),
- 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





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