Simple Denotational Semantics for the Lambda Calculus, Pω Revisited?

I've been trying to understand Dana Scott's \(P_{\omega}\) and \(D_{\infty}\) models of the lambda calculus, as well as a couple large Coq formalizations of domain theory, and in the process have come up with an extraordinarily simple denotational semantics for the call-by-value lambda calculus. It borrows some of the main ideas from \(P_{\omega}\) but doesn't encode everything into numbers and puts infinity in a different place. (More discussion about this near the bottom of the post.) That being said, I still don't 100% understand \(P_{\omega}\), so there may be other subtle differences. In any event, what follows is so simple that it's either wrong or amazing that it's not already a well-known semantics.

UPDATE: It's wrong. See the section titled Counterexample to Completeness below. Now I need to go and read more literature.
UPDATE: It seems that there is an easy fix to the problem! See the subsequent post.

To get started, here's the syntax of the lambda calculus.

\[ \begin{array}{lrcl} \text{variables} & x \\ \text{numbers} & n & \in & \mathbb{N} \\ \text{expressions} & e & ::= & n \mid x \mid \lambda x.e \mid e\;e \end{array} \]

So we've got a language with numbers and first-class functions. I'm going to represent functions as data in the most simple way possible, as a lookup table, i.e., a list of pairs, each pair is an input value \(v_i\) and it's corresponding output \(v'_i\). Of course, functions can have an infinite number of inputs, so how will a finite-length list suffice?

\[ \begin{array}{lrcl} \text{values} & v & ::= & n \mid [(v_1,v'_1),\ldots,(v_n,v'_n)] \end{array} \]

The answer is that we're going to write the denotational semantics as a logic program, that is, as a relation instead of a function. (We'll turn it back into a function later.) Instead of producing the result value, the semantics will ask for a result value and then say whether it is correct or not. So when it comes to a program that produces a function, the semantics will ask for a list of input-output values and say whether they agree with the function. A finite list suffices because, after all, you can't actually build an infinite list to pass into the semantics.

So here we go, our first version of the semantics, in relational style, or equivalently, as a function with three parameters that returns a Boolean. We name the function denoto, with an o at the end as a nod to The Reasoned Schemer. The meaning of a \(\lambda x.e\) is any table \(T\) that agrees with the semantics of the body \(e\). (This allows the table to be empty!) The meaning of an application \(e_1 e_2\) is simply to do a lookup in a table for \(e_1\). (Requiring a non-empty table.) We write \((v,v') \in T\) when \((v,v')\) is one of the pairs in the table \(T\).

\begin{align*} \mathit{denoto}(n, \rho, n) &= \mathit{true} \\ \mathit{denoto}(x, \rho, \rho(x)) &= \mathit{true} \\ \mathit{denoto}(\lambda x. e, \rho, T) &= \forall v v'.\, (v,v') \in T \Rightarrow \mathit{denoto}(e,\rho(x:=v),v') \\ \mathit{denoto}(e_1 \; e_2, \rho, v) &= \left(\begin{array}{l} \exists T v_2.\; \mathit{denoto}(e_1, \rho, T) \land \mathit{denoto}(e_2, \rho, v_2) \\ \qquad \land (v_2,v) \in T \end{array} \right) \end{align*}

The existential quantifier in the line for application is powerful. It enables the semantics to guess a sufficiently large table \(T\), so long as the table agrees with the semantics of \(e_1\) and the later uses of the result value. Because the execution of a terminating program can only call the function with a finite number of arguments, and the execution can only use the results in a finite number of ways, there is a sufficiently large table \(T\) to cover all its uses in the execution of the whole program. Also, note that \(T\) can be large in a couple dimensions: it may handle a large number of inputs, but also, it can specify large outputs (in the case when the outputs are functions).

Denotational semantics are usually written as functions, not relations, so we remove the third parameter and instead return a set of values. This will bring the semantics more in line with \(P_{\omega}\). Also, for this version we'll use the name \(E\) for the semantic function instead of denoto.

\begin{align*} E[\!| n |\!](\rho) &= \{ n \} \\ E[\!| x |\!](\rho) &= \{ \rho(x) \} \\ E[\!| \lambda x.\; e |\!](\rho) &= \{ T \mid \forall v v'. (v,v') \in T \Rightarrow v' \in E[\!|e|\!](\rho(x:=v)) \} \\ E[\!| e_1\;e_2 |\!](\rho) &= \{ v \mid \exists T v_2. T {\in} E[\!| e_1 |\!](\rho) \land v_2 {\in} E[\!| e_2 |\!](\rho) \land (v_2,v) {\in} T \} \end{align*}

With the semantics written this way, it is clear that the meaning of a \(\lambda\) is not just a finite table, but instead it is typically an infinite set of tables, each of which is an approximation of the actual infinite graph of the function.

Is this semantics correct? I'm not entirely sure yet, but I have proved that it is sound with respect to the big-step semantics.

Theorem (Soundness).
If \(v \in E[\!| e |\!](\rho) \) and \( \rho \approx \rho' \), then \( \rho' \vdash e \Downarrow v' \) and \(v \approx v'\) for some \(v'\).

The two semantics have different notions of values, so the relation \(\approx\) is defined to bridge the two worlds.

\begin{gather*} n \approx n \\[2ex] \frac{\forall v_1 v_2 v'_1. (v_1,v_2) \in T \land v_1 {\approx} v'_1 \Rightarrow \exists v'_2. \rho(x:=v'_1) \vdash e \Downarrow v'_2 \land v_2 {\approx} v'_2} {T \approx \langle \lambda x.e, \rho \rangle} \end{gather*} The definition of \(\approx\) extends to environments in the natural way.

The semantics and proof of soundness in Isabelle is here.

Counterexample to Completeness

This semantics does not handle self application properly. Consider the program \[ (\lambda f. f \; f) \; (\lambda g. 1) \] The operational semantics says the answer is \(1\). The denotational semantics requires us to find some tables \(T \in [\!|\lambda f. f\;f|\!]\) and \(T' \in [\!|\lambda g.1|\!]\). We need \( (T',1) \in T\), so we need \(1 \in [\!|f\; f|\!](f:=T') \). That requires \((T', 1) \in T'\), but that's impossible given that we've defined the values and tables in a way that does not allow cycles.

Relationship with \(P_{\omega}\)

The idea of representing functions as data, and as a lookup table, comes from \(P_{\omega}\), as does having the denotation's result be a set of values. As mentioned above, one (minor) difference is that \(P_{\omega}\) encodes everything into numbers, whereas here we've used a datatype definition for the values. However, the most important difference (if I understand \(P_{\omega}\) correctly) is that its functions are infinite in a first-class sense. That is, \(P_{\omega}\) is a solution to \[ D = \mathbb{N} + (D \to D) \] and the things in \(D \to D\) are functions with potentially infinite graphs. In contrast, I've taken a stratified approach in which I've defined the values \(V\) to include only finite representations of functions \[ V = \mathbb{N} + (V \times V) \, \mathit{list} \] and then, only at the top level, I've allowed for infinity by making the denotation of an expression be a (potentially infinite) set of values. \[ E : \mathit{exp} \to \mathit{env} \to V\, \mathit{set} \]