A note on the expressiveness of logic

Reachability problem. Fix a graph $\mathcal{G}$. A vertex $u$ is said to be reachable from a vertex $v$ in $\mathcal{G}$ if there exist $r \ge 0$ vertices $x_1$, ..., $x_r$, such that $(v, x_1)$, $(x_1, x_2)$, ..., $(x_{r−1}, u)$ are edges of $\mathcal{G}$. A formula $\phi(x,y)$ with exactly two free variables $x, y$ and one relation symbol $E$ is said to "express" reachability if and only if for any finite graph $\mathcal{G}$, vertex $u$ is reachable from vertex $v$ in $\mathcal{G}$ if and only if $\mathcal{G}$ is a model of $\phi(x,y)$ with respect to some interpretation that associates $E$ to edge relation and $x,\ y$ to vertices $u,\ v$.
Reachability is not expressible in first-order logic. Suppose $\phi(x,y)$ is a FO logic formula expressing reachability. Define three sentences $s_1$, $s_2$, and $s_3$, such that
$s_1 \equiv \forall x \forall y. \phi(x, y)$, i.e., all vertices are reachable from all vertices;
$s_2 \equiv \forall x. (\exists y. E(x, y) \wedge \forall z. E(x, z) \implies z = y)$, i.e., every vertex has out-degree one;
$s_3 \equiv \forall x. (\exists y. E(y, x) \wedge \forall z. E(z, x) \implies z = y)$, i.e., every vertex has in-degree one.
Let $s \equiv s_1 \wedge \ s_2 \wedge \ s_3$. Observe that a graph is a model of $s$ if and only if the graph is cycle. Since there are finite cycles with as many vertices as desired, $s$ has arbitrary large finite models. It then follows by Lowenheim-Skolem theorem that $s$ has an infinite model. But infinite cycles do not exist, and thus our assumption that there exists a FO logic formula expressing reachability is contradicted.
Reachability is expressible in second-order logic. Given constants $x$ and $y$ and a binary relation symbol $L$, we use the following sentences to characterize $L$ as a path from $x$ to $y$:
1. $L$ is a linear order over the vertices : $$ \begin{align*} \psi_1 \equiv\ & \forall u. \neg L(u,u) \\ & \wedge \forall u\forall v. (L(u,v) \implies \neg L(v,u)) \\ & \wedge \forall u\forall v \forall w. (L(u,v) \wedge L(v,w) \implies L(u,w)) \end{align*} $$ 2. Any two consecutive vertices in the order must be joined by an edge: $$ \begin{align*} \psi_2 \equiv\ &\forall u \forall v. ((L(u,v) \wedge \forall w. (\neg L(u,w) \vee \neg L(w,v))) \implies E(u,v)). \end{align*}$$3. The first vertex in the order is $x$, the last vertex is $y$, and $x$, $y$ are in the order: $$ \psi_3 \equiv (\forall u.\ \neg L(u,x)) \wedge (\forall v.\ \neg L(y,v)) \ \wedge L(x,y).$$ Now an expression for reachability can be defined as$$\phi(x,y) \equiv \exists L. ((x=y) \vee (\psi_1 \wedge \psi_2 \wedge \psi_3)).$$

Expressiveness of first-order Logic

It was known that the natural deduction proof system for FO logic is both sound and complete. Therefore, since verifying a proof is mechanical, deriving a proof must be as hard as checking its validity. Hence it is impossible to build a perfect automatic theorem prover for FO logic. In fact, validity of FO is undecidable since FO can formulate the Post correspondence problem. On the other hand, validity of FO is easier than satisfiability, since the former is enumerable while the latter is not.
Suppose we have only equality and edge relation in our language. A $\phi$-graph problem is to decide whether there exists an interpretation such that a given finite graph is a model of formula $\phi$. The class L-graph is formed by all $\phi$-graph problems where $\phi$ is a formula defined in logic L.
Fact. FO-graph is strictly in $P$.
The inclusion is strict because reachability problem (which is P-complete) is not expressible in FO and thus not captured by FO-graph. In fact, any FO-graph problem can be decided in LOGSPACE (check this). Immerman and Vardi (1982) added inductive definitions to FO to get the logic LFP, which is sufficient to express P problems over ordered graphs, namely, there is a distinguished relation $<$ that is interpreted as a linear order over the vertices.
Theorem. (Immerman-Vardi 1982) LFP-graph is in $P$.
However, for graphs without the ordering assumption, there are easily poly-time computable properties that are not definable in LFP. Hence LFP is still too weak to capture $P$. Grohe, Holm, and Laubner have added linear-algebraic operators to LFP. This properly extends the power of LFP with counting, but its relationship to $P$ remains an open question.

Expressiveness of second-order Logic

Second-order logic (SO) extends first-order logic with quantifications over relations and sets. Monadic second-order logic (MSO) is the restriction of SO where the second-order quantifiers are only over sets. Existential second-order logic (ESO) is a restricted version of SO where only existential quantifications are allowed.
Fact. MSO-graph is strictly between P and NP, since 3-colorability is in MSO-graph but Hamiltonian path problem is not (the latter two problems are NP-complete). However, Hamiltonian path problem can be captured by extending MSO with quantifiers over sets of edges.
The following result shows that ESO is in some senses the normal form of SO.
Proposition. (Buchi 1976) Any MSO formula can be re-written to an equivalent EMSO formula.
ESO-graph captures NP. It is straightforward to show that ESO-graph is in NP by non-deterministically choosing a relation for in polynomial time. Now let $\phi_1$ and $\phi_2$ be defined as before. In addition, define $\phi_4 \equiv \forall u\forall v. L(u, v)\vee L(v, u) \vee u = v$. Observe that $\mathcal{G}$ is a model of $\exists L. \psi_1 \wedge \psi_2 \wedge \psi_4$ if and only if $\mathcal{G}$ contains a Hamiltonian path. Since deciding the existence of a Hamiltonian path is NP-complete, we have
Theorem. (Fagin, 1974) $NP$ = ESO-graph.
By Fagin's theorem, ESO is closed under negation if and only if NP = co-NP. Since P $\subseteq$ NP$~\cap~$co-NP, second-order logic covers all languages in the polynomial time hierarchy. Other second-order concepts, e.g., least fixed-point operator and transitive closure operator, lead to logics which characterise further complexity classes like P, NLOGSPACE, PSPACE. For these results of descriptive complexity theory see [1].
The "weak" MSO (WMSO) is a further restricted version of MSO such that the set quantifiers range only over finite sets. The WMSO theory of $(\mathbb N, <)$ is a particular useful theory called Weak (monadic) Second-order Logic with one Successor (WS1S). Buchi has shown that WS1S is decidable via automata-theoretic approaches.
Theorem. (Buchi 1960) One an effectively construct an input-free finite automaton $A_\varphi$ from a sentence $\varphi$ in WS1S, such that $L(A_\varphi)\neq \emptyset$ iff $\varphi$ holds. Conversely, given an input-free automaton $A$ one can defined a sentence $\varphi_A$ in WS1S such that $L(A)\neq \emptyset$ iff $\varphi_A$ holds.
The idea of reduction is to represent numbers in binary, namely, as finite words over $\{0,1\}$, and to view a finite word as the (characteristic function of) a finite set via finite-set interpretation [3,4]. For instance, integer $21$ corresponds to the word $10101$, which is interpreted to a finite set $\{1,3,5\}$.

It is interesting to note that the expressiveness power of WS1S is equivalent to a first-order theory. Presburger Arithmetic (PA) is the first-order theory of the structure $(\mathbb N, +)$. In Buchi's 1960 paper it is noted that the decidability of PA can be inferred from that of WS1S. The decidability of Presburger arithmetic follows by translating first-order sentences in the signature $+$ to WS1S. To translate back from WS1S (or from finite automata), we would need to extend PA with some arithmetical means such as $|_2$, which associates each number $m>0$ with the greatest power of 2 that divides $m$. [4]
Theorem. A relation is definable in WS1S iff it is definable in the FO theory of $(\mathbb N, +, |_2)$.

References

1. Finite Model Theory, Springer-Verlag, New York 1995.

2. Languages, Automata, and Logic, Handbook of Formal Languages, Volume 3.
3. Transforming structures by set interpretations. LMCS 2007.
4. Automatic Structures. PhD Thesis. 2004.

Intuition behind a mathematical puzzle

Sometimes, it is helpful to reason about a mathematical puzzle in a concrete context. A solution may reveal itself after you reword the problem statement in intuitive terms. The following example shows how the solution to a seemingly nontrivial problem becomes obvious after the statement of the problem is reworded appropri-ately.
Example. Consider the following function:

function f (n: int) {
  if n == 1 return n
  choose integers a, b ≥ 0 such that a + b == n
  return a * b + f(a) + f(b)
}

Our goal is to show that the output of f(n) does not depend on how a and b are determined in the function body. This fact is far from obvious by inspecting the code. A standard approach to show this kind of fact is via mathematical induction. However, to establish the induction hypothesis, one must first express the value of f(n) in $n$. This is not easy given that values of a and b are not specified. Besides, an inductive proof typically proceeds by manipulating formulas. In that case, the proof itself is not very helpful for us to gain insights to the fact it proves.
On the other hand, the fact turns evident once you notice what the function intends to compute. The key observation here is that f(n) effectively counts the number of hand-shaking in a group of $n$ people. A group of size $n$ is is divided into two groups of size $a$ and $b.$ People from different groups then shake hand with each other. This process continues recursively until no smaller group can be form. At that time, each person eventually shakes hand with everybody else for exactly once. Therefore, the value of f(n) is $n\cdot(n-1)/2$ regardless of how groups are divided during the process.

A technique called double counting is closely related to the idea expressed above.
Example. We know that there are ${n \choose k}$ ways to select a set of size $k$ from a set $S$ of $n$ distinct elements. If $S$ is divided into two partitions of size $a$ and $b$, then selecting a subset from $S$ amounts to selecting a subset from each of the partitions respectively. Therefore, no matter how the partitions are divided, i.e., $a + b = n$, we have $$\sum_{i+j=k}{a \choose i}{b \choose j} = {n \choose k}$$(recall that ${n \choose 0}=1$ and ${n \choose k}=0$ for $k<0$ or $k>n$).

A note on Angluin’s Learning Algorithm

The L* Learning Algorithm, also known as Angluin’s Learning Algorithm for DFAs, was first developed by Angluin [1] and later improved by Rivest and Schapire [2]. L* learns an unknown regular language, say $U$ over an alphabet $\Sigma$, and produces a DFA $C$ such that $L(C) = U$. L* works by incrementally producing a sequence of candidate DFAs $C_1 , C_2, ...$ converging to $C$. In order to learn $U$, L* needs a Teacher to answer two type of questions. The first type is a membership query, consisting of a string $\sigma \in \Sigma*$; the answer is true if $\sigma \in U$, and false otherwise. The second type of question is a conjecture, which is a candidate DFA $C$ whose language the algorithm believes to be identical to $U$. The answer is true if $L(C) = U$. Otherwise the Teacher returns a counterexample, which is a string $\sigma'$ in the symmetric difference of $L(C)$ and $U$.
At a higher level, L* creates a table where it incrementally records whether strings in $\Sigma^*$ belong to $U$. It does this by making membership queries to the Teacher. At various stages, L* would decide to make a conjecture. It constructs a candidate automaton $C$ based on the information contained in the table, and asks the Teacher whether the conjecture is correct. If it is, the algorithm terminates. Otherwise, L* uses the counterexample returned by the Teacher to expand the table with strings that witness differences between $L(C)$ and $U$.
The Learner maintains a Boolean table with index set $X\times Y \subset \Sigma^*\times\Sigma^*.$ The rows of the table are indexed by $X$ while the columns are indexed by $Y$. Each cell $(x,y)$ indicates whether or not $xy \in U$. Two strings $a,b\in X$ are called $Y$-equivalent, written as $a\equiv_Y b$, if $ay\in U \iff by\in U$ for all $y\in Y.$ Note that $a\equiv_Y b$ iff the rows indexed by $a$ and $b$ are identical binary strings. The table is called consistent iff all distinct strings $x,x'\in X$ are not $Y$-equivalent. The table is called closed iff for all $x\in X$ and $a\in\Sigma$, there exists $x'\in X$ such that $xa\equiv_Y x'$.
The table determines a reduced DFA when it is consistent and closed. The states of the DFA are $\{[x]_Y:x\in X\}$ (here $[\cdot]_Y$ is the equivalence classes induced by $\equiv_Y$); accepting states are $\{[x]_Y: x\in X\cap U\}$; the transition function $\delta:[X]_Y\times\Sigma\to [X]_Y$ is given by $\delta([x]_Y,a)=[xa]_Y.$ This DFA is reduced as every two states of it can be distinguished by some string in $Y$ by the definition of consistency. The L* algorithm can now be sketched as follows:
Step 1. Start with a one-cell table with index set $\{\epsilon\}\times \{\epsilon\}$.
Step 2. Fill the table cells with membership queries and expand the index set when necessary until the table is consistent and closed. This procedure guarantees to find the minimal expansion of the table that is consistent and closed. Construct a conjecture DFA $C$ from the table.
Step 3. Check the conjecture using an equivalence query. If it is correct then output it and halt. Otherwise, expand the table with the provided counterexample and go to Step 2.
We give more details about Step 3. Suppose the Teacher returns a counterexample $w=w_1\dots w_n \in \Sigma^n$ for conjecture $C$. Let the trace of this string in $C$ be$$x_0\overset{w_1}{\longrightarrow}x_1\overset{w_2}{\longrightarrow}\cdots\overset{w_n}{\longrightarrow}x_n,$$for $x_0,...,x_n\in X.$ Then there is $1\le i\le n$ such that $x_i w_{i+1}...w_n \in U \iff w \not\in U.$ The table is then expanded by including $x_{i-1}w_i$ and $w_{i+1}...w_n$ in $X$ and $Y$, respectively.
Recall that the number of states of a conjecture DFA is the same as the number of distinct rows in the table. Also, the number of distinct rows increases by at least one each time an equivalence query fails. The L* algorithm would therefore terminate after making at most $|C| − 1$ incorrect equivalence queries and learn the reduced automaton $C$ for the target language.

Difficulty of learning DFAs

Difficulty of offline learning. Let $\mathcal{A}, \mathcal{B} \subset \Sigma^*$ be two finite sets of strings. Given $k$, it is NP-complete to decide whether a DFA $D$ with $k$ states exists such that $\mathcal{A} \subseteq L(D)$ and $\mathcal{B} \subseteq \Sigma^* \setminus L(D)$. It is still NP-complete to find such a DFA with the minimum size. In fact, even finding a DFA with a number of states polynomial on the number of states of the minimum one is NP-complete. If all strings of length $n$ or less are given, then the problem can be solved in time polynomial on the input size. Note, however, that the size of the input is itself exponential on the number of states in the resulting DFA. Angluin has shown that this problem remains NP-complete if an arbitrarily small fixed fraction is missing from the input set.
Difficulty of online learning. Learning a minimal DFA becomes easier if the algorithm is allowed to make queries to the unknown automaton. The L* algorithm proposed by Angluin [1] solves the problem in polynomial time by allowing the algorithm to ask membership and equivalence queries. Rivest and Schapire [2] later improved the algorithm so that it does not need to reset the unknown automaton to the initial state after each query.

References

1. D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 1987.
2. R. L. Rivest and R. E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 1993.
3. Michael Kearns and Umesh Vazirani. An Introduction to Computational Learning Theory. MIT Press, 1994.
4. Ron Rivest, Machine Learning Lecture Notes at MIT, Lecture 23 & 24.
5. Rajesh Parekh, Vasant Honavar. Learning DFA from Simple Examples. Machine Learning, 2001.

Contextual equivalence (in progress)

\( \def\[#1]{[\![\,#1\,]\!]} \def\V[#1]{\mathcal{V}\,[\![#1]\!]} \def\E[#1]{\mathcal{E}\,[\![#1]\!]} \def\G[#1]{\mathcal{G}\,[\![#1]\!]} \)

A type environment $\Delta$ is defined by $\Delta ::= \cdot\ |\ \Delta, \alpha$, where $\alpha$ denotes a type variable. A judgement in form of $\Delta\vdash  \tau$ states that type $\tau$ is well-formed in $\Delta$, i.e., all free type variables in $\tau$ appear in $\Delta$. An example of judgements of this kind is $\beta \vdash \forall \alpha.\, \alpha\rightarrow \beta$. We lift the judgement to define $\Delta \vdash \Gamma$, meaning $\forall x\in Dom(\Gamma).\,\Delta\vdash\Gamma(x)$. That is, all the types in the range of $\Gamma$ are well-formed in $\Delta$. When we write $\Delta; \Gamma \vdash e:\tau$, we mean $\Gamma \vdash e:\tau$ plus that $\tau$ is well-formed in $\Delta$. A type parameter $\alpha$ is introduced to term $e$ by type abstraction $\Lambda \alpha.\, e$, and eliminated from $e$ by type application $e[\tau]$ (for $e$ in form of $\Lambda \alpha.\, e$). The corresponding typing rules are$$\frac{\Delta, \alpha; \Gamma \vdash e: \tau}{\Delta; \Gamma \vdash \Lambda \alpha.\,e: \forall\alpha.\tau}\quad\mbox{and}\quad\frac{\Delta; \Gamma \vdash e: \forall\alpha.\tau\quad\Delta \vdash \tau'}{\Delta; \Gamma \vdash e[\tau']: \tau[\tau'/\alpha]}.$$In this lecture, we shall consider an extension of STLC with type abstraction and type application. This extension is in fact a terminating fragment of System F.
A context is comprehended as a complete program with a single hole that is capable of accepting an expression of a certain type. Context typing is in general expressed as $C: (\Gamma\vdash \tau) \leadsto (\Gamma'\vdash \tau')$. That is, given a context $C$, we can embed any expression $e$ in it such that $\Gamma\vdash e:\tau$ implies $\Gamma'\vdash C[e]:\tau'$.
Two expressions $e_1$ and $e_2$ are contextual equivalent in $\Gamma$ (written as $\Gamma \vdash e_1 \approx_{ctx} e_2: \tau$) iff $\Gamma \vdash e_1:\tau$, $\Gamma \vdash e_2:\tau$, and for all $C:(\Gamma \vdash \tau) \leadsto (\cdot \vdash bool)$, $\exists v:\tau.$ $e_1 \Downarrow v \wedge e_2 \Downarrow v$.
Note that here we only consider contextual equivalence for terminating programs. We shall extend its definition for general programs a bit later in this lecture. Also, we assume that the context yields a closed Boolean program after $e$ is embedded. This assumption is made without loss of generality: for any two programs of type inhabited by at least two members, there exists a context to differentiate their return values with Boolean if and only if the two programs are not contextual equivalent. (Any two programs of type with only one inhabitant are contextual equivalent by definition.)
The main difficulty of reasoning about contextual equivalence lies in the fact that equivalence must be shown for all contexts $C$. Proving equivalence by inducting on the structure of $C$ is problematic for $C = \lambda x:\tau.\, C$ and $C = \Lambda \alpha.\,C$. Hence, instead of proving contextual equivalence directly, people usually use proof methods such as logical relations or other technical bisimulations. We shall prove the following two interesting theorems in this lecture to demonstrate the technique of logical relations:
Theorem 1. If $\vdash e: \forall \alpha.\, \alpha\rightarrow\alpha$ and $\vdash \tau$ and $\vdash v:\tau$, then $e[\tau]\ v \hookrightarrow^* v$.
Theorem 2. If $\vdash e: \forall \alpha.\, \alpha\rightarrow bool$, $\vdash \tau_1 $, $\vdash \tau_2$, $\vdash v_1:\tau_1$, $\vdash v_2:\tau_2$, then $e[\tau_1]\ v_1 = e[\tau_2]\ v_2$.
The idea is to define logical relations such that contextual equivalent terms can be related by hypothesis. Let's first define value interpretations for some closed types:
$\V[bool]=\{\ (true,true),\ (false,false)\ \}$
The slogan of LRs for function types is "You give me related inputs; I give you related outputs." Do not confuse this with Theorem 2, where the two inputs are not required to be related.
$\V[\tau\rightarrow\tau']=\{\ (\lambda x:\tau.\, e_1,\lambda x:\tau.\, e_2)\ |\ \forall (v_1, v_2)\in \V[\tau].\, (e_1[v_1/x], e_2[v_2/x]) \in \E[\tau']\ \}$
The interpretation for polymorphic types is new.
$\V[\forall \alpha.\, \tau]=\{\ (\Lambda \alpha.\,e_1, \Lambda \alpha.\,e_2)\ |\ \forall \tau_1, \tau_2.\, (e_1[\tau_1/\alpha], e_2[\tau_2/\alpha]) \in \V[\tau](\rho[\alpha\mapsto(\tau_1, \tau_2)])\ \}$
Note that $\tau_1[\tau'/\alpha]$ and $\tau_2[\tau'/\alpha]$ are different types. Hence we relate them with a LR for parametric type $\tau$, and use $\rho$ (called a relational substitution) to remember the types $\tau_1,\ \tau_2$ picked for type parameter $\alpha$. In general, a relational substitution is in form of $\{\alpha_1\mapsto(\tau_{11},\tau_{12}), \alpha_2\mapsto(\tau_{21},\tau_{22}), ... \}$. We shall write $\V[\tau](\rho)$ to express the fact that $\V[\tau]$ is parametrized by substitution $\rho$, assuming that $dom(\rho)\supseteq FTV(\tau)$.
$\V[\alpha]=\{\ (\tau_1, \tau_2)\ |\ \rho(\alpha)=(\tau_1, \tau_2)\ \}$
(to be continued)

Logical relations as a proof technique — Part II

\( \def\[#1]{[\![\,#1\,]\!]} \def\V[#1]{\mathcal{V}\,[\![#1]\!]} \def\E[#1]{\mathcal{E}\,[\![#1]\!]} \def\G[#1]{\mathcal{G}\,[\![#1]\!]} \)

This is the part II of my lecture note based on the lecture series "Logical Relations" given by Amal Ahmed at Oregon Programming Languages Summer School, 2015. See here for the Part I of this note.

Type safety. The slogan for type safety is "if a term is well-typed, it won't get stuck." Formally, this means that if $\vdash e:\tau$ and $e\hookrightarrow^* e'$, then either $e'$ is a value, or there exists $e''$ such that $e'\hookrightarrow e''$. Note that type safety doesn't require termination, and thus is weaker than strong normalization we proved earlier. On the other hand, type safety can be proved for Turing-complete languages such as STLC with recursive types (whereas strong normalization can not).
A well-known approach to prove type safety is via proving progress and preservation (note that these are proof methods for type safety, not the definition of it):
Progress lemma. If $\vdash e:\tau$, then either $e'$ is a value, or $\exists e''.\, e'\hookrightarrow e''.$
Preservation lemma. If $\vdash e:\tau$ and and $e'\hookrightarrow e''$, then $\vdash e'':\tau$.
Once these lemmas are established, type safety can be proved easily by induction. In this lecture, however, we shall use logical relations instead of the above lemmas to prove type safety.

We need a bunch of definitions before we proceed. Define that $val(e)$ holds iff $e$ is a value; $red(e)$ holds iff $\exists e'.\, e\hookrightarrow e'$; $safe(e)$ holds iff $\forall e'.\, e \hookrightarrow^* e' \implies red(e') \vee val(e')$. Now the definition of type safety can be stated as $\vdash e:\tau \implies safe(e)$. Recall that to prove strong normalization, we introduced a logical predicate $SN_\tau$ and used it to break statement $\vdash e:\tau \implies e\Downarrow$ into $\vdash e:\tau \implies SN_\tau(e)$ and $SN_\tau(e) \implies e\Downarrow$. Here we shall adopt a similar strategy. To begin with, we define the value interpretations of type-safe values and closed expressions as
$\V[bool] = \{\ false,\, true\ \}$
$\V[\tau\rightarrow\tau']=\{\ \lambda x:\tau.\, e\ |\ \forall v \in \V[\tau].\, e[v/x] \in \E[\tau']\ \}$
$\E[\tau]=\{\ e\ |\ \forall e'.\, e \hookrightarrow e' \implies red(e') \vee e' \in \V[\tau]\ \}$
Now, to prove $\vdash e:\tau \implies safe(e)$, it suffices to prove that $\vdash e:\tau \implies e \in \E[\tau]$ and $e \in \E[\tau] \implies safe(e)$. As before, the main difficulty lies in proving the first part, since the second follows immediately from the definition of $\E[\tau]$. Also, while we are proving type safety for closed terms, we need to use a hypothesis about open terms so as to apply induction to lambda expressions. For this purpose, we define a value interpretation for environments as follows:
$\G[\emptyset] = \{\emptyset\}$
$\G[\,\Gamma, x:\tau\,] = \{\ \gamma[x\mapsto v]\ |\ \gamma \in \G[\Gamma] \wedge v \in \V[\tau]\ \}$
Hence, a substitution $\gamma$ is in $\G[\Gamma]$ iff it maps variables to values that are type-safe and consistent with $\Gamma$. An expression is called semantically type-safe in $\Gamma$, written as $\Gamma \models e:\tau$, if and only if $\gamma(e) \in \E[\tau]$ for all substitutions $\gamma \in \G[\Gamma]$. That is, $\Gamma \models e:\tau$ iff $e$ always reduces to a type-safe closed term after its free variables are replaced by type-safe values consistent with $\Gamma$.
As mentioned above, to prove type-safety it suffices to show A) $\vdash e:\tau \implies \models e:\tau$, and B) $\models e:\tau \implies safe(e)$. Part A says that the syntactic notion of type safety (ie., well-typedness) implies a semantic notion of type safety which says that a term will not get stuck in execution. It is in fact a special case of the so-called "Fundamental Property" of logical relation $\ \Gamma \vdash e:\tau \implies \Gamma \models e:\tau$. Part B can be shown directly as follows. Recall that $safe(e)$ holds iff $\forall e'.\, e \hookrightarrow^* e' \implies red(e') \vee val(e')$. Suppose that $e \hookrightarrow^* e'$. If $\models e:\tau$, then we have $e\in \E[\tau]$ since $\emptyset(e)=e$. But this means $red(e') \vee e' \in \V[\tau]$, that is, $e'$ is reducible or $e'$ is a value. This concludes the proof.
You can see here and in the example of strong normalization that the property of interest follows almost immediately from the definition of the logical relations we use. This is often the case if you construct suitable logical relations to assist your proof.
Now we are going to prove the Fundamental Property, i.e., $\Gamma \vdash e:\tau \implies \Gamma \models e:\tau$. As we did in the proof of strong normalization, we perform induction on the type derivations case by case.


(to be continued)

Logical relations as a proof technique — Part I

This is the part I of my lecture note based on the lecture series "Logical Relations" given by Amal Ahmed at Oregon Programming Languages Summer School, 2015. See here for Part II.

Overview. These lectures will introduce the proof method of logical relations. Logical relations have been used to prove a wide range of properties, including normalization, type safety, equivalence of programs, non-interference (in security typed languages), and compiler correctness. We will start by looking at how to prove normalization and type safety for the simply-typed lambda calculus (STLC). We will then add recursive types to STLC and develop a step-indexed logical relation, using step-indexing to ensure that the logical relation remains well-founded. We will cover polymorphic and existential types and develop a logical relation to reason about the associated notions of parametricity and representation independence. The lectures will also discuss how to establish that a logical relation corresponds to contextual equivalence.

Free theorems. In parametric polymorphism, types cannot be checked, inspected or instantiated by programs. Hence, programs with polymorphic types don't change behaviors according to their type parameters. It follows that all functions of type $\forall a.\, a \rightarrow a$ are identity functions, since nothing but the argument can be returned by the function. Similarly, all functions of type $\forall a.\, a \rightarrow Int$ are constant functions. In contrast, there doesn't exist a function of type $\forall a.\, Int \rightarrow a$, since the return value can be obtained from nowhere. Results of this kind are called free theorems, and many of them can be proved using logical relations.

Logical predicates. Unary logical relations are also called logical predicates. They are used to assert properties of one single program, such as termination. In contrast, binary logical relations are used to assert relations between two programs, such as equivalence. Note that we only put closed programs in a logical relation. By and large, to prove that a well-typed and closed term $e$ has some special property, we shall set up a predicate $P_\tau$ such that $P_\tau(e)$ holds if and only if all of the following conditions hold: i) $\vdash e: \tau$, ii) $e$ has the property of interests, and iii) the property of interests is preserved by elimination forms (or introduction forms) of type $\tau$.

Strong normalization. In history, logical relations first appeared as a technique to prove strong normalization, which means that a well-typed term always reduces to the same value regardless of the strategies of evaluation. Since typing rules in STLC are deterministic, proving strong normalization for STLC amounts to showing that every well-typed program terminates, that is, $\vdash e:\tau \implies e \Downarrow$. Observe that this statement cannot be proved by applying structural induction on typing derivations directly. The problem of induction occurs at the application rule: we cannot conclude $e_1\ e_2\Downarrow$ from $e_1 \Downarrow$ and $e_2 \Downarrow$. Nevertheless, this problem can be resolved by using a stronger induction hypothesis, which leads to the following definition of logical predicates.
We shall set up a predicate $SN_\tau(\cdot)$ such that $SN_\tau(e)$ holds only if term $e$ has type $\tau$ and is strongly normalizing. We consider two types for STLC: boolean and function types. For boolean, it suffices to define that $SN_{bool}(e)$ holds iff $\vdash e:bool \wedge e \Downarrow$, since boolean doesn't has elimination forms. For functions types, we define that $SN_{\tau\rightarrow\tau'}(e)$ holds iff

$\vdash e':\tau\rightarrow\tau'\quad\wedge\quad e' \Downarrow\quad \wedge\quad (\forall e.\, SN_{\tau}(e) \implies SN_{\tau'}(e'\ e))$.

(1)

We shall see that this definition provides the strengthened hypothesis we need to deal with the application rule. The proof of $\vdash e:\tau \implies e \Downarrow$ now breaks into two parts: A) $\vdash e:\tau \implies SN_{\tau}(e)$, and B) $SN_{\tau}(e) \implies e \Downarrow$. Part B follows immediately from the definition of $SN_\tau(e)$. It remains to prove part A, and we rely on structural induction to do this. But again, we cannot use the statement $\vdash e:\tau \implies SN_{\tau}(e)$ we are going to prove as an induction hypothesis. It only asserts closed terms, but to show that it holds for terms of function type, say, for $(\lambda x:\tau.\, e'): \tau \rightarrow \tau'$, we need the hypothesis to hold for open term $e'$ so as to perform induction.
Instead, we shall use the following stronger claim as an induction hypothesis. Given a mapping $\gamma$ from variables to values, we write $\gamma \models \Gamma$ when $dom(\gamma)=dom(\Gamma)$ and $\forall x\in dom(\Gamma).\, SN_{\Gamma(x)}(\gamma(x))$ holds. That is, $\gamma$ maps variables in $dom(\Gamma)$ to values that strongly normalize with types compatible with $\Gamma$. We claim that for any term $e$ and substitution $\gamma$,

$\Gamma \vdash e:\tau \wedge \gamma \models \Gamma  \implies SN_{\tau}(\gamma(e))$.

(2)

It is clear that part A follows from this claim by setting $\Gamma$ to be empty. Now we shall prove (2) by inducting on the derivation rules case by case.
Case $\quad\rhd\ \ \vdash true: bool\quad$ and $\quad\rhd\ \ \vdash false: bool$.
　Note that $\gamma(x)=x$ for $x\in \{\,true,\,false\,\}$, which is of course strongly normalizing.
Case $\quad\Gamma(x)=\tau\ \ \rhd\ \ \Gamma \vdash x:\tau$.
　By premises $\Gamma(x)=\tau$ and $\gamma\models\Gamma$, $\gamma(x)$ has type $\tau$. Thus $SN_{\tau}(\gamma(x))$ holds by $\gamma\models\Gamma$.
Case $\quad\vdash e': \tau\rightarrow\tau'$, $\vdash e: \tau\ \ \rhd\ \ \vdash e'\ e: \tau'$.
　Note that $\gamma(e'\ e)=\gamma(e')\ \gamma(e)$. By premise $\gamma\models\Gamma$, both $SN_{\tau\rightarrow\tau'}(\gamma(e'))$ and $SN_{\tau}(\gamma(e))$ holds by induction. Thus $SN_{\tau'}(\gamma(e')\ \gamma(e))$, which equals to $SN_{\tau'}(\gamma(e'\ e))$, holds by (1).
Case $\quad\Gamma, x:\tau \vdash e':\tau'\ \ \rhd\ \ \Gamma\vdash\lambda x:\tau.\, e': \tau\rightarrow\tau'$.
　 This is the case we got stuck with before introducing logical predicates, so it is not surprising that the proof for this case is far more complicated than others. Before we proceed, we need the following two lemmas:
Lemma 1. (substitution lemma) If $\Gamma \vdash e:\tau$ and $\gamma \models \Gamma$, then $\Gamma \vdash \gamma(e):\tau.$
Lemma 2. (SN is preserved by forward/backward reductions) Suppose that $\vdash e:\tau$ and $e \hookrightarrow e'$. Then $SN_{\tau}(e)$ holds if and only if $SN_{\tau}(e')$ holds.
To prove (2), i.e., $\Gamma \vdash \lambda x:\tau.\, e' \wedge \gamma\models\Gamma$ implies $SN_{\tau\rightarrow\tau'}(\gamma(\lambda x:\tau.\, e'))$, it suffices to prove the following three statements:
1) $\gamma(\lambda x:\tau.\, e')$ has type $\tau\rightarrow\tau'$. This follows by premise $\gamma\models \Gamma$ and Lemma 1;
2) $\gamma(\lambda x:\tau.\, e')\Downarrow$. This is obvious, since $\gamma(\lambda x:\tau.\, e')=\lambda x:\tau.\,\gamma(e')$ is a lambda value;
3) $\forall e.\,SN_\tau(e)\implies SN_{\tau'}(\gamma(\lambda x:\tau.\, e')\ e)$. By induction, we know that $\Gamma, x:\tau \vdash e':\tau'$ and $\gamma'\models \Gamma, x:\tau$ implies $SN_{\tau'}(\gamma'(e'))$. Suppose that $SN_\tau(e)$ holds for some $e$. Then $e\Downarrow v$ for some value $v$, and $SN_{\tau}(v)$ holds by Lemma 2. Given premises $\Gamma \vdash \lambda x:\tau.\, e'$ and $\gamma\models\Gamma$, define $\gamma'=\gamma[x \mapsto v]$. Note that $\gamma'\models\Gamma,x:\tau$. Thus $SN_{\tau'}(\gamma'(e'))$ holds by induction. However, note that
$\gamma'(e')=\gamma(e')[x \mapsto v]=(\lambda x:\tau.\,\gamma(e'))\ v=\gamma(\lambda x:\tau.\,e')\ v$.
It then follows from $SN_{\tau'}(\gamma'(e'))$ and Lemma 2 that $SN_{\tau'}(\gamma(\lambda x:\tau.\,e')\ e)$ holds. This concludes our proof of strong normalization for STLC.

(End of lecture note Part I. See here for Part II.)