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



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

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







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