Separate Compilation, Take Two, Compositionally

A couple weeks ago I wrote about what separate compilation means for the lambda calculus. To capture the observable behavior of the compilation units, I defined an abstract machine that produced a trace of the calls between them. The idea was that an optimizing compiler has free reign within a compilation unit, but that it must make and respond to the appropriate external function calls. I noted that while the abstract machine approach got the job done, it would be preferable to map directly from the syntax of the lambda calculus to a trace instead of indirectly via the abstract machine. Further, we would like to know what a a single compilation unit means in isolation, but the abstract machine only gives a semantics to whole programs.

A semantics that can give meaning to parts of a program is, roughly speaking, called a compositional semantics. A compositional semantics defines the meaning of each construct of the language in terms of the meaning of the sub-parts of the construct. For example, a conditional 'if' is defined in terms of the meaning of the conditional and the two branches. One of the main styles of semantics that is compositional is denotational semantics. Such a semantics maps from the syntax of the program to some mathematical constructs that specify the behavior of the program (typically a function from inputs to outputs). A big-step semantics also maps from syntax to mathematical constructs, but big-step semantics are often not compositional. For example, the meaning of a lambda term is not defined in terms of the meaning of its body. Instead, a big-step semantics maps a lambda term to a closure, which is still syntax. (For reference, see Big-step, diverging or stuck?.)

Here I'm going to give a denotational semantics for the separately compiled lambda calculus, mapping from the syntax of a compilation unit to a set of all possible execution traces.

Syntax

The following will serve as the syntax for the separately-compiled lambda calculus. The main addition is the notation $c.f$ for referring to functions in other compilation units. Also, each compilation unit consists of a function table that maps function names to lambdas and a whole program is a mapping from compilation unit names to function tables. $$\begin{array}{lrcl} \text{Variables} & x & \in & \mathsf{Var} \\ \text{Function Names} & f &\in & \mathsf{Var} \\ \text{Comp. Unit Names} & c &\in & \mathsf{Var} \\ \text{Integers} & n &\in &\mathbb{Z} \\ \text{Expressions} & e &::= &n \mid x \mid \lambda x.e \mid e(e) \mid c.f \\ \text{Function Tables} & F & ::= & \{ (f,\lambda x.e), \ldots \} \\ \text{Programs} & P & ::= & \{ (c,F),\ldots \} \end{array}$$

Traces

A trace is a sequence of actions. In our setting, actions are function calls or producing a result value. For a function call, we record the name of the function, the argument, and the return value. We'll need three kinds of values: integers, external functions, and functions. From within one compilation unit, we don't know what the external functions do, so we treat them symbolically. On the other hand, functions from within the current unit are known and we represent them directly in terms of their observable behavior, that is, as a mapping from values to a set of traces. $$\begin{array}{lrcl} \text{Values} & v \in \mathsf{Val} & ::= & n \mid c.f \mid \varphi \\ \text{Exports} & \chi \in \mathsf{Ex} & ::= & n \mid c.f \\ \text{Functions} & \varphi \in \mathsf{Fun}& = & \mathsf{Val} \to \mathsf{Beh} \\ \text{Actions} & a \in \mathsf{Act} & ::= & c.f(v){\to}v \mid \mathsf{val}(v) \\ \text{Traces} & \overline{a} \in \mathsf{Act}^{*} \\ \text{Behavior} & \beta \in \mathsf{Beh} & = & \mathcal{P}(\mathsf{Act}^{*}) \end{array}$$ The definitions of the sets $\mathsf{Val}$, $\mathsf{Fun}$, $\mathsf{Act}$, and $\mathsf{Beh}$ are mutually recursive. One doesn't do that with run-of-the-mill set theory. Here we must invoke the inverse limit construction to obtain sets that solve the above equations. Thanks Dana Scott! (If you want to read more about this, I recommend starting with Chapter 11 of David A. Schmidt's book on denotational semantics.)

We'll represent function tables with the following function maps, and programs with the following unit maps. $$\begin{array}{lrcl} \text{Function Maps} & \Phi \in \mathsf{FunMap} & = & \mathsf{Var} \to \mathsf{Fun} \\ \text{Unit Maps} & U \in \mathsf{UnitMap} & = & \mathsf{Var} \to \mathsf{FunMap} \end{array}$$

Preview of the Semantics

Before giving the general definition of the semantics, let's consider a couple examples. We'll write $\mathcal{M}(e,\rho)$ for the behavior (set of traces) of expression $e$ in environment $\rho$. (Environments map variables to values.)

First, let's consider the semantics of the identify function. It's behavior is captured by a single trace which consists of the single action of producing a function $\varphi_{\mathit{id}}$. Of course, this function maps every value to itself. $$\begin{align*} \varphi_{\mathit{id}} &= \{ (v, \{ \mathsf{val}(v)\}) \mid v \in \mathsf{Val} \} \\ \mathcal{M}(\lambda x. x,\emptyset) &= \{ \mathsf{val}(\varphi_{\mathit{id}}) \} \end{align*}$$

Next let's consider a call to an external function. We don't know anything about the other compilation units, so we'll include all possible return values as possible behavior. $$\mathcal{M}(c_1.g(41),\emptyset) = \{ c_1.g(41){\to}v\,\mathsf{val}(v) \mid v \in \mathsf{Val} \ \}$$ For example, we'll have $$\begin{align*} c_1.g(41){\to}42\;\mathsf{val}(42) & \in \mathcal{M}(c_1.g(41),\emptyset) \\ c_1.g(41){\to}\varphi_{\mathit{id}}\;\mathsf{val}(\varphi_{\mathit{id}}) & \in \mathcal{M}(c_1.g(41),\emptyset) \end{align*}$$

Semantics as Traces

The interesting part of the semantics is in function application. The result from $e_1$ may be either an external function or an internal function. The helper function $\mathcal{E}$ handles the external calls and $\mathcal{I}$ the internal calls. $$\begin{align*} \mathcal{M}(n,\rho) &= \{ \mathsf{val}(n) \} \\ \mathcal{M}(x,\rho) &= \{ \mathsf{val}(\rho(x)) \} \\ \mathcal{M}(c.f,\rho) &= \{ \mathsf{val}(c.f) \} \\ \mathcal{M}(\lambda x.e,\rho) &= \{ \mathsf{val}(\varphi) \} \\ \text{where } \varphi &= \{ (v, \mathcal{M}(e,\rho[x\mapsto v])) \mid v \in \mathsf{Val} \} \\ \mathcal{M}(e_1\,e_2,\rho) &= \text{let } \beta_1 = \mathcal{M}(e_1,\rho), \beta_2 = \mathcal{M}(e_2,\rho) \\ & \quad\;\, \text{in } \mathcal{I}(\beta_1, \beta_2) \cup \mathcal{E}(\beta_1, \beta_2) \end{align*}$$ where $$\begin{align*} \mathcal{I}(\beta_{\mathit{fun}},\beta_{\mathit{arg}}) & = \{ \overline{a}_1\overline{a}_2\overline{a}_3\,\mathsf{val}(v_r) \mid \overline{a}_1\,\mathsf{val}(\varphi) \in \beta_{\mathit{fun}} \land \overline{a}_2\,\mathsf{val}(v_a) \in \beta_{\mathit{arg}} \land \overline{a}_3\,\mathsf{val}(v_r) \in \varphi(v_a) \} \\ \mathcal{E}(\beta_{\mathit{fun}},\beta_{\mathit{arg}}) & = \{ \overline{a}_1\overline{a}_2 \overline{a}_3 \, (c.f(v){\to}v')\,\mathsf{val}(v') \mid \overline{a}_1\,\mathsf{val}(c.f) \in \beta_{\mathit{fun}} \land \overline{a}_2\,\mathsf{val}(v) \in \beta_{\mathit{arg}} \} \end{align*}$$ We can now define the meaning of a compilation unit, that is, the meaning of a function table, as follows. $$\begin{align*} \mathcal{M}(F,c) &= \{ (f,\varphi) \mid (f,\lambda x.e) \in F\} \\ \text{where } \varphi & = \{ (v,\mathcal{M}(e,\emptyset[x\mapsto v])) \mid v \in \mathsf{Val} \} \end{align*}$$

Meaning of Whole Programs via Composition

That was the main event, but let's go a bit further and see how we can give the meaning of a program in terms of the meanings of the compilation units. To do this, we need a way of filtering out traces that include calls to external functions that couldn't happen, that is, calls whose argument and return values don't match what you'd actually get from the given function in the other compilation unit. To do this, we'll need to pass values back and forth between units. If the values are just numbers, this is easy, but for functions things are a bit more complex because we need to convert back and forth from the symbolic (hidden) representation of a function to the value to behavior mapping. First, we define a reg function for registering a function under a fresh name. $$\begin{align*} \mathit{reg}(n,c,U) &= (n,U) \\ \mathit{reg}(c'.f,c,U) &= (c'.f,U) \\ \mathit{reg}(\varphi,c,U) &= (c.f, U[c \mapsto U(c)[f \mapsto \varphi]] & f \notin \mathrm{dom}(U(c)) \end{align*}$$ We also need a way to convert from a symbolic function back to the value to behavior mapping, which we accomplish with the following up-arrow function. $$\begin{align*} n\uparrow^c_U &= n \\ c'.f\uparrow^c_U &= \begin{cases} U(c)(f) & \text{if } c' = c \\ c'.f & \text{otherwise} \end{cases} \end{align*}$$ We now define the following predicates on actions and sequences of actions. $$\begin{gather*} \frac{ \begin{array}{c} \mathit{reg}(v_1,c,U_1) = (\chi,U_2) \qquad \chi\uparrow^{c'}_{U_2} = v_2 \\ \overline{a}\,\mathsf{val}\,v_3 \in U_2(c')(f)(v_2) \qquad c'; U_2 \vdash \overline{a} \Rightarrow U_3 \\ \mathit{reg}(v_3,c', U_3) = (\chi',U_4) \qquad \chi'\uparrow^{c}_{U_4} = v_4 \end{array} }{ c ; U_1 \vdash c'.f(v_1){\to}v_4 \Rightarrow U_4 } \\[2ex] \frac{ }{ c; U \vdash \epsilon \Rightarrow U } \qquad \frac{ c;U_1 \vdash a \Rightarrow U_2 \quad c;U_2 \vdash \overline{a} \Rightarrow U_3 }{ c;U_1 \vdash a \overline{a} \Rightarrow U_3 } \end{gather*}$$ Next we define a filter that takes a behavior (set of traces) and keeps only those traces that can really happen. $$\begin{align*} \mathsf{filter}(\beta,c,U) &= \{ \mathsf{val}(v') \mid \overline{a}\,\mathsf{val}(v') \in \beta \land c;U \vdash \overline{a} \Rightarrow U' \} \end{align*}$$ Filtering extends naturally to functions and unit maps. $$\begin{align*} \mathsf{filter}(\varphi,c,U) &= \{ (v, \mathsf{filter}(\varphi(v), c, U)) \mid v \in \mathsf{Val} \} \\ \mathsf{filter}(\Phi,c,U) &= \{ (f,\mathsf{filter}(\varphi,c,U)) \mid (f,\varphi) \in \Phi \} \end{align*}$$

With filtering in place, we are now ready to give the meaning of a whole program in terms of the meaning of each compilation unit. $$\mathcal{M}( P ) = \Phi_1(\mathsf{main})$$ where $$\begin{align*} P &= \{ (c_1,F_1), \ldots, (c_n,F_n) \} \\ U &= \{ (c_1,\mathcal{M}(F_1,c_1)), \ldots, (c_n,\mathcal{M}(F_n,c_n))\} \\ \Phi_1 &= \mathsf{filter}(\mathcal{M}(F_1,c_1),c_1,U) \end{align*}$$

Critique

I'm not completely happy with the above semantics. The reason is that the behavior of an expression includes receiving internal functions that it never created. Hopefully I'll read about or discover a solution to this!