# What is a 'free model'?

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?).

• 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). – Kaveh Apr 23 '18 at 23:01
• if you have an equational theory (no relation symbols), its free model is essentially the free algebra. – Kaveh Apr 23 '18 at 23:03
• 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) – user Apr 24 '18 at 0:09
• 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. – Kaveh Apr 24 '18 at 0:17
• 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) – user Apr 24 '18 at 0:43

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}{\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.

• 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? – user Apr 27 '18 at 0:59
• I do not understand your question. The model $\overline{X+E}$ from the paper is the model $C$ in my answer. – Andrej Bauer Apr 27 '18 at 12:21
• 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? – user Apr 28 '18 at 7:10
• I supplememented the answer. I also think this question is more appropriate for cs.stackexchange.com. – Andrej Bauer Apr 28 '18 at 8:11
• I don’t feel strongly, or else I would not have answered. – Andrej Bauer Apr 28 '18 at 17:01