Email Gateway (Aug 19 2022 at 12:44): Email Gateway (Aug 19 2022 at 12:44):From: John Wickerson <johnwickerson@cantab.net>
Hi,
Could I make a feature request regarding the "definition" package?
Current status
Statements like { definition "foo (a,b) == blah /\ bleh" } are not accepted, since the definition package does not support tupled arguments.
Proposal
That the definition package allows tupled arguments. Slightly more generally, since (a,b) is just shorthand for the constructed term "Pair a b", I propose that the definition package should support pattern-matching of arguments whenever the types of those arguments have exactly one constructor. For instance, I could then write { datatype proc = Procedure string command } and { definition "exec (Procedure s c) == ..." }.
Current workarounds
Write { definition "foo == %(a,b). blah /\ bleh" }. But this changes the foo_def theorem, and doesn't look so visually nice.
Write { fun foo where "foo (a,b) = (blah /\ bleh)" }. But this changes the foo_def theorem, and I have to remember to use foo.simps instead. And I have to put extra parentheses around the definiens, because "=" has different precedence to "==". And I have to remove foo.simps from the simplifier if I don't want foo expanding all the time. And I prefer to reserve "fun" for proper recursive functions, which foo isn't.
Write { definition "foo a b == blah /\ bleh" }. But there are times when it's more idiomatic to tuple than to curry.
cheers,
John
Email Gateway (Aug 19 2022 at 12:45):From: Tobias Nipkow <nipkow@in.tum.de>
That would indeed be convenient and I have frequently felt like adding it to
Isabelle/HOL. HOL Light supports this, and maybe HOL4 too.
Tobias
Email Gateway (Aug 19 2022 at 12:45):From: Makarius <makarius@sketis.net>
For me this is a genuine "feature", i.e. could be done or could be done
differently. I've myself considered it around 1996, and rejected the idea
as too much extra complication (after discussion with Konrad Slind and
John Harrison).
We need to strive to remove more features that are not strictly
necessary. All this is a heavy weight, and some day the system will just
collapse due to the laws of gravity.
Makarius
Email Gateway (Aug 19 2022 at 12:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I feel uneasy about this idea, because “definition” is the low-level definitional mechanism of Isabelle, which doesn’t presume the existence of such things as ordered pairs. Your suggestion makes sense for Isabelle/HOL, but not in the wider context of generic theories, where ordered pairs may not exist. One of the specific purposes of “fun” is to support pattern matching.
Larry Paulson
Email Gateway (Aug 19 2022 at 12:45):From: John Wickerson <johnwickerson@cantab.net>
Hi Larry,
I see, yes, that sounds sensible. What about my slight generalisation, of pattern-matching an argument whenever its type has just one constructor? Ordered pairs don't always exist, but do datatypes always exist?
John
Email Gateway (Aug 19 2022 at 12:45):From: Michael Norrish <Michael.Norrish@nicta.com.au>
HOL4 does support this for its new_definition "primitive". Later theories can interpose pre and post transformations on the input term and the output theorem so that definitions appearing to be on tuples get turned into "real" definitions of the form var = rhs, and then turned back into the characterising theorem that the user expects. (Even handling f x = x + 1 uses this machinery.)
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:45):From: Tobias Nipkow <nipkow@in.tum.de>
Am 28/11/2013 21:35, schrieb Michael Norrish:
HOL4 does support this for its new_definition "primitive". Later theories can interpose pre and post transformations on the input term and the output theorem so that definitions appearing to be on tuples get turned into "real" definitions of the form
var = rhs, and then turned back into the characterising theorem that the user expects. (Even handlingf x = x + 1uses this machinery.)
Thanks, I thought so. Awesome how you manage to support all this complexity!
Tobias
Michael
On 29 Nov 2013, at 2:20, "Tobias Nipkow" <nipkow@in.tum.de> wrote:
That would indeed be convenient and I have frequently felt like adding it to
Isabelle/HOL. HOL Light supports this, and maybe HOL4 too.Tobias
Am 28/11/2013 15:55, schrieb John Wickerson:
Hi,
Could I make a feature request regarding the "definition" package?
Current status
Statements like { definition "foo (a,b) == blah /\ bleh" } are not accepted, since the definition package does not support tupled arguments.
Proposal
That the definition package allows tupled arguments. Slightly more generally, since (a,b) is just shorthand for the constructed term "Pair a b", I propose that the definition package should support pattern-matching of arguments whenever the types of those arguments have exactly one constructor. For instance, I could then write { datatype proc = Procedure string command } and { definition "exec (Procedure s c) == ..." }.
Current workarounds
Write { definition "foo == %(a,b). blah /\ bleh" }. But this changes the foo_def theorem, and doesn't look so visually nice.
Write { fun foo where "foo (a,b) = (blah /\ bleh)" }. But this changes the foo_def theorem, and I have to remember to use foo.simps instead. And I have to put extra parentheses around the definiens, because "=" has different precedence to "==". And I have to remove foo.simps from the simplifier if I don't want foo expanding all the time. And I prefer to reserve "fun" for proper recursive functions, which foo isn't.
Write { definition "foo a b == blah /\ bleh" }. But there are times when it's more idiomatic to tuple than to curry.
cheers,
John
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:45):From: Lawrence Paulson <lp15@cam.ac.uk>
Well, no, in general nothing exists.
Of course I see that “fun” might be cumbersome in such a simple case.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:10):From: Makarius <makarius@sketis.net>
vs. 'fun' / 'function' is not fully clear.
The 'definition' package is for "simple definitions". It wraps up the
basic Local_Theory.define concept, which in turn goes releatively straight
to primitive definitions of the logical core (which are not accessible to
users these days). It presents itself in an object-logic friendly manner,
to allow writing "f x y = rhs" (with HOL equality). The Pure form "f x y
== rhs" or even "f == %x y. rhs" is mostly historic -- it is only required
for object-logics like ZF that cannot internalize all forms of definition.
The conversion of the user specification is represented as higher-order
rewrite system via 'defn' rules -- whatever works here works, what doesn't
work doesn't.
The 'function' package is somehow dual: it incorporates as many features
as possible, just before gravitational collapse. Pattern matching
probably even outweighs the recursion / termination aspect.
(Interestingly, Scala is a higher-order functional language, where
recursion and pattern matching are separate. Odersky then uses his
remaining complexity budget elsewhere to make it more sophisticated than
ML or Haskell.)
The practical situation can be improved in a simple manner like this:
* Refrain from using == in definitions. Uniform = simplifies theories
and allows to move specifications between different tools and packages
more easily: 'theorem', 'definition', 'primrec', 'fun', 'function' etc.
* The function package could refrain from exposing its internal
construction of f as f_def. This was technically not possible when
first implemented, but is now just a matter how Local_Theory.define is
invoked. This also avoids well-known confusion due to unintended
"unfold f_def" seen routinely with fresh users.
Then the difference is just implicit simplification or not, and you write
something like:
fun f where [simp del]: "f (x, y, z) ((a, b), (u, v, w)) = rhs"
and make patterns as complex as the function package allows. Later you
simplify with f.simps as usual.
A side-alley of this thread is the old question, what the "unfold" proof
method or 'unfolding' command should really do. There are various
well-known anomalies in its wording and technical snags of "unfolding
f_def" where the equation does not always apply (because patterns don't
match).
So far I always considered a puristic approach more desirable (at least in
theory): reconstruct a precise equation "f == %x y z. rhs" from the
user-space equation f x y z = rhs. Really unfold that, and don't
rewrite with arbitray rules. Any such change and clarification is apt to
break existing applications, as usual.
An alternative speculation is this: "unfold f" takes a term f and looks up
its equational "Spec_Rules", which is a new concept from some years ago.
It then just rewrites with them by simplification, like the present f_def
or f.simps would do. This unifies 'definition' and 'fun' in that respect,
and makes the system appear more like Coq, where terms have canonical
"computation rules".
Makarius
Email Gateway (Aug 19 2022 at 13:10):From: John Wickerson <johnwickerson@cantab.net>
Thanks Makarius, particularly for the "where [simp del]" tip. That's much nicer than having to issue a separate "declare" instruction.
John
Email Gateway (Aug 19 2022 at 13:10):From: Makarius <makarius@sketis.net>
Concerning the fundamental laws of General Relativity in Software
Construction, I've recently found this interesting information about the
forthcoming JDK 8:
* http://openjdk.java.net/projects/jdk8/features#122
122 Remove the Permanent Generation
Remove the permanent generation from the Hotspot JVM and thus the need
to tune the size of the permanent generation.
* http://openjdk.java.net/projects/jdk8/features#173
173 Retire Some Rarely-Used GC Combinations
Remove three rarely-used combinations of garbage collectors in order to
reduce ongoing development, maintenance, and testing costs.
This is a major revolution -- I can imagine the screeming of some existing
users of the platform.
Sun never retired old things: there are tons of deprecated APIs from Java
1.0 until today. Oracle seems to recover some common sense now, seeing
that it cannot handle arbitrary weight, although Oracle is a much larger
company than Sun ever was.
Lets hope that JDK 8, when it is released next spring, will make a big
step forward (like JDK 7 did over JDK 6). Isabelle/Scala and its various
front-ends depend on it. (It is the weakest point in the PIDE equation.)
Makarius
Email Gateway (Aug 19 2022 at 13:15):From: Konrad Slind <konrad.slind@gmail.com>
Handling tuples in the input to the HOL4 definition mechanism
was definitely annoying. (Bear in mind that tuples would also
have to be handled for the derived induction theorem.) I think the
HOL4 implementation tries to handle arbitrarily nested tuple arguments,
but that is probably overkill.
Konrad.
Last updated: Apr 25 2024 at 01:08 UTC