Formal Representation of Haskell Data-Types

Question

I come from Haskell programming and currently writing my (Diploma/Master) thesis. I'm having trouble finding a formal/mathematical notation for a Haskell data-type.

The Haskell data type is:

data ARE = ARE [(ARF, ARF)] [ARF]   -- Haskell form
type ARE = ( [(ARF, ARF)], [ARF] )  -- alternate form

An ARE is an affine randomized encoding and an ARF is an affine randomized function. You can think of an ARF just as an abstract entity, just like a field or group element. My problem is how to formally notate a definition for an ARE.

First, I'll try to describe what an ARE is in english: An ARE is a tuple (in the "alternate form", in my Haskell program it's represented as in the "Haskell form") containing:

• a list (not a set since it could contain duplicates) containing tuples. Each of these tuples is just two ARFs
• a list of ARFs

What I'm looking for is a formal notation of such an ARE.

(edit: removed nonsense notation proposal...)

About the expected audience (and their knowledge domain) of my thesis: I will provide Haskell code, but the entire thesis should be understandable by someone who is not a programmer (and in particular no Haskell programmer). The reader will need some knowledge in cryptography, computer science (but not programming) and basic mathematics (some field theory, especially the finite fields $\mathbb{F}_{2^n}$). In the text I simply want to tell the reader what AREs are and how I transform general expressions to AREs.

Answer 1

Unter the assumption, that lists simply represents arbitrary sets, the mathematical notation should probably read:

An ARE is an element of the following set:

$\{ (P, Q) \mid P \subseteq ARF \times ARF, Q \subseteq ARF \} $

But as you stated, lists in your domain are always finite, ordering is not important, but multiplicity is. Thus, I would model the lists as finite multisets. Using an explicit notation for mulitsets, a possible definition would be:

An ARE is an element of the following set:

$\{ (P_\chi, Q_\xi) \mid P \subseteq ARF \times ARF, P~\text{finite},~ \chi \in (P \to \mathbb{N}^+), Q \subseteq ARF, Q~\text{finite},~ \xi \in (Q \to \mathbb{N}^+) \} $

Here, the notation $P_\chi$ denotes a multiset with P being the underlying ordinary set and $\chi \in P \to \mathbb{N}^+$ being the multiplicity function of the multiset.