Exercise 8.4
The following formal text in flag format is about some well-known notions in algebra, where ‘op’ means a binary operation on $S$, in Curried form (cf. Remark 1.2.6).
(a) Translate the text into a more usual format, as you might find in a textbook. Use infix notation when appropriate.
(b) Underline all variables that are bound to a binding variable introduced in the text.
(c) Rewrite lines (1) and (2) in the format $Γ \triangleright a(...) := M : N$ as described in Section 8.5.
(a)
(1) Given a set $S$ and a binary operator op that takes two elements of $S$ and returns an element of $S$, then $(S,\textit{op})$ is a semigroup if for all $x, y, z \in S$
$$ x \textit{ op } (y \textit{ op } z) \; = \; (x \textit{ op } y) \textit{ op } z $$
(2) Given a semigroup $(S,\textit{op})$, the element $e \in S$ is a unit if for all $x \in S$
$$ x \textit { op } e = x \quad \land \quad e \text{ op } x = x $$
(3) A semigroup $(S,\textit{op})$ is a monoid if there exists an element $e \in S$ that is a unit.
(4) The unit of a semigroup is unique. That is, if $e_1$ and $e_2$ are units of a semigroup then $e_1 = e_2$.
(b) The following shows all the bound variables.
(c)
(1)
$$ S:*_s, \textit{op}:S \to S \to S \; \triangleright \; \textit{semigroup}(S, \textit{op}) \; := \; \forall_{x,y,z:S} \left ( \textit{op} \; x \; (\textit{op} \; y \; z) = \textit{op} \; (\textit{op} \; x \; y) \; z \right ) \; : \; *_p $$
(2)
$$ \begin{gather*} S:*_s, \textit{op}:S \to S \to S, u:\textit{semigroup}(S, \textit{op}), e:S \; \triangleright \\ \\ \textit{unit}(S, \textit{op}, u, e) \; := \; \forall_{x:S} \left ( \textit{op} \; x \; e = x \land \textit{op} \; e \; x =x \right ) \; : \; *_p \end{gather*}$$
