Algebrajski učinki

Algebrajski učinki#

Težave z monadami#

Monade elegantno opisujejo denotacijsko semantiko učinkov, vendar imajo nekaj pomanjkljivosti:

  • Sama monada opisuje le semantiko tipov ter enoto in veriženje, izpusti pa specifične operacije, ki jih potrebujemo za opis učinkov (npr. get, set, raise, try, choose). Vsako izmed njih moramo podati naknadno.

  • Iz istega razloga težko podamo splošno operacijsko semantiko.

  • Monade se poleg tega težko kombinirajo: če sta \(T_1, T_2 : \mathbf{Set} \to \mathbf{Set}\) monadi, njuna kompozicija \(T_1 \circ T_2\) na splošno ni monada. Enoto se sicer da sestaviti:

    \[\eta^{T_1 \circ T_2}_X : X \to T_1(T_2 X), \qquad \eta^{T_1 \circ T_2}_X(x) = \eta^{T_1}_{T_2 X}\bigl(\eta^{T_2}_X(x)\bigr)\]

    Težava nastopi pri veriženju, kar je lažje videti pri ekvivalentni predstavitvi z množenjem \(\mu_X : TTX \to TX\): iz \(\mu^{T_1}\) in \(\mu^{T_2}\) dobimo preslikavo \(T_1(T_1(T_2(T_2 X))) \to T_1(T_2 X)\), potrebovali pa bi pa \(T_1(T_2(T_1(T_2 X))) \to T_1(T_2 X)\).

Zato se osredotočimo na manjkajoči opis specifičnih operacij. S študijem operacij se ukvarja področje algebrajskih teorij, ki v splošnosti preiskuje strukture, kot so polgrupe, grupe, kolobarji, …

Signature in algebrajske teorije#

Def. Signatura \(\Sigma\) za algebrajsko teorijo je seznam operacij in njihovih členosti (= arity):

\[\Sigma = \op_1 : n_1,\ \dots,\ \op_k : n_k\]

Primer. \(\Sigma_{\text{grupa}} = \{\underbrace{m : 2}_{\text{množenje}},\ \underbrace{i : 1}_{\text{inverz}},\ \underbrace{e : 0}_{\text{enota}}\}\)

Iz spremenljivk in operacij iz \(\Sigma\) sestavljamo izraze, npr. \(m(i(x), m(m(y, e()), z))\). Formalno jih definiramo induktivno. Za kontekst \(\Gamma = x_1, \dots, x_n\) uvedemo sodbe \(\Gamma \vdash_\Sigma t\) s pravili:

\[ \infer{ x \in \Gamma }{ \Gamma \vdash_\Sigma x } \qquad \infer{ \op : n \in \Sigma \quad (\Gamma \vdash_\Sigma t_i)_{i=1}^n }{ \Gamma \vdash_\Sigma \op(t_1, \dots, t_n) } \]

Def. Algebrajska teorija nad signaturo \(\Sigma\) je množica enačb med izrazi.

Primer. Teorija za grupe:

\[\begin{split} \begin{align*} x, y, z \vdash m(x, m(y, z)) &= m(m(x, y), z) \\ x \vdash m(x, e()) &= x \\ x \vdash m(e(), x) &= x \\ x \vdash m(x, i(x)) &= e() \\ x \vdash m(i(x), x) &= e() \end{align*} \end{split}\]

Primer. Teorija za polmreže, kjer vzamemo signaturo \(\Sigma = \{\vee : 2\}\):

\[\begin{split} \begin{align*} x \vee (y \vee z) &= (x \vee y) \vee z \\ x \vee y &= y \vee x \\ x \vee x &= x \end{align*} \end{split}\]

Neprimer. Obsegi: ker je inverz za množenje definiran samo na neničelnih elementih. Kmalu bomo tudi dokazali, da ne obstaja nobena teorija, ki bi opisovala obsege.

Interpretacije in modeli#

Def. Interpretacija signature \(\Sigma\) je množica \(X\) skupaj s funkcijo \(\op_X : X^{n} \to X\) za vsak \((\op : n) \in \Sigma\).

Interpretacija nam omogoča interpretirati vsak izraz \(x_1, \dots, x_n \vdash t\) s preslikavo \(\itp{t} : X^n \to X\), definirano kot:

\[\begin{split} \begin{align*} \itp{x_1, \dots, x_n \vdash x_i}(a_1, \dots, a_n) &= a_i \\ \itp{\op(t_1, \dots, t_n)} &= \op_X(\itp{t_1}, \dots, \itp{t_n}) \end{align*} \end{split}\]

Def. Model algebrajske teorije \(M\) je taka interpretacija njene signature \(\Sigma\), ki zadošča vsem enačbam, torej: \(\itp{t} = \itp{t'}\) za vsako enačbo \(t = t'\) v teoriji.

Primer. Vsaka grupa \(G\) je model teorije za grupe.

Trditev. Za poljubna modela \((X, (\op_X)_{\op \in \Sigma})\) in \((Y, (\op_Y)_{\op \in \Sigma})\) lahko definiramo model na \(X \times Y\), pri čemer operacijo \((\op : n) \in \Sigma\) interpretiramo kot:

\[ \op_{X \times Y}((x_1, y_1), \dots, (x_n, y_n)) = (\op_X(x_1, \dots, x_n),\ \op_Y(y_1, \dots, y_n)) \]

Posledica tega je, da ne obstaja algebrajska teorija za obsege, saj bi za poljubna obsega \(X\) in \(Y\) dobili obseg \(X \times Y\), ki pa ni obseg, saj je \((1, 0) \cdot (0, 1) = (0, 0)\), torej imamo delitelje niča.

Def. Homomorfizem med modeloma \(X\) in \(Y\) je taka preslikava \(h : X \to Y\), da za vsako operacijo \((\op : n) \in \Sigma\) velja

\[ h\bigl(\op(a_1, \dots, a_n)) = \op(h(a_1), \dots, h(a_m)) \]
Contents