\subsection {Mathematical background}

As background for the semantics, we revise the one presented in
\cite{Gui03,GS03}.

{\Str} denotes the type of strings and its elements are the finite sequences
of Unicode \cite{Unicode} characters.
Grammatical productions denote the subtype of {\Str} containing the produced
sequences of characters.

{\Num} denotes the type of numbers and is the subtype of {\Str} defined by 
\GP{num}. In this type, numbers are represented by their decimal expansion.

$ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
sequences without repetitions) over $ Y $ and
$ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences)
over $ Y $.
We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements 
are $ y_1, \cdots, y_m $ ($ \{y_1, \cdots, y_m\} $ will denote a set as
usual).

{\Boole}, the type of Boolean values, is defined as the set
$ \{\ES, \{("", \ES)\}\} $ of type $ \Setof\ \Setof\ (\Str \times \Setof\ Y) $ 
where the first element stands for \emph{false} (denoted by {\F}) and the
second element stands for \emph{true} (denoted by {\T}).%
\footnote{This definition allows to treat a Boolean value as an {\av} set.}

$ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements
are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $.
The notation is also extended to a ternary product.
$ Y \to Z $ denotes the type of functions from $ Y $ to $ Z $ and $ f\ y $
denotes the application of $ f \oft Y \to Z $ to $ y \oft Y $.
Relations over types, such as equality, are seen as functions to {\Boole}.

With the above constructors we can give a formal meaning to most of the
standard notation. For instance we will use the following:  

\begin{itemize}

\item
$ {\ES} \oft (\Setof\ Y) $ 

\item
$ {\lex} \oft ((\Setof\ Y) \to \Boole) \to \Boole $

\item
$ {\lall} \oft ((\Setof\ Y) \to \Boole) \to \Boole $

\item
$ {\in} \oft Y \to (\Setof\ Y) \to \Boole $ (infix) 

\item
$ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix) 

\item
$ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)

\item
$ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)

\item
$ {\sor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)

\item
$ {\sdor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $
(the disjoint union, infix)

\item
$ \le \oft \Num \to \Num \to \Boole $ (infix)

\item
$ < \oft \Num \to \Num \to \Boole $ (infix)

\item
$ \# \oft (\Setof\ Y) \to \Num $ (the size operator)

\item
$ \app \oft (\Listof\ Y) \to (\Listof\ Y) \to (\Listof\ Y) $
(the concatenation, infix)

\item
$ \lnot \oft \Boole \to \Boole $

\end{itemize}

\noindent
Note that $ \lall $ and $ \lex $ are always decidable because the sets are
finite by definition.

\noindent
$ U \meet W $ means $ (\lex u \in U)\ u \in W $ and expresses the fact that
$ U \sand W $ is inhabited as a primitive notion, {\ie} without mentioning
intersection and equality as for $ U \sand W \neq \ES $, which is equivalent
but may be implemented less efficiently in real cases%
\footnote{As for the Boolean condition $ \fa \lor \fb $ which may have a more
efficient implementation than $ \lnot(\lnot \fa \land \lnot \fb) $.}.
$ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual
(recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $)
and is already being used successfully in the context of a constructive
({\ie} intuitionistic and predicative) approach to point-free topology
\cite{Sam00}.

Sets of couples play a central role in our presentation and we will use:

\begin{itemize}

\item
$ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $.

\item
$ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $.

\item
$ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that 
$ \Fsts\ U = \{\Fst\ u \st u \in U\} $.

\item 
With the same notation, if $ W $ contains just one couple whose first
component is $ y $, then $ \get{W}{y} $ is the second component of that couple.
In the other cases $ \get{W}{y} $ is not defined.
This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $.  

\item
Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every
couple whose first component is $ y $ and adding the couple $ (y, z) $.
The type of this operator is
$ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.  

\item 
Also $ U + W $ is the union of two sets of couples in the following sense:

\begin{footnotesize}
\begin{center} \begin{tabular}{rll}
%
$ U + \ES $ & rewrites to & $ U $ \\
$ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $   
%
\end{tabular} \end{center}
\end{footnotesize}

\end{itemize}

The last three operators are used to read, write and join association sets,
which are sets of couples such that the first components of two different
elements are always different.
These sets will be exploited to formalize the memories appearing in evaluation
contexts. 
