Fritz Müller Home Page

email: (λ

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.


On Berry's conjectures about the stable order in PCF

final version of September 2012, 39 pages,
Logical Methods in Computer Science vol. 8(4:7) 2012,
also available from

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.

Full abstraction for a recursively typed lambda calculus with parallel conditional

revised version of Report 12/1993 of SFB 124, Informatik, Universität des Saarlandes, Saarbrücken 1993, 54 pages.
Also available from

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

Ein konstruktives Typsystem für funktionale Programmiersprachen.
(A constructive type system for functional programming languages, in German.)

in: Programmiersprachen und Programmentwicklung, Urs Ammann ed., Informatik-Fachberichte 77, Springer-Verlag, Berlin 1984

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).

Entwurf und Implementierung eines Interpreter-Generators unter Verwendung von Baumtransformatoren und schnellen Verfahren zur Einbettung von Bäumen.
(Design and implementation of an interpreter-generator using tree transformers and fast algorithms for tree pattern matching, in German.)

Diplom thesis, Abteilung Informatik, Universität Dortmund, 1980.

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.