I received a Diplom degree in Informatik from Universität Dortmund,
Germany, in 1981.
From 1981 to 1997 I have been working in the
Compiler Design Lab of Prof. Dr. Reinhard
Wilhelm in the
Department of Computer Schience
of Saarland University, Saarbrücken, Germany.
I have been working mainly on functional programming, term rewriting systems, lambda calculus, type systems, and semantics of functional programming languages.
Abstract:
PCF is a sequential simply typed lambda calculus language.
There is a unique order-extensional fully abstract cpo-model of PCF, built up from
equivalence classes of terms.
In 1979, Gérard Berry defined the stable order in this model and proved
that the extensional and the stable order together form a bicpo.
He made the following two conjectures:
1) "Extensional and stable order form not only a bicpo, but a bidomain."
We refute this conjecture by showing that the stable order is not bounded complete,
already for finitary PCF of second-order types.
2) "The stable order of the model
has the syntactic order as its image:
If a is less than b in the stable order of the model, for finite a and b,
then there are normal form terms A and B with the semantics a, resp. b,
such that A is less than B in the syntactic order."
We give counter-examples to this conjecture, again in finitary PCF of second-order
types, and also refute an improved conjecture: There seems to be no
simple syntactic characterization of the stable order. But we show that Berry's
conjecture is true for unary PCF.
For the preliminaries, we explain the basic fully abstract semantics of PCF in the general setting of
(not-necessarily complete) partial order models (f-models).
And we restrict the syntax to "game terms", with a graphical representation.
Key words:
functional program, typed lambda calculus, PCF, denotational semantics,
fully abstract model, non-cpo model,
game semantics, stable function, stable order, dI-domain, bicpo, bidomain,
syntactic order
Supplementary material:
The first version of section 4. Game Terms:
The proof of the game term theorem without reducibility predicate.
Abstract: We define the syntax and reduction relation of a recursively typed lambda
calculus with a parallel case-function (a parallel conditional).
The reduction is shown to be confluent.
We interpret the recursive types as information systems in a restricted form,
which we call prime systems. A denotational semantics is defined
with this interpretation. We define the syntactical normal form approximations
of a term and prove the Approximation Theorem: The semantics of a term
equals the limit of the semantics of its approximations. The proof uses
inclusive predicates (logical relations).
The semantics is adequate with respect to the
observation of Boolean values. It is also fully abstract in the presence
of the parallel case-function.
Key words: lambda calculus, recursive type, parallel conditional,
parallel or, confluence, denotational semantics, information system,
approximation theorem, limiting completeness, inclusive predicates,
adequacy, full abstraction
Confluence of the lambda calculus with
left-linear algebraic rewriting
Information Processing Letters 41(1992) 293-299
[Please do not use the printed version, Elsevier introduced some typos (they even
left out a whole sentence), without giving me the chance to correct them.]
Abstract: We consider the untyped λ-calculus with β-reduction and algebraic
rewrite rules for some constants. The rules must be left-linear and must
not contain applications of variables in their left sides.
We prove that the combined reduction relation is confluent
(Church-Rosser) if the algebraic rewrite system alone is confluent.
This result also holds when reduction is restricted to a subset of terms
with suitable closure conditions. (This subset may be a set of well-typed
terms.)
Key words: functional program, lambda calculus, term rewriting system, confluence,
Church-Rosser, parallel conditional
Abstract: We develop the concept of a constructive type system for
functional programming languages. As with Martin-Löf's Intuitionistic Theory
of Types, the underlying principle says: A type is defined by the rules for
constructing its elements. We describe these constructions as processes modelled
by Concrete Data Structures (Kahn/Plotkin). A hierarchy of type universes is
introduced. In addition to simple types it contains higher order objects composed of
types and operators acting on these objects. These language constructs support
the formulation of abstract programming schemes as type procedures.
Comment in 2008: The paper is just a proposal, not a fully formalized system.
But it contains a nice programming example: a recursion over a list of
dependent kind (kind = type of the second universe).
Abstract: The main content of the work is a generalization of Huet/Levy: “Call by need computations in non-ambiguous linear term rewriting systems” for constructor term rewriting systems that may contain fairly parallel operators, like parallel or. Independent work on this problem was published by Sekar and Ramakrishnan: “Programming in equational logic: Beyond strong sequentiality”, Information and Computation 104(1993) 78-109.