Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes

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.


On 17/11/15 18:31, Manuel Eberl wrote:
size_foo sz x = setsum sz (set_foo x)
Apologies, this is, of course, rubbish â multiple occurrences must, of course, be counted
multiple times!

On 17/11/15 18:22, Manuel Eberl wrote:
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

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.



On 17/11/15 13:45, Jasmin Blanchette wrote:
Hi Manuel,

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?â
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

     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.


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