# leithaus/XTrace

… logic of monoids.
 @@ -1,3 +1,178 @@ \section{How our web framework enables different kinds of application queries} -TBD +\subsubsection{An alternative presentation} + +If you recall, there's an alternative way to present monads that are +algebras, like our monoid monad. Algebras are presented in terms of +generators and relations. In our case the generators presentation is +really just a grammar for monoid expressions. + +\begin{mathpar} + \inferrule* [lab=expression] {} {{m,n} ::=} + \and + \inferrule* [lab=identity element] {} {e} + \and + \inferrule* [lab=generators] {} {\;| \; g_1 \; | \; ... \; | \; g_n} + \and + \inferrule* [lab=monoid-multiplication] {} {\;| \; m * n} +\end{mathpar} + +This is subject to the following constraints, meaning that we will +treat syntactic expressions of certain forms as denoting the same +element of the monoid. To emphasize the nearly purely syntactic role +of these constraints we will use a different symbol for the +constraints. We also use the same symbol, $\equiv$, for the smallest equivalence +relation respecting these constraints. + +\begin{mathpar} + \inferrule* [lab=identity laws] {} {m * e \equiv m \equiv e * m} + \and + \inferrule* [lab=associativity] {} {m_1 * (m_2 * m_3) \equiv (m_1 * m_2) * m_3} +\end{mathpar} + +\paragraph{Logic: the set monad as an algebra} +In a similar manner, there is a language associated with the monad of +sets \emph{considered as an algebra}. This language is very familiar +to most programmers. + +\begin{mathpar} + \inferrule* [lab=expression] {} {{c,d} ::=} + \and + \inferrule* [lab=identity verity] {} {true} + \and + \inferrule* [lab=negation] {} {\;| \; \neg c} + \and + \inferrule* [lab=conjunction] {} {\;| \; c \& d} +\end{mathpar} + +Now, if we had a specific set in hand, say $L$ (which we'll call a +universe in the sequel), we can interpret the expressions in the this +language, aka formulae, in terms of operations on subsets of that +set. As with our compiler for the concrete syntax of the +$lambda$-calculus in chapter 1, we can express this translation very +compactly as + +\begin{mathpar} + \inferrule* {} {\meaningof{true} = L} + \and + \inferrule* {} {\meaningof{\neg c} = L \backslash c} + \and + \inferrule* {} {\meaningof{c \& d} = \meaningof{c} \cap \meaningof{d}} +\end{mathpar} + +Now, what's happening when we pull the monoid monad through the set +monad via a distributive map is this. First, the monoid monad +furnishes the universe, $L$, as the set of expressions generated by +the grammar. We'll denote this by $L(m)$. Then, we enrich the set of +formulae by the operations of the monoid \emph{acting on sets}. + +\begin{mathpar} + \inferrule* [lab=expression] {} {{c,d} ::=} + \and + \inferrule* [lab=identity verity] {} {true} + \and + \inferrule* [lab=negation] {} {\;| \; \neg c} + \and + \inferrule* [lab=conjunction] {} {\;| \; c \& d} + \and + \inferrule* [lab=identity verity] {} {\bf{e}} + \and + \inferrule* [lab=negation] {} {\;| \; \bf{g_1} \; | \; ... \; | \; \bf{g_n}} + \and + \inferrule* [lab=conjunction] {} {\;| \; c * d} +\end{mathpar} + +The identity element, $e$ and the generators of the monoid, $g_1$, +..., $g_n$, can be considered $0$-ary operations in the same way that +we usually consider constants as $0$-ary operations. To avoid +confusion between these elements and the \emph{logical formulae} that +pick them out of the crowd, we write the logical formulae in +$\bf{boldface}$. + +Now, we can write our distributive map. Surprisingly, it is exactly a +meaning for our logic! + +\begin{mathpar} + \inferrule* {} {\meaningof{true} = L(m)} + \and + \inferrule* {} {\meaningof{\neg c} = L(m) \backslash c} + \and + \inferrule* {} {\meaningof{c \& d} = \meaningof{c} \cap \meaningof{d}} + \and + \inferrule* {} {\meaningof{\bf{e}} = \{ m \; \in \; L(m) \; | \; m \equiv e \}} + \and + \inferrule* {} {\meaningof{\bf{g_i}} = \{ m \; \in \; L(m) \; | \; m \equiv g_i \}} + \and + \inferrule* {} {\meaningof{c*d} = \{ m \; \in \; L(m) \; | \; m \equiv m_1 * m_2, m_1 \; \in \; \meaningof{c}, m_2 \; \in \; \meaningof{d} \}} +\end{mathpar} + +\paragraph{Primes: an application} +Before going any further, let's look at an example of how to use these +new operators. Suppose we wanted to pick out all the elements of the +monoid that were not expressible as a composition of other +elements. Obviously, for monoids with a finite set of generators, this +is exactly just the generators, so we could write $\bf{g_1} || ... || +\bf{g_n}$\footnote{We get the disjunction, $||$, by the usual DeMorgan + translation: $c || d \stackrel{def}{=} \neg( \neg c \& \neg + d)$}. However, when the set of generators is not finite, as it is +when the monoid is the integers under multiplication, we need another +way to write this down. That's where our other operators come in +handy. A moment's thought suggests that we could say that since $true$ +denotes any possible element in the monoid, an element is not a +composition using negation plus our composition formula, i.e. $\neg +(true * true)$. This is a little overkill, however. We just want to +eliminate non-trivial compositions. We know how to express the +identity element, that's $\bf{e}$, so we are interested in those +elements that are not the identity, i.e. $\neg \bf{e}$. Then a formula +that eliminates compositions of non-trivial elements is spelled out +$\neg (\neg e * \neg e)$. Finally, we want to eliminate the identity +as a solution. So, we arrive at $\neg (\neg e * \neg e) \& \neg +e$. There, that formula picks out the \emph{primes} of \emph{any} +monoid. + +\paragraph{Summary} + +What have we done? We've illustrated a specific distributive map, one +that pulls the set monad through the monoid monad. We've shown that +this particular distributive map coincides with giving a semantics to +a particular logic, one whose structure is derived solely from the +shape of the collection monad, i.e. set, and the shape of the term +language, in this case monoid. + +\subsubsection{Iterating the design pattern} + +The whole point of working in this manner is that by virtue of its +compositional structure it provides a much higher level of abstraction +and greater opportunities for reuse. To illustrate the point, we will +now iterate the construction using our toy language, the +$lambda$-calculus, as the term language. As we saw in chapter 1, the +$lambda$-calculus also has a generators and relations +presentation. Unlike a monoid, however, the lambda calculus has +another piece of machinery: reduction! In addition to structural +equivalence of terms (which is a bi-directional relation) there is the +$beta$-reduction rule that captures the \emph{behavioral} aspect of +the lambda calculus. + +It is key to understand this underlying structure of language +definitions. In essence, when a DSL is purely about structure it is +presented entirely in terms of generators (read a grammar) and +relations (like the monoid laws). When the DSL is also about behavior, +i.e. the terms in the language somehow express some kind of +computation, then the language has a third component, some kind of +reduction relation. \footnote{In some sense this is one of the central + contributions of the theory of computation back to + mathematics. Algebraists have known for a long time about generators + and relations presentations of algebraic structures (of which + algebraic data types are a subset). This collective wisdom is + studied, for example, in the field of universal + algebra. Computational models like the $lambda$-calculus and more + recently the process calculi, like Milner's $\pi$-calculus or + Cardelli and Gordon's ambient calculus, take this presentation one + step further and add a set of conditional rewrite rules to express + the computational content of the model. It was Milner who first + recognized this particular decomposition of language definitions in + his seminal paper, Functions as Processes, where he reformulated the + presentation $\pi$-calculus along these lines.} This organization, +this common factoring of the specification of a language, makes it +possible to factor code that handles a wide range of semantic +features. The logic we derive below provides a great example.