Ken Kubota

2016-08-21 09:41:18 UTC

Dear Isabelle Developers,

Concerning the type definitions in Isabelle and the article by Ondřej Kunčar and Andrei Popescu, I have some questions.

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

http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3)

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

http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33)].

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].)"

http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf (p. 17)

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.

http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 39).

Let me remark that the section "8.5.2 Defining New Types" in

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/tutorial.pdf (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

http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 4)?

My R0 implementation is a dependent type theory, and there are no empty types in it.

Kind regards,

Ken Kubota

____________________

Ken Kubota

doi: 10.4444/100

http://dx.doi.org/10.4444/100

Concerning the type definitions in Isabelle and the article by Ondřej Kunčar and Andrei Popescu, I have some questions.

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

http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3)

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

http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33)].

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].)"

http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf (p. 17)

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.

http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 39).

Let me remark that the section "8.5.2 Defining New Types" in

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/tutorial.pdf (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

http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 4)?

My R0 implementation is a dependent type theory, and there are no empty types in it.

Kind regards,

Ken Kubota

____________________

Ken Kubota

doi: 10.4444/100

http://dx.doi.org/10.4444/100