Total Definitional Interpreters for Looping Programs

Total Definitional Interpreters for Looping Programs
Nils Anders Danielsson
Draft, 2018. [pdf, highlighted Agda code, zip file with code]

Abstract

A question has been raised regarding how useful total definitional interpreters are in a setting in which programs run forever. For instance, is it possible to give a semantics in the form of a total definitional interpreter in such a way that one can distinguish between non-terminating programs that run in bounded space and those that do not? Here it is shown that this is possible.

The main object of study is an untyped λ-calculus with named recursive definitions. The semantics of this language is specified using a ‶big-step″ definitional interpreter, using the delay monad to ensure that the definition is a total function. A (provably correct) compiler is given to the language of a virtual machine with tail calls, which is specified using a ‶small-step″ definitional interpreter. A big-step definitional interpreter which is instrumented with information about stack sizes is also given for the λ-calculus, and these stack sizes are shown to agree with those encountered by the virtual machine. Two non-terminating programs are presented, and it is shown that one runs in bounded stack space, and that the other does not.

The development is accompanied by machine-checked proofs.