search

ilya-klyuchnikov / tapl-scala

Code from the book "Types and Programming Languages" in Scala
175 stars 22 forks source link

Small-step interpreter in chapter 3-4 diverges unexpectedly #5

Closed svenkeidel closed 4 years ago

svenkeidel commented 4 years ago

Hi,

I added some tests for the interpreters in chapter 3-4 of the book. In this process I found a small issue with the small-step interpreter. In particular, it does not terminate for expressions such as iszero false, because of this small-step transition:

 case TmIsZero(t1) =>
      val t2 = eval(t1)
      TmIsZero(t2)

I fixed this issue by requiring that t1 is not a value. Then the interpreter throws an NoRulesApply exception as expected.

Regards, Sven

ilya-klyuchnikov commented 4 years ago

Thanks! A good catch. I have just checked - the same logic is in the original TAPL code (https://www.cis.upenn.edu/~bcpierce/tapl/checkers/).

A good non-trivial educational example. This small-step interpreter doesn't diverge for well-typed programs, but does diverge (instead of doing dynamic check) for some ill-typed programs.

svenkeidel commented 4 years ago

Well, actually the real problem is that the rule for iszero uses eval instead of eval1. eval is the reflexive transitive closure of eval1 and hence false can step to false.

When you replace eval with eval1 then the term iszero false is indeed stuck. Here is the fix: https://github.com/svenkeidel/tapl-scala/commit/0f37c4bf7778cb35c5f41fd1590ee481b402fdd2

Sorry that I did not see this right away.

ilya-klyuchnikov commented 4 years ago

NP. Pushed.