*To*: Corey Richardson <corey at octayn.net>*Subject*: [isabelle] Specification of the type system of Isabelle/HOL, expressiveness (was: Declaration of (co)datatypes)*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 25 Jul 2016 15:26:55 +0200*Cc*: "Prof. Peter B. Andrews" <andrews at cmu.edu>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1468731439.2162406.668416497.16BBD60D@webmail.messagingengine.com>*References*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de> <5F22105EAD3CAD4689EC4570AA1802B0BF0197C539@WGFP-EXMAV1.uni.mdx.ac.uk> <A6A56921-0B58-4CF4-9786-DBF6E77F286C@kenkubota.de> <1468731439.2162406.668416497.16BBD60D@webmail.messagingengine.com>

> 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

**References**:**[isabelle] Some corrections and amendments***From:*Ken Kubota

**[isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)***From:*Corey Richardson

- Previous by Date: Re: [isabelle] Private/qualified in locales
- Next by Date: Re: [isabelle] Plugin error with Isabelle-2016
- Previous by Thread: [isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)
- Next by Thread: [isabelle] Corrections of and amendments to prior publications on Goedel's First Incompleteness Theorem; Russell O'Connor's definitions for its proof in Peter B. Andrews' logic Q0; Comparison of the proofs by O'Connor and Paulson
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list