*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 17 Nov 2015 13:21:29 +0100*In-reply-to*: <564B1075.5060706@in.tum.de>*References*: <564B1075.5060706@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Hi Manuel,

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

**References**:**[isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

- Previous by Date: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: [isabelle] [Fwd: Re: Failing afp-2015 build]
- Previous by Thread: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list