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!