Email Gateway (Aug 22 2022 at 11:54): Email Gateway (Aug 22 2022 at 11:54):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have been playing around with some analytic combinatorics lately,
asking questions like ‘How many values are there of a given datatype
with a certain size?’
For this, it is very convenient to view the definition of the algebraic
datatype in terms of a (possibly recursive) sum of products. For
instance, for binary trees, I have the following "encodings":
datatype 'a bintree = Leaf 'a | Node "'a bintree" "'a bintree"
primrec encode_bintree :: "'a bintree ⇒ 'a + 'a bintree × 'a bintree" where
"encode_bintree (Leaf x) = Inl x"
| "encode_bintree (Node l r) = Inr (l, r)"
fun decode_bintree :: "'a + 'a bintree × 'a bintree ⇒ 'a bintree" where
"decode_bintree (Inl x) = Leaf x"
| "decode_bintree (Inr (l, r)) = Node l r"
Essentially, I exploit the fact that ‘α bintree’ is a fixed point of
'λα. α + (α bintree)²' and therefore ‘α bintree’ is isomorphic to ‘α + α
bintree × α bintree’.
My question is now: is there an easy way to generate these encode/decode
isomorphisms automatically and prove that they are inverses of one
another? Is there perhaps a similar construction inside the internals of
the datatype package already?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
The BNF package internally generates such unfolding and folding constants. They are called
ctor_<typename> and dtor_<typename>. Internally, it also proves that they are inverses of
each other, but AFAIK these theorems are only made available if the attribute bnf_note_all
is set at the declaration time of the datatype.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 11:54):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Manuel,
Andreas gave you the most important pointer. Since you seem to be envisioning an ML command for generating them automatically, I suspect you will want to access the ML interfaces of the BNF package directly, and not use "bnf_note_all" (which is mostly useful for debugging and/or for sketching BNF extensions).
The low-level theorems you'd need, e.g. "ctor_dtor", are stored in the BNF (co)datatype database:
ML {*
BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name bintree}
|> the
|> #fp_res
|> #ctor_dtors
|> hd
*}
You might find the code in "~~/src/HOL/Library/bnf_lfp_countable.ML" a useful source of inspiration. The "mk_encode_funs" function constructs a "to_nat" function for a datatype (LFP) from "to_nat" functions about the types on which it depends. If you find that of any interest, I can send you the (more readable) theory files that mock up the construction performed at the ML level.
Incidentally, I'm tempted to rename "ctor" to "in" and "dtor" to "out", in keeping with some of the literature, to avoid any confusion between the actual high-level constructors (called "ctr"s in the code and some theorems) and the low-level constructors. If anybody is against this renaming, please speak out now.
Jasmin
Email Gateway (Aug 22 2022 at 11:55):From: Dmitriy Traytel <traytel@inf.ethz.ch>
I am against the renaming. Note that “in” is a keyword in ML and you would need to start decorating the identifiers in the ML code with “x”, “‘“ or “0”. Also in/out are much less symmetric than ctor/dtor. We have actual code that is parametric in the view (there the name xtor is used).
Dmitriy
Email Gateway (Aug 22 2022 at 11:55):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I am against the renaming. Note that “in” is a keyword in ML and you would need to start decorating the identifiers in the ML code with “x”, “‘“ or “0”.
We have clashes with many other names, e.g. "rec" (a keyword, or a recursor), "map", "fold" (ML functions one does not want to shadow), even "in"... (Grep "recx", "mapx", "foldx", "inx".) Such clashes, and their crude fix with an "x", are not pretty, but they are a reasonable price to pay for having the right names at the Isar level.
But there is in fact a possible confusion at the ML level, which is much worse than the inelegant "inx": "in" is already used in the code for set membership (\<in>), e.g.
val inx = mk_in Asets sets T;
So maybe statu quo is best for now.
Also in/out are much less symmetric than ctor/dtor. We have actual code that is parametric in the view (there the name xtor is used).
"in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".
Jasmin
Email Gateway (Aug 22 2022 at 11:55):From: Manuel Eberl <eberlm@in.tum.de>
Thanks, that already looks like pretty much exactly what I want.
Another problem is that I need a kind of parameterised ‘size’ function,
which simply adds together the size of all the contained objects while
ignoring the structure of the datatype itself.
Essentially, for a datatype ‘α foo’ with a single type parameter, the
behaviour should be something like
size_foo sz x = setsum sz (set_foo x)
Or, in other words: I would something that works like datatype's builtin
size_foo, but without counting the structure of the datatype itself.
(e.g. I would the size of ‘[0,0,0]’ to be 0, not 3)
How would I best go about doing something like this generically for
datatypes with arbitrarily many type parameters? This is not a very
urgent question; the above construction with set_foo works fine for one
parameter and one parameter is all I currently need, but it would be
nice to know.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:55):From: Manuel Eberl <eberlm@in.tum.de>
size_foo sz x = setsum sz (set_foo x)
Apologies, this is, of course, rubbish – multiple occurrences must, of
course, be counted multiple times!
Email Gateway (Aug 22 2022 at 11:55):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
There is no generic construction like that at the moment in BNF, but it would be easy to
define. Have you looked at how the existing size function works? For polymorphic types
like 'a list, there is a more general function size_list which takes a size function for
the type argument. The size_list function sums the given function over all elements of a
list and then adds the list structure to it. So if you just want the sum over the
elements, how about using list_size f xs - size xs? Alternatively, you can also copy the
size plugin and change it to produce the function you need.
Of course, this only works for datatypes for which the size plugin can generate size
functions. For example, I have not yet tried whether there is also a size function if the
datatype contains finite sets and multisets.
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:56):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Andreas wrote:
Of course, this only works for datatypes for which the size plugin can generate size functions. For example, I have not yet tried whether there is also a size function if the datatype contains finite sets and multisets.
Interesting examples. These actually work, thanks to a hook in the "size" plugin:
HOL$ grep BNF_LFP_Size /thy
Library/FSet.thy:BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
Library/Multiset.thy: BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
Jasmin
Email Gateway (Aug 22 2022 at 11:56):From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,
this is very nifty, thanks for the hint! Maybe at some point we can use
this to support generic programming à la de Vries & Löh
(<http://www.andres-loeh.de/TrueSumsOfProducts/TrueSumsOfProducts.pdf>).
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:56):From: Manuel Eberl <eberlm@in.tum.de>
So if you just want the sum over the elements, how about using
list_size f xs - size xs?
That's a great idea. It may not be the most elegant solution, but it
sounds pretty foolproof. Thanks!
Email Gateway (Aug 22 2022 at 11:56):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Incidentally, for the record, this would have led to off-by-one bugs with the old datatype package. From "datatypes.pdf":
"The size function has a slightly different definition. The new function returns 1 instead of 0 for some nonrecursive constructors. This departure from the old behavior made it possible to implement size in terms of the generic function t.size_t."
In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.
Jasmin
Email Gateway (Aug 22 2022 at 11:56):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/11/2015 10:01, Jasmin Blanchette wrote:
On 18.11.2015, at 09:52, Manuel Eberl <eberlm@in.tum.de> wrote:
So if you just want the sum over the elements, how about using
list_size f xs - size xs?That's a great idea. It may not be the most elegant solution, but it
sounds pretty foolproof.Incidentally, for the record, this would have led to off-by-one bugs with the old datatype package. From "datatypes.pdf":
"The size function has a slightly different definition. The new function returns 1 instead of 0 for some nonrecursive constructors. This departure from the old behavior made it possible to implement size in terms of the generic function t.size_t."
When I read "some" I wondered what that means. Experimentally I found:
datatype t1 = A bool
==> size (A True) = 0
datatype 'a t2 = A 'a
==> size (A True) = 1
I understand why, but I am not convinced this difference in behaviour is
beneficial for users of size.
In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.
I could have told you that because that is one of the reasons for the old
design. Experience, not only doctrine.
Tobias
Jasmin
Email Gateway (Aug 22 2022 at 11:56):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
When I read "some" I wondered what that means. Experimentally I found:
datatype t1 = A bool
==> size (A True) = 0datatype 'a t2 = A 'a
==> size (A True) = 1I understand why, but I am not convinced this difference in behaviour is beneficial for users of size.
Beneficial as opposed to what? Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible). And of course, the old way of doing things required two "primrec" definitions instead of one "primrec" and one simple "definition".
If I could go back in time, I'm still not sure if we would go for 100% compatibility with the old package or for the current scheme, but I would have brought it up for discussion on "isabelle-users". I suspect the outcome of the discussion would have been "don't fix it if it ain't broken".
In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.
I could have told you that because that is one of the reasons for the old design. Experience, not only doctrine.
I believe you are mistaking lethargy for strategy.
If the old design had been documented in any way, it might have helped me understand it and replicate it. But not only it wasn't documented, the odd behavior looked so much like an oversight (in terms of both behavior and code) that it didn't cross my mind to ask around. Had I realized for one second that there might be a deeper reason for the behavior, I would have not hesitated to bring this up.
If there is a strong consensus in favor of restoring the old behavior, it wouldn't be terribly hard for me to change things to how they used to be. But from what I understand, the porting pains where not very big and are now behind us, and the new behavior is actually useful sometimes (cf. Andreas's solution and Manuel's "foolproof" comment).
Jasmin
Email Gateway (Aug 22 2022 at 11:57):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/11/2015 11:56, Jasmin Blanchette wrote:
When I read "some" I wondered what that means. Experimentally I found:
datatype t1 = A bool
==> size (A True) = 0datatype 'a t2 = A 'a
==> size (A True) = 1I understand why, but I am not convinced this difference in behaviour is beneficial for users of size.
Beneficial as opposed to what?
Detrimental. In the above example an abstraction step now changes the behaviour
of size.
Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible).
I assume by "exhibits an odd difference in behavior" you mean some term
involving both size and size_t? They were never claimed or intended to have a
fixed relationship. You can of course view that as an advantage of the new
definition of size.
And of course, the old way of doing things required two "primrec" definitions instead of one "primrec" and one simple "definition".
That is an implementation advantage.
The raison d'etre of the old size function were termination proofs and for those
it works slightly better than the new schema. On the other hand there is the
relationship to size_t that seems to be useful in at least one case. Hence I am
not saying we must go back to the previous definitions. But your argument that
this feature was not documented and seemed crazy to you and that thus you felt
free to change it shows a cavalier attitude towards source code. Let me assume
in your favour that the change had no negative effect in the distribution and
the AFP and that the problems in IsaFor only showed up later.
Tobias
If I could go back in time, I'm still not sure if we would go for 100% compatibility with the old package or for the current scheme, but I would have brought it up for discussion on "isabelle-users". I suspect the outcome of the discussion would have been "don't fix it if it ain't broken".
In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.
I could have told you that because that is one of the reasons for the old design. Experience, not only doctrine.
I believe you are mistaking lethargy for strategy.
If the old design had been documented in any way, it might have helped me understand it and replicate it. But not only it wasn't documented, the odd behavior looked so much like an oversight (in terms of both behavior and code) that it didn't cross my mind to ask around. Had I realized for one second that there might be a deeper reason for the behavior, I would have not hesitated to bring this up.
If there is a strong consensus in favor of restoring the old behavior, it wouldn't be terribly hard for me to change things to how they used to be. But from what I understand, the porting pains where not very big and are now behind us, and the new behavior is actually useful sometimes (cf. Andreas's solution and Manuel's "foolproof" comment).
Jasmin
Email Gateway (Aug 22 2022 at 11:57):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible).
I assume by "exhibits an odd difference in behavior" you mean some term involving both size and size_t? They were never claimed or intended to have a fixed relationship.
If you define type U by nesting through type T, the "size" function of U will depend on "size_T" -- hence there is a connection between the two. The lack of uniformity of the old definition is visible in examples such as
(* with Isabelle2014 *)
datatype 'a x = X 'a
thm x.size
datatype 'a y = Y "'a y x" | Y'
thm y.size
value "size (X Y')" -- "returns 0"
value "size (Y (X Y'))" -- "returns 2"
But your argument that this feature was not documented and seemed crazy to you and that thus you felt free to change it shows a cavalier attitude towards source code.
The tone of some of your emails reveals a cavalier attitude towards the people who work or worked for or with you. We have had instances of passive-aggressive emails from your part regarding minor points of datatypes (minor compared with the scale of the whole BNF entreprise), some of it on-list, some off-list. You will remember how this ended. Because you had the courage to apologize, you came out of the deal as an (even) greater man in my eyes than before.
I had reasons to believe this would be the first and last time we would be going into that loop, but alas the same nonconstructive pattern is arising again -- and again in connection with the datatypes.
I would greatly appreciate if you could keep your comments -- whether on-list or off-list -- to objective observations, as opposed to a procès d'intention. I don't know what I've done to you to deserve this; clearly, I must have done something to annoy you, but I doubt it has anything to do with the "size" function. I would appreciate if you could tell it to me frankly off-list rather than through insinuations on-list.
I'm in Nancy this week. You can also pick up the phone if you think this would be more helpful. The phone number is on my web page.
Let me assume in your favour
(No comment on this condescending phrase.)
that the change had no negative effect in the distribution and the AFP
It had one negative effect on one AFP entry (Fitting), which was nearly trivial to work around.
and that the problems in IsaFor only showed up later.
That's correct.
Jasmin
Email Gateway (Aug 22 2022 at 11:57):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
But your argument that this feature was not documented and seemed crazy to you and that thus you felt free to change it shows a cavalier attitude towards source code.
For the record: I did not change the source code. The code for the new package had to be rewritten from scratch (a few hundred lines), and we had to choose how to design it. Compatibility was a high concern, but I failed to realize that this apparently minor issue would have any impact at all on existing formalizations (failing to think that anything of the form "0 <= ..." is trivial to prove), while leading to (in my eyes) a cleaner approach. Implementing the old approach wouldn't have been harder; but it just felt "uglier" and "wrong". Now I know better.
Overall, we managed to achieve very high levels of backward compatibility and actually pulled it off. The ongoing "Nominal2" vs. "Nominal" is reminder of how hard it is to subsume and replace an existing Isabelle package. We (I) have made bona fide errors along the way, but I think our record is remarkable and deserves more praise than criticism.
Jasmin
Email Gateway (Aug 22 2022 at 11:57):From: Makarius <makarius@sketis.net>
Definitely. I am impressed how the BNF datatype upgrade went through,
while the task was looking bigger and bigger as the years passed by. One
of the greatest engineering projects since Stonehenge!
Makarius
Email Gateway (Aug 22 2022 at 11:58):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Jasmin,
The only point I was trying to make is a very general one: In the absence of
external documentation, the source code should be taken seriously or questioned
but not just changed. I am sure we agree on this but in the light of the size
discussion I felt it was worth reemphasizing on the list. No insult intended.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 11:58):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Jasmin wrote:
"in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".
I don't have a strong position about these names. Just a historic note: These were initially called "fold" and "unfold,"
which I still think are the most accurate names. Of course, they clash with traditional combinator names, and this is why we renounced them.
All the best,
Andrei
-----Original Message-----
From: Jasmin Blanchette [mailto:jasmin.blanchette@inria.fr]
Sent: 17 November 2015 15:16
To: Dmitriy Traytel
Cc: Manuel Eberl; cl-isabelle-users@lists.cam.ac.uk; Andrei Popescu
Subject: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
I am against the renaming. Note that “in” is a keyword in ML and you would need to start decorating the identifiers in the ML code with “x”, “‘“ or “0”.
We have clashes with many other names, e.g. "rec" (a keyword, or a recursor), "map", "fold" (ML functions one does not want to shadow), even "in"... (Grep "recx", "mapx", "foldx", "inx".) Such clashes, and their crude fix with an "x", are not pretty, but they are a reasonable price to pay for having the right names at the Isar level.
But there is in fact a possible confusion at the ML level, which is much worse than the inelegant "inx": "in" is already used in the code for set membership (\<in>), e.g.
val inx = mk_in Asets sets T;
So maybe statu quo is best for now.
Also in/out are much less symmetric than ctor/dtor. We have actual code that is parametric in the view (there the name xtor is used).
"in/out" are semantically very symmetric. I invented "xtor" out of sheer desperation and would happily trade it against "inout" or "io" or even "thru".
Jasmin
Email Gateway (Aug 22 2022 at 11:58):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Tobias already clarified what he was aiming at, but let me chime in to say that I also was impressed with how professionally the new BNF datatypes were introduced and with the prompt support I got from Jasmin and everyone involved to help iron out the few issues it raised in our proofs.
It does deserve praise, I don’t think anyone doubts that.
Cheers,
Gerwin
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.
Last updated: Nov 21 2024 at 12:39 UTC