Download Version 2

of modularity is not only a practical inconvenience for the language designer because it more than
doubles the number of derivation rules in ones language definition, but it does not scale either.
Consider now also adding parametric exceptions, return to functions, break/continue to loops, etc.
Each of these will more than double again the number of rules, not to mention that they may
interfere in rather unexpected ways.
Moreover, from a computational granularity perspective, big-step and/or small-step SOS definitions of control-intensive statements such as halt are not entirely correct: they fail to capture
the intended computational granularity of these statements, which, like their functional behavior,
is an important component of their formal semantics. Indeed, the intended semantics of halt(E) is
“evaluate E to a value V and then return V as the result of the entire program”; compare that with
“evaluate E to a value V and then propagate a halting signal with V through all the remaining
statements until none left and then return V as the result of the entire program”, which is how
halt is defined in big-step or small-step SOS.
As already seen in previous sections, control-intensive statements present no difficulty in K. Like
in context reduction or other continuation-based approaches, in K we maintain the control of the
program explicit as part of the state infrastructure, so contextual rules defining the semantics of
control-intensive constructs can easily store, remove or modify the control context of the program.
This allows for an increased modularity of language definitions, because no “propagation” rules
of control-changing signals are needed; in particular, as shown at the botom of Figure 2 the Ksemantics of halt consists of precisely one rule, which stops the program with the desired value in
one computational step, exactly as expected.
8.5.3
On Orthogonality of Language Features
Let us now discuss in more depth the subtle issue of when two or more language features are “unrelated” or orthogonal, which is the criterion that we use informally to characterize the modularity
of language definitional frameworks: a framework is modular when the addition of a new language
construct does not require one to modify the definition of any of the existing, “unrelated” language features. At one extreme, one could say that programming languages are monolithic, in the
sense that any feature is related to any other feature in the language, in which case the concept of
modularity is superfluous because any definition of the language in any framework is modular.
At another extreme, one could say that all language features should be orthogonal to each
other, in which case modularity becomes again a non-issue because no open-ended language design
can be modular: one can always add features to a language that interact in previously unexpected
ways with other features. For example, one can add dynamic aspects to an otherwise pure objectoriented programming language, in which case additional code may need to be executed when
certain events take place, such as, e.g., returns from method calls or updates of values stored
at particular locations. Another common example would be the addition of concurrency to a
language whose functions are allowed to terminate abruptly with return statemens; if one decides
that all locks acquired during the execution of a function should be automatically released when the
function is terminated with a return (which is actually a “must” if locks are acquired and released
via “synchronized (Lock) {Code}” blocks, like in Java), then the previous definition of the function
call originally designed for a sequential language is not orthogonal to the addition of concurrency
and locks: indeed, it needs to be changed to account for the release of the locks accumulated since
the function was called.
We believe that the related notions of orthogonality and modularity of language features are
85