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

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.



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 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.


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