Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle - Correct System Design: Recent Insights and Advances - page 23

programming language that was presented by an operational semantics. A recent
model [Abramsky, Hyland] represents a type of a programming language by the
rules of a two-person game, and a function by a strategy for playing the game. A
large and complex collection of healthiness conditions is imposed on the games
and strategies to ensure that every strategy that satises them can be denoted
by a program expressed in the syntax of PCF. It is generally considered sucient
to prove this just for nite games, which correspond to programs that do not
use recursion or any other form of unbounded iteration. That is the best that
can be done, because it is impossible within an abstract model to formulate
healthiness conditions that will select exactly those sets of observations that are
implementable as iterative programs.
In the practical development and analysis of programs, it is quite uncom-
mon to make a direct appeal to the denition of the programming language,
whether denotational or operational. Much more useful are theorems that have
been based on those denitions; many of these take the form of algebraic laws,
either proven from denitions or postulated as healthiness conditions. The im-
portance of laws is recognised both by top-downers and by bottom-uppers, who
measure progress in their chosen direction by accumulation of larger collections
of useful laws. When both theories have been adequately developed, I suggest
that an appropriate measure of successful meeting in the middle is provided by
the overlap of the two collections of laws. Adjustments can (and should) then
be made to the details of both theories, until the overlap is suciently broad to
meet all the needs of practice. If the practitioner uses just the appropriate laws
in the appropriate circumstances, the merits of both approaches can be safely
combined.
In a perfect meeting, the laws derived from the top-down and from the
bottom-up would be exactly the same. In fact, this is not necessary. All that
is needed is that the operationally dened axioms and laws should be a subset
of those provable from the denotational denitions. Then all the remaining laws
proveable from the denotations will be contextual equivalences. The existence of
the denotational model guarantees their consistency, even without the need for
an exhaustive inductive argument on contexts.
Identity of dierently derived theories is not the only goal; and when applying
the same derivational techniques to dierent programming paradigms, dierences
in the algebraic laws are to be expected and even welcomed. It turns out that
a great many algebraic laws are common to nearly all paradigms, but it is the
laws that they do not share that are even more interesting. The fundamental
property that distinguishes two paradigms is often very neatly expressed by an
algebraic law, free of all the clutter of detail involved in a formal denition,
and unaltered when the detail changes. For example, functional programming
languages are classied as lazy or non-lazy. In a non-lazy language, each function
evaluates its arguments rst, so if an argument aborts, so does the function call.
As a consequence, functional composition (denoted by semicolon) has abortion
as its left zero: true ; = true . However, a lazy functional language does not

satisfy this law. It allows a constant function

P

K to deliver its answer without