Big-step, diverging or stuck?

In a naive big-step semantics, one can't tell the difference between the following two programs, even though their behavior is quite different according to single-step reduction rules. $$\mathsf{fix}\,(\lambda f. \lambda y. f \, y)\,3$$ $$42 \;\, 3$$ The first program diverges (runs forever) whereas the second program is stuck, that is, it results in a run-time type error because you can't perform function application with a number in the function position. However, a naive big-step semantics is undefined for both programs. That is, you can't build a derivation of the evaluation relation for either program.

The naive big-step semantics that I'm referring to is the following. The $\rho$ maps variables to values (parameters to their arguments), and is called the environment. $$\rho \vdash x \Downarrow \rho(x) \qquad \rho \vdash \lambda x. e \Downarrow \langle \lambda x.e , \rho \rangle \\[2ex] \frac{ \begin{array}{c} \rho \vdash e_1 \Downarrow \langle \lambda x.e', \rho' \rangle \quad \rho \vdash e_2 \Downarrow v' \\ \rho'[x\mapsto v'] \vdash e' \Downarrow v \end{array} }{ \rho \vdash e_1 \, e_2 \Downarrow v } \\[3ex] \frac{ \rho \vdash e \Downarrow \langle \lambda f. e', \rho' \rangle \quad \rho'[f\mapsto \langle \lambda f. e', \rho' \rangle] \vdash e' \Downarrow v }{ \rho \vdash \mathsf{fix}\, e \Downarrow v }$$

Trouble formulating type safety

This inability to distinguish between divergence and stuck makes it difficult to formulate type safety using a naive big-step semantics. The following statement is true but not very strong. $$\text{If } \emptyset \vdash e : T \text{ and } \emptyset \vdash e \Downarrow v \text{ then } \emptyset \vdash v : T.$$ It captures the notion of type preservation, but not progress. That is, the above does not rule out the possibility of type errors because the premise $\emptyset \vdash e \Downarrow v$ is false in such cases, making the entire statement vacuously true. On the other hand, the following statement is so strong that it is false. $$\text{If } \emptyset \vdash e : T \text{ then } \emptyset \vdash e \Downarrow v \text{ and } \emptyset \vdash v : T \text{ for some } v.$$ One counter-example to the above statement is the diverging program above. The program is well typed, but it does not terminate and return a value.

Several textbooks stop at this point and just say that the above is a problem with big-step semantics. Not true! There are several solutions to this problem in the literature. I've included papers that address the divergence/stuck issue at the bottom of this blog. If you know of others, please let me know! The solutions I've seen fall into three categories:

• Introduce a separate co-inductive definition of divergence for the language in question.
• Develop a notion of partial derivations.
• Add a time counter that causes a time-out error when it gets to zero. That is, make the semantics step-indexed.

Of the three kinds of solutions, the counter-based solution is the simplest, and it gets the job done, so I won't discuss the other two. I first learned of this approach from the paper A Virtual Class Calculus by Ernst, Ostermann, and Cook.

Big-step Semantics with Counters

The first part of the solution is to augment the big-step semantics with a counter k, making sure to decrement the counter in the premises of each rule. $$\rho; k \vdash x \Downarrow \rho(x) \qquad \rho; k \vdash \lambda x. e \Downarrow \langle \lambda x.e , \rho \rangle \\[2ex] \frac{ \begin{array}{c} \rho; k-1 \vdash e_1 \Downarrow \langle \lambda x.e', \rho' \rangle \quad \rho; k-1 \vdash e_2 \Downarrow v' \\ \rho'[x\mapsto v']; k-1 \vdash e' \Downarrow v \end{array} }{ \rho; k \vdash e_1 \, e_2 \Downarrow v } \\[3ex] \frac{ \rho; k-1 \vdash e \Downarrow \langle \lambda f. e', \rho' \rangle \quad \rho'[f\mapsto \langle \lambda f. e', \rho' \rangle]; k-1 \vdash e' \Downarrow v }{ \rho; k \vdash \mathsf{fix}\, e \Downarrow v }$$ In addition, all of the above rules have a side condition requiring $k > 0$. Next, we add a rule to handle the $k = 0$ case. $$\rho; 0 \vdash e \Downarrow \mathsf{TimeOut}$$ Finally, we add the usual rules for propagating errors such as this time out. $$\frac{ \rho; k-1 \vdash e_1 \Downarrow \mathsf{TimeOut} }{ \rho; k \vdash e_1 \, e_2 \Downarrow \mathsf{TimeOut} } \\[3ex] \frac{ \rho; k-1 \vdash e_1 \Downarrow \langle \lambda x.e', \rho' \rangle \quad \rho; k-1 \vdash e_2 \Downarrow \mathsf{TimeOut} }{ \rho; k \vdash e_1 \, e_2 \Downarrow \mathsf{TimeOut} } \\[3ex] \frac{ \begin{array}{c} \rho; k-1 \vdash e_1 \Downarrow \langle \lambda x.e', \rho' \rangle \quad \rho; k-1 \vdash e_2 \Downarrow v' \\ \rho'[x\mapsto v']; k-1 \vdash e' \Downarrow \mathsf{TimeOut} \end{array} }{ \rho; k \vdash e_1 \, e_2 \Downarrow \mathsf{TimeOut} }\\[3ex] \frac{ \rho; k-1 \vdash e \Downarrow \mathsf{TimeOut} }{ \rho; k \vdash \mathsf{fix}\, e \Downarrow \mathsf{TimeOut} }$$

With the addition of the counter, we can always build a derivation for a diverging program, with the result being a time out, no matter how high you set the counter to begin with. However, for a program that gets stuck, there will be some starting counter that is high enough so that you can't build a derivation anymore (you might have been able to get time outs with lower values).

The type safety theorem can now be stated in a way that is both strong enough and true! Let r range over both values and the time out. $$\text{For any } k, \text{ if } \emptyset \vdash e : T \text{ then } \emptyset; k \vdash e \Downarrow r \text{ and } \emptyset \vdash r : T \text{ for some } r.$$ (We let the time out take on any type.) At first glance this statement might seem weak. If the counter k is 0, then its trivial to build a derivation of $\emptyset; k \vdash e \Downarrow r$. However, note that the statement says for any k. Thus, if the program get's stuck, there will be some value for k for which you can't build a derivation, making the above statement false. So this indeed is a good formulation of type safety. If the above holds, then no well-typed program will get stuck!

One parting comment. The addition of propagation rules was rather annoying. I'll discuss how to avoid propagation rules in big-step semantics in an upcoming blog post, summarizing a talk I gave at Scottish Programming Languages Seminar in 2010.

References

• C. A. Gunter and D. Rémy. A Proof-Theoretic Assesment of Runtime Type Errors. AT&T Bell Laboratories Technical Memo 11261-921230-43TM, 1993.
• A. Stoughton. An operational semantics framework supporting the incremental construction of derivation trees. Electr. Notes Theor. Comput. Sci., 10, 1997.
• H. Ibraheem and D. A. Schmidt. Adapting big-step semantics to small-step style: Coinductive interpretations and “higher-order” derivations. In Second Workshop on Higher-Order Techniques in Operational Semantics (HOOTS2). Elsevier, 1997.
• Kathleen Fisher and John Reppy. Statically typed traits. University of Chicago, technical report TR-2003-13, December 2003.
• Erik Ernst, Klaus Ostermann, and William R. Cook. A Virtual Class Calculus. In POPL 2006.
• Xavier Leroy and Herve Grall. Coinductive big-step operational semantics. Journal of Information and Computation. Vol. 207, Issue 2, February 2009.
• Big-step Operational Semantics Revisited, by Jarosław Dominik, Mateusz Kuśmierek, and Viviana Bono. In Fundamenta Informaticae Volume 103, Issue 1-4, January 2010.