+++ /dev/null
-\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.
projects / helm.git / blobdiff