Scott’s model of lambda calculus
Lambda calculus constructs a set of terms starting from a set of variables using operations and rules. If we treat lambda calculus as a programming language, we can consider a model as a way of giving an implementation of lambda calculus. This essentially gives an implementation of a typed programming language with product types, function types and certain inductive types.
1 Introduction
Lambda calculus constructs a set of terms starting from a set of variables \{x,y,\cdots \} and by using a application operation, M \cdot N, and \lambda-abstraction \lambda x.M. Furthermore, given a term M and a variable x not bound by a \lambda in M, one can substitute a term N \neq M for x in M (i.e. M[N/x]). There are also two axioms relating application and abstraction known as \eta and \beta rules:
\beta : (\lambda x.M)(N) = M[N/x] \eta : \lambda x.M = \lambda y. M[y/x]
There is a variant of lambda calculus called \pi \lambda-calculus. This calculus has subjective pairing which uses the binary operator \pi, and unary operators \pi_{0} and \pi_{1} that have the following properties:
\pi(\pi_{0}(M),\pi_{1}(M)) = M \pi_{0}(\pi(M,N)) = M \pi_{1}(\pi(M,N)) = N
Given lambda calculus, we seek to have a model of it to show that lambda calculus is a consistent. If we treat lambda calculus as a programming language, we can consider a model as a way of giving an implementation of lambda calculus. A simple model of lambda calculus is the The Scott’s Model of Lambda Calculus.
This model is very concrete as it is derived from the power set of the natural numbers. It is very easy to implement as it only requires the type of natural numbers, the type of booleans, and function types. Additionally, from this model one can construct a cartesian closed category the resembles the category of domains. This category essentially gives an implementation of a typed programming language with product types, function types and certain inductive types.
2 What is Scott’s Model
The Scott’s Model of Lambda Calculus is a model on P(\mathbb{N}) that utilizes a topology on P(\mathbb{N}). The topology in question is generated by the basis \{ B_{k}| k \subset \mathbb{N}\ \text{finite} \} where B_{k} = \{A \subseteq \mathbb{N}| k \subseteq A\}. Given the set of continuous functions on P(\mathbb{N}), Cont(P(\mathbb{N}),P(\mathbb{N})), we have the following:
Proof. We make use of the fact that \mathbb{N} is isomorphic to \mathbb{N}\times \mathbb{N} and the set of finite subsets of \mathbb{N}. We denoted the set of code representing finite subsets of C \subseteq \mathbb{N} as C^{*}. First we construct the function [-]: P(\mathbb{N}) \to Cont(P(\mathbb{N}),P(\mathbb{N})) where [A](C) := \{m | \exists n \in C^{*} \ \text{s.t.} (n,m) \in A\}.
Given a basis element B_{k} ,where k is a finite set, and an element D \in [A]^{-1}(B_{k}), one has that k \subseteq [A](D). By definition, for any element x \in k, there is a finite set \beta_{x} \in D^{*} s.t. (\beta_{x},x) \in A. Thus D \in B_{\bigcup_{x} \beta_{x}} \subseteq [A]^{-1}(B_{k}) where \bigcup_{x} \beta_{x} is a finite set. Thus [A]^{-1}(B_{k}) is the union of basis elements showing [A] to be continuous.
We now construct the function \langle -\rangle:Cont(P(\mathbb{N}),P(\mathbb{N})) \to P(\mathbb{N}) where \langle F\rangle = \{(n,m)| m \in F(n)\}. To show that [-] is a retract of \langle -\rangle, first we show that F(X) = \bigcup_{y \in X^{*}} F(y).
Given a finite subset d \subseteq F(X), by continuity of F, we can find a subset e \subset X such that d \subset F(e), so F(X) \subseteq \bigcup_{y \in X^{*}} F(y). Given a finite subset y \in X^{*} and an element z \in F(y), we have a finite subset e \subseteq y \subseteq X such that B_{e} \subseteq F^{-1}(B_{\{z\}}), so z \in F(X). Thus F(X) = \bigcup_{y \in X^{*}} F(y).
Using the above fact, one can see that: \begin{aligned} [\langle F\rangle](X) &= \{m | \exists n \in X^{*} \ \text{s.t.} \ (n,m) \in \langle F\rangle \} \\&= \{m | \exists n \in X^{*} \ \text{s.t.} \ m \in F(n) \} \\&= \bigcup_{n \in X^{*}} F(n) \end{aligned} This completes the proof.
The above lemma allows us to encode any continuous function on P(\mathbb{N}) as a subset of \mathbb{N}. Furthermore we can also encode continuous functions F: P(\mathbb{N})^{n} \to P(\mathbb{N}). We can already encode functions for n = 1. Given an encoding for functions G:P(\mathbb{N})^{k} \to P(\mathbb{N}), we can encode F:P(\mathbb{N})^{k + 1} \to P(\mathbb{N}) as \langle F'\rangle where F'(X) = \langle F(X,-)\rangle.
Two particular continuous functions we can consider are K: P(\mathbb{N})^{2} \to P(\mathbb{N}) and S: P(\mathbb{N})^{3} \to P(\mathbb{N}) where K(A)(B) = A and S(A)(B)(C) = [[A](C)]([B](C)). K and S can be used to generate every lambda term, so it isn’t too much of a stretch to consider P(\mathbb{N}) as a set of lambda terms. A particular continuous function and lambda term of note is Y:P(\mathbb{N})\to P(\mathbb{N}) where Y(X) is the least fixed point of [X].
We can also consider the functions [-] and \langle -\rangle as application and abstraction respectively. Thus the equality [\langle F\rangle] = F represents the \beta-rule. The lack of an equality X = \langle [X]\rangle betrays the lack of an \eta-rule. However, we do have that X \subseteq \langle [X]\rangle.
3 Category of Closure Operators
An interesting feature of P(\mathbb{N}) is that from it one can construct a cartesian closed category of objects that essentially functions as a “category of domains”. In order to construct this category, we must introduce closure operators which are the objects of this category.
A closure operator is a continuous function C: P(\mathbb{N}) \to P(\mathbb{N}) s.t. C \circ C = C and for X \subseteq \mathbb{N}, X \subseteq C(X). A morphism between C and D is a continuous function F s.t. F = D \circ F \circ C and composition is composition of continuous functions. A closure operator C induces a lattice whose elements are fixed points of C, The fixed point of C are closed under directed joins. A morphism F from C to D is a directed join preserving lattice morphism between the lattices of C and D.
There is also a closure operator \mathrm{Clos} s.t. [\mathrm{Clos}(X)] is the smallest closure operator bound below by [X]. In fact the fixed points of \mathrm{Clos} are the elements \langle C\rangle for every closure operator C.
What makes this category a “category of domains” is that the endomorphisms of closure operators have fixed points. In particular, endomorphisms of \mathrm{Clos} have fixed points. Given a morphism F: C \to C, the least fixed point of F is Y(\langle F\rangle). In particular, there is a continuous function taking a closure operator C to the exponent closure operator C \Rightarrow C. This defines a continuous endomorphism on \mathrm{Clos}. Thus we have a closure operator L = Y(\langle \Rightarrow \rangle) such that L = L\Rightarrow L. Since L is equal to its object of continuous endomorphisms, L is a model of lambda calculus similarly to P(\mathbb{N}), but unlike P(\mathbb{N}), L is an \eta-rule.
We can also construct another model of lambda calculus. To do this we must find a closure operator I such that I \times I = I. In our case, we have I = \mathrm{Id}. We then construct the function \Rightarrow \mathrm{Id}: \mathrm{Clos}\to \mathrm{Clos} which takes a closure operator to the closure operator C \Rightarrow\mathrm{Id}. This gives us the closure operator Q = Y(\langle \Rightarrow \mathrm{Id}\rangle). We have the following: Q = Q \Rightarrow \mathrm{Id}= Q \Rightarrow (\mathrm{Id}\times \mathrm{Id}) = (Q \Rightarrow \mathrm{Id}) \times (Q \Rightarrow \mathrm{Id}) = Q \times Q Q = Q \Rightarrow \mathrm{Id}= (Q \times Q) \Rightarrow \mathrm{Id}= Q \Rightarrow (Q \Rightarrow \mathrm{Id}) = Q \Rightarrow Q Q is special because not only is it a model of lambda calculus with an \eta-rule, the equality Q = Q \times Q makes Q model of lambda calculus with subjective pairing.
4 Conclusion
In conclusion, P(\mathbb{N}) is a model of lambda calculus without an \eta-rule. Additionally, one can construct a category similar to the category of domains that is cartesian closed and is closed under the fixed points of certain functions; in particular the function \Rightarrow which gives a model of lambda calculus. What is fascinating about this model is that it is built solely from the natural numbers and the powerset operator. There is another model of lambda calculus construction on the set of partial functions \mathbb{N}\rightharpoonup 2. An interesting follow-up would be to consider derivate models of P(\mathbb{N}), for example the set of functions from \mathbb{N} into the unit interval.