Formal representation of algorithm using recursive algebraic data types

Question

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this:

data Data = A Int | B Data | C Data

Now I am thinking about how to explain this in a formal way, in a way that feels natural and clear. Note that B and C contain the same data.

The only reasonable alternative I have come up with is to use some kind of tagged union, like this:

Let $Data$ be a recursively defined set given by:

• Let $i$ be an integer. Then $\langle \mathcal{A}, i \rangle \in Data$.
• Let $d \in Data$. Then $\langle \mathcal{B}, d \rangle \in Data$.
• Let $d \in Data$. Then $\langle \mathcal{C}, d \rangle \in Data$.

With this definition I write functions over $Data$ like this:

$$ func(\langle \mathcal{A}, i \rangle) = \cdots \\ func(\langle \mathcal{B}, d \rangle) = \cdots \\ func(\langle \mathcal{C}, d \rangle) = \cdots \\ $$

And predicated about is like this: $$ Pred(\langle \mathcal{A}, i \rangle) \text{ holds if ... } \\ Pred(\langle \mathcal{B}, d \rangle) \text{ holds if ... } \\ Pred(\langle \mathcal{C}, d \rangle) \text{ holds if ... } \\ $$

This representation is very close to the Haskell source code, which is good, but it feels rather unnatural to mathematicians.

Is there a more elegant and natural way to do this?

EDIT: Thanks for the replays, sorry if I am being unclear.

I am writing a master's thesis in CS about alias analysis. The text should be comprehensible for students on master level in CS with a background in algorithms (does master level mean the same in the USA? In EU you get this degree after 5 years of study including an 1 term thesis project).

I have used this paper as a starting point, implemented that algorithm in Haskell and made some extensions. Now I want to describe my extension in a way that is similar to the paper in formulation and level of formalism. However I use a recursive algebraic data type in my extension and I'm not sure about the most natural and clear way to represent it.

EDIT: The example $Data$ above is intended to have finite values only.

EDIT: I see that my question is very similar to this: Formal Representation of Haskell Data-Types

Except that I'm also interested in how to represent recursive data types.

EDIT: Summary of the alternative suggestions I have received

1. Tagged tuples (my example above and Andrej Bauer's alternative)

2. Function applications (Shahab's first alternative) $$ data(a(d)) = \dots $$

3. Objects with special notation / operators (Shahab's second alternative) $$ \langle d \rangle = \dots $$

4. Un-data-type-ization (yatima2975's alternative)

   Transform into non-recursive form. Works only for data types with one recursive element. "the Cartesian product of finite strings over {B,C} and the integers"

I think all of the have advantages and disadvantages.

Answer 1

First of all, I think that there is nothing wrong with your current definition and I think it can be understood by any mathematician. However, if you still want it to look nicer, I can give you a few hints:

Firstly, you might have a look at a few papers that introduce intuitionistic type theory. There, the set of possible proofs for a disjunctive type $A \vee B$ is the disjoint union of all possible proofs for $A$ and all possible proofs for $B$. For example, if you look at this paper by Martin-Lof, on page 7 (page 13 of the pdf file), you see that it uses $i(a)$ and $j(a)$ to mark whether $a$ is a proof of $A$ or a proof of $B$. You can do the same and use notation $a(d)$ and $b(d)$ to denote $\mathcal{A}~Data$ or $\mathcal{B}~Data$.

The second way and, to me, the more elegant way is to use different notations. For example, your definition of $Data$ would look something like this:

$Data$ is the minimal set that contains $\mathbb{N}$ and is closed under the $[.]$ and $\langle .\rangle$ containers, i.e., if $d \in Data$ then so are $[d]$ and $\langle d \rangle$. This way, a function $f : Data \mapsto A$ can be defined by defining it over $\mathbb{N}$ as well as $f([d])$ and $f(\langle d \rangle)$ (for $d \in Data$).

As you can see, this is not very different from your own way as I mentioned in the beginning. The only difference, to me, is the aesthetics. My version just seems cleaner and less like programming (I would also change the name $Data$ in the thesis explanation to a one-letter name to make it even cleaner).

Answer 2

You should get acquainted with inductive definitions.

Instead of saying that $Data$ is recursively defined, say that it is a set constructed inductively by:

• $(0,i) \in Data$ for every $i \in \mathbb{Z}$,
• $(1,d) \in Data$ for every $d \in Data$,
• $(2,d) \in Data$ for every $d \in Data$.

Another way to say the same thing is that $Data$ is the smallest set such that $$Data = \lbrace (0,i) \mid i \in \mathbb{Z} \rbrace \cup \lbrace (1,d) \mid d \in Data \rbrace \cup \lbrace (2,d) \mid d \in Data \rbrace.$$ Then remark that you use abbreviations $\mathcal{A} = 0$, $\mathcal{B} = 1$, $\mathcal{C} = 2$. Mathematicians are not used to introduction of basic symbols or tags, unless they are considering polynomials in a "variable" $X$ (which they really should call "symbol").

But it may be better not to cater to old-fashioned traditions of mathematicians. We should push them into the 21st century and teach them some math which they think of as "computer science". What is wrong with assuming your reader knows what an inductive data type is?

One word of warning: Haskell does not have inductive datatypes, but rather coindcutive data types. If you define the type in Haskell you will also get infinite elements of the form B (B (C (B ....))). There is just no way to get this right in Haskell. ML has proper datatypes.