Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu

Dear Ken,

Please see *** below.

1. Which restriction was introduced in Isabelle (2016) in order to avoid the inconsistency of earlier versions revealed by Kunčar/Popescu? See (p. 3)

*** As explained in the paper, now the definitional dependency is tracked through types as well.

The definition of the constant c contains a free variable y.
Constant definitions in Gordon's original HOL do not allow free variables, but only "a closed term" [Gordon/Melham, 1993, p. 220; or (p. 33)].

*** No: y is also bound there, by a forall quantifier.

2. Are all types still constructed via the "typedef" mechanism?
The following formulation allows two interpretations: a mechanism on top of "typedef",
or a new mechanism at the same (basic) level as and in addition to "typedef":
"In the post-Isabelle 2012 development version, we have converted the numeric types int, rat, and real to use Lifting and Transfer. (Previously they were constructed as quotients with typedef, in the style of Paulson [6].)" (p. 17)

*** All these types, including int, rat and real, as well as all the (co)datatypes, are ultimately compiled into typedefs.

3. The main questions is, whether in Isabelle still all new types are (besides being tested for non-emptiness)
introduced with an axiom stating a mapping, like in Gordon's original HOL,
where for each new type an axiom is asserted saying that the new type is isomorphic to the defined (sub)set, cf. (p. 39).

*** Yes: One can also *declare* types (which are assumed non-empty).  But all the *defined* types come with the two functions
representing the back and forth isomorphisms with a subset of the host type.

Let me remark that the section "8.5.2 Defining New Types" in (pp. 173 ff.)
explaining "typedef" is quite hidden.
It would be desirable to have it in a separate logic manual like in the HOL4 logic part linked above.

4. Why should "dependent types" be "to a large extent incompatible with the HOL philosophy of keeping all types non-empty" as claimed at (p. 4)?
My R0 implementation is a dependent type theory, and there are no empty types in it.

*** Having all types non-empty is incompatible with the mainstream dependent type approach, where one uses the Curry-Howard isomorphism
to model propositions as types, with their elements representing proofs -- then the existence of empty types simply means that not everything is provable.


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