Email Gateway (Aug 19 2022 at 13:56): Email Gateway (Aug 19 2022 at 13:56):From: Rob Arthan <rda@lemma-one.com>
I am trying to address a comment to this short paper proposing an improved method of constant specification in the non-Isabelle implementations of HOL: http://www.lemma-one.com/papers/hcddr.pdf. The comment is asking me to say more about Isabelle/HOL. My reason for excluding Isabelle/HOL when I first wrote the paper, was that I believed, based on hearsay and guesswork, that all the mechanisms for defining constants in Isabelle/HOL are founded on a primitive that is part of the logical framework and that supports definition via (non-recursive) equations. So anything like the HOL4 new_specification would be implemented under the covers using the Hilbert choice function. Is that correct?
Alternatively, so I can found out the answer for myself, can anyone point me at the definitive definition of the Isabelle/HOL logic, including the definitional mechanisms, please. (Sorry about all that definiteness :-)) The nearest I can find on the documentation page is the logics manual and that doesn’t seem to answer my question and is marked as out-of-date.
Regards,
Rob.
Email Gateway (Aug 19 2022 at 13:56):From: Makarius <makarius@sketis.net>
On Sat, 29 Mar 2014, Rob Arthan wrote:
I am trying to address a comment to this short paper proposing an
improved method of constant specification in the non-Isabelle
implementations of HOL: http://www.lemma-one.com/papers/hcddr.pdf. The
comment is asking me to say more about Isabelle/HOL. My reason for
excluding Isabelle/HOL when I first wrote the paper, was that I
believed, based on hearsay and guesswork, that all the mechanisms for
defining constants in Isabelle/HOL are founded on a primitive that is
part of the logical framework and that supports definition via
(non-recursive) equations.
There is a long story behind that, started by Larry some decades ago, but
it continously changed according to new requirements.
The original Pure logical framework by Larry merely had axiomatic
specifications, which were introduced as 'types', 'consts', 'rules'
(similar to LF).
In the mid-1990-ies we added a slightly restricted version of 'rules' that
was called 'defs', with a few local checks, but no global guarantees of
the well-formedness of the theory.
When I introduced the Isar theory syntax in 1998/1999, I renamed 'rules'
to 'axioms'. Later the 'defs' became a bit more serious, with some
non-local checks, to track dependencies of overloaded and non-overloaded
constants more explicitly. This was substantially refined in 2005, and
2007/2008.
Later the 'axioms' became 'axiomatization', with some explicit dependency
tracking of which constants are supposed to be axiomatized. The 'defs'
were also de-emphasized in favour of the Local_Theory.define abstraction,
which merely uses a restricted 'defs' form at the bottom: just c == t for
closed terms, and no longer any pre-conditions that were still allowed in
'defs'.
Isabelle/HOL relies on constant definitions of Isabelle/Pure in the above
form, but invents its own axiom schemes, notably 'typedef' (which is not
quite definitional as we all know).
Our current version of typedef is notable, since it does not depend on a
proven non-emptiness theorem in advance, it merely needs that to turn a
conditional axiomatization into an actual one. That formal trick makes
the constant definitions independent on the typedefs, because the
"meaning" of consts is not needed to introduce new typedefs.
So anything like the HOL4 new_specification would be implemented under
the covers using the Hilbert choice function. Is that correct?
There is indeed an Isabelle/HOL emulation of HOL4 new_specification called
'specification', which uses Hilbert choice + definition. It has an
alternative axiomatic personality without the Hilbert Choice, but that was
actually never used and is already deleted for the coming Isabelle
release.
In Isabelle2013-2 documentation
http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf there is
still a description of ax_specification, but its worries about exposing
the definition to the user are actually obsolete: with Local_Theory.define
the kernel produces a precise definition c == @x. ... at the very bottom,
but that is only for foundational purposes. After the next renovation of
the 'specification' element, it will just refrain from exposing that
definition to the normal fact name space, and the user will have a hard
time to come across it accidentally.
This is analogous to something that is "private" in Java. Normally
inaccesible and not to be worried about, but with some tricks you can get
it from the low-level JVM environment, because it is there for
foundational purposes
This separation of Local_Theory primitives vs. theory foundations at the
bottom circumvents some old problems, although it introduces new
complexity to be dealt with.
Makarius
Email Gateway (Aug 19 2022 at 14:17):From: Rob Arthan <rda@lemma-one.com>
Makarius,
Thanks again for that. My current plan for the paper is to not to exclude Isabelle/HOL, but to discuss it alongside the other implementations. Perhaps you could let me know if you there is anything wrong with the following outline of my understanding, based on your reply below.
Isabelle/HOl was first implemented in the early ‘90s after the unsoundness problem with type variables appearing on the right-hand side of a definition, c = t, but not on the left-hand side was known, so it never suffered from that problem. Its internal mechanisms for doing definitions have involved over the years, but the current position for type definitions is quite like HOL Light when you look right under the covers, i.e., new_specification is emulated using an equational definition and Hilbert choice. However, Isabelle has information-hiding mechanisms that are more powerful than HOL Light’s, so this is not so problematic in practice. I think it is also fair to say that locales in Isabelle/HOL provide an alternative abstraction mechanism that can be used as a replacement for the kind of abstraction offered by new_specification, in that it lets you identify the abstract properties needed to carry out a given set of proofs without requiring you to be explicit about the actual types and constants that satisfy those properties. Locales (or a slight variant of them) would perhaps give you a nice way of implementing the generalised new_specification proposed in my paper.
Do you do anything to avoid the potential problem whereby two calls of new_specification with the same predicate will result in provably equal constants if you implement new_specification naively with Hilbert choice. E.g., ?x.1 < x < 10 used to define c and d? This is addressed in HOL Light along the following lines: it defines a function on the natural numbers such that 1 < x(n) < 10 for all n, and then defines c = x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light has been asked to define.
What you say about type definitions in Isabelle/HOL sounds interesting and is reminiscent of what we do in ProofPower to allow users to defer consistency proofs.
Regards,
Rob.
Email Gateway (Aug 19 2022 at 14:17):From: Rob Arthan <rda@lemma-one.com>
Makarius,
Thanks again for that. My current plan for the paper is to not to exclude Isabelle/HOL, but to discuss it alongside the other implementations. Perhaps you could let me know if you there is anything wrong with the following outline of my understanding, based on your reply below.
Isabelle/HOl was first implemented in the early ‘90s after the unsoundness problem with type variables appearing on the right-hand side of a definition, c = t, but not on the left-hand side was known, so it never suffered from that problem. Its internal mechanisms for doing definitions have involved over the years, but the current position for type definitions is quite like HOL Light when you look right under the covers, i.e., new_specification is emulated using an equational definition and Hilbert choice. However, Isabelle has information-hiding mechanisms that are more powerful than HOL Light’s, so this is not so problematic in practice. I think it is also fair to say that locales in Isabelle/HOL provide an alternative abstraction mechanism that can be used as a replacement for the kind of abstraction offered by new_specification, in that it lets you identify the abstract properties needed to carry out a given set of proofs without requiring you to be explicit about the actual types and constants that satisfy those properties. Locales (or a slight variant of them) would perhaps give you a nice way of implementing the generalised new_specification proposed in my paper.
Do you do anything to avoid the potential problem whereby two calls of new_specification with the same predicate will result in provably equal constants if you implement new_specification naively with Hilbert choice. E.g., ?x.1 < x < 10 used to define c and d? This is addressed in HOL Light along the following lines: it defines a function on the natural numbers such that 1 < x(n) < 10 for all n, and then defines c = x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light has been asked to define.
What you say about type definitions in Isabelle/HOL sounds interesting and is reminiscent of what we do in ProofPower to allow users to defer consistency proofs.
Regards,
Rob.
Email Gateway (Aug 19 2022 at 14:17):From: Makarius <makarius@sketis.net>
There is nothing like this in the 'specification' command of Isabelle/HOL,
but that add-on feature from 2004 got hardly ever used in practice. It
also fell behind a lot concerning general system infrastructure for
Isabelle specifications.
I have recently asked around the canonical question if 'specification'
should be be removed or renovated, and it came out a slight tendency
towards renovation (after removal of some of its obsolete sub-features).
Locales are indeed better in most situations to work in a context of
abstract term parameters with some logical premises in the local context.
Almost all specification mechanisms in Isabelle/HOL are now "localized",
i.e. work in such hypothetical situations of "fixes" and "assumes", so
that is a real practical benefit. The cost for it is increasingly complex
system infrastructure (outside the core logical framework).
Makarius
Email Gateway (Aug 19 2022 at 14:17):From: Makarius <makarius@sketis.net>
Another observation about this detail: this approach of HOL Light assumes
a single linear theort context. In Isabelle we've had a DAG of theories
(with merge), ever since Larry introduced that in 1989. One could still
do a similar trick there, but with more structure for these intro-logical
indentifiers.
Makarius
Email Gateway (Aug 19 2022 at 14:17):From: Rob Arthan <rda@lemma-one.com>
Makarius,
Good point! This trick wouldn’t work properly in HOL4 or ProofPower for exactly the same reason.
Regards,
Rob.
Last updated: Nov 21 2024 at 12:39 UTC