5
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ When you say "in logic" I thnink you mean "in set theory", or more likely "in informal mathematics". That is, is it correct that you are asking how to formulate your datatype so that ordinary mathematicians who do not speak Haskell will understand it? $\endgroup$ – Andrej Bauer Jun 5 '13 at 11:32
  • $\begingroup$ Yes, that is correct. I have to describe the algorithm so that non-programers can understand it in a more or less formal way using ordinary notation for functions and relations. I don't have to use sets to represent data structures but I don't don't come up with any better way of doing it. $\endgroup$ – Lii Jun 5 '13 at 11:59
  • 1
    $\begingroup$ @lii could you explain the degree for which you are writing the thesis, your background, and the expected audience for your thesis. It seem to me you want to explain or formalise your work in mathematical terms. That is not the same as explaining your work to working, professional mathematicians. What is your goal? $\endgroup$ – Vijay D Jun 5 '13 at 22:07
  • 1
    $\begingroup$ @Lii, Dave Clarke's answer here cstheory.stackexchange.com/a/16128/4155 might help you with the mathematics of inductive definitions. $\endgroup$ – Vijay D Jun 6 '13 at 0:42
  • 1
    $\begingroup$ Do you care about infinite structures (such as 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$ – yatima2975 Jun 6 '13 at 9:52
4
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Thanks for you suggestions, this kind of discussion is exactly what I am looking for. $\endgroup$ – Lii Jun 6 '13 at 12:19
  • $\begingroup$ "Firstly...": Interesting alternative! (I find the discussion on disjoint unions on page 29 of Lööf's paper) I'll spend some more time thinking about this. $\endgroup$ – Lii Jun 6 '13 at 12:20
  • $\begingroup$ "The second way..." Interesting alternative! This looks equivalent to you first suggestion, except that you another kind of notation. Is this correct? I like the idea of using named functions more. I think this is the way I should do it. $\endgroup$ – Lii Jun 6 '13 at 12:22
  • 1
    $\begingroup$ Yes, both ways are essentially equivalent. I like the second way more just because it is cleaner and you don't have to describe what name functions $i(.)$ and $j(.)$ do. $\endgroup$ – Shahab Jun 7 '13 at 5:24
  • $\begingroup$ Having given this some thought I have some considerations: Alt 1: It is a bit confusing to use functions without actually caring what kind of objects they signify. I'll have to explain this to the reader, and say things like $b(d) \neq c(d)$. Alt 2: I would have to explain what this notation really means. Is $\langle . \rangle$ some kind of function? Then it's just different notion for Alt 1. Or is it notation for some special kind of object? This would have to be explained. $\endgroup$ – Lii Jun 11 '13 at 9:04
6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I was expecting the phrase "Initial Algebra". $\endgroup$ – Dave Clarke Jun 6 '13 at 11:03
  • 3
    $\begingroup$ Mathematicians get jobs as computer scientists. True story. $\endgroup$ – Dave Clarke Jun 6 '13 at 11:49
  • 2
    $\begingroup$ Data types in universal algebra are represented using "initial algebras". $\endgroup$ – Dave Clarke Jun 6 '13 at 12:41
  • 2
    $\begingroup$ @Lii: yes, our formulations are essentially the same. You can use tags, just make sure you explain them and say that they could be "anything, for example numbers or symbols", but you chose descriptive ones. "Recursive set" in logic means "a set whose membership can be tested by a computable function", which is not what you want. The correct term is indeed "inductive set". $\endgroup$ – Andrej Bauer Jun 6 '13 at 12:44
  • 4
    $\begingroup$ I would use $\mathtt{A}, \mathtt{B}, \mathtt{C}$, or actually words, like $\mathtt{Fruit}$, $\mathtt{Veggie}$. This is another obsession of mathematicians' -- they'd rather use exocit alphabets than a name consisting of more than one letter. $\endgroup$ – Andrej Bauer Jun 6 '13 at 14:38

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.