multi-trie-0.1: tex/multi-trie.tex

%-------------------------------------------------------------------
%
% Author    : Vadim Vinnik
% E-mail    : vadim.vinnik@gmail.com
% Status    : Draft
% License   : Creative commons
%
%-------------------------------------------------------------------

\documentclass{article}

\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{dirtree}
\usepackage{listings}
\usepackage{stackrel}

\lstloadlanguages{Haskell}
\lstset{%
  basicstyle={\small\ttfamily},%
  language=Haskell%
}

\DTsetlength{0.2em}{2em}{0.2em}{0.4pt}{1pt}

\theoremstyle{definition}
\newtheorem{Df}{Definition}
\newtheorem{St}{Statement}
\newtheorem{Ex}{Example}

\newcommand{\setcharmvcn}{M}
\newcommand{\setcharmt}{T}

\newcommand{\setsymbol}[3]{\mathcal{#1}_{#2,#3}}

\newcommand{\setmvcn}[2]{\setsymbol{\setcharmvcn}{#1}{#2}}
\newcommand{\setmt}[2]{\setsymbol{\setcharmt}{#1}{#2}}

\newcommand{\seta}{\mathcal{A}}
\newcommand{\setn}{\mathcal{N}}

\newcommand{\flatten}{\operatorname{Fl}}
\newcommand{\select}{\operatorname{Sel}}
\newcommand{\deref}{\operatorname{Get}}
\newcommand{\putval}{\operatorname{Put}}
\newcommand{\proj}[2]{\operatorname{pr}^{#1}_{#2}}
\newcommand{\fmap}{\operatorname{Map}}
\newcommand{\fpam}{\operatorname{Pam}}
\newcommand{\id}{\operatorname{id}}
\newcommand{\apply}{\operatorname{Apply}}
\newcommand{\ylppa}{\operatorname{Ylppa}}
\newcommand{\eval}{\operatorname{Eval}}

\newcommand{\inapply}{\mathbin{\nabla}}



\title{Compound names with multiple values: formalisation, properties and implementation}
\author{Vadim Vinnik}
\date{2016}



\begin{document}

\maketitle

\begin{abstract}
Naming is one of the most fundamental concepts in programming.  In most cases,
a name is considered to be atomic and to have a unique value.  This paper
describes a kind of naming with both these principles negated: names form a
monoid under concatenation, and each name can be associated with multiple
values.  Two different but equivalent formalisations are defined, their
isomorphism is shown.  Counterparts of set-theoretical union, intersection and
cartesian product operations are defined, their properties are described.  A
data type implementing this kind of naming is designed in Haskell, it fits into
functor, applicative functor and monad classes.

Keywords:
applicative functor,
atomicity,
cartesian product,
compoundness,
concatenation,
denotation,
dereferencing,
functor,
Haskell,
implementation,
intersection,
monad,
monoid,
multivaluedness,
name,
relation,
set,
trie,
union.
\end{abstract}



\tableofcontents



\section{Introduction}

A trilateral relation between a \emph{name}, its \emph{meaning} and
\emph{value} has been in the focus of philosophical and mathematical logic,
metamathematics, semiotics and epistemology for a long time.  For example,
important questions about naming were raised and deeply investigated in
fundamental works by G.\,Frege~\cite{bib:frege},
L.\,Wittgenstein~\cite{bib:wittgenstein}, W.\,Quine~\cite{bib:quine}.  With
arising of computer science, naming gained a special significance~-- for
example, \emph{a name that refers to a name that, finally, relates to an
entity} is not a purely philosophical excercise anymore but a working tool for
everyday~-- an \emph{indirect pointer}; a \emph{a name with a meaning but
without a value} turned into a \emph{null reference} with both its power and
danger; \emph{names changing their values depeding on the context} became
\emph{variables} in the sense of imperative programming. Since \emph{addresses}
of some entities in memory are obviously a special case of names, and since
addresses are, in their turn, computable values, relations and interactions
between names and values in programming are even more complicated than in
pre-computer semiotics.

Therefore, every comprehensive theory of programming must give a special
explication of naming and include a mathematical model that reflects its
properties and behaviour.  Approaches and formal techniques however could be
very different.

For example, \emph{A Practical Theory of Programming}~\cite{bib:ptop} as well
as \emph{Unifying Theories of Programming}~\cite{bib:utp} represent a variable
declaration by means of a quantifier in some first order logic.  In the
first-order logic, a variable refers to an unspecified object of a semantic
domain; the formula tells about the objects using names to represent them.
Objects belong to the semantic level, and names to the syntactical level that
do not intersect.  Therefore, the first order formalism works fine for programs
that have a predefined list of variables but hardly can describe programs that
dynamically allocate memory for objects whose number is not known \emph{a
priori}.

On the contrast to above, there are theories that explicitly describe memory
layout and allocation operations, for example in terms of memory block
references~\cite{bib:leroy}, and other formal memory models.
Such theories reflect semantics of programs on a
relatively low, implementation-aware level, and their primary application is
formal specification and verification of compilers and OS kernels.

There is yet another option between these two extremes.  Names can be regarded
as computable values without cumbersome specifics of \emph{being addresses}.  A
typical example arises from array processing: \lstinline{a[i]} is a computable
name because this expression, depending on the current value of~\lstinline{i},
can refer to any of the array's elements and, therefore, evaluates to one of
the elements' names~--- and it is exactly how array indexing operation is
treated in C~language: adding offset \lstinline{i * size} to the base
address~\lstinline{a} gives a pointer to the element.

An elegant and general formalism for naming that does not burden names
with any alien specifics, but allows any specifics to be added if needed,
is a notion of \emph{naming set} introduced by V.\,N.\,Redko in a
comprehensive conception of \emph{compositional programming}~\cite{bib:redko}.

\begin{Df}\label{df:naming-set}
Suppose there is a given set~$D$ whose elements are called \emph{values}, or
\emph{denotata}, and a set~$V$ of objects called \emph{names}.
A \emph{$(V,D)$-naming set} (the prefix will be omitted when possible) is a
partial mapping $s: V\to D$.
\end{Df}

In other words, a naming set is an object of the form
\[
  s = \{ (v_1, d_1), (v_2, d_2), \ldots, \} ,
\]
where $v_i\in V$, $d_i\in D$, and all~$v_i$ are pairwise distinct. The
latter requirement formalizes \emph{unambiguity}, or \emph{univaluedness}: a
name cannot have different values in a given context.

\begin{Ex}\label{ex:naming-set}
A naming set $s = \{ (a, 1), (t, 7), (w, 1) \}$ represents a context where
the name~$a$ has a value~1, the name~$b$ refers to a value~7 and the name~$w$
denotes~1, no other names have values.
\end{Ex}

A set-theoretical intersection  of naming sets is obviously a naming set
whe\-re\-as a union is not because it can violate univaluedness:
\[
  \{ (a, 0) \} \cup \{ (a, 1) \} = \{ (a, 0), (a, 1) \} .
\]

Mappings similar to the one defined above are widely used in theoretical
computer science for syntactical as well as semantical tasks, a good example
could be an approach to definition of programming
languages~\cite{bib:ollongren}.  \emph{Dictionaries}~\cite{bib:dictionary} and
\emph{associative arrays}~\cite{bib:mehlhorn-assoc} are abstract data types
implementing the same idea, included into standard libraries of various
programming languages and widely used in practice.

At the topmost abstraction level, a naming set represents a ``plain'' relation
where names and values are atomic in the sense that their internal structures
and any non-trivial properties are hidden as irrelevant.  In fact, the only
special property taken into account by the definition above is
\emph{equatability} of names: for any two names, it should be possible to
decide whether they are identical.

Although def.~\ref{df:naming-set} does not mention or use any special properties
of names and values, it does not require their absense.
Introducing various properties of names and/or denotata, one can obtain a
number of interesting and useful specialised formalisations of naming for
theoretical purposes as well as implementable data structures suitable for
practical tasks. This article describes a kind of naming with
two important differences from the definition~\ref{df:naming-set}.
\begin{itemize}
\item \emph{Multivaluedness}: any name can be related to zero or more values;
\item \emph{Compoundness of names}: compound names could be concatenated from
shorter ones, i.e. names form a monoid under concatenation.
\end{itemize}
The first difference may seem violating the general definition of the
naming set but multivaluedness could be easily modelled as a special case of
univaluedness: the value is unique and is a set (of `proper' values).


\subsection*{Conventions about notation}

For any set~$X$, let~$X^\ast$ denote a set of all sequences of its elements
(also known as \emph{chains}), and~$2^X$ be a set of all subsets of~$X$.
If~$a,b\in X^\ast$ are two chains, their concatenation will be denoted simply
as~$ab$. Let~$\varepsilon$ stand for the empty chain.
Let $\proj{n}{k}$ be a function that maps an $n$-tuple to its $k$-th component.

A set of Latin letters (the alphabet) is denoted as~$\seta$,
and~$\setn$ denotes a set of natural numbers~-- these two sets will be
used in examples.

Throughout this paper, a class of atomic names is denoted with~$V$. The
variable~$u$ (maybe, with indices or other decorations) always takes values
in~$V$, whereas $v$ and $w$ take values from~$V^\ast$.

Some more notations will be introduced later, immediately before they are used.



\section{Relation-based definition and basic properties}

Let~$V$ be a given set of objects called \emph{atomic names}. Elements
of~$V^\ast$ are called \emph{compound names}. Let us omit the words ``atomic''
and ``compound'' if it does not lead to confusion.

\begin{Df}\label{df:mvcn}
A \emph{$(V,D)$-multinaming set} is a binary relation
\[
  s \subseteq V^\ast \times D .
\]
Whenever $V$ and $D$ are obvious from the context, we'll omit ``$(V,D)$-''
prefix and write simply ``multinaming set''. A set of $(V,D)$-multinaming sets will be
denoted~$\setmvcn{V}{D}$.
\end{Df}

Note that there is an obvious mapping from the class of $(V,D)$-multinaming
sets to the class of $(V^\ast, 2^D)$-naming sets as well as an opposite
mapping. Therefore, a multivalued naming could be modelled as a special case of
a univalued naming with extra specifics applied to values (being sets) and
names (being chains). Such modelling is not investigated below~-- instead, two
formalisations are described that reflect the essence of the notion in a more
direct way.

\begin{Ex}\label{ex:mvcn}
The following object is an $(\seta, \setn)$-multinaming set:
\[
  s = \{
    (\varepsilon, 0),
    (\varepsilon, 1),
    (a,           2),
    (a,           3),
    (a,           4),
    (aa,          5),
    (ab,          6),
    (b,           7),
    (baaa,        8)
  \} .
\]
Here the empty name has two values (0 and~1), name~$a$ has three (2, 3 and~4),
comound names~$aa$ and~$ab$ have each a single value (5 and~6, respectively),
name~$b$ has a value~7 and, finally, a name~$baaa$ has one value~8. All other
names from~$\seta^\ast$ have no values.
\end{Ex}

Note that, in contrast with naming sets, no special conditions are imposed
on a multinaming set~--- it is just an arbitrary set of name-value pairs.
Therefore, $\setmvcn{V}{D}$ is closed against set-theore\-tical union
and intersection.
\begin{St}\label{st:mvcn-setop}
If~$s$ and~$t$ are $(V,D)$-multinaming sets, so are~$s\cup t$ and~$s\cap t$.
\end{St}

When it is important to emphasise that union and intersection are operations
on multinaming sets rather than on general case of sets, we will
write~$\cup_\setcharmvcn$ and~$\cap_\setcharmvcn$.

One of the fundamental operations on (univalued) naming sets is retrieving the
only (if any) value~$d$ associated with the name~$v$ in a naming set~$s$.
Depending on the goals and abstraction level of a particular context, it could
be regarded either as~$s(v)=d$, i.e. applying a function~$s$ to an
argument~$v$, or as an operation whose arguments are the naming set and the
name, i.e.~$\deref(s, v)=d$. Its counterpart in multinaming set world that
retrieves all values of a name, no matter how many, obviously cannot be denoted
using the first style.

\begin{Df}\label{df:mvcn-dereferencing}
\emph{Dereferencing} is an operation~$\deref_\setcharmvcn$ (or, whenever
possible, omiting the subscript, simply~$\deref$) of type
$\setmvcn{V}{D} \times V^\ast \to 2^D$,
such that
\[
  \deref_\setcharmvcn(s, v) = \{ d \mid (v, d) \in s \} .
\]
\end{Df}

Unlike the univalued case, here~$\deref$ is a total operation: even if a
name~$v$ does not have any associated value in a multinaming set~$s$, dereferencing
it just yields an empty set of values.

\begin{Ex}\label{ex:mvcn-dereferencing}
Consider a multinaming set~$s$ from ex.~\ref{ex:mvcn}. Then
\begin{eqnarray*}
  \deref(s, \varepsilon) & = & \{ 0, 1 \}, \\
  \deref(s, baaa)        & = & \{ 8 \}, \\
  \deref(s, cdcd)        & = & \varnothing .
\end{eqnarray*}

\end{Ex}

It follows immediately from the definition that dereferencing distributes
over set-theore\-tical operations.
\begin{St}\label{st:mvcn-deref-distributivity}
Let~$\odot$ stand for either~$\cup$ or~$\cap$, and let~$s$ and~$t$ be
$(V,D)$-multinaming sets. Then, for every~$v\in V^\ast$,
\[
  \deref(s\odot t, v) = \deref(s, v) \odot \deref(t, v) .
\]
\end{St}

The following important property means, in fact, that every multinaming set is completely
defined by the values of all its names.  In terms of programming, it means that
if two multinaming set objects' behaviours (observed through the $\deref$ selector) are
indiscernible, the objects are identical.
\begin{St}\label{st:mvcn-deref-equality}
Let $s, t \in \setmvcn{V}{D}$. Then
\[
  (\forall v\in V^\ast . \deref(s,v) = \deref(t,v)) \implies (s = t) .
\]
\end{St}

The following operation is, in a reasonable sense, an opposite to
dereferencing.  It replaces all values of some name with a new set of values.
Thus, it is similar to assignment in the sense of imperative programming.
\begin{Df}\label{df:mvcn-replace}
\emph{Replacement} is an operation
\begin{eqnarray*}
 & \putval_\setcharmvcn :
    \setmvcn{V}{D} \times V^\ast \times 2^D \to \setmvcn{V}{D}, \\
 & \putval_\setcharmvcn(s, v, x) =
      \{ (w, d) \mid (w, d) \in s, w \neq v \} \cup
      \{ (v, d) \mid d \in x \} .
\end{eqnarray*}
The subscript will be omitted further whenever possible.
\end{Df}
In other words, this operation deletes from~$s$ all values corresponding to
the name~$v$, leaves all other name-value pairs intact and assigns new values
to~$v$.

\begin{Ex}\label{ex:mvcn-replace}
Let~$s$ be a multinaming set from ex.~\ref{ex:mvcn}. Then
\[
  \putval(s, a, \{ 9, 10 \}) = \{
    (\varepsilon, 0),
    (\varepsilon, 1),
    (a,           9),
    (a,           10),
    (aa,          5),
    (ab,          6),
    (b,           7),
    (baaa,        8)
  \} .
\]
\end{Ex}

The main property of replacement is obvious and immediately follows from the
definition: it changes the values of one name and does not influence the other
names. Except this, two replacement operations commute if they
relate to different names, otherwise the outer operation absorbs the inner one.
\begin{St}\label{st:mvcn-replace-deref}
Let~$s \in \setmvcn{V}{D}$, $v, w \in V^\ast$, $x, y \in 2^D$. Then
\begin{eqnarray*}
  & \deref(\putval(s, v, x), v) = x , \\
  & v \neq w \implies \deref(\putval(s, v, x), w) = \deref(s, w) , \\
  & \putval(\putval(s, v, x), v, y) = \putval(s, v, y) , \\
  & v \neq w \implies \putval(\putval(s, v, x), w, y) = \putval(\putval(s, w, y), v, x) .
\end{eqnarray*}
\end{St}

Let us introduce special terms and symbols for the two extreme cases of
multinaming sets, namely:
\begin{Df}\label{df:mvcn-extreme}
Multinaming set $\bot_\setcharmvcn$ called \emph{empty} and $\top_\setcharmvcn$ called
\emph{full} are defined by
\begin{eqnarray*}
  \bot_\setcharmvcn &  = &  \varnothing ; \\
  \top_\setcharmvcn &  = &  V^\ast \times D .
\end{eqnarray*}
Further, we'll omit the subscript when it does not lead to confusion.
\end{Df}

In other words, each name in the empty multinaming set has no value whereas in the
full multinaming set every name has all possible values.
\begin{St}\label{st:mvcn-extreme-deref}
For any~$v\in V^\ast$,
\begin{eqnarray*}
  \deref(\bot, v) & = & \varnothing, \\
  \putval(\bot, v, \varnothing) & = & \bot , \\
  \deref(\top, v) & = & D , \\
  \putval(\top, v, D) & = & \top .
\end{eqnarray*}
\end{St}

The next property is also just a trivial consequence of the definition:~$\bot$
and~$\top$ objects are units of~$\cup$ and~$\cap$ operations respectively and
zeros vice versa.
\begin{St}\label{st:mvcn-neutrals}
For any multinaming set~$s$,
\begin{eqnarray*}
  \bot \cup s & = & s,    \\
  \top \cap s & = & s,    \\
  \bot \cap s & = & \bot, \\
  \top \cup s & = & \top.
\end{eqnarray*}
\end{St}

Note that a compound name~$v$ in a multinaming set~$s$ not only refers to its
values but also is a common prefix for a ``bunch'' of names starting with~$v$.
A name~$vw$ in a multinaming set~$s$ can be regarded as a name~$w$
\emph{relative} to a point referred to by~$v$ or, in other words, as a name~$w$
in a multinaming set subobject selected from~$s$. To select a subobject means:
throw away names that do not start with~$v$, and remove this comon prefix from
those that do. Formally, it leads to the definition.

\begin{Df}\label{df:mvcn-select}
Let~$s\in\setmvcn{V}{D}$, $v\in V^\ast$, then \emph{selection} from~$s$
under~$v$ is
\[
  \select_\setcharmvcn(s,v) = \{ (w, d) \mid (vw, d)\in s \} \in\setmvcn{V}{D}.
\]
As always, the subscript will be omited if possible.
\end{Df}

\begin{Ex}\label{ex:mvcn-select}
Let~$s$ be a multinaming set from ex.~\ref{ex:mvcn}, then
\begin{eqnarray*}
  \select(s, a) & = & \{
    (\varepsilon, 2),
    (\varepsilon, 3),
    (\varepsilon, 4),
    (a,           5),
    (b,           6)
  \} , \\
  \select(s, b) & = & \{
    (\varepsilon, 7),
    (aaa,         8)
  \} , \\
  \select(s, cdcd) & = & \bot .
\end{eqnarray*}
\end{Ex}

\begin{St}\label{st:mvcn-selection-properties}
For any~$s,t\in\setmvcn{V}{D}$, $v, w\in V^\ast$, $\odot\in\{\cup, \cap\}$,
\begin{eqnarray*}
  & \select(\bot,v) = \bot, \\
  & \select(\top,v) = \top, \\
  & \select(s,\varepsilon) = s, \\
  & \select(s,vw) = \select(\select(s,v), w), \\
  & \select(s\odot t, v) = \select(s,v)\odot \select(t,v).
\end{eqnarray*}
\end{St}
In other words,
\begin{itemize}
\item selection preserves empty and full multinaming set;
\item selection under an empty name is an identity over multinaming sets;
\item selection under a compound name can be performed by parts;
\item selection distributes over union and intersection.
\end{itemize}

It is interesting to note that there is another formalisation of the
multivalued naming that is, however, equivalent to the above definitions.  It
is described in the next section.



\section{Trie-based definition}

Take a closer look at the multinaming set~$s$ from ex.~\ref{ex:mvcn}.  Recall
the idea underlying selection operation: any name~$v$ is a common prefix for a
bunch of names of the form~$vw$~-- and, therefore, is a root of a sub-naming
relative to~$v$. Except this, take into account that the empty
name~$\varepsilon$ is a common prefix for all names.

The name~$\varepsilon$, the simplest name ever, refers in~$s$ to a set of
values~$\{0,1\}$. Name~$a=\varepsilon a$ is an extension of~$\varepsilon$ by
one atomic name and refers to values~$\{2,3,4\}$. In its turn, name~$a$ can be
extended by one atomic name to~$aa$, $ab$, \ldots, $az$, from which only the
former two have values.  Now return to the empty name and compose another its
continuation, namely~$b$.  This name has no values but it is a prefix for~$ba$
that, in its turn, can be extended to~$baa$ and then to~$baaa$ that has
non-empty set of values.

This gives a hierarchical view of~$V^\ast$ where
\begin{itemize}
\item the root of the hierarchy is the empty name;
\item appending an atomic component to a name moves one level deeper;
\item a common prefix is a common ancestor.
\end{itemize}
The corresponding tree-like representation of the multinaming set~$s$ is shown on
fig.~\ref{fig:trie}.

\begin{figure}[ht]
\begin{center}
\begin{minipage}{17em}
\dirtree{%
  .1 $\varepsilon$\DTcomment{$\{0, 1\}$} .
    .2 $a$\DTcomment{$\{2, 3, 4\}$} .
      .3 $a$\DTcomment{$\{5\}$} .
      .3 $b$\DTcomment{$\{6\}$} .
    .2 $b$\DTcomment{$\{7\}$} .
      .3 $a$\DTcomment{$\varnothing$} .
        .4 $a$\DTcomment{$\varnothing$} .
          .5 $a$\DTcomment{$\{8\}$} .
}
\end{minipage}
\end{center}
\caption{A multitrie corresponding to the multinaming set~$s$}\label{fig:trie}
\end{figure}

To grasp this informal consideration in a definition, it would be convenient to
assume that every node in the hierarchy has \emph{all} possible children~-- i.e.
that the hierarchy includes all names from~$V^\ast$ regardless of whether they
have values: otherwise we needed a special treatment for missing names in
every subsequent definition or statement. This leads to the following

\begin{Df}\label{df:mt}
A class of \emph{$(V,D)$-multitries} (or simply \emph{multitries} when~$V$
and~$D$ are known from the context or irrelevant):
\[
  \setmt{V}{D} = 2^D \times (V \to \setmt{V}{D}) .
\]
\end{Df}

In other words, a $(V,D)$-multitrie is a pair $s = (x, m)$ where~$x\subseteq D$
is a set of values and $m: V \to \setmt{V}{D}$ is a total mapping of
atomic names to some $(V,D)$-multitries called \emph{children}.
Note that this recursive definition does
not have any basic case: every multitrie contains child multitries
under all atomic names, hence there are no leaf nodes.
Depicting multitries graphically, as on fig.~\ref{fig:trie}, we will however
only draw nodes of interest assuning that all other nodes have empty sets of
values.  Note that a $(V,D)$-multitrie is a \emph{trie} also known as
a prefx tree~\cite{bib:knuth-trie}~-- that justifies the term.

Extreme multitries have the following recurrent definitions.
\begin{Df}\label{df:mt-extreme}
\emph{Empty} and \emph{full} $(V,D)$-multitries:
\begin{eqnarray*}
  \bot_\setcharmt & = &
      ( \varnothing, \{ u \mapsto \bot_\setcharmt \mid u\in V \} ) , \\
  \top_\setcharmt & = &
      ( D,           \{ u \mapsto \top_\setcharmt \mid u\in V \} ) .
\end{eqnarray*}
Subscripts will be further omited whenever possible.
\end{Df}
In other words, empty (full) multitrie is a multitrie that has an empty
(full) set of values and whose children under all atomic names are, in their
turn, empty (full) multitries.

\begin{Df}\label{df:mt-select}
\emph{Selection} operation. Let $s=(x,m) \in \setmt{V}{D}$, $u\in V$,
$v\in V^\ast$, then
\begin{eqnarray*}
  \select_\setcharmt(s, \varepsilon) & = & s , \\
  \select_\setcharmt(s, u v) & = & \select_\setcharmt(m(u), v) .
\end{eqnarray*}
Subscripts will be omited if possible.
\end{Df}

In other words, selection operation finds a node pointed to by the
compound name as a path in the trie, and takes a sub-trie starting
at this node.

\begin{Ex}\label{ex:mt-select}
Consider a multitrie~$s$ depicted on fig.~\ref{fig:trie}. Selection under a
name~$a$ results in a multitrie~$\select(s,a)$ shown on
fig.~\ref{fig:mt-select}.
\end{Ex}

\begin{figure}[ht]
\begin{center}
\begin{minipage}{17em}
\dirtree{%
  .1 $\varepsilon$\DTcomment{$\{2, 3, 4\}$} .
    .2 $a$\DTcomment{$\{5\}$} .
    .2 $b$\DTcomment{$\{6\}$} .
}
\end{minipage}
\end{center}
\caption{Selection of a multitrie}\label{fig:mt-select}
\end{figure}

\begin{Df}\label{df:mt-deref}
Given a $(V,D)$-multitrie~$s$ and a name~$v\in V^\ast$, \emph{dereferencing}
of~$v$ in~$s$ is
\[
  \deref_\setcharmt(s, v) = \proj{2}{1}(\select(s, v)) .
\]
As always, we'll not write the subscript if it is obvious from the context.
\end{Df}

In other words, if $\select(s,v) = (x,m)$, then $\deref(s, v) = x$. To
dereference a name in a multitrie, one needs to follow the compound name
as a path to a node in the trie and then take the value stored in that node.

\begin{Df}\label{df:mt-setop}
\emph{Union} and \emph{intersection}.
Let
$\odot \in \{ \cup, \cap \}$,
$s, t \in \setmt{V}{D}$,
$s = (x, m)$, $t = (y, n)$.
Then
\[
  s \odot_\setcharmt  t =
    (x \odot y, \{ u \mapsto m(u) \odot_\setcharmt n(u) \mid u \in V \}) .
\]
\end{Df}
Note that subscripts in this definition help to distinguish between
set-the\-o\-re\-ti\-cal operations on sets of values and corresponding operations
on multitries.

In other words, to build $r = s \cup t$, one needs to go through all compound
names and, for each name, build a union of the value sets contained in the
operands under that name.

Let us also define an operation that corresponds to replacement
defined for multinaming sets (see def.~\ref{df:mvcn-replace}). Like other multitrie
operations, the most natural way of defining it is recursive.

\begin{Df}\label{df:mt-replace}
\emph{Replacement} is an operation
\[
  \putval_\setcharmt : \setmt{V}{D} \times V^\ast \times 2^D \to \setmt{V}{D},
\]
such that, for any
$s = (x, m) \in \setmt{V}{D}$, $y \in 2^D$, $u \in V$, $v \in V^\ast$,
\begin{eqnarray*}
  \putval_\setcharmt(s, \varepsilon, y) & = & (y, m) , \\
  \putval_\setcharmt(s, u v, y) & = & (x, m') ,
\end{eqnarray*}
where $m' : V \to \setmt{V}{D}$ is such a function that $m'(u') = m(u')$ for any
$u'\neq u$, and
\[
  m'(u) = \putval_\setcharmt(m(u), v, y) .
\]
The subscript after the operation will be omited whenever it does not lead to
confusion.
\end{Df}

In other words, to perform a replacement in a multitrie, one has to distunguish
between two cases. If the name to be replaced is empty, just replase the set of
values in the root node of the trie. Otherwise, take the first atomic component
of the name, go to the child node associated with that atom, and perform a
replacement under a remainder of the name.

It is easy to see that properties identical to those of multinaming sets
hold for multitries, namely counterparts of
st.~\ref{st:mvcn-deref-distributivity},
\ref{st:mvcn-deref-equality},
\ref{st:mvcn-replace-deref},
\ref{st:mvcn-extreme-deref},
\ref{st:mvcn-neutrals}
and~\ref{st:mvcn-selection-properties}.
Moreover, all properties of multinaming sets and multitries are identical because
of the following property.

\begin{St}\label{st:isomorph}
Consider a mapping~$\varphi: \setmvcn{V}{D} \to \setmt{V}{D}$, such that,
for any~$s\in \setmvcn{V}{D}$,
\[
  \varphi(s) = (
    \deref_\setcharmvcn(s, \varepsilon) ,
    \{ u \mapsto \varphi(\select_\setcharmvcn(s, u) \mid u\in V \})
  ) .
\]
Then~$\varphi$ is a bijection that preserves
extreme elements, union, intersection, dereferencing, replacement and selection
operations:
\begin{eqnarray*}
  & \varphi(\bot_{\setcharmvcn}) = \bot_{\setcharmt}, \\
  & \varphi(\top_{\setcharmvcn}) = \top_{\setcharmt}, \\
  & \varphi(s \mathbin{\odot_{\setcharmvcn}} t) =
      \varphi(s) \mathbin{\odot_{\setcharmt}} \varphi(t) , \\
  & \deref_{\setcharmvcn}(s, v) =
      \deref_{\setcharmt}(\varphi(s), v) , \\
  & \varphi(\putval_{\setcharmvcn}(s, v, s)) =
      \putval_{\setcharmt}(\varphi(s), v, s) , \\
  & \varphi(\select_{\setcharmvcn}(s, v)) =
      \select_{\setcharmt}(\varphi(s), v) ,
\end{eqnarray*}
for all $s,t \in \setmvcn{V}{D}$, $v \in V^\ast$.
\end{St}

In other words, $\varphi$~is an isomorphism from many-sorted algebra of
multinaming sets to an algebra of multitries.
This allows us to switch flexibly between multinaming set and multitrie
languages when describing further notions, choosing the most
appropriate form in each particular case.



\section{Cartesian product and flattening}

Operations described in the previous sections (union, intersection, selection)
preserve the type and structure of their operands. This section describes two
more complicated operations.

Before giving a formal definition for a cartesian product of namings, let us
informally describe how should an operation look like to deserve this name.
Let~$s'$ and~$s''$ be two multinaming sets. The values in their cartesian
product should be pairs~$(d',d'')$ where $d'$~is a value from~$s'$ and $d''$~is
taken from~$s''$. But these values are attached to some names~-- say,
$v'$~and~$v''$, respectively.  Therefore, the product should contain the
combined value~$(d',d'')$ under a name combined from~$v'$ and $v''$, and the
only combining operation defined for names is concatenation.

\begin{Df}\label{df:mvcn-cartesian}
Let~$s'$ and~$s''$ be $(V,D')$- and $(V,D'')$-multinaming sets, respectively. Their
\emph{cartesian product} is a $(V,D'\times D'')$-multinaming set
\[
  s'\times s'' = \{ (v' v'', (d',d'')) \mid (v',d')\in s', (v'',d'')\in s'' \} .
\]
\end{Df}

\begin{Ex}\label{ex:cartesian}
Consider the following multinaming sets:
\begin{eqnarray*}
  s'  & = & \{ (\varepsilon, 0), (a, 1), (a, 2) \} , \\
  s'' & = & \{ (\varepsilon, 3), (\varepsilon, 4), (b, 5) \} .
\end{eqnarray*}
Then their cartesian product is
\begin{eqnarray*}
  s' \times s'' & = &  \{ (\varepsilon, (0, 3)), (\varepsilon, (0, 4)) \} \cup \\
    & \cup & \{ (b, (0, 5)) \} \cup \\
    & \cup & \{ (a, (1, 3)), (a, (1, 4)), (a, (2, 3)), (a, (2, 4)) \} \cup \\
    & \cup & \{ (ab, (1, 5)), (ab, (2, 5)) \} .
\end{eqnarray*}
\end{Ex}

\begin{St}\label{st:cartesian-distributivity}
Obviously,~$\times$ distributes over $\cap$ and $\cup$.
For any $s' \in \setmvcn{V}{D'}$ and $s''_1, s''_2 \in \setmvcn{V}{D''}$,
\[
  s'\times(s''_1\odot s''_2) = (s'\times s''_1) \odot (s'\times s''_2) .
\]
The same holds for the left operand.
\end{St}

\begin{St}\label{st:deref-cartesian}
For any $s' \in \setmvcn{V}{D'}$ and $s'' \in \setmvcn{V}{D''}$,
\[
  \deref(s' \times s'', w) =
      \bigcup_{v',v''\in V^\ast: v' v'' = w}
          \deref(s', v')
          \times
          \deref(s'', v'') .
\]
\end{St}

This is the main property of cartesian product. Since a multinaming set is
completely defined by values of all names (st.~\ref{st:mvcn-deref-equality}),
it is preserved by the mapping~$\varphi$ from st.~\ref{st:isomorph}. Also, this
property may be taken as a definition of cartesian product for multitries.

Consider a multinaming set~$s$ whose values are, in their turn, multinaming
sets.  Flattening operation formally defined below turns it into a ``plain''
multinaming set.  Supose a name~$v'$ in~$s$ has a value~$t$ (and, maybe, some
other values).  Take a name~$v''$ that has a value~$d$ in the multinaming set~$t$
(and maybe other values).  Then flattening should turn~$s$ into such a
multinaming set~$r$, where~$d$ is a value of the name~$v'v''$.

\begin{Df}\label{df:flatten}
\emph{Flattening} is a unary operation
$\flatten : \setmvcn{V}{\setmvcn{V}{D}} \to\setmvcn{V}{D}$,
such that, for any $(V,\setmvcn{V}{D})$-multinaming set~$s$,
\[
  \flatten(s) = \{ (v'v'', d) \mid (v', t) \in s, (v'', d) \in t \} .
\]
\end{Df}

\begin{Ex}\label{ex:flatten}
Let
\begin{eqnarray*}
  t_1 & = & \{ (\varepsilon, 0), (a, 1) \} ,\\
  t_2 & = & \{ (a, 2), (aa, 3) \} ,\\
  t_3 & = & \{ (\varepsilon, 4), (a, 5) \} ,\\
  s   & = & \{ (\varepsilon, t_1), (\varepsilon, t_2), (a, t_3) \} .
\end{eqnarray*}
Then
\[
  \flatten(s) = \{
      (\varepsilon, 0), (a, 1), (a, 2), (a, 4), (aa, 3), (aa, 5)
  \} .
\]
The empty name~$\varepsilon$ has two values in~$s$, namely~$t_1$ and~$t_2$.
In~$t_1$, in its turn, the only value of~$\varepsilon$ is~0, whereas in~$t_2$
it does not have any value. Therefore, 0~is the only value of $\varepsilon
\varepsilon = \varepsilon$ in~$\flatten(s)$.  The name~$a$ has one value in~$t_1$
and one value in~$t_2$, it is~1 and~2, respectively.  Then $a = \varepsilon a$
has values~1 and~2 in $\flatten(s)$.  The name~$a$ in~$s$ has a value~$t_3$
where the empty name's value is~4. Thus, 4~is also a value of $a \varepsilon =
a$ in~$\flatten(s)$.

Now look at the name~$aa$. Its value~3 is inherited from~$t_2$. Except this,
name~$a$ in~$s$ has a valaue~$t_3$ that, in its turn, contains a name~$a$ with
a value~5. Hence, the name~$aa$ has in $\flatten(s)$ the second value~5.
\end{Ex}

The following property can be used to define flattening for multitries~--
in terms of dereferencing operation.
\begin{St}\label{st:deref-flatten}
For any $(V,\setmvcn{V}{D})$-multinaming set~$s$,
\[
  \deref(\flatten(s), w) =
      \bigcup_{v',v''\in V^\ast: v' v'' = w}
        \deref(\deref(s, v'), v'') .
\]
\end{St}



\section{Elementwise mappings and applications}

The previous sections described operations on namings containing some
`ordinary' values. Now let us consider how do namings interact with
functions, including how can a naming populated with functions act itself
as a function.

\begin{Df}\label{df:mvcn-map}
Let $f : D \to D'$. Then $\fmap$ operation turns it into a \emph{mapping
function} $\fmap_{\setcharmvcn} f : \setmvcn{V}{D} \to \setmvcn{V}{D'}$, such
that
\[
  (\fmap_{\setcharmvcn} f)(s) = \{ (v, f(d)) \mid (v, d) \in s \}
\]
for any $s \in \setmvcn{V}{D}$.
\end{Df}

The definition of mapping for multitries is straightforward, it can be easily
obtained from isomorphism. There are following well-known properties:

\begin{St}\label{st:map-properties}
If $\circ$ is a composition of unary functions, i.e. $(g\circ f)(x) = g(f(x))$ for
all $f$, $g$, $x$ of matching types, and $\id_X : X \to X$ is an identity function,
$\id_X(x) = x$ for any $x\in X$, then
\begin{eqnarray*}
  & \fmap \id_D = \id_{\setmvcn{V}{D}} , \\
  & \fmap (g \circ f) = (\fmap g) \circ (\fmap f) .
\end{eqnarray*}
\end{St}

\begin{St}\label{st:map-distributivity}
Mapping function distributes over set-theoretical union (but not intersection, in general):
Let $f: D \to D'$, $s, t \in \setmvcn{V}{D}$. Then
\[
  (\fmap f) (s \cup t) = (\fmap f)(s) \cup (\fmap f)(t) .
\]
\end{St}

Thus, $\fmap$ operation can apply a single unary function to a multinaming set of
values. It is easy to define an operation $\fpam$ that does the opposite:
applies a multinaming set of unary functions to a single value. For this purpose,
let us define first an auxiliary function that turns a value~$x$ into a
high order function applying an argument function to~$x$:

\begin{Df}\label{df:ylppa}
\emph{Reverse application} is a function
\[
  \ylppa : X \to ((X \to Y) \to Y),
\]
such that, for every $x\in X$, $\xi = \ylppa x$ is a function satisfying the
equation
\[
  \xi(f) = f(x)
\]
for every $f: X\to Y$.
\end{Df}

Then the reverse mapping operation gets a concise definition.

\begin{Df}\label{df:mvcn-pam}
\emph{Reverse mapping} is an operation
\[
  \fpam_{\setcharmvcn} : \setmvcn{V}{D \to D'} \to (D \to \setmvcn{V}{D'}),
\]
such that
\[
  (\fpam s)(d) = (\fmap (\ylppa d))(s) .
\]
for any $s\in \setmvcn{V}{D \to D'}$, $d\in D$.
\end{Df}

It is easy to see from the definitions of $\fmap$ and $\ylppa$ that $\fpam$
really does what was intended:

\begin{St}\label{st:mvcn-pam}
If $s$ is a $(V, D\to D')$-multinaming set, $d\in D$,
\[
  (\fpam s)(d) = \{ (v, f(d)) \mid (v, f) \in s \} .
\]
\end{St}

Since reverse mapping is defined as a special case of mapping, it inherits
distributivity, see st.~\ref{st:map-distributivity}.

\begin{St}\label{st:pam-distributivity}
Let $d\in D$, $s, t \in \setmvcn{V}{D \to D'}$. Then
\[
  (\fpam (s \cup t))(d) = (\fpam s)(d) \cup (\fpam t)(d) .
\]
\end{St}

Having defined operations that apply a single function to a multinaming set of values
and a multinaming set of functions to a single value, let us define an
operation that applies a multinaming set of functions to a multinaming set of values. The
operation must preserve trie-like naming structures of both operands~-- the
considerations motivating the definition of cartesian product apply here
as well. To avoid rewriting essentially the same definition twice, let us
instead introduce an auxiliary operation and reuse a previously defined
operation.

\begin{Df}\label{df:eval}
Operation $\eval$ called \emph{(unary) evaluation} has type
$(X \to Y) \times X \to Y$ and is defined as follows.
\[
  \eval (f, x) = f(x) .
\]
\end{Df}

In other words, this operation takes a pair whose first element is a unary
function and the second is an argument, and applies the function to the
argument. Thus, the application operation over multinaming sets can be defined as
follows.

\begin{Df}\label{df:mvcn-apply-cartesian}
\emph{Cartesian application} is an operation of type
\[
\setmvcn{V}{D\to D'} \times \setmvcn{V}{D} \to \setmvcn{V}{D'} ,
\]
such that
\[
  \apply_{\setcharmvcn}^{\times} (s, t) = (\fmap \eval) (s \times t)
\]
for any~$s$ and~$t$ of matching types.
\end{Df}

Recalling the definitions of cartesian product and evaluation, one can
obtain the main property of cartesian application (that could be also taken
for a definition, in which case def.~\ref{df:mvcn-apply-cartesian} would turn
into a theorem).
 
\begin{St}\label{st:mvcn-apply-cartesian}
If $s\in \setmvcn{V}{D\to D'}$, $t\in \setmvcn{V}{D}$,
\[
  \apply_{\setcharmvcn}^{\times} (s, t) =
    \{ (vw, f(d)) \mid (v,f) \in s, (w,d) \in t \} .
\]
\end{St}

Therefore, for every function~$f$ contained in~$s$ under a compound name~$v$
and every object~$d$ contained in~$t$ under a name~$w$, the resulting
multitrie contains a value~$f(d)$ under a name~$vw$.

Let us introduce an infix alias for the cartesian application operation to make
formulation of its properties more elegant:
\[
  s \inapply t = \apply^{\times} (s, t) .
\]

\begin{St}\label{st:apply-distr}
Cartesian application distributes over set-theoretical union.
For any~$s, s_1, s_2, t, t_1, t_2$ of matching types,
\begin{eqnarray*}
  (s_1 \cup s_2) \inapply t = (s_1 \inapply t) \cup (s_2 \inapply t) , \\
  s \inapply (t_1 \cup t_2) = (s \inapply t_1) \cup (s \inapply t_2) .
\end{eqnarray*}
\end{St}


\section{Notes about implementation}

A container type implementing the multivalued naming with compound names has
been defined in Haskell programming language. Some trade-offs between the
mathematical purity and implementability could hardly be avoided. On the other
hand, the conceptual framework provided by Haskell gave a
direction towards some additional features that turn an abstract mathematical
notion into a potentially useful tool.

The mathematical construct described above formalizes manyvaluedness by means
of a \emph{set}: the value of $\deref$ function is a set of the name's values.
In Haskell programming, however, the most common representation of a many-valued
function is a function whose value is a \emph{list} of possible
values~\cite[p.~285]{bib:lipovaca}.  Using lists instead of sets gives some
benefits. For example, the many-valued function, as a value generator, does not
need to compare every newly produced value with all previous ones. Lists can be
generated by one function and consumed by another in a lazy manner. Elements'
type needs to be an instance of \lstinline{Ord} class for sets and does not for
lists.  Note that,  from the
mathematical perspective, lists are closer to multisets than to sets because of
possibly duplicate elements.  Keeping in mind that a list-based implementation
is not isomorphic to the set-based specification, let us justify it as an
acceptable approximation.

The previous sections presented two isomorphic though different formalisations:
multinaming sets and multitries. The former has higer abstraction level and suits well
for specification purposes whereas the latter involves a trie~-- a practical
data structure suitable for an efficient implementation. The only impractical
feature of multitries definition introduced for the sake of mathematical
simplicity is their infiniteness~-- every multitrie has a child node under
every atomic name; this helped to simplify formulae by omiting check whether a
name is present in the trie.  In the trie-based implementation, however, it would be
better to store finite maps and perform such checks for the sake of efficiency.
In particular, if the underlying trie does not contain any child node for a
particular name, the object's behaviour observed via functions is the same as if
it associated this name with an empty multitrie.

All this leads to the following basic definition (indeed, the module hides it
behind smart constructors).

\begin{lstlisting}
data MultiTrie v d = MultiTrie {
        values :: [d],
        children :: Data.Map.Map v (MultiTrie v d) }
\end{lstlisting}

The most important functions defined in the module are listed below.

\begin{lstlisting}
empty ::
  MultiTrie v d
leaf ::
    [d] -> MultiTrie v d
addValue ::
    d -> MultiTrie v d -> MultiTrie v d
values ::
    MultiTrie v d -> [d]
children ::
    MultiTrie v d -> MultiTrieMap v d
null ::
    MultiTrie v d -> Bool
size ::
    MultiTrie v d -> Int
isEqualStrict :: (Ord v, Eq d) =>
    MultiTrie v d -> MultiTrie v d -> Bool
subnode :: Ord v =>
    [v] -> MultiTrie v d -> MultiTrie v d
map :: Ord v =>
    (d -> w) -> MultiTrie v d -> MultiTrie v w
cartesian :: Ord v =>
    MultiTrie v d -> MultiTrie v w -> MultiTrie v (d, w)
union :: Ord v =>
    MultiTrie v d -> MultiTrie v d -> MultiTrie v d
flatten :: Ord v =>
    MultiTrie v (MultiTrie v d) -> MultiTrie v d
apply :: Ord v =>
    MultiTrie v (d -> w) -> MultiTrie v d -> MultiTrie v w
toMap :: Ord v =>
    MultiTrie v d -> Map [v] [d]
toList :: Ord v =>
    MultiTrie v d -> [([v], d)]
fromList :: Ord v =>
    [([v], d)] -> MultiTrie v d
\end{lstlisting}

Here is a short explanation of their semantics.
\begin{description}
\item [empty]
  A constant for the empty multitrie~$\bot$, see def.~\ref{df:mvcn-extreme}
  and~\ref{df:mt-extreme}.
\item [leaf] Given a list of values, constructs a multitrie that has this list
  in its root node and no other valies (i.e. all other names yield to an empty
  list of values).
\item [addValue]
  Given a value and a multitrie, prepend the value to the list stored in the
  root node.
\item [values]
  Get a list of values from the root node of a multitrie.
\item [children]
  From the root node of a multitrie, get a mapping of atomic names to the
  child nodes.
\item [null]
  Check whether the argument multitrie is empty.
\item [size]
  Get the total number of values in the multitrie.
\item [isEqualStrict]
  Compare two multitries: they are considered equal if equal are lists of
  values under all compound names. I.e. if the multitries have equal lists
  of values in their root nodes and, for every atomic name, the corresponding
  child multitries are equal in this sense, in their turn. There is another
  function for weak comparison~-- it ignores order of elements in the lists
  treating them as multisets.
\item [subnode]
  Get a node pointed to by a compound name. If the name is not present in the
  underlying data structure, the function anyway yields a correct value, the
  empty multitrie. This function implements selection operation from
  def.~\ref{df:mvcn-select} and~\ref{df:mt-select}.
\item [map]
  Apply a function to each value in a multitrie and combine results into
  a new multitrie preserving the names (and, therefore, the trie structure),
  see def.~\ref{df:mvcn-map}.
  This is a specific implementation of the \lstinline{fmap} method from the
  \lstinline{Functor} class.
\item [cartesian]
  Construct a cartesian product of two multitries in the sense of
  def.~\ref{df:mvcn-cartesian} and st.~\ref{st:deref-cartesian}.
\item [union]
  Construct a union of two multitries, see st.~\ref{st:mvcn-setop} and
  def.~\ref{df:mt-setop}. There is another function for intersection.
\item [flatten]
  Given a multitrie whose values are, in their turn, multitries, construct
  a flattened multitrie, see def.~\ref{df:flatten} and
  st.~\ref{st:deref-flatten}. This is a specific implementation of the
  \lstinline{join} function defined for all types of the \lstinline{Monad}
  class.
\item [apply]
  Cartesian
  application of a multitrie of functions to a multitrie of arguments, see
  def.~\ref{df:mvcn-apply-cartesian}.
\item [toMap]
  Convert a multitrie to a \lstinline{Data.Map} that maps compound names to
  lists of values. Corresponds to an inverse of the isomorphism~$\varphi$
  from st.~\ref{st:isomorph}.
\item [toList]
  Convert a multitrie to a list of name--value pairs.
\item [fromList]
  Convert a list of name--value pairs to a multitrie.
\end{description}

Finally, \lstinline{map} function that implements the $\fmap$ operation
(def.~\ref{df:mvcn-map} and st.~\ref{st:map-properties})
makes \lstinline{MultiTrie} type an instance of the \lstinline{Functor} class; 
\lstinline{apply} function as an implementation of $\apply^{\times}$
operation makes it an instance of the \lstinline{Applicative} class; 
\emph{bind} operation (not shown in this article; easy to define using mapping
and flattening operations) makes the type an instance of the
\lstinline{Monad} class.



\section{Conclusion}

The notion of naming and its most general formalisation, taken as a starting
point, has been transformed into a more concrete notion enriched with specifics of
\emph{structuredness} and \emph{many-valuedness}. Being structured
means that a name can not only refer to an atomic value but also
to a structured value, i.e. to a subobject that, in its turn, has named parts.
Being many-valued means that, instead of a unique atomic value, each leaf node
of a structured object can have zero, one or multiple, even infinitely many
values.

It is not surprising that structuredness and manyvaluedness appear together.
Although univalued structured objects seem more familiar (and, in fact, found
in practical programming everywhere), it is multivaluedness that makes
mathematical properties of structured namings elegant and harmonic: otherwise
set-theoretical union and intersection, cartesian product, flattening and
application would not make sense. Due to multivaluedness, these operations are
not just meaningful but also obey `good' properties, e.g.  associativity and/or
distributivity over other operations.

From the two formalisations of multivalued structured objects, the first
approach is \emph{extensional}~-- it concentrates on the properties of the
naming relation taken as a whole. The second approach is \emph{intensional}, it
reveals a decomposition of the whole naming into simpler sub-naming and thus
gives a hint about how it could be implemented programmatically.  The `good'
properties of operations fit the multitrie data type into rich typeclasses that
makes multitries a first-class member of Haskell container types, together with
lists, maps and trees.

As far as a list is a conventional model for a non-deterministic computation
that generates cases one by one in a lazy manner, a multitrie could be used to
represent a non-deterministic structure unfolding when the consumer needs more
detail.  On the other hand, in the same way as a list could be \emph{simply a
list}, a multitrie could represent a static entity for which a list is a normal
contents (i.e. not a set of possibilities). A typical example could be a
directory tree where an atomic name corresponds to a directory, a compound name
means a path, and values correspond to individual files.  A structure of an XML
document is another example of such objects.



\begin{thebibliography}{00}

\bibitem{bib:frege}
  Gottlob Frege,
  \"Uber Sinn und Bedeutung.
  In: Zeitschrift f\"ur Philosophie und philosophische Kritik,
  NF~100. 1892, S.~25--50.

\bibitem{bib:wittgenstein}
  Ludwig Wittgenstein,
  Tractatus logico-philosophicus, Logisch-phi\-lo\-so\-phi\-sche Abhandlung.
  Suhrkamp,
  Frankfurt am Main,
  2003.

\bibitem{bib:quine}
  Quine, Willard Van Orman,
  Word and Object [1960].
  New edition, with a foreword by Patricia Churchland,
  Cambridge,
  Mass.: MIT Press,
  2015.

\bibitem{bib:ptop}
  Eric C.R. Hehner,
  A Practical Theory of Programming,
  2016-4-14 edition,
  http://www.cs.utoronto.ca/~hehner/aPToP/aPToP.pdf.

\bibitem{bib:utp}
  C.\,A.\,R.\,Hoare, He Jifeng,
  Unifying Theories of Programming,
  Prentice-Hall,
  1998.

\bibitem{bib:leroy}
  Xavier Leroy, Sandrine Blazy.
  Formal verification of a C-like memory model and its uses for verifying program transformations.
  Journal of Automated Reasoning.
  41(1), pp.1-31, July 2008.

\bibitem{bib:redko}
  Basarab~I., Nikitchenko~N., Red’ko~V.
  Compositional Databases.
  Kiev: Lybed’, 1992.~-- 191~p. (In Russian).

\bibitem{bib:ollongren}
  Alexander Ollongren,
  Definition of programming languages by interpreting automata.
  London: Academic Press,
  1974.

\bibitem{bib:dictionary}
  Paul~E.~Black,
  ``Dictionary'', in Dictionary of Algorithms and Data Structures [online],
  Vreda Pieterse and Paul E. Black, eds.
  Available from: http://www.nist.gov/dads/HTML/dictionary.html

\bibitem{bib:mehlhorn-assoc}
  Kurt Mehlhorn, Peter Sanders
  ``4: Hash Tables and Associative Arrays'',
  Algorithms and Data Structures: The Basic Toolbox
  Springer, pp.~81--98.

\bibitem{bib:knuth-trie}
  Donald Knuth,
  ``6.3: Digital Searching''.
  The Art of Computer Programming,
  Volume 3: Sorting and Searching (2nd ed.).
  Addison-Wesley. p.~492.


\bibitem{bib:lipovaca}
  Miran Lipova\v{c}a.
  Learn You Haskell for Great Good!
  360 pages,
  No Starch Press,
  2011.

\end{thebibliography}

\end{document}