5
$\begingroup$

I was reading this paper on effect handlers and got hung up on the phrase 'free model'.

In context:

[...] From an algebraic point of view, the $x_e$ provide a model for the theory of exceptions on $X + E$, interpreting each operation $raise_e$ by $x_e$. If we write $X + E$ for the free model and $\overline{X + E}$ for the new model on the same carrier set, we see from the above two equations that [...]

I want to reach for something being freely generated from something else, but I'm not sure what (e.g. right after the comment about $x_e$ providing some other model, where're the parts of the 'free model' coming from?).

$\endgroup$
  • $\begingroup$ in logic free model is the syntatic model generated by talking equivalence classes of provably equal terms of the language. The name comes from algebra (free algebra). $\endgroup$ – Kaveh Apr 23 '18 at 23:01
  • $\begingroup$ if you have an equational theory (no relation symbols), its free model is essentially the free algebra. $\endgroup$ – Kaveh Apr 23 '18 at 23:03
  • $\begingroup$ So the free model is just... the syntax? If I take definition 6 from here and make A in the definition be the set of all terms, then interpret every term as itself, is that the free model? (I'm missing something here; I don't see how equivalence classes fit in) $\endgroup$ – user Apr 24 '18 at 0:09
  • $\begingroup$ you have to take the equivalence classes for terms rather than terms themselves: [[t]] in the universe of the model represents not just term t but all terms s which T proves they are equal to t. $\endgroup$ – Kaveh Apr 24 '18 at 0:17
  • $\begingroup$ Do I have to take the interpretation function's domain as being the set of terms (so $Interpret(t) = [[t]]$ trivially) rather than the set of function/constant/relation symbols to define a free model (and thus making definition 6 here not useful)? Or is there some sort of property that guarantees I can always define the interpretation function over those symbols instead of over whole terms? Or... something else? (I feel that I might be getting mixed up between disciplines) $\endgroup$ – user Apr 24 '18 at 0:43
5
$\begingroup$

Consider a set $E$. The theory of $E$-exceptions is an algebraic theory given by:

  • for every $e \in E$ a nullary operation symbol $\mathsf{raise}_e$
  • no equations.

Given a set $X$, we may consider the free algebra $A$ for the theory of $E$-exceptions, with generators from $X$. The algebra $A$ contains everything that we can generate from the generators and the operation symbols. Since our operation symbols are nullary (do not take any arguments), $A$ will contain precisely the generators $X$ and, for each $e \in E$, the operation symbol $\mathsf{raise}_e$. (There are no equations, so we need not quotient at all.) It is not surprising that we would write "$X + E$" for $A$.

In general, an algebra for the theory of $E$-exceptions is given by:

  • a carrier set $C$
  • for every $e \in E$, an element $r_e \in C$ which interprets the nullary operation $\mathsf{raise}_e$.

A particulary strange way to create an algebra is to take $$C = X + E$$ and for each $e \in E$ an element $x_e \in C$. This seems strange only untilwe notice that such an algebra is precisely the same thing as an exception handler. Think of $C$ as the set of "computations" that may either return a "final result" from $X$, or raise an exception from $E$. An exception handler takes an element $c \in C$ and explains how to replace each exception $\mathsf{raise}_e$ with another computation $x_e \in C$ (note: an exception handler may re-raise exceptions, which is why $x_e \in C$ instead of just $x_e \in X$).


$\newcommand{\raise}[1]{\mathsf{raise}_{#1}}$

Supplemental: Perhaps a concrete example will help. A model is given by a set $C$ and a mapping of the constant symbols $\raise{e}$ to elements of $C$.

Let us take $E = \{a,b\}$ and $X = \{u, v, w\}$. Then the free model is given by the carrier $$X + E = \{u, v, w, \raise{a}, \raise{b}\}$$ together with the mapping $$\raise{a} \mapsto \raise{a}, \quad \raise{b} \mapsto \raise{b}.$$

The model $\overline{X + E}$ is not fixed, it depends on the mapping $x : E \to X + E$. For example, if we take $x_a = u$ and $x_b = \raise{a}$ then we get the model $\overline{X + E}$ whose carrier is $X + E$ and $$\raise{a} \mapsto u, \quad \raise{b} \mapsto \raise{a}.$$ Another possibility for $\overline{X + E}$ is to take $x(a) = \raise{b}$ and $(b) = \raise{a}$. This will not be the same as the free model because it exchanges the meaning of $\raise{a}$ and $\raise{b}$. If we take $x(a) = \raise{a}$ and $x(b) = \raise{b}$ then $\overline{X + E}$ is equal to the free model.

$\endgroup$
  • $\begingroup$ I'm confused. I was under the impression that what you're describing was the model $\overline{X + E}$ (what with interpreting $raise_e$ as $x_e$), rather than the 'free model', whatever that is. Is this the wrong impression? $\endgroup$ – user Apr 27 '18 at 0:59
  • $\begingroup$ I do not understand your question. The model $\overline{X+E}$ from the paper is the model $C$ in my answer. $\endgroup$ – Andrej Bauer Apr 27 '18 at 12:21
  • $\begingroup$ I was under the impression that the 'free model', which I am asking for, was not the same as $\overline{X+E}$ (specifically since the authors appear to make a statement contrasting the 'free model' with $\overline{X+E}$). Are they the same? $\endgroup$ – user Apr 28 '18 at 7:10
  • $\begingroup$ I supplememented the answer. I also think this question is more appropriate for cs.stackexchange.com. $\endgroup$ – Andrej Bauer Apr 28 '18 at 8:11
  • 1
    $\begingroup$ I don’t feel strongly, or else I would not have answered. $\endgroup$ – Andrej Bauer Apr 28 '18 at 17:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.