X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_operational_background.tex;fp=helm%2Fmathql%2Fdoc%2Fmathql_operational_background.tex;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=ad0be5122dec7577e77532d6bc0228dce579b75e;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/mathql/doc/mathql_operational_background.tex b/helm/mathql/doc/mathql_operational_background.tex deleted file mode 100644 index ad0be5122..000000000 --- a/helm/mathql/doc/mathql_operational_background.tex +++ /dev/null @@ -1,147 +0,0 @@ -\subsection {Mathematical background} - -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 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 -\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 $ 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 $ ($ \{y_1, \cdots, y_m\} $ will denote a set as -usual). - -{\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}).% -\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}. - -With the above constructors we can give a formal meaning to most of the -standard notation. For instance we will use the following: - -\begin{itemize} - -\item -$ {\ES} \oft (\Setof\ Y) $ - -\item -$ {\lex} \oft ((\Setof\ Y) \to \Boole) \to \Boole $ - -\item -$ {\lall} \oft ((\Setof\ Y) \to \Boole) \to \Boole $ - -\item -$ {\in} \oft Y \to (\Setof\ Y) \to \Boole $ (infix) - -\item -$ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix) - -\item -$ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix) - -\item -$ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix) - -\item -$ {\sor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix) - -\item -$ {\sdor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ -(the disjoint union, infix) - -\item -$ \le \oft \Num \to \Num \to \Boole $ (infix) - -\item -$ < \oft \Num \to \Num \to \Boole $ (infix) - -\item -$ \# \oft (\Setof\ Y) \to \Num $ (the size operator) - -\item -$ \app \oft (\Listof\ Y) \to (\Listof\ Y) \to (\Listof\ Y) $ -(the concatenation, infix) - -\item -$ \lnot \oft \Boole \to \Boole $ - -\end{itemize} - -\noindent -Note that $ \lall $ and $ \lex $ are always decidable because the sets are -finite by definition. - -\noindent -$ 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 $ \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 presentation and we will use: - -\begin{itemize} - -\item -$ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $. - -\item -$ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $. - -\item -$ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that -$ \Fsts\ U = \{\Fst\ u \st u \in U\} $. - -\item -With the same notation, if $ W $ contains just one couple whose first -component is $ y $, then $ \get{W}{y} $ is the second component of that couple. -In the other cases $ \get{W}{y} $ is not defined. -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 -$ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $. - -\item -Also $ U + W $ is the union of two sets of couples in the following sense: - -\begin{footnotesize} -\begin{center} \begin{tabular}{rll} -% -$ U + \ES $ & rewrites to & $ U $ \\ -$ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $ -% -\end{tabular} \end{center} -\end{footnotesize} - -\end{itemize} - -The last three operators are used to read, write and join association sets, -which are sets of couples such that the first components of two different -elements are always different. -These sets will be exploited to formalize the memories appearing in evaluation -contexts.