Compositional Separate Compilation, Take Three

In the post Separate Compilation, Take Two, Compositionally, I tried to write down a trace-based semantics for the lambda calculus that was compositional, that is, a semantics that could tell us the meaning of an individual compilation unit. The result was a semantics that wasn't quite right. A call to an external function could return a function masquerading as an internal function but that was never created by the compilation unit. Here I solve the problem in a fairly straightforward way, by threading an internal function map through the semantics.

Syntax

The syntax is the same as before: $$\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{Func. Tables} & F & ::= & \{ (f,\lambda x.e), \ldots \} \\ \text{Programs} & P & ::= & \{ (c,F),\ldots \} \end{array}$$

Traces

We make a few changes to the definition of traces and behavior. Our representation of a function now has an extra parameter for the internal function map. We only have one kind of action, the function-call action, whose argument and result are now required to be exportables. A function map is just a map from function names to functions. Behavior is now a set of 3-tuples, whose parts include the trace, result value, and updated internal function map. $$\begin{array}{lrcl} \text{Values} & v \in \mathsf{Val} & ::= & n \mid c.f \mid \varphi \\ \text{Exportables} & \chi \in \mathsf{Ex} & ::= & n \mid c.f \\ \text{Functions} & \varphi \in \mathsf{Fun}& = & \mathsf{Val} \times \mathsf{FunMap} \to \mathsf{Beh} \\ \text{Actions} & a \in \mathsf{Act} & ::= & c.f(\chi){\to}\chi \\ \text{Trace} & \overline{a} \in \mathsf{Act}^{*} \\ \text{Function Maps} & \Phi \in \mathsf{FunMap} & = & \mathsf{Var} \to \mathsf{Fun} \\ \text{Behavior} & \beta \in \mathsf{Beh} & = & \mathcal{P}(\mathsf{Act}^{*} \times \mathsf{Val} \times \mathsf{FunMap}) \end{array}$$

Trace Semantics

To handle external function calls, we'll need to be able to convert from values to exportables and back again. If the value being exported is a function, we need to create a new name for it and add it to the internal function map. On the way back, if the function reference is to an internal function, we need to look it up in the internal function map. The $\mathit{export}$ and $\mathit{import}$ functions handle this logic. Both of these functions act like the identify function on integers and external functions. $$\begin{align*} \mathit{export}(n,c,\Phi) &= (n,\Phi) \\ \mathit{export}(\varphi,c,\Phi) &= (c.f,\Phi[f \mapsto \varphi]) & f \notin \mathrm{dom}(\Phi) \\ \mathit{export}(c'.f,c,\Phi) & = (c'.f,\Phi) \end{align*}$$ $$\begin{align*} \mathit{import}(n,c,\Phi) &= n \\ \mathit{import}(c'.f,c,\Phi) &= \begin{cases} \Phi(f) & \text{if } c = c' \\ c'.f \end{cases} \end{align*}$$ The meaning function for expressions now takes two more parameters, the name of the current compilation unit and the internal function map. As before, the result is the behavior of the expression. $$\begin{align*} \mathcal{M}(n,\rho, c, \Phi) &= \{ (\epsilon,n,\Phi) \} \\ \mathcal{M}(x,\rho,c,\Phi) &= \{ (\epsilon,\rho(x),\Phi) \} \\ \mathcal{M}(c.f,\rho,c,\Phi) &= \{ (\epsilon,c.f,\Phi) \} \\ \mathcal{M}(\lambda x.e,\rho,c,\Phi) &= \{ (\epsilon, \varphi, \Phi) \} \\ \text{where } \varphi & = \{ ((v, \Phi'), \mathcal{M}(e,\rho[x\mapsto v],c,\Phi'))\\ & \qquad \mid v \in \mathsf{Val} \land \Phi' \in \mathsf{FunMap} \} \\ \mathcal{M}(e_1\,e_2,\rho,c,\Phi) &= \{ (\overline{a}, v', \Phi') \mid (\overline{a}_1,v_1,\Phi_1) \in \mathcal{M}(e_1,\rho,c,\Phi) \\ & \qquad \land (\overline{a}_2,v_2,\Phi_2) \in \mathcal{M}(e_2,\rho,c,\Phi_1) \\ & \qquad \land (\mathcal{I}(\overline{a}_1,v_1,\overline{a}_2,v_2,c,\Phi_2,\overline{a},v',\Phi') \\ & \qquad\quad \lor \mathcal{E}(\overline{a}_1,v_1,\overline{a}_2,v_2,c,\Phi_2,\overline{a},v',\Phi')) \} \end{align*}$$ where $\mathcal{I}$ handles calls to internal functions $$\begin{align*} & \mathcal{I}(\overline{a}_1,v_1,\overline{a}_2,v_2,c,\Phi_2,\overline{a},v',\Phi') = \\ & \qquad \exists \varphi \overline{a}_3.\, (\varphi = v_1 \lor (\exists f.\, c.f = v_1 \land \varphi = \Phi_2(f))) \\ & \qquad \qquad \land (\overline{a_3}, v', \Phi') \in \varphi(v_2,\Phi_2) \land \overline{a} = \overline{a}_1\overline{a}_2\overline{a}_3 \end{align*}$$ and $\mathcal{E}$ handles calls to external functions $$\begin{align*} & \mathcal{E}(\overline{a}_1,v_1,\overline{a}_2,v_2,c,\Phi_2,\overline{a},v',\Phi') = \\ & \qquad \exists c' f \chi \chi'.\, v_1 = c'.f \land c \neq c' \\ & \qquad \land \mathit{export}(v_2,c,\Phi_2) = (\chi,\Phi') \land \mathit{import}(\chi',c,\Phi_2) = v' \\ & \qquad \land \overline{a} = \overline{a}_1\overline{a}_2\,(c'.f(\chi){\to}\chi') \end{align*}$$ To wrap things up, we define the meaning of a compilation unit as follows, with the internal function map not part of the observable behavior. $$\begin{align*} \mathcal{M}(c,F) &= \{ (f, \psi) \mid (f,\lambda x.e) \in F\} \\ \text{where } &\psi = \{ (\chi, (\overline{a}, \chi')) \mid \chi \in \mathsf{Ex} \land (\overline{a},v,\Phi) \in \mathcal{M}(e,\emptyset[x\mapsto \chi],c,\emptyset) \\ & \qquad \land \mathit{export}(v,c,\Phi) = (\chi',\Phi') \} \end{align*}$$