4
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ To answer your questions: The order is not important (--> multiset) and the "lists" are finite $\endgroup$ – Johannes Weiss Aug 16 '12 at 22:38
  • $\begingroup$ My "mathematical" notation was indeed complete nonsense. Besides formatting issues (non-visible curly brackets because I sometimes typed { ... } instead of \{ ... \}), I completely messed it up anyway :-(. Your suggestion using P and Q being subsets of all possible ARFs and $ARF \times ARF$s seems very good. Thanks! $\endgroup$ – Johannes Weiss Aug 16 '12 at 23:49
  • $\begingroup$ Sorry, unfortunately, I identified one problem: How could one notate that $P$ and $Q$ are multisets? $Q \subseteq ARF$ looks like $Q$ being an ordinary set. $\endgroup$ – Johannes Weiss Aug 17 '12 at 15:29
  • $\begingroup$ If you look at, for example, multisets on Wikipedia, for better or worse they use the same notation as regular sets. If you're only talking about multisets, I think it's fair to just say "by 'set' I mean 'multiset'" and go from there. $\endgroup$ – Rob Simmons Aug 18 '12 at 15:51
  • 1
    $\begingroup$ @Johannes Weiß: Why don’t you just write “P and Q are multisets” explicitly? I do not think that there is a widely accepted notation for multisets. $\endgroup$ – Tsuyoshi Ito Aug 18 '12 at 22:25

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.