Logic and Programming Languages

Logic has been long in terested in whether answers
to certain questions are computable in principle, 
since the outcome puts bounds on the possibilities of
formalization.  More recently, precise comparisons 
in the efficiency of decision methods have become available
through the developments in complexity theory. 
 These, however, are applications to logic, and a big question
is whether methods of logic have significance 
in the other direction for the more applied parts of
computability theory.  Programming languages offer 
an obvious opportunity as their syntactic formalization
is well advanced; however, the semantical theory 
can hardly be said to be complete.  Though we have
many examples, we have still to give wide-ranging 
mathematical answers to these queries:  What is a machine?
 What is a computable process?  How (or how 
well) does a machine simulate a process?  Programs naturally
enter in giving descriptions of processes. 
 The definition of the precise meaning of a program
then requires us to explain what are the objects 
of computation (in a way, the statics of the problem)
and how they are to be transformed (the dynamics). 
 So far the theories of automata and of nets, though
most in teresting for dynamics, have formalized only 
a portion of the field, and there has been perhaps too
much concentration on the finite-state and algebraic 
aspects.  It would seem that the understanding of higher-level
program features involves us with infinite 
objects and forces us to pass through several levels
of explanation to go from the conceptual ideas to 
the final simulation on a real machine.  These levels
can be made mathematically exact if we can find 
the right abstractions to represent the necessary structures.
 The experience of many independent workers 
with the method of data types as lattices (or partial
orderings) under an information content ordering, 
and with their continuous mappings, has demonstrated the
flexibility of this approach in providing definitions 
and proofs, which are clean and without undue dependence
on implementations.  Nevertheless much remains 
to be done in showing how abstract conceptualizations
can (or cannot) be actualized before we can say 
we have a unified theory.

CACM September, 1977

Scott, D. S.

logic, programming languages, automata, denotational
semantics, a-calculus models, computability, 
partial functions, approximation, function spaces

1.2 4.20 5.21 5.24 5.27

CA770902 JB December 28, 1977  6:49 AM

2931	5	2931
2931	5	2931
2931	5	2931