--- /dev/null
+\subsection {Mathematical background}
+
+As a mathematical background for the semantics, we take the one presented in
+\cite{Gui03}.
+
+{\Str} denotes the type of strings and its elements are the finite sequences
+of Unicode \cite{Unicode} characters.
+Grammatical productions, represented as strings in angle brackets, 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 the
+regular expression: \TT{'0 - 9' [ '0 - 9' ]*}.
+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 $.
+$ \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 $.
+
+{\Boole}, the type of Boolean values, is defined as
+$ \{\ES, \{("", \ES)\}\} \oft \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}).
+
+$ 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 $ \a \lor \b $ which may have a more
+efficient implementation than $ \lnot(\lnot \a \land \lnot \b) $.}.
+
+$ 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 formalization and in particular 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.
projects / helm.git / blobdiff