]> matita.cs.unibo.it Git - helm.git/blob - mathql/doc/mathql_operational_background.tex
Much ado about nothing:
[helm.git] / 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.