Prefix encoding of algebraic data types

I'm new to coding theory and formal proofs, and am struggling to understand how to construct and reason about prefix-free encoding algorithms on algebraic data types. I hope it's clear if I use notation from haskell below.

I'm tasked with writing a generic prefix encoding algorithm (encode) on ADTs, as well as giving guidance to my users in defining their own implementations of encode for their own types if they wish (this being a major reason I want to understand things better).

I've been jumping around sections of Berstel and Perrin's Theory of Codes which has been very helpful, but it's slow going and my goals are pretty narrow here.

One implementation

I believe I have one obvious implementation, which works like this:


for products, concatenate the results of applying encode to each of
the children (arguments to the constructor):

data P a b c ... = P a b c ...

encode (P a b c...) = encode a <> encode b <> encode c <> ...

for coproducts (or a sum of products), assign to each constructor a
distinct number tag (using a prefix encoding, to be pedantic) which
will start the code word, then apply the product rule above

data XYZ a b c d... = X a b ... | Y c d ... | Z ...

encode (X a b...) = encode 1 <> encode a <> encode b <> ...
encode (Y c d...) = encode 2 <> encode c <> encode d <> ...
encode (Z ...)    = encode 3 <> ...
...

The product rule I'm comfortable with: I've proved to myself that the cartesian product of two independent prefix codes is also prefix.

The coproduct rule also seems to be obviously correct if we're thinking in terms of sums-of-products, and if the product rule holds.

Where I'm struggling, I think is in reasoning about recursion, for instance for inductively-defined lists:

List a = Cons a (List a) | Empty

I believe my algorithm works in the presence of recursion, but how can I go about proving this using induction? I think my trouble is that "prefix" is a property of the (infinite) set of c

A code is prefix-free if there does not exist any distinct two values v, w such that encode(v) is a prefix of encode(w). So, to prove that your encoding is prefix-free, you start by considering two arbitrary distinct values v, w and demonstrate that encode(v) is not a prefix of encode(w).

I suggest you use proof by induction on the "size" of the largest value, so you'll consider two arbitrary values v, w that are both of size at most $n$. In this case, a reasonable choice for the "size" is the number of times the recursion was applied, i.e., the number of cells in the list. Your inductive predicate $P(n)$ states that for every pair of distinct values v, w both of whose size is at most $n$, encode(v) is not a prefix of encode(w). You want to prove $P(n)$ for all $n$. To do that using the principle of induction, you need to prove $P(0)$ and prove $P(n) \implies P(n+1)$. Here $P(0)$ is trivial, so we can focus on the inductive step $P(n) \implies P(n+1)$.

For your example of the list data structure, that shouldn't be too hard. You'll just case-split on the size and structure of v, w. There are four cases:

• case (a): v has size $\le n$, w has size $\le n$

• case (b): v has size $\le n$, w has size $n+1$

• case (c): v has size $n+1$, w has size $\le n$

• case (d): v has size $n+1$, w has size $n+1$

Case (a) is already covered by $P(n)$, so you only need to reason about the three other cases. Each one can be handled by using the induction predicate.

I'll describe how to prove case (d). You should be able to see how to handle the other cases similarly. Let a = hd(v) and k = tl(v), so that v == a::k. Similarly let b = hd(w) and l = tl(w) so that w == b::l. We can see that

encode(v) == encode(1) <> encode(a) <> encode(k)
encode(w) == encode(1) <> encode(b) <> encode(l)

Now we assumed that v, w are distinct, i.e., v != w. It follows that either a != b or k != l. If a != b, the fact that encode is prefix-free on ground terms implies that encode(a) is not a prefix of encode(b), which in turn implies that encode(v) is not a prefix of encode(w). If a == b and k != l, the inductive hypothesis $P(n)$ implies that encode(k) is not a prefix of encode(l) (since both k and l have size one less than v, w, i.e., size $n$), which in turn implies that encode(v) is not a prefix of encode(w).

Ultimately, once you've handled all four cases, you'll have proven that encode(v) is not a prefix of encode(w) for an arbitrary pair of distinct values v, w of size $n+1$, from which $P(n+1)$ follows.

The same techniques can be applied to any algebraic data types that is formed as a recursive combination of products and co-products.

StackExchange Computer Science Q#74065, answer score: 4