13 |
13 |
14 We illustrate these basic concepts by the following formulation of |
14 We illustrate these basic concepts by the following formulation of |
15 semigroups.% |
15 semigroups.% |
16 \end{isamarkuptext}% |
16 \end{isamarkuptext}% |
17 \isacommand{consts}\isanewline |
17 \isacommand{consts}\isanewline |
18 \ \ times\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline |
18 \ \ times\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline |
19 \isacommand{axclass}\isanewline |
19 \isacommand{axclass}\isanewline |
20 \ \ semigroup\ <\ {"}term{"}\isanewline |
20 \ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
21 \ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}% |
21 \ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}% |
22 \begin{isamarkuptext}% |
22 \begin{isamarkuptext}% |
23 \noindent Above we have first declared a polymorphic constant $\TIMES |
23 \noindent Above we have first declared a polymorphic constant $\TIMES |
24 :: \alpha \To \alpha \To \alpha$ and then defined the class |
24 :: \alpha \To \alpha \To \alpha$ and then defined the class |
25 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau |
25 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau |
26 \To \tau$ is indeed an associative operator. The $assoc$ axiom |
26 \To \tau$ is indeed an associative operator. The $assoc$ axiom |
35 Below, class $plus_semigroup$ represents semigroups of the form |
35 Below, class $plus_semigroup$ represents semigroups of the form |
36 $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond |
36 $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond |
37 to semigroups $(\tau, \TIMES^\tau)$.% |
37 to semigroups $(\tau, \TIMES^\tau)$.% |
38 \end{isamarkuptext}% |
38 \end{isamarkuptext}% |
39 \isacommand{consts}\isanewline |
39 \isacommand{consts}\isanewline |
40 \ \ plus\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOplus}{"}\ 70)\isanewline |
40 \ \ plus\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOplus}{\isachardoublequote}\ 70{\isacharparenright}\isanewline |
41 \isacommand{axclass}\isanewline |
41 \isacommand{axclass}\isanewline |
42 \ \ plus\_semigroup\ <\ {"}term{"}\isanewline |
42 \ \ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
43 \ \ assoc:\ {"}(x\ {\isasymOplus}\ y)\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ (y\ {\isasymOplus}\ z){"}% |
43 \ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}% |
44 \begin{isamarkuptext}% |
44 \begin{isamarkuptext}% |
45 \noindent Even if classes $plus_semigroup$ and $semigroup$ both |
45 \noindent Even if classes $plus_semigroup$ and $semigroup$ both |
46 represent semigroups in a sense, they are certainly not quite the |
46 represent semigroups in a sense, they are certainly not quite the |
47 same.% |
47 same.% |
48 \end{isamarkuptext}% |
48 \end{isamarkuptext}% |