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



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.

Jasmin





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