[proofplan] We prove the result by induction on the derivation of the closed typing judgment $\varnothing \vdash t:A$. The variable case is impossible because no variable can be typed in the empty context. The abstraction case is immediate because abstractions are exactly the values. In the application case, the induction hypotheses classify the function and argument subterms; if either subterm can step, the corresponding call-by-value congruence rule gives a step of the whole application, and if both are values, the function value must be a lambda abstraction, so call-by-value beta-reduction applies. [/proofplan] [step:Induct on the closed typing derivation] Fix a term $t \in \textsf{Tm}$ and a type $A \in \textsf{Ty}$ with \begin{align*} \varnothing \vdash t:A. \end{align*} We prove, by induction on the given typing derivation, the assertion \begin{align*} \mathcal{P}(t,A) := \text{$t$ is a value or there exists $t' \in \textsf{Tm}$ such that $t \to t'$}. \end{align*} The induction is legitimate because the typing derivation is finite and each typing rule has premises whose derivations are proper subderivations of the conclusion derivation. [guided] Fix a closed typing derivation \begin{align*} \varnothing \vdash t:A. \end{align*} The word “closed” is important: it means that the context is the empty context $\varnothing$, so the term has no free variables that can be supplied by assumptions. We prove the proposition \begin{align*} \mathcal{P}(t,A) := \text{$t$ is a value or there exists $t' \in \textsf{Tm}$ such that $t \to t'$} \end{align*} by induction on the typing derivation of $\varnothing \vdash t:A$. This is structural induction on derivations, not induction on the textual size of $t$. The reason this is the right induction is that every possible final typing rule gives exactly the syntactic form of $t$ that must be analyzed: variable, abstraction, or application. Since each premise of a typing rule has a smaller derivation than its conclusion, the induction hypotheses are available precisely for the immediate subterms appearing in the final typing rule. [/guided] [/step] [step:Exclude the variable case using emptiness of the context] Suppose the last rule of the derivation is the variable rule. Then $t$ has the form $x$ for some variable $x$, and the variable rule requires an assumption $x:A$ in the typing context. The context is $\varnothing$, so there is no such assumption. Hence the variable case cannot occur. [/step] [step:Conclude immediately in the abstraction case] Suppose the last rule of the derivation is the abstraction rule. Then $t$ has the form \begin{align*} \lambda x:B.\,u \end{align*} for some variable $x$, some type $B \in \textsf{Ty}$, and some term $u \in \textsf{Tm}$. By the definition of value in this calculus, every lambda abstraction is a value. Therefore $t$ is a value, so $\mathcal{P}(t,A)$ holds. [/step] [step:Analyze applications by the induction hypotheses] Suppose the last rule of the derivation is the application rule. Then there are terms $r,s \in \textsf{Tm}$ and a type $B \in \textsf{Ty}$ such that \begin{align*} t = r\,s, \end{align*} and the premises of the final typing rule are \begin{align*} \varnothing \vdash r:B \to A \end{align*} and \begin{align*} \varnothing \vdash s:B. \end{align*} By the induction hypothesis applied to the first premise, either $r$ is a value or there exists $r' \in \textsf{Tm}$ such that $r \to r'$. If $r \to r'$, then the function-position congruence rule for call-by-value reduction gives \begin{align*} r\,s \to r'\,s. \end{align*} Thus $t$ steps. It remains to consider the case where $r$ is a value. By the induction hypothesis applied to the second premise, either $s$ is a value or there exists $s' \in \textsf{Tm}$ such that $s \to s'$. If $s \to s'$, then, since $r$ is a value, the argument-position congruence rule gives \begin{align*} r\,s \to r\,s'. \end{align*} Thus $t$ steps. Finally suppose both $r$ and $s$ are values. Since values are exactly lambda abstractions and $r$ is a value, there are a variable $x$, a type $C \in \textsf{Ty}$, and a term $u \in \textsf{Tm}$ such that \begin{align*} r = \lambda x:C.\,u. \end{align*} The application is well typed with $r$ of function type $B \to A$, and the argument $s$ is a value, so the call-by-value beta-reduction rule applies and yields \begin{align*} (\lambda x:C.\,u)\,s \to u[s/x]. \end{align*} Since $t = r\,s$, there exists a term $t' \in \textsf{Tm}$, namely \begin{align*} t' = u[s/x], \end{align*} such that $t \to t'$. [guided] Now assume the final typing rule is application. Then the term being typed has the form $r\,s$ for terms $r,s \in \textsf{Tm}$. Because the conclusion is \begin{align*} \varnothing \vdash r\,s:A, \end{align*} inversion of the application typing rule gives a type $B \in \textsf{Ty}$ such that \begin{align*} \varnothing \vdash r:B \to A \end{align*} and \begin{align*} \varnothing \vdash s:B. \end{align*} The induction hypothesis applies to both premise derivations because both premises have smaller typing derivations than the application conclusion. Applying it to $\varnothing \vdash r:B \to A$, we get two possibilities. First, suppose there exists $r' \in \textsf{Tm}$ such that \begin{align*} r \to r'. \end{align*} Then the call-by-value function-position congruence rule permits reduction of the function part before inspecting the argument. Therefore \begin{align*} r\,s \to r'\,s. \end{align*} Since $t = r\,s$, this proves that $t$ can step. The remaining possibility from the first induction hypothesis is that $r$ is a value. In call-by-value evaluation, the argument position may step only after the function position is already a value, so this is exactly the condition needed to use the argument congruence rule. Applying the induction hypothesis to \begin{align*} \varnothing \vdash s:B, \end{align*} we again get two possibilities. If there exists $s' \in \textsf{Tm}$ such that \begin{align*} s \to s', \end{align*} then, because $r$ is a value, the argument-position congruence rule gives \begin{align*} r\,s \to r\,s'. \end{align*} Thus $t$ can step in this case as well. It remains only to handle the case where both $r$ and $s$ are values. The definition of values in this calculus says that the values are exactly the lambda abstractions. Since $r$ is a value, there exist a variable $x$, a type $C \in \textsf{Ty}$, and a term $u \in \textsf{Tm}$ such that \begin{align*} r = \lambda x:C.\,u. \end{align*} The term $s$ is also a value, so the hypothesis required by the call-by-value beta rule is satisfied. Therefore \begin{align*} (\lambda x:C.\,u)\,s \to u[s/x]. \end{align*} Substituting $r = \lambda x:C.\,u$ and $t = r\,s$, we obtain a term \begin{align*} t' = u[s/x] \end{align*} with \begin{align*} t \to t'. \end{align*} So in every application subcase, the application either steps because one of its subterms steps, or it steps by beta-reduction once both subterms are ready. [/guided] [/step] [step:Assemble the cases to obtain progress] The induction has covered every possible final typing rule for a derivation in the calculus: the variable case is impossible in the empty context, the abstraction case produces a value, and the application case either produces a one-step reduct or reduces by beta-reduction. Hence, for every $t \in \textsf{Tm}$ and $A \in \textsf{Ty}$ satisfying \begin{align*} \varnothing \vdash t:A, \end{align*} the term $t$ is a value or there exists $t' \in \textsf{Tm}$ such that \begin{align*} t \to t'. \end{align*} This is the desired progress property. [/step]