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

Proving that a proposed law P = Q leads to contradiction is quite a chal-

lenge, because the context [ ] that reveals it may be very large. But proving

that something is not a contradiction can be even harder, because it involves con-
sideration of the innite set of all possible contexts that can be written around
P

C

; such a universal hypothesis requires an inductive case analysis over
all the combinators of the calculus. Sometimes, only a reduced set of contexts
is sucient; this fact is established by proof of a context lemma . As a result of
their syntactic orientation, proofs by induction tend to be specic to a particular
calculus, and care is needed in extending their results to calculi with a slightly
dierent syntax, dierent reductions, or dierent structural laws. For this reason,
each new variation of a familiar calculus is usually presented from scratch.

and Q

Heavy reliance on induction certainly provides a strong motive for keeping
down the number of notations in the original syntax to an inescapable core of
primitives, even if this makes the language less expressive or ecient in prac-
tical use. The pursuit of minimality tends to favour the design of a language
at a relatively low level of abstraction. The power of such a language matches
that of machine code, which oers enormous power, including the opportunity
for each instruction to interfere with the eect of any other. In the presence of
multi-threading or non-determinacy, understanding of the behaviour of an arbi-
trary program becomes rapidly impossible. And there are few general theorems
applicable to arbitrary programs that can aid the understanding, or permit op-
timising transformations that preserve behavioural equivalence. The solution to
this problem is to conne attention to programs that follow dened protocols
and restrictive conventions to limit their mutual interaction. The meaning of
conformity with the convention is dened by means of a type system , which is
also usually presented in a bottom-up fashion. The syntax gives a notation for
expressing all the types that will be needed. Then a collection of axioms and
proof rules provide a means of deducing which parts of each program can be
judged to belong to a particular type. In a higher level programming language
the programmer may be required or allowed to provide adequate type infor-
mation for variables and parameters; but most of the labour of type checking
or even type inference can be delegated to a compiler. The consistency of the
typing system is established by showing that pairs of programs equated by the
structural laws have the same type, and that each reduction step in execution
preserves the proper typing of its operand. This is called a subject reduction the-
orem. Subsequent development of the theory can then be conned to properly
typed programs.
A type system based on an operational model may be designed to supply
information that is highly relevant to program optimisation. For example, it can
detect dead code that will never be executed, and code that will be executed at
most once. Other type systems can guarantee absence of certain kinds of pro-
gramming error such as deadlock. If it is known that no type can be deduced
for such an erroneous program, then type consistency ensures that the error can
never occur a run time. Because type systems enforce disciplined interaction,
well-typed programs often obey additional laws, useful both for comprehension