Wednesday, July 25, 2012

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. 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 maps variables to values (parameters to their arguments), and is called the environment.

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. 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 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. 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. In addition, all of the above rules have a side condition requiring . Next, we add a rule to handle the case. Finally, we add the usual rules for propagating errors such as this time out.

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. (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 . 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.

2 comments:

  1. I did a double take on the statement 42 3 because it looked to me like 423. You might want to increase the space to \: or even \;.

    Typo: JarosłAw should be Jarosław.

    ReplyDelete