Formal representation of algorithm using recursive algebraic data types 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


Tagged tuples (my example above and  Andrej Bauer's alternative)
Function applications (Shahab's first alternative)
$$
  data(a(d)) = \dots
$$
Objects with special notation / operators (Shahab's second alternative)
$$
  \langle d \rangle = \dots
$$
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.
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.