Partial Semantics

I'm starting to notice a few instances of semantic aspects of programming languages that are only partially captured by formal semantics.

Each case deals with some aspect of the runtime or evaluation strategy which has no effect on the partial correctness (or “partial behavior”) of the program, but does influence its termination behavior or change its space complexity in a manner which puts at risk the “effective termination” of the program (ie whether it terminates before allocating an “unreasonable” amount of memory for some definition of “unreasonable”).

Laziness

(see my thoughts on laziness)

Programs which are total (ie Coq programs) will terminate under any evaluation strategy (ie ML or Haskell).

Some programs are not total, but will terminate under certain evaluation strategies (for example, programs which take a finite number of elements from an infinite list). These programs fail to terminate under certain evaluation strategies (ie strict evaluation).

Therefore, the laziness of the runtime is part of the partial semantics of the language: changing the laziness of the runtime will never alter the partial correctness of a program, but it might make a program fail to terminate.

Tail Call Space Complexity

Some programs are written in such a manner that they will require only constant space if the runtime implements zero-space tail calls (effectively: does not create a call stack record). When such programs are executed under a runtime that uses nonzero-space tail calls (effectively: creates a call stack record), their space consumption changes from O(1) to some asymptotically larger function. Often this asymptotically larger function is “effectively impractical” in the sense that no reasonable computer actually has that much storage, and the program will never finish execution on a reasonable computer.

rendered from WIX