Linking isn't substitution: the separately-compiled lambda calculus

I've been reading some papers on separate compilation, such as Cardelli's Program fragments, linking, and modularization, and I'm seeing a trend in using substitution to model the linking of compilation units (units for short). While substitution does a fine job of conveying the semantics of the final executable, I think it falls down in conveying the semantics of a unit, especially from the point of view of a compiler writer.

What I'm interested in here is the situation in which one or more compilers are used to compile several units, and then these units are linked together into an executable. We want to allow the compilers to perform aggressive optimizations within a unit, while still requiring the compilers to respect the application binary interface (ABI), which says how different units must talk to each other.

To take a stab at such a semantics, let's consider a variant of the lambda calculus that supports separate compilation. Each compilation unit will have a name c and a function table $\varphi$, which maps function names to lambdas. At run-time, each compilation unit will also need a stack $\kappa$ to store it's part of the procedure call stack. In addition to the usual expressions of the lambda calculus, we'll allow references to functions in other compilation units: the expression c.f refers to the function named f in unit c. Now, we want the observable behavior to be function calls and returns that cross from one unit to another. One way to specify this behavior is to create an abstract machine that logs the crossings (producing a trace). It would be preferable to map directly from a program to the trace, but I'm better at thinking in terms of abstract machines. Thus, the approach I'm using here is similar to that of the paper Java Jr.: Fully abstract trace semantics for a core Java language by Jeffrey and Rathke, which addresses the same problem that we're concerned with here, but for a subset of Java. More generally, the use of transition systems to generate traces goes back at least as far as A Theory of Communicating Sequential Processes by Brookes, Hoare, and Roscoe.

The lambda calculus includes first-class functions, so we need to address the question: what happens when a lambda is passed from one compilation unit to another? Drawing inspiration from the paper Temporal higher-order contracts, we don't literally pass lambdas, but instead the originating unit must give the lambda a name and then pass a reference to the lambda. We'll let $\chi$ range over the exportable values. $$\begin{array}{rcl} n &\in & \mathbb{Z} \\ v & ::= & n \mid \lambda x.e \mid c{.}f \\ \chi &::= & n \mid c{.}f \end{array}$$

The state of the machine is the actively executing expression e, the current compilation unit c, the previous compilation unit $c'$ (that called the current one), and the unit table U (mapping unit names to units). $$\langle e, c, c', U \rangle$$ We write $\varphi_c$ for accessing the function table of unit c from inside U and we write $\kappa_c$ for accessing it's stack. To allow internal computation within a unit, we define the following transition which single-steps the active expression according to reduction rules of the lambda calculus. $$\begin{align*} & \langle e, c, c' , U \rangle \\ \longmapsto\; & \langle e', c, c' , U \rangle \qquad \text{if } e \longrightarrow e' \qquad \text{(Red)} \end{align*}$$ A call to an external function looks up the function in the target unit $c'$, installs the function body as the active expression, and records the continuation (evaluation context) $E$ and the previous unit $c''$ on the stack of the caller unit. The annotation on top of the $\longmapsto$ is how we log that an observable action occurred. $$\begin{align*} & \langle E[c'{.}f(\chi)], c, c'' , U\rangle \\ \overset{c'{.}f(\chi)}{\longmapsto} \; & \langle [x:=\chi]e, c', c , U[c:=((E,c'') \cdot \kappa_c, \varphi_c)] \rangle \qquad \text{(Call)} \\ & \qquad \text{if } c \neq c' \text{ and } \varphi_{c'}(f) = \lambda x.e \end{align*}$$ We also need to deal with the case where an internal function has been passed to another unit and then passed back. A call to such a function should not be observable. Thus, we have the following transition rule to convert from a reference to a function back to a lambda expression. $$\begin{align*} & \langle E[c{.}f(v)], c, c' , U\rangle \\ \longmapsto \; & \langle E[(\lambda x.e) \, v], c, c' , U\rangle \qquad \text{(InFun)} \\ & \qquad \text{if } \varphi_{c}(f) = \lambda x.e \end{align*}$$ When the active expression has been reduced to an exportable value, it's time to return to the caller $c'$. We pop the activation record $(E,c'')$ from the top of the caller's stack and install $E[\chi]$ as the active expression. $$\begin{align*} &\langle \chi,c,c', U \rangle \\ \overset{\chi}{\longmapsto} \;& \langle E[\chi], c', c'', U[c' := (\kappa',\varphi_{c'})] \rangle \qquad \text{(Ret)} \\ &\qquad \text{if } \kappa_{c'} = (E,c'') \cdot \kappa' \end{align*}$$ The following transition rule converts a lambda into a reference that is suitable for export by registering it in the function table. $$\begin{align*} &\langle R_c[\lambda x.e],c,c' , U \rangle \\ \longmapsto\;& \langle R_c[c{.}f], c, c' , U[c:= (\kappa_c, \varphi_c[f{:=} \lambda x.e]) ] \rangle \qquad \text{(Reg)} \\ &\qquad \text{if } f \notin \mathrm{dom}(\varphi_c) \end{align*}$$ where the $R_c$ context is defined as follows $$R_c ::= \Box \mid E[c'{.}f(\Box)] \qquad c \neq c'$$ So this rule converts lambdas to references when they need to be returned to another unit or when they are to be passed as an argument to another unit.

We can now define the semantics, the eval function, for the separately-compiled lambda calculus. Let s be an initial state (all the stacks are empty, the current unit is I (for initial), which represents the operating system, and the active expression is a call to the main function in the first unit with argument 42). $$\mathit{eval}(s) = \begin{cases} \overline{a} & \text{if } s \overset{\overline{a}}{\longmapsto^{*}} \langle \chi, I, I, U' \rangle \\ \bot & \text{otherwise} \end{cases}$$

Exercise: Write down the machine transitions for the following initial state. $$\begin{align*} s_0 &= \langle A{.}\mathit{main}(42), I, I, \\ &\qquad \{ I \mapsto (\epsilon,\emptyset), \\ &\qquad\; A \mapsto (\epsilon,\{ \mathit{main} \mapsto \lambda x. B{.}f(\lambda y. y) \}),\\ &\qquad\; B \mapsto (\epsilon, \{ f \mapsto \lambda h. h(3) \}) \} \rangle \end{align*}$$ Then compute the result of $\mathit{eval}(s_0)$. It should be $$A{.}main(42), B{.}f(A{.}g), A{.}g(3), 3, 3, 3$$ (Up to your choice of name for the lambda passed to $B{.}f$. Here we've named it $g$.)

The take-away for the compiler writer is that they can compile a unit any way they want, so long as the log comes out as specified by eval.