X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_operational_background.tex;h=ad0be5122dec7577e77532d6bc0228dce579b75e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0c831f812eda5afc4dd427179a5626d49f9a4ea7;hpb=468da7af4b52d01451073ff1cca5aa1949b9657f;p=helm.git

diff --git a/helm/mathql/doc/mathql_operational_background.tex b/helm/mathql/doc/mathql_operational_background.tex
index 0c831f812..ad0be5122 100644
--- a/helm/mathql/doc/mathql_operational_background.tex
+++ b/helm/mathql/doc/mathql_operational_background.tex
@@ -1,33 +1,33 @@
 \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}.
@@ -55,7 +55,7 @@ $ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 \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
@@ -92,17 +92,15 @@ $ 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) $.}.
-
+\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}
 
@@ -125,7 +123,7 @@ 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 \\
+The type of this operator is
 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.  
 
 \item