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.
let x = B y; y = C x in x
) and undefined values? If not, you can just use a description like 'the Cartesian product of finite strings over{B,C}
and the integers modulo (at least) 2^30'. $\endgroup$