I'm still quite excited about the simple denotational semantics and looking forward to applying it to the semantics of gradually typed languages. However, before building on it I'd like to make sure it's correct. Recall that I proved soundness of the simple semantics with respect to a standard big-step operational semantics, but I did not prove completeness. Completeness says that if the operational semantics says that the program reduces to a particular value, then the denotational semantics does too. Recall that the first version of the simple semantics that I gave was not complete! It couldn't handle applying a function to itself, which is needed for the \(Y\) combinator and recursion. I've written down a fix, but the question remains whether the fix is good enough, that is, can we prove completeness? In the mean time, I learned that the simple semantics is closely related to filter models based on type systems with intersection types. This is quite helpful because that literature includes many completeness results for pure lambda calculi, see for example Intersection Types and Computational Rules by Alessi, Barbanera, and Dezani-Ciancaglini (2003).
In this blog post I prove completeness for an intersection type system with respect to a call-by-value lambda calculus augmented with numbers, primitive operators (addition, multiplication, etc.), and a conditional if-expression. The main outline of the proof is adapted from the above-cited paper, in which completeness is proved with respect to small-step operational semantics, though you'll find more details (i.e. lemmas) here because I've mechanized the proof in Isabelle and can't help but share in my suffering ;) (Lambda.thy, SmallStepLam.thy, IntersectComplete.thy) Ultimately I would like to prove completeness for the simple denotational semantics, but a good first step is doing the proof for a system that is in between the simple semantics and the intersection type systems in the literature.
The intersection type system I use here differs from ones in the literature in that I restrict the \(\wedge\) introduction rule to \(\lambda\)'s instead of applying it to any expression, as shown below. I recently realized that this change does not disturb the proof of Completeness because we're dealing with a call-by-value language. \[ \frac{\Gamma \vdash \lambda x.\, e : A \quad \Gamma \vdash \lambda x.\, e : B} {\Gamma \vdash \lambda x.\, e : A \wedge B}(\wedge\,\mathrm{intro}) \] I would like to remove the subsumption rule \[ \frac{\Gamma \vdash e : A \quad A <: B} {\Gamma \vdash e : B}(\mathrm{Sub}) \] but doing so was increasing the complexity of the proof of Completeness. Instead I plan to separately prove that the version without subsumption is equivalent to the version with subsumption. One might also consider doing the same regarding our above change to the \(\wedge\) introduction rule. I have also been working on that approach, but proving the admissibility of the standard \(\wedge\) introduction rule has turned out to be rather difficult (but interesting!).
Definition of an Applied CBV Lambda Calculus
Let us dive into the formalities and define the language that we're interested in. Here's the types, which include function types, intersection types, the top function type (written \(\top\)), and singleton numbers. Our \(\top\) corresponds to the type \(\nu\) from Egidi, Honsell, and Rocca (1992). See also Alessi et al. (2003). \[ A,B,C ::= A \to B \mid A \wedge B \mid \top \mid n \] and here's the expressions: \[ e ::= n \mid \mathit{op}(e,e) \mid \mathrm{if}\,e\,\mathrm{then}\,e\,\mathrm{else}\,e \mid x \mid \lambda x.\, e \mid e\,e \] where \(n\) ranges over numbers and \(\mathit{op}\) ranges over arithmetic operators such as addition.
We define type environments as an association list mapping variables to types. \[ \Gamma ::= \emptyset \mid \Gamma,x:A \]
The type system, defined below, is unusual in that it is highly precise. Note that the rule for arithmetic operators produces a precise singleton result and that the rules for if-expressions require the condition to be a singleton number (zero or non-zero) so that it knows which branch is taken. Thus, this type system is really a kind of dynamic semantics.
\begin{gather*} \frac{}{\Gamma \vdash n : n} \\[2ex] \frac{} {\Gamma \vdash \lambda x.\, e : \top}(\top\,\mathrm{intro}) \quad \frac{\Gamma \vdash \lambda x.\, e : A \quad \Gamma \vdash \lambda x.\, e : B} {\Gamma \vdash \lambda x.\, e : A \wedge B}(\wedge\,\mathrm{intro}) \\[2ex] \frac{\Gamma \vdash e : A \quad A <: B} {\Gamma \vdash e : B}(\mathrm{Sub}) \\[2ex] \frac{x:A \in \Gamma}{\Gamma \vdash x : A} \quad \frac{\Gamma,x:A \vdash B} {\Gamma \vdash \lambda x.\, e : A \to B} \quad \frac{\Gamma \vdash e_1: A \to B \quad \Gamma \vdash e_2 : A} {\Gamma \vdash e_1 \; e_2 : B}(\to\mathrm{intro}) \\[2ex] \frac{\Gamma \vdash e_1 : n_1 \quad \Gamma \vdash e_2 : n_2 \quad [\!|\mathit{op}|\!](n_1,n_2) = n_3} {\Gamma \vdash \mathit{op}(e_1,e_2) : n_3} \\[2ex] \frac{\Gamma \vdash e_1 : 0 \quad \Gamma \vdash e_3 : B} {\Gamma \vdash \mathrm{if}\,e_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 : B} \quad \frac{\Gamma \vdash e_1 : n \quad n \neq 0 \quad \Gamma \vdash e_2 : A} {\Gamma \vdash \mathrm{if}\,e_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 : A} \end{gather*}The rules for subtyping come from the literature.
\begin{gather*} \frac{}{n <: n} \quad \frac{}{\top <: \top} \quad \frac{}{A \to B <: \top} \quad \frac{A' <: A \quad B <: B'} {A \to B <: A' \to B'}(<:\to) \\[2ex] \frac{C <: A \quad C <: B}{C <: A \wedge B} \quad \frac{}{A \wedge B <: A} \quad \frac{}{A \wedge B <: B} \\[2ex] \frac{}{(C\to A) \wedge (C \to B) <: C \to (A \wedge B)} \end{gather*}We shall be working with values that are well typed in an empty type environment. This usually implies that the values have no free variables. However, that is not true of the current type system because of the \(\top\) introduction rule. So we add a side condition for \(\lambda\) in our definition of values. (In retrospect, I should have instead included a statement about free variables in the main Completeness theorem and then propagated that information to where it is needed.) \[ v ::= n \mid \lambda x.\, e \quad \text{where } FV(e) \subseteq \{x\} \]
We use a naive notion of substitution (not capture avoiding) because the \(v\)'s have no free variables to capture. \begin{align*} [x:=v] y &= \begin{cases} v & \text{if } x = y \\ y & \text{if } x \neq y \end{cases} \\ [x:=v] n &= n \\ [x:=v] (\lambda y.\, e) &= \begin{cases} \lambda y.\, e & \text{if } x = y \\ \lambda y.\, [x:=v] e & \text{if } x \neq y \end{cases} \\ [x:=v](e_1\, e_2) &= ([x:=v]e_1\, [x:=v]e_2) \\ [x:=v]\mathit{op}(e_1, e_2) &= \mathit{op}([x:=v]e_1, [x:=v]e_2) \\ [x:=v](\mathrm{if}\,e_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3) &= \mathrm{if}\,[x:=v]e_1\,\mathrm{then}\,[x:=v]e_2\,\mathrm{else}\,[x:=v]e_3 \end{align*}
The small-step operational semantics is defined by the following reduction rules. I'm not sure why I chose to use SOS-style rules instead of evaluation contexts. \begin{gather*} \frac{}{(\lambda x.\,e) \; v \longrightarrow [x:=v]e} \quad \frac{e_1 \longrightarrow e'_1}{e_1\,e_2 \longrightarrow e'_1 \, e_2} \quad \frac{e_2 \longrightarrow e'_2}{e_1\,e_2 \longrightarrow e_1 \, e'_2} \\[2ex] \frac{}{\mathit{op}(n_1,n_2) \longrightarrow [\!|\mathit{op}|\!](n_1,n_2)} \quad \frac{e_1 \longrightarrow e'_1} {\mathit{op}(e_1,e_2) \longrightarrow \mathit{op}(e'_1,e_2)} \quad \frac{e_2 \longrightarrow e'_2} {\mathit{op}(e_1,e_2) \longrightarrow \mathit{op}(e_1,e'_2)} \\[2ex] \frac{}{\mathrm{if}\,0\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 \longrightarrow e_3} \quad \frac{n \neq 0} {\mathrm{if}\,n\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 \longrightarrow e_2} \\[2ex] \frac{e_1 \longrightarrow e'_1} {\mathrm{if}\,e_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 \longrightarrow \mathrm{if}\,e'_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3} \end{gather*} \[ \frac{}{e \longrightarrow^{*} e} \qquad \frac{e_1 \longrightarrow e_2 \quad e_2 \longrightarrow^{*} e_3} {e_1 \longrightarrow^{*} e_3} \]
Proof of Completeness
The theorem that we aim to prove is that if the operational semantics says that a program reduces to a value, then the program is typable in the intersection type system and that the result type precisely describes the result value. I'm going to present the proof in a top-down style, so the proof of each lemma that I use is found further along in this blog post.
Theorem (Completeness)
If \(e \longmapsto^{*} v\), then
\(\emptyset \vdash e : A\) and \(\emptyset \vdash v : A\)
for some type \(A\).
Proof
Every value is typable (use the \(\top\) introduction rule for
\(\lambda\)), so we have some \(A\) such that \(\emptyset \vdash v :
A\). We shall show that typing is preserved by reverse reduction,
which will give us \(\emptyset \vdash e : A\).
QED
Lemma (Reverse Multi-Step Preserves Types)
If \(e \longrightarrow^{*} e'\) and \(\emptyset \vdash e' : A\),
then \(\emptyset \vdash e : A\).
Poof
The proof is by induction on the derivation of \(e \longrightarrow^{*} e'\).
The base case is trivial.
The induction case requires that typing be preserved for
a single-step of reduction, which we prove next.
QED
Lemma (Reverse Single-Step Preserves Types)
If \(e \longrightarrow e'\) and \(\emptyset \vdash e' : A\),
then \(\emptyset \vdash e : A\).
Proof
The proof is by induction on the derivation of \(e \longrightarrow e'\).
The most important case is for function application:
\[
(\lambda x.\,e) \; v \longrightarrow [x:=v]e
\]
We have that \(\emptyset \vdash [x:=v]e : A\) and need to show that
\(\emptyset \vdash (\lambda x.\,e) \; v : A\). That is, we need to
show that call-by-value \(\beta\)-expansion preserves types. So we need
\(x:B \vdash e : A\) and \(\emptyset \vdash v : B\) for some type
\(B\). The proof of this was the crux and required some generalization;
I found it difficult to find the right statement of the lemma. It is
proved below under the name Reverse Substitution Preserves Types.
The other cases of this proof are straightforward except for one
hiccup. They all require inversion lemmas (aka. generation lemmas) to
unpack the information from \(\emptyset \vdash e' : A\). However,
as is usual for languages with subsumption, the inversion lemmas are not simply proved by
case analysis on typing rules, but must instead be proved by induction
on the typing derivations.
QED
Lemma (Inversion)
- If \(\Gamma \vdash n : A \), then \(n <: A\).
- If \(\Gamma \vdash e_1\,e_2 : A \), then \( \Gamma \vdash e_1 : B \to A' \), \( A' <: A \), and \( \Gamma \vdash e_2 : B \) for some \(A'\) and \(B\).
- If \(\Gamma \vdash \mathit{op}(e_1,e_2) : A\), then \(\Gamma \vdash e_1 : n_1\), \(\Gamma \vdash e_2 : n_2 \), \(\Gamma \vdash \mathit{op}(e_1,e_2) : [\!|\mathit{op}|\!](n_1,n_2) \), and \([\!|\mathit{op}|\!](n_1,n_2) <: A\) for some \(n_1\) and \(n_2\).
- If \(\Gamma \vdash \mathrm{if}\,e_1\,\mathrm{then}\,e_2\,\mathrm{else}\,e_3 : A\), then either
- \(\Gamma \vdash e_1 : 0\), \(\Gamma\vdash e_3 : B\), and \(B <: A\), for some \(B\).
- \(\Gamma \vdash e_1 : n\), \(n \neq 0\), \(\Gamma\vdash e_2 : A'\), and \(A' <: A\), for some \(A'\).
To state the reverse substitution lemma in a way that provides a useful induction hypothesis in the case for \(\lambda\), we introduce a notion of equivalence of type environments: \[ \Gamma \approx \Gamma' = (x : A \in \Gamma \text{ iff } x : A \in \Gamma') \] The reverse substitution lemma will show that if \([y:=v]e\) is well typed, then so is \(e\) in the environment extended with \(y:B\), for some appropriate choice of \(B\). Now, the value \(v\) may appear in multiple places within \([y:=v]e\) and in each place, \(v\) may have been assigned a different type. For example, \(v\) could be \(\lambda x.\, {+}(x,1)\) and it could have the type \(0\to 1\) in one place and \(1\to 2\) in another place. However, we must choose a single type \(B\) for \(y\). But thanks to intersection types, we can choose \(B\) to be the intersection of all the types assigned to \(v\).
Lemma (Reverse Substitution Preserves Types)
If \(\Gamma \vdash [y:=v]e : A\) and \(y \notin \mathrm{dom}(\Gamma)\),
then \( \emptyset \vdash v : B \),
\( \Gamma' \vdash e : A\), and \(\Gamma' \approx \Gamma,y:B\)
for some \(\Gamma'\) and \(B\).
Proof
The proof is by induction on the derivation of \(\Gamma \vdash [y:=v]e : A\).
(I wonder if the proof would have been easier if done by
induction on \(e\).) The proof is rather long, so I'll just highlight
the lemmas that were needed here. The full details are in the Isabelle
mechanization.
- The cases for variables and numbers are relatively straightforward.
- The case for \(\lambda\) requires lemmas regarding Environment Strengthening and Environment Lowering and their corollaries.
- The case for subsumption is relatively easy.
- The case for function application is interesting. We have \( (e_1 \, e_2) = [y:=v]e \), so \(e = e'_1 \, e'_2\) where \(e_1 = [y:=v]e'_1\) and \(e_2 = [y:=v]e'_2\). From the induction hypotheses for \(e_1\) and \(e_2\), we have \(\emptyset \vdash v : B_1\) and \(\emptyset \vdash v : B_2\). The lemma Combine Values gives us some \(B_3\) such that \(\emptyset \vdash v : B_3\) and \(B_3 <: B_1\) and \(B_3 <: B_2\). We choose \(\Gamma' = \Gamma,y:B_3\). To show \(\Gamma' \vdash e'_1\, e'_2 : A\) we use the induction hypotheses for \(e_1\) and \(e_2\), along with the lemmas Equivalent Environments and Environment Lowering.
- The case for \(\top\) introduction is straightforward.
- The case for \(\wedge\) introduction uses the lemmas Well-typed with No Free Variables, Environment Strengthening, Combine Values, Equivalent Environments, and Environment Lowering.
- The cases for arithmetic operators and if-expressions follow a pattern similar to that of function application.
Lemma (Environment Strengthening)
If \(\Gamma \vdash e : A\) and for every free variable \(x\) in \(e\),
\( x:A \in \Gamma \text{ iff } x:A \in \Gamma' \), then
\(\Gamma' \vdash e : A\).
Proof
The proof is by induction on the derivation of
\(\Gamma \vdash e : A\).
QED
Corollary (Well-typed with No Free Variables)
If \(\Gamma \vdash e : A\) and \(\mathit{FV}(e) = \emptyset\),
then \(\emptyset \vdash e : A\).
We define the following ordering relation on environments: \[ \Gamma \sqsupseteq \Gamma' = (x:A \in \Gamma \Longrightarrow x:A' \in \Gamma \text{ and } A' <: A) \]
Lemma (Environment Lowering)
If \(\Gamma \vdash e : A\) and \(\Gamma \sqsupseteq \Gamma'\),
then \(\Gamma' \vdash e : A\).
Proof
The proof is by induction on the derivation of
\(\Gamma \vdash e : A\).
QED
Corollary (Equivalent Environments)
If \(\Gamma \vdash e : A\) and \(\Gamma \approx \Gamma'\),
then \(\Gamma' \vdash e : A\).
Proof
If \(\Gamma \approx \Gamma'\) then we also have
\(\Gamma \sqsupseteq \Gamma'\), so we conclude by
applying Environment Lowering.
QED
Lemma (Combine Values)
If \(\Gamma \vdash v : B_1\) and \(\Gamma \vdash v : B_2\),
then \(\Gamma \vdash v : B_3\), \(B_3 <: B_1 \wedge B_2\),
and \(B_1 \wedge B_2 <: B_3\) for some \(B_3\).
Proof
The proof is by cases on \(v\). It uses the Inversion lemma
for numbers and the \(\wedge\) introduction rule for \(\lambda\)'s.
QED
No comments:
Post a Comment