Monday, December 19, 2016

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!