<p>Consider a set $E$. The <em>theory of $E$-exceptions</em> is an algebraic theory given by:</p>

<ul>
<li>for every $e \in E$ a nullary operation symbol $\mathsf{raise}_e$</li>
<li>no equations.</li>
</ul>

<p>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$.</p>

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

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

<p>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 <em>re-raise</em> exceptions, which is why $x_e \in C$ instead of just $x_e \in X$).</p>

<hr>

<p>$\newcommand{\raise}[1]{\mathsf{raise}_{#1}}$</p>

<p><strong>Supplemental:</strong> 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$.</p>

<p>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}.$$</p>

<p>The model $\overline{X + E}$ is <em>not</em> 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 <em>not</em> 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}$ <em>is</em> equal to the free model.</p>

CC BY-SA 3.0
2018-04-27T00:59:16.610Z
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
CC BY-SA 3.0
2018-04-27T12:21:42.850Z
I do not understand your question. The model $\overline{X+E}$ from the paper is the model $C$ in my answer.
Andrej Bauer
CC BY-SA 3.0
2018-04-28T07:10:50.053Z
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
CC BY-SA 3.0
2018-04-28T08:11:35.200Z
I supplememented the answer. I also think this question is more appropriate for cs.stackexchange.com.
Andrej Bauer
CC BY-SA 3.0
2018-04-28T16:10:03.857Z
I don't know how movement between sites is handled; if you feel it is strongly justified (I'm not sure why but that's not my place), please feel free. The additional information more directly addresses my question, and aligns (I think) with the comment discussion under it. Thanks!
user
CC BY-SA 3.0
2018-04-28T17:01:19.863Z
I don’t feel strongly, or else I would not have answered.
Andrej Bauer
CC BY-SA 3.0
2018-04-26T22:20:16.560Z
2018-04-28T08:10:50.757Z
2018-04-28T08:10:50.757Z
Andrej Bauer
<p>I was reading <a href="http://homepages.inf.ed.ac.uk/gdp/publications/Effect_Handlers.pdf" rel="noreferrer">this paper on effect handlers</a> and got hung up on the phrase 'free model'.</p>

<p>In context:</p>

<blockquote>
  <blockquote>
    <blockquote>
      <p>[...] 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 [...]</p>
    </blockquote>
  </blockquote>
</blockquote>

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

CC BY-SA 3.0
2018-04-23T23:01:01.363Z
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
CC BY-SA 3.0
2018-04-23T23:03:52.720Z
if you have an equational theory (no relation symbols), its free model is essentially the free algebra.
Kaveh
CC BY-SA 3.0
2018-04-24T00:09:42.640Z
So the free model is just... the syntax? If I take definition 6 from [here](http://www.math.toronto.edu/weiss/model_theory.pdf) 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
CC BY-SA 3.0
2018-04-24T00:17:35.447Z
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
CC BY-SA 3.0
2018-04-24T00:43:54.373Z
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](http://www.math.toronto.edu/weiss/model_theory.pdf) 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
CC BY-SA 3.0
2018-04-24T01:38:48.910Z
you can extended the interpretation to functions, ... symbols as well: Interpretation(f([[t0]],...,[[tn]])) = Interpretation([[f(t0,...tn)]]). An example would help I think. Think of language of 0,1,+,-,= and usual arithmetic laws. The universe would be integers, e.g. 2 would be the equivalence class containing terms 0+1+1, 0+0+1+1, 1+0+1, 0+1+1+(-1)+1, ...; for any term t in 2 and s in 3, t+s is provably equal to term 1+1+1+1+1 which is in equivalence class 5; ...
Kaveh
CC BY-SA 3.0
2018-04-24T01:59:36.650Z
Oh. Duh, yeah my brain turned off there for a sec. Thanks!
user
<semantics>
What is a 'free model'?
user
# What is a 'free model'?

(Asked by: username_0 on 2018-04-23)

I was reading [this paper on effect handlers](http://homepages.inf.ed.ac.uk/gdp/publications/Effect_Handlers.pdf) 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?).

**Tags:** semantics

> **Comments:**
> **username_1**: 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).  
> **username_1**: if you have an equational theory (no relation symbols), its free model is essentially the free algebra.  
> **username_0**: So the free model is just... the syntax? If I take definition 6 from [here](http://www.math.toronto.edu/weiss/model_theory.pdf) 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)  
> **username_1**: 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.  
> **username_0**: 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](http://www.math.toronto.edu/weiss/model_theory.pdf) 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)  
> **username_1**: you can extended the interpretation to functions, ... symbols as well: Interpretation(f([[t0]],...,[[tn]])) = Interpretation([[f(t0,...tn)]]). An example would help I think. Think of language of 0,1,+,-,= and usual arithmetic laws. The universe would be integers, e.g. 2 would be the equivalence class containing terms 0+1+1, 0+0+1+1, 1+0+1, 0+1+1+(-1)+1, ...; for any term t in 2 and s in 3, t+s is provably equal to term 1+1+1+1+1 which is in equivalence class 5; ...  
> **username_0**: Oh. Duh, yeah my brain turned off there for a sec. Thanks!  

---

## 1 answers

### Answer by username_2 on 2018-04-26. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: I do not understand your question. The model $\overline{X+E}$ from the paper is the model $C$ in my answer.  
> **username_0**: 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?  
> **username_2**: I supplememented the answer. I also think this question is more appropriate for cs.stackexchange.com.  
> **username_0**: I don't know how movement between sites is handled; if you feel it is strongly justified (I'm not sure why but that's not my place), please feel free. The additional information more directly addresses my question, and aligns (I think) with the comment discussion under it. Thanks!  
> **username_2**: I don’t feel strongly, or else I would not have answered.  

---

