This talk is
a general survey of some issues at the branch points of
logic, semantics, computation, and programming language
design, rather than a report on particular research results
of the speaker. It was felt that this more global outlook
would be more informative to the researchers in the Volen
Center, who are for the most part biological scientists.
It is important, however, to remember that the Volen Center
houses many different scientists with disparate research
agendas. The point of this talk was to explain one such
agenda.
Just as the
world of freshman physics, with its massless beams and
frictionless pulleys, describes the essence of the Newtonian
world, and the Turing Machine defines the essence of computer
architecture, the Lambda Calculus, whose properties we
will discuss in some detail, defines the essence of programming
languages. In particular, it allows a fundamental insight
into the design of procedure calling protocols -- the
mechanism that connects inputs and outputs in the functional
style of programming.
In the "call-by-name"
protocol, where arguments input to functions are not evaluated
until they are needed, there is a fundamental and practical
implementation problem where these arguments are recomputed
each time they are needed. While a naive "caching" strategy
works for base values, this naive approach fails when
the argument is itself a function. We discuss an interpretative
technology known as "optimal evaluation" to address this
fundamental issue of sharing inputs in a functional computation.
It turns out
that in recent years, a kind of logic has been invented
that captures many of the computational issues involved
in optimal evaluation. This logic is called "linear logic"
-- it is also referred to as a "resource-conscious logic"
which addresses the problem of persistence of truth in
time. This problem is particularly acute in computations
that cannot be reversed. It turns out that building blocks
in this logic correspond strongly to technology employed
in implementation of programming languages, and that we
can learn more about one from studying the other. The
fundamental paradigm of "computational logic" unifies
the two, where we can extract real computational information
from the structure of proofs.
Finally, we
discuss the "geometry of interaction", a beginning approach
to understanding the semantics of proofs and of computer
programs. Two entirely different proofs of the same theorem
should have different denotational meanings, while simplifying
a proof (through so-called "cut elimination") should preserve
denotational meaning. We look at the basic idea of the
geometry of interaction in the lambda calculus, showing
how it models information flow in a computer program.
