helm/mathql/doc/mathql_operational_background.tex

   1 \subsection {Mathematical background}
   2
   3 As a mathematical background for the semantics, we take the one presented in
   4 \cite{Gui03}.
   5
   6 {\Str} denotes the type of strings and its elements are the finite sequences
   7 of Unicode \cite{Unicode} characters.
   8 Grammatical productions, represented as strings in angle brackets, denote the
   9 subtype of {\Str} containing the produced sequences of characters.
  10
  11 {\Num} denotes the type of numbers and is the subtype of {\Str} defined by the
  12 regular expression: \TT{'0 - 9' [ '0 - 9' ]*}.
  13 In this type, numbers are represented by their decimal expansion.
  14
  15 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
  16 sequences without repetitions) over $ Y $.
  17 $ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences)
  18 over $ Y $.
  19 We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements
  20 are $ y_1, \cdots, y_m $.
  21
  22 {\Boole}, the type of Boolean values, is defined as
  23 $ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $
  24 where the first element stands for \emph{false} (denoted by {\F}) and the
  25 second element stands for \emph{true} (denoted by {\T}).
  26
  27 $ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements
  28 are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $.
  29 The notation is also extended to a ternary product.
  30
  31 $ Y \to Z $ denotes the type of functions from $ Y $ to $ Z $ and $ f\ y $
  32 denotes the application of $ f \oft Y \to Z $ to $ y \oft Y $.
  33 Relations over types, such as equality, are seen as functions to {\Boole}.
  34
  35 With the above constructors we can give a formal meaning to most of the
  36 standard notation. For instance we will use the following:
  37
  38 \begin{itemize}
  39
  40 \item
  41 $ {\ES} \oft (\Setof\ Y) $
  42
  43 \item
  44 $ {\lex} \oft ((\Setof\ Y) \to \Boole) \to \Boole $
  45
  46 \item
  47 $ {\lall} \oft ((\Setof\ Y) \to \Boole) \to \Boole $
  48
  49 \item
  50 $ {\in} \oft Y \to (\Setof\ Y) \to \Boole $ (infix)
  51
  52 \item
  53 $ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
  54
  55 \item
  56 $ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
  57
  58 %\item
  59 $ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
  60
  61 \item
  62 $ {\sor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
  63
  64 \item
  65 $ {\sdor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $
  66 (the disjoint union, infix)
  67
  68 \item
  69 $ \le \oft \Num \to \Num \to \Boole $ (infix)
  70
  71 \item
  72 $ < \oft \Num \to \Num \to \Boole $ (infix)
  73
  74 \item
  75 $ \# \oft (\Setof\ Y) \to \Num $ (the size operator)
  76
  77 \item
  78 $ \app \oft (\Listof\ Y) \to (\Listof\ Y) \to (\Listof\ Y) $
  79 (the concatenation, infix)
  80
  81 \item
  82 $ \lnot \oft \Boole \to \Boole $
  83
  84 \end{itemize}
  85
  86 \noindent
  87 Note that $ \lall $ and $ \lex $ are always decidable because the sets are
  88 finite by definition.
  89
  90 \noindent
  91 $ U \meet W $ means $ (\lex u \in U)\ u \in W $ and expresses the fact that
  92 $ U \sand W $ is inhabited as a primitive notion, {\ie} without mentioning
  93 intersection and equality as for $ U \sand W \neq \ES $, which is equivalent
  94 but may be implemented less efficiently in real cases%
  95 \footnote{As for the Boolean condition $ \a \lor \b $ which may have a more
  96 efficient implementation than $ \lnot(\lnot \a \land \lnot \b) $.}.
  97
  98 $ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual
  99 (recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $)
 100 and is already being used successfully in the context of a constructive
 101 ({\ie} intuitionistic and predicative) approach to point-free topology
 102 \cite{Sam00}.
 103
 104 Sets of couples play a central role in our formalization and in particular we
 105 will use:
 106
 107 \begin{itemize}
 108
 109 \item
 110 $ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $.
 111
 112 \item
 113 $ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $.
 114
 115 \item
 116 $ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that
 117 $ \Fsts\ U = \{\Fst\ u \st u \in U\} $.
 118
 119 \item
 120 With the same notation, if $ W $ contains just one couple whose first
 121 component is $ y $, then $ \get{W}{y} $ is the second component of that couple.
 122 In the other cases $ \get{W}{y} $ is not defined.
 123 This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $.
 124
 125 \item
 126 Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every
 127 couple whose first component is $ y $ and adding the couple $ (y, z) $.
 128 The type of this operator is \\
 129 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.
 130
 131 \item
 132 Also $ U + W $ is the union of two sets of couples in the following sense:
 133
 134 \begin{footnotesize}
 135 \begin{center} \begin{tabular}{rll}
 136 %
 137 $ U + \ES $ & rewrites to & $ U $ \\
 138 $ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $
 139 %
 140 \end{tabular} \end{center}
 141 \end{footnotesize}
 142
 143 \end{itemize}
 144
 145 The last three operators are used to read, write and join association sets,
 146 which are sets of couples such that the first components of two different
 147 elements are always different.
 148 These sets will be exploited to formalize the memories appearing in evaluation
 149 contexts.