PRELIMINARY Meeting Plan for Dagstuhl 9823
Last revised June 3, 1998
The following is a first cut at a plan of times and topics for
Dagstuhl Seminar
9823, titled Programs: Improvements, Complexity, and Meanings. Note that
some of the one-hour time blocks have only one talk, and other blocks contain two
30 minute talks.
This topic concerns the interfaces among groups of researchers,
whose methods and goals are sometimes rather different. Because of this, the
schedule contains four blocks labeled "Problem formulation".
The idea is to use this time to work together. One goal can be to find
problems
- that are of interest to researchers in programming languages and
complexity theory;
- that seem susceptible in formulation or solution to the methods and
viewpoints of the people present;
- that are worth being solved, using criteria such as conceptual
significance, practical utility, intellectual beauty, etc.; and
- that seem potentially able to be solved, e.g., defined
precisely enough to be answered exactly, and avoiding the well-known pitfalls of
undecidability or hardness for large complexity classes.
Another goal can be to report progress towards solving problems
formulated in earlier sessions. This will undoubtedly lead to more discussions and
formulation of new problems.
Time scheme
| Hour/day |
|
Monday |
Tuesday |
Wednesday |
Thursday |
Friday |
| |
| 0845-0945 |
|
Jones |
Problem formulation |
Problem formulation |
Problem formulation |
Problem formulation |
| 0945-1000 |
|
Break |
Break |
Break |
Break |
Break |
| 1000-1100 |
|
Royer |
Voda |
Börger
Christensen
|
Hofmann
Kapron
|
Open
|
| 1100-1115 |
|
Break |
Break |
Break |
Break |
Break |
| 1115-1215 |
|
Ben-Amram
de Moor
|
Leivant |
Clote
Dancanet
|
Nickau
Niggl
|
Conclusions,
summary
|
|
|
| 1215-1400 |
|
Lunch |
Lunch |
Lunch |
Lunch |
Lunch |
|
|
| 1400-1500 |
|
Gurevich |
Möller |
Excursion
|
O'Hearn
Otto
|
|
| 1500-1530 |
|
Break |
Break |
Excursion |
Break |
|
| 1530-1630 |
|
Schwichtenberg |
Basin
Tannen
|
Excursion |
Petersen
Schellekens
|
|
| 1630-1700 |
|
Break |
Break |
Excursion |
Break |
|
| 1700-1800 |
|
Sands |
Schönhage
Guessarian
|
Excursion |
Spreen
Open
|
|
|
|
| 1800- |
|
Dinner |
Dinner |
Dinner |
Dinner |
|
Participants, speakers, titles, and abstracts
David Basin:
Complexity Analysis of Logic Programs based on Ordered Resolution.
Amir Ben-Amram:
Pippenger's Comparison of Pure and Impure Lisp.
In a POPL '96 and TOPLAS paper,
Pippenger showed that, at least in an appropriate framework,
"pure LISP" is inherently less efficient than "impure LISP" which has
destructive update operations (setcar, setcdr).
This kind of result has been long awaited by people interested in
complexity aspects of programming languages.
The purpose of this talk will be to present Pippenger's work
and discuss its relation to former results, its restrictions and
implications, follow-ups and open problems.
Egon Börger:
Operational Models for Compiler Verification.
We show how the use of operational models, enhanced
by appropriate abstraction mechanisms, helps bridging the gap between
program semantics as seen by a programmer and its implementation on
executing machines. The approach helps reducing the complexity of
compiler construction and adds to the reliability of the compilation
processs. The talk is illustrated by my work on provably correct
compilation schemes for compiling Prolog programs to WAM code, of Occam
programs to Transputer code and of Java programs to JVM code.
Abstract.
Peter Clote:
Type 2 Parallel Computable Functions.
Abstract.
Denis
Dancanet:
Refinement Type Inference using Sequential Algorithms.
We present a new application of Berry and Curien's intensional
semantics of sequential algorithms on concrete data structures
and its related programming language, CDS0.
We define a typing system based on concrete data structures
and featuring recursive types, subtyping, intersection types,
polymorphism, and overloading. Then we translate programs
written in a high-level language to CDS0 and use the precise
information on the dependence of pieces of output on pieces
of input provided by sequential algorithms to derive very
detailed types, similar to Freeman and Pfenning's refinement types.
Yuri Gurevich:
Abstract State Machines and Linear Time Hierarchy.
We recall the notion of abstract state machines and mention some
recent applications, in particular, the ASM model of Java. The rest
of the lecture is devoted to the concept of linear time. Contrary to
polynomial time, linear time is capricious and badly depends on the
computation model. In 1992, Neil Jones designed a number of
computation models where the linear-speed-up theorem fails and
linear-time computable functions form a hierarchy. The linear time of
those models is too restrictive, however. We explain the linear time
hierarchy theorem (coauthored Andreas Blass) for abstract state
machines. One (very long-term) goal of this line of research is to
prove lower bounds for natural linear time problems.
Martin
Hofmann:
Extending "Safe Recursion" to Higher Types, Lists, Trees, and
Polymorphism.
Bellantoni-Cook's function algebra BC is a first-order
system which defines exactly the PTIME functions in a "resource free"
way by imposing a certain syntactic restriction on primitive recursion
on notation. We extend this idea to a fully-fledged simply-typed
lambda calculus with lists, trees, and impredicative polymorphism. The
syntactic restriction contained in the Bellantoni-Cook approach is
captured by way of an S4 modality on types. The presence of trees and
higher-typed functions further introduces the need for linearity (in
the sense of linear logic) in certain places. The proof that the
resulting calculus defined PTIME functions only proceeds by giving a
semantic interpretation using realisability and functor categories.
From the outside this work can be seen as an integration of recent
work by Bellantoni-Niggl-Schwichtenberg (which adds higher-types to
Bellantoni-Cook's system) and Caseiro's thesis, which adds lists and
trees without having higher-order functions. Altogether new is the
semantic method employed in the soundness proof.
Neil D. Jones:
The Interface between Programming Languages and Complexity Theory.
Abstract.
Bruce Kapron:
Resource-bounded notions of continuity.
We consider two plausibe definitions for feasible continuity of
type-two functionals, and show that they are NOT equivalent. We
will consider what this state of affairs has to say (if anything)
about the relationship between computational complexity and
intensionality.
Daniel Leivant:
Ramified Recurrence and Alternation.
Abstract
Christian Lengauer:
The Skeletal Approach to Performance-directed Program Parallelization.
An approach is sketched for transforming functional program schemata
to obtain efficient parallel implementations. The focus is on divide-
and-conquer recursions.
Abstract
Oege de
Moor:
More Haste, Less Speed: Lazy Versus Eager Evaluation.
Abstract
Bernhard
Möller:
A Survey of Efficiency-Increasing Transformation Techniques
Program transformations serve a dual purpose:
1. Constructing first correct implementations from formal specifications.
2. Improving the efficiency of such implementations concerning
-- asymptotic time complexity (A)
-- constant factors (C)
-- space complexity (S).
In this talk we sketch the most important strategies for the latter aspect
using some simple examples. The most important techniques, with an indication
of their main improvement potentials, are:
I. Control fusion, both parallel (tupling (C)) and sequentially
(deforestation (C,S)).
II. Hornering and strength reduction (formal differentiation,
Delta-optimization) (A,C).
III. Memoization and pre-computation (A).
IV. Change of data structure (A,S).
V. Re-use of variables (S).
Abstract.
Hanno Nickau:
"A topic relating game semantics and higher type complexity"
Abstract.
Karl-Heinz Niggl:
Characterising Polytime Through Higher Type Recursion.
It is shown how to restrict recursion on notation in all
finite types so as to characterise the polynomial time
computable functions. The restrictions are obtained by
enriching the type structure with $\bang \sigma$, and by
adding linear concepts to the lambda calculus (Joint work
with S.Bellantoni and H.Schwichtenberg)
Peter
O'Hearn:
The logic of bunched implications.
The logic BI of bunched implications is a logic in which
an additive (intuitionistic) and multiplicative (linear) live
side by side. We give two semantics for BI (a semantics of truth
and a semantics of proofs), and discuss its "resource sensitive"
aspect. We also discuss "resource sensitivity" in logics
that control structural rules more generally, in an attempt to
understand the sense of "resource" that is meant.
Luke Ong:
A "machine" model for complexity analysis of higher-type
sequential computable functional/complexity model for PCF.
Abstract.
J. R. Otto:
Resolutions, Towers, and Low Degree Type 2 Functionals.
We collapse towers of bicategories of resolutions (in a logic
programming sense) to towers of fibrations (with fragments of local
smallness) where the towers describe both tiers (Bellantoni, Cook,
Leivant) and (hopefully) degree stratification of type 2 functionals
(Irwin, Kapron, Royer). (There are linearity issues to be explored.)
Holger
Petersen:
CONS-Free Programs with Tree Input.
We investigate programs operating on LISP-style input data that may
not allocate additional storage. For programs without a test of
pointer equality we obtain a strict hierarchy of sets accepted by
deterministic, non-deterministic, and recursive programs. We also show
that the classes accepted by programs with the ability to test
pointers for equality are closely related to well-known complexity
classes. For these classes, strictness of the hierarchy is an
important open problem. Joint work with Amir M. Ben-Amram.
Jim Royer:
An overview of higher-type complexity.
We sketch some of the basic motivations, ideas, results,
and deficiencies of higher-type complexity theory.
David Sands:
Improvement Theory and its Applications
Improvement theory is a variant of the standard theories of observational
approximation (or equivalence) in which the basic observations made of a
program's execution include some intensional information about, for
example, the program's computational cost. One program is an improvement
of another if its execution is no less costly in any program context. In
this talk we give an overview of our work on the improvement theory and its
applications. Applications include reasoning about time properties of
functional programs, and to proving the correctness of program
transformation methods.
Michel
Schellekens:
Partial Metrics = Generalized (E)valuations.
Abstract.
Uwe
Schöning: schoenin@informatik.uni-ulm.de
Arnold
Schönhage: schoe@informatik.uni-bonn.de.
Soft branching and soft correctness for gains in efficiency.
Abstract.
We extend normalization by evaluation (first presented in [4]) from the pure typed
lambda-calculus to general higher order type term rewrite systems. Different
versions are worked out, motivated by efficiency considerations. This work also
gives a theoretical justification of the normalization algorithm implemented in
the MINLOG system. (Joint work with U.Berger and M. Eberl).
sestoft@dina.kvl.dk
Dieter Spreen:
A lambda model made up by functions of bounded growth.
Abstract
Val Tannen:
Formal methods for query optimization.
Abstract
Paul J. Voda:
Computer Programming as Mathematics.
This is basically the philosophy of the programming language and proof
system system CL (pairing, Clausal Language, Proof system) which has
a precise mathematical characterization of what exactly are the
functions definable in CL (unary primitive recursive functions) and
what kind of theorems about them can be proved in the formal system,
ie. what is the strength of the formal system. This turns out to be
the I\Sigma_1-fragment of Peano arithmetic.
The language and proof system CL is extremely simple to justify. On
the other hand, the characterization is quite involved and
difficult. This is because there is an inherent trade off between
computer programming and proving properties of programs. For efficient
programming one needs quite a fine way of controlling the execution
speed of programs (i.e. functions) by means of rich recursive and other
control instructions. It turns out that the more efficient the
function is, the harder it is to prove its properties. This is because
the proofs call for a quite rich set of induction and other proof
rules. To show that all such rules are admissible in
I\Sigma_1-fragment of Peano arithmetic rquires advanced proof and
recursion-theoretical techniques. Basically this involves the Theorem
of R. Peter on simple (i.e. 1-fold) nested recursive definitions and
the theorem of Parsons on admissibility of \Pi_2-rules in
I\Sigma_1 arithmetic.
Neil D. Jones
University of Copenhagen
DIKU, Department of Computer Science
Universitetsparken 1
2100 Copenhagen East,
Denmark
Email: neil@diku.dk