\subsection {Mathematical background}
-As a mathematical background for the semantics, we take the one presented in
-\cite{Gui03}.
+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, represented as strings in angle brackets, denote the
-subtype of {\Str} containing the produced sequences of 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 the
-regular expression: \TT{'0 - 9' [ '0 - 9' ]*}.
-In this type, numbers are represented by their decimal expansion.
+{\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 $.
+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 $.
+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
-$ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $
+{\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}).
+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}.
\item
$ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
-%\item
+\item
$ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
\item
$ 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) $.}.
-
+\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 formalization and in particular we
-will use:
+Sets of couples play a central role in our presentation and we will use:
\begin{itemize}
\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 \\
+The type of this operator is
$ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.
\item
projects / helm.git / blobdiff