helm/mathql/doc/mathql_operational_background.tex

   1 \subsection {Mathematical background}
   2
   3 As background for the semantics, we revise the one presented in
   4 \cite{Gui03,GS03}.
   5
   6 {\Str} denotes the type of strings and its elements are the finite sequences
   7 of Unicode \cite{Unicode} characters.
   8 Grammatical productions denote the subtype of {\Str} containing the produced
   9 sequences of characters.
  10
  11 {\Num} denotes the type of numbers and is the subtype of {\Str} defined by
  12 \GP{num}. In this type, numbers are represented by their decimal expansion.
  13
  14 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
  15 sequences without repetitions) over $ Y $ and
  16 $ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences)
  17 over $ Y $.
  18 We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements
  19 are $ y_1, \cdots, y_m $ ($ \{y_1, \cdots, y_m\} $ will denote a set as
  20 usual).
  21
  22 {\Boole}, the type of Boolean values, is defined as the set
  23 $ \{\ES, \{("", \ES)\}\} $ of type $ \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 \footnote{This definition allows to treat a Boolean value as an {\av} set.}
  27
  28 $ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements
  29 are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $.
  30 The notation is also extended to a ternary product.
  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 $ \fa \lor \fb $ which may have a more
  96 efficient implementation than $ \lnot(\lnot \fa \land \lnot \fb) $.}.
  97 $ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual
  98 (recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $)
  99 and is already being used successfully in the context of a constructive
 100 ({\ie} intuitionistic and predicative) approach to point-free topology
 101 \cite{Sam00}.
 102
 103 Sets of couples play a central role in our presentation and we will use:
 104
 105 \begin{itemize}
 106
 107 \item
 108 $ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $.
 109
 110 \item
 111 $ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $.
 112
 113 \item
 114 $ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that
 115 $ \Fsts\ U = \{\Fst\ u \st u \in U\} $.
 116
 117 \item
 118 With the same notation, if $ W $ contains just one couple whose first
 119 component is $ y $, then $ \get{W}{y} $ is the second component of that couple.
 120 In the other cases $ \get{W}{y} $ is not defined.
 121 This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $.
 122
 123 \item
 124 Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every
 125 couple whose first component is $ y $ and adding the couple $ (y, z) $.
 126 The type of this operator is
 127 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.
 128
 129 \item
 130 Also $ U + W $ is the union of two sets of couples in the following sense:
 131
 132 \begin{footnotesize}
 133 \begin{center} \begin{tabular}{rll}
 134 %
 135 $ U + \ES $ & rewrites to & $ U $ \\
 136 $ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $
 137 %
 138 \end{tabular} \end{center}
 139 \end{footnotesize}
 140
 141 \end{itemize}
 142
 143 The last three operators are used to read, write and join association sets,
 144 which are sets of couples such that the first components of two different
 145 elements are always different.
 146 These sets will be exploited to formalize the memories appearing in evaluation
 147 contexts.