Take 2: Graph of Tables for the Denotational Semantics of the Lambda Calculus

In the previous post, the denotational semantics I gave for the lambda calculus could not deal with self application, such as the program

$$(\lambda f. f\;f)\;(\lambda g. 42)$$ whose result should be $42$. The problem was that I defined function values to be tables of pairs of values, using a datatype definition, which rules out the possibility of cycles. In the above program, the table for $\lambda g. 42$ needs to include itself so that the application $f \; f$ makes sense.

A straightforward way to solve this problem is to allow cycles by representing all the functions created by the program as a graph of tables. A function value will just contain an index, i.e. it will have the form $\mathsf{fun}[i]$ with index $i$, and the graph will map the index to a table. So we define values as follows.

$$\begin{array}{lccl} \text{numbers} & n \in \mathbb{N} \\ \text{values} & v \in \mathbb{V} & ::= & n \mid \mathsf{fun}[i] \\ & \mathit{graph} & = & \mathbb{N} \to (\mathbb{V} \times \mathbb{V})\,\mathit{list} \end{array}$$ Given a function value $v$ and graph $G$, we write $\mathit{tab}(v,G)$ for the table $t$ when $v= \mathsf{fun}[i]$ and $G(i)=t$ for some index $i$. So we modify the semantic function $E$ to be defined as follows.

$$\begin{align*} E & : \mathit{exp} \to \mathit{env} \to (\mathbb{V} \times \mathit{graph})\,\mathit{set} \\ E[\!| n |\!](\rho) &= \{ (v,G) \mid v = n \} \\ E[\!| x |\!](\rho) &= \{ (v,G) \mid v = \rho(x) \} \\ E[\!| \lambda x.\; e |\!](\rho) &= \left\{ (v,G) \middle| \begin{array}{l} \forall v_1 v_2. (v_1,v_2) \in \mathit{tab}(v,G) \\ \Rightarrow v_2 \in E[\!|e|\!](\rho(x:=v_1)) \end{array} \right\} \\ E[\!| e_1\;e_2 |\!](\rho) &= \left\{ (v,G) \middle| \begin{array}{l}\exists v_1 v_2. v_1 {\in} E[\!| e_1 |\!](\rho) \land v_2 {\in} E[\!| e_2 |\!](\rho) \\ \land (v_2,v) {\in} \mathit{tab}(v_1,G) \end{array} \right\} \end{align*}$$

Example 1. Let's consider again the program

$$(\lambda f. f\;f)\;(\lambda g. 42)$$ We'll define a graph $G$ as follows. $$G(0) = [(\mathsf{fun}[1], 42)] \qquad G(1) = [(\mathsf{fun}[1], 42)]$$ To show $$(42,G) \in E[\!|(\lambda f. f\;f)\;(\lambda g. 42)|\!]\emptyset$$ we need to show

1. $(\mathsf{fun}[0],G) \in E[\!|(\lambda f. f\;f)|\!]\emptyset$. So we need to show $$(42,G) \in E[\!|f\;f|\!](f:=\mathsf{fun}[1])$$ which we have because $(\mathsf{fun}[1], 42) \in \mathsf{fun}[1]$.
2. $(\mathsf{fun}[1],G) \in E[\!|(\lambda g. 42)|\!]\emptyset$. We need $$(42,G) \in E[\!|42|\!](f:=\mathsf{fun}[1])$$ which is immediate.
3. $(\mathsf{fun}[1], 42) \in \mathit{tab}(\mathsf{fun}[0])$. This is immediate.

Example 2. We shall compute the factorial of 3 using the strict version of the Y combinator, that is, the Z combinator.

$$\begin{align*} R & \equiv \lambda v. (x\; x) \; v \\ M & \equiv \lambda x. f \; R \\ Z & \equiv \lambda f. M \; M \\ F & \equiv \lambda n. \mathbf{if}\,n=0\,\mathbf{then}\, 1\,\mathbf{else}\, n \times r \,(n-1)\\ H & \equiv \lambda r. F \\ \mathit{fact} & \equiv Z\, H \end{align*}$$ We shall show that $$(6,G) \in E[\!|\mathit{fact}\;3|\!]\emptyset$$ for some graph $G$ that we need to construct. By instrumenting an interpreter for the lambda calculus and running $\mathit{fact}\,3$, we observe the following graph. $$\begin{align*} G(0) &= [(\mathsf{fun}[1],\mathsf{fun}[4])] & \text{for } Z \\ G(1) &= [(\mathsf{fun}[3],\mathsf{fun}[4])] & \text{for } H \\ G(2) &= [(\mathsf{fun}[2],\mathsf{fun}[4])]& \text{for } M \\ G(3) &= [(0,1),(1,1),(2,2)] & \text{for } R \\ G(4) &= [(0,1),(1,1),(2,2),(3,6)] & \text{for } F \end{align*}$$ We check all of the following (Tedious! I'm going to write a program to do this next time.):

• $(\mathsf{fun}[4],G) \in E[Z\,H]\emptyset$
• $(3,6) \in G(4)$
• $(\mathsf{fun}[0],G) \in E[\!|Z|\!]\emptyset$
• $(\mathsf{fun}[4],G) \in E[\!|M\;M|\!](f:=\mathsf{fun}[1])$
• $(\mathsf{fun}[2],G) \in E[\!|M|\!](f:=\mathsf{fun}[1])$
• $(\mathsf{fun}[4],G) \in E[\!|f \; R|\!](f:=\mathsf{fun}[1],x:=\mathsf{fun}[2])$
• $(\mathsf{fun}[3],G) \in E[\!|R|\!](f:=\mathsf{fun}[1],x:=\mathsf{fun}[2])$
• $(1,G) \in E[\!|(x\;x)\;v|\!](f:=\mathsf{fun}[1],x:=\mathsf{fun}[2],v:=0)$ and $(0,1) \in G(4)$
• $(1,G) \in E[\!|(x\;x)\;v|\!](f:=\mathsf{fun}[1],x:=\mathsf{fun}[2],v:=1)$ and $(1,1) \in G(4)$
• $(2,G) \in E[\!|(x\;x)\;v|\!](f:=\mathsf{fun}[1],x:=\mathsf{fun}[2],v:=2)$ and $(2,2) \in G(4)$
• $(\mathsf{fun}[2], \mathsf{fun}[4]) \in G(2)$
• $(\mathsf{fun}[1],G) \in E[\!|H|\!]\emptyset$
• $(\mathsf{fun}[4],G) \in E[\!|F|\!](r:=\mathsf{fun}[3])$
• $(1,G) \in E[\!|\mathbf{if}\,n=0\,\mathbf{then}\, 1\,\mathbf{else}\, n \times r \,(n-1)|\!](r:=\mathsf{fun}[3],n:=0)$
• $(1,G) \in E[\!|\mathbf{if}\,n=0\,\mathbf{then}\, 1\,\mathbf{else}\, n \times r \,(n-1)|\!](r:=\mathsf{fun}[3],n:=1)$
• $(2,G) \in E[\!|\mathbf{if}\,n=0\,\mathbf{then}\, 1\,\mathbf{else}\, n \times r \,(n-1)|\!](r:=\mathsf{fun}[3],n:=2)$
• $(6,G) \in E[\!|\mathbf{if}\,n=0\,\mathbf{then}\, 1\,\mathbf{else}\, n \times r \,(n-1)|\!](r:=\mathsf{fun}[3],n:=3)$

The next step is to update the proof of soundness wrt. the big-step semantics. The graphs will make it a bit more challenging. But hopefully they will make it possible to also prove completeness!