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

Dear Andrei,

Thank you for the quick answer, and also thanks to Larry Paulson and Makarius Wenzel.

I had read the abbreviated notation with the forall quantifier too quickly, but still the third restriction specified at (p. 33) or at [Gordon/Melham, 1993, p. 220].
seems to be violated, as the type variable sigma occurs in the definiens, but not in (the type of) the definiendum.
Your example 
	c:bool = ~(AL x:sigma AL y:sigma  .  x = y)
is very similar to the standard example on the next page of the logic manual with type variable alpha not occurring in type of the definiendum "c:bool":
	c:bool = EX f: alpha -> alpha  .  One_One f /\ ~(Onto f)
It seems to me that a remedy simply would have been the restriction of Gordon's HOL (the third restriction).

Larry Paulson's argument at
seems to aim at a strict distinction between reasoning (inference) and circular definitions (language).
I doubt that this distinction can be made that strictly, since what restriction (iii) in Gordon's HOL tries to prevent,
in Andrews' logic is prevented by the restrictions on Rule R' [cf. Andrews, 2002, p. 214], where an inference from
	H  >  A = B   and   H  >  C
	H  >  C [A/B]
('H' denotes a set of hypotheses, '>' the turnstile) by substituting one occurrence of A in C by B is subject to a certain restriction
concerning variables, i.e., if a variable x is free in a member of H and free in (A = B).
If one steps from polymorphic to dependent type theory, type variables are also subject to binding (quantification),
such that type variable dependencies are preserved.
For example, from
	{}  >  ~(AL x:sigma AL y:sigma  .  x = y)
one could infer by the derived Rule of Universal Generalization (5220) [cf. Andrews, 2002, p. 222]
	{}  >  AL sigma:tau ~(AL x:sigma AL y:sigma  .  x = y)
(tau denotes the type of types) and then
	{}  >  F
because some types are singletons.
In other words, your c:bool would be F (false), because free (type) variables are implicitly universally quantified.
In contrast, if there were a condition upon sigma, for example, being bool: H = { sigma = bool }, then from
	{ sigma = bool }  >  ~(AL x:sigma AL y:sigma  .  x = y)
one couldn't use the derived Rule of Universal Generalization (5220) to infer
	{ sigma = bool }  >  AL sigma:tau ~(AL x:sigma AL y:sigma  .  x = y)
since (type) variable sigma occurs free in the set of hypotheses H, which violates the condition of rule 5220,
which is a condition derived from Rule R', since 5220 (like all rules in Q0 except Rule R/R') is a derived rule.
Hence, circular definitions are prevented by the inference rule (the reasoning) in Q0/R0 in a very simple manner.

Best wishes,

Ken Kubota


Ken Kubota
doi: 10.4444/100

> Am 21.08.2016 um 12:17 schrieb Andrei Popescu <a.popescu at>:
> 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. 
> Best, 
>   Andrei 

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