Publications by Dr Stefan Kahrs

We describe a cumulative series of transformations to simplify regular expressions, and investigate their effectiveness and cost. Transformations depending on increasingly powerful comparisons of expressions give results clearly superior to commonly used algebraic simplifications. Early in the series, efficient transformations enabled by language-invariant attributes are surprisingly effective. Later in the series, transformations depending on comparisons of expressed languages are made feasible by bounding the size of subexpressions to which they are applied. We set out the principles of our transformations, address some key implementation issues, and evaluate the results of systematic test measurements.

Infinitary Term Rewriting allows to express infinite terms and transfinite reductions that converge to those terms. Underpinning the machinery of infinitary rewriting are closure operators on relations that facilitate the formation of transfinite reductions and transfinite equivalence proofs. The literature on infinitary rewriting has largely neglected to single out such closure operators, leaving them implicit in definitions of (transfinite) rewrite reductions, or equivalence relations. This paper unpicks some of those definitions, extracting the underlying closure principles used, as well as constructing alternative operators that lead to alternative notions of reduction and equivalence. A consequence of this unpicking is an insight into the abstraction level at which these operators can be defined. Some of the material in this paper already appeared in Kahrs (2010). The paper also generalises the notion of equational model for infinitary rewriting. This leads to semantics-based notions of equivalence that tie in with the equivalences constructed from the closure operators.

Properties of Term Rewriting Systems are called modular iff they are preserved under (and reflected by) disjoint union, i.e. when combining two Term Rewriting Systems with disjoint signatures. Convergence is the property of Infinitary Term Rewriting Systems that all reduction sequences converge to a limit. Strong Convergence requires in addition that redex positions in a reduction sequence move arbitrarily deep. In this paper it is shown that both Convergence and Strong Convergence are modular properties of non-collapsing Infinitary Term Rewriting Systems, provided (for convergence) that the term metrics are granular. This generalises known modularity results beyond metric d\infty.

When infinitary rewriting was introduced by Kaplan et.al. at the beginning of the 1990s, its term universe was explained as the metric completion of a metric on finite terms. The motivation for this connection to topology was that it allowed to import other well-studied notions from metric spaces, in particular the notion of convergence as a replacement for normalisation. This paper generalises the approach by parameterising it with a term metric, and applying the process of metric completion not only to terms but also to operations on and relations between terms. The resulting meta-theory is studied, leading to a revised notion of infinitary rewrite system. For these systems a method is devised to prove their convergence.

Chris Okasaki showed how to implement red-black trees in a functional programming language. Ralf Hinze incorporated even the invariants of such data structures into their types, using higher-order nested datatypes. We show how one can achieve something very similar without the usual performance penalty of such types, by combining the features of nested datatypes, phantom types and existential type variables.

Extended ML (EML) is a framework for the formal development of modular Standard ML (SML) software systems. Development commences with a specification of the behaviour required and proceeds via a sequence of partial solutions until a complete solution, an executable SML program, is obtained. All stages in this development process are expressed in the EML language, an extension of SML with axioms for describing properties of module components. This is an overview of the formal definition of the EML language. To complement the full technical details presented elsewhere, it provides an informal explanation of the main ideas, gives the rationale for certain design decisions, and outlines some of the technical issues involved. EML is unusual in being built around a ``real'' programming language having a formally-defined syntax and semantics. Interesting and complex problems arise both from the nature of this relationship and from interactions between the features of the language.

Term rewriting systems operate on first-order terms. Presenting such terms in curried form is usually regarded as a trivial change of notation. However, in the absence of a type-discipline, or in the presence of a more powerful type-discipline than simply typed ?-calculus, the change is not as trivial as one might first think. It is shown that currying preserves confluence of em arbitrary/ term rewriting systems. The structure of the proof is similar to Toyama's proof that confluence is a modular property of TRS.

This is a position paper giving our views on the uses and makeup of module interfaces. The position espoused is inspired by our work on the Extended ML (EML) formal software development framework and by ideas in the algebraic foundations of specification and formal development. The present state of interfaces in EML is outlined and set in the context of plans for a more general EML-like framework with axioms in interfaces taken from an arbitrary logical system formulated as an emphinstitution. Some more speculative plans are sketched concerning the simultaneous use of multiple institutions in specification and development.

Infinitary Term Rewriting allows to express infinitary terms and infinitary reductions that converge to them. As their notion of transfinite reduction in general, and as binary relations in particular two concepts have been studied in the past: strongly and weakly convergent reductions, and in the last decade research has mostly focused around the former. Finitary rewriting has a strong connection to the equational theory of its rule set: if the rewrite system is confluent this (implies consistency of the theory and) gives rise to a semi-decision procedure for the theory, and if the rewrite system is in addition terminating this becomes a decision procedure. This connection is the original reason for the study of these properties in rewriting. For infinitary rewriting there is barely an established notion of an equational theory. The reason this issue is not trivial is that such a theory would need to include some form of ``getting to limits'', and there are different options one can pursue. These options are being looked at here, as well as several alternatives for the notion of reduction relation and their relationships to these equational theories.

Properties of Term Rewriting Systems are called Modular iff they are preserved tinder disjoint union, i.e. when combining two Term Rewriting Systems with disjoint signatures. Convergence is the property of Infinitary Term Rewriting Systems that all reduction Sequences converge to a limit. Strong Convergence requires in addition that no redex position in a reduction sequence is used infinitely often. In this paper it is shown that Strong Convergence is it modular property, lifting a restriction from a known result by Simonsen, and that Convergence is modular for non-collapsing Infinitary Term Rewriting Systems

When Genetic Programming is used to evolve arithmetic functions it often operates by composing them from a fixed collection of elementary operators and applying them to parameters or certain primitive constants. This limits the expressiveness of the programs that can be evolved. It is possible to extend the expressiveness of such an approach significantly without leaving the comfort of terminating programs by including primitive recursion as a control operation.The technique used here was gene expression programming [2], a variation of grammatical evolution [8]. Grammatical evolution avoids the problem of program bloat; its separation of genotype (string of symbols) and phenotype (expression tree) permits to optimise the generated programs without interfering with the evolutionary process.

Our idiomatically objectionable title is a pun on Milner's ``well-typed programs do not go wrong'' --- because we provide a completeness result for type-checking rather than a soundness result. We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.

We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development, of Standard ML programs. Our aim is to isolate problems and issues that are intrinsic to the general enterprise of designing a specification language for use with a given programming language. Consequently the lessons learned go far beyond our original aim of designing a specification language for ML.

The essentially free variables of a term \(t\) in some \(\lambda\)-calculus, FV \(_{\beta}(t)\), form the set (\(x\) \(_{\mid}^{\mid}\) \(\forall u.t=_{\beta}u\Rightarrow x\) \(\epsilon\) FV\((u)\)}. This set is significant once we consider equivalence classes of \(\lambda\)-terms rather than \(\lambda\)-terms themselves, as for instance in higher-order rewriting. An important problem for (generalised) higher-order rewrite systems is the variable containment problem: given two terms \(t\) and \(u\), do we have for all substitutions \(\theta\) and contexts \(C\)[] that FV\(_{\beta}(C[t]^{\theta}) \supseteq\) FV\(_{\beta}(C[u^{\theta}])\)? This property is important when we want to consider \(t \to u\) as a rewrite rule and keep \(n\)-step rewriting decidable. Variable containment is in general not implied by FV \(_{\beta} (t)\supseteq\) FV\(_{\beta}(u)\). We give a decision procedure for the variable containment problem of the second-order fragment of \(\lambda^{\to}\). For full \(\lambda^{\to}\) we show the equivalence of variable containment to an open problem in the theory of PCF; this equivalence also shows that the problem is decidable in the third-order case.

We present a general framework for termination proofs for Higher-Order Rewrite Systems. The method is tailor-made for having simple proofs showing the termination of enriched λ-calculi.

Polymorphism in ML is implicit: type variables are silently introduced and eliminated. The lack of an explicit declaration of type variables restricts the expressiveness of parameterised modules (functors). Certain polymorphic functions cannot be expressed as functors, because implicit type parameters of polymorphic functions are in one respect more powerful than formal type parameters of functors. The title suggests that this lack of expressiveness is due to a restricted ability to abstract --- polymorphism is restricted. Type variables can only be abstracted from value declarations, but not from other forms of declarations, especially not from structure declarations. The paper shows in the case of Standard ML how (syntax and) semantics can be modified to fill this language gap. This is not so much a question of programming language design as a contribution for better understanding the relationship between polymorphic functions, polymorphic types, and functors.

Combinatory Reduction Systems generalise Term Rewriting Systems. They are powerful enough to express β-reduction of λ-calculus as a single rewrite rule. The additional expressive power has its price — CRSs are much harder to implement than ordinary TRSs. We propose an abstract machine suitable for executing CRSs. We define what it means to execute an instruction, and give a translation from CRS rules into sequences of instructions. Applying a rewrite rule to a term is realised by initialising the machine with this term, and then successively executing the instructions of the compiled rule.

When evaluation in functional programming languages is explained using ?-calculus and/or term rewriting systems, expressions and function definitions are often defined as terms, that is as em trees. Similarly, the collection of all terms is defined as a em forest, that is a directed, acyclic graph where every vertex has at most one incoming edge. Concrete implementations usually drop the last restriction (and sometimes acyclicity as well), i.e. many terms can share a common subterm, meaning that different paths of subterm edges reach the same vertex in the graph. Any vertex in such a graph represents a term. A term is represented uniquely in such a graph if there are no two different vertices representing it. Such a representation can be established by using em hash-consing for the creation of heap objects. We investigate the consequences of adopting uniqueness in this sense as a leitmotiv for implementation (called Unlimp), i.e. not em allowing any two different vertices in a graph to represent the same term.

This document was originally produced as lecture notes for the MSc and PG course ``Formal Program Development'' early in 1997. After some initial general considerations on this subject the paper focusses on the way one can use Extended ML (EML) for formal program development, which features EML contains and why, and which pitfalls one has to avoid when formally developing ML programs. Usage, features, and pitfalls are all presented through examples.

This document formally defines the syntax and semantics of the Extended~ML language. It is based directly on the published semantics of Standard~ML in an attempt to ensure compatibility between the two languages.

The em Definition of Standard ML contains several errors and ambiguities. Some of them have already been published in the em Commentary on Standard ML, but the list given there is incomplete. The paper lists all errors known to me today, including the errors listed in the Commentary. On most of the others I came across when writing the semantics of Extended ML. Most errors are supplied with an explanation ``what goes wrong'' and with a suggested correction. I understand ``error'' in a very broad sense --- ranging from typos to serious flaws in the rules. Some of the problems I mention are originated by a certain tension between formal definitions and informal explanations, e.g. overloading is informally explained though impossible in the given formal setting. Some parts of the paper are difficult to understand without prior knowledge of the Definition and the Commentary, because I rely on the notation and jargon introduced in these books. However, the nature of this paper has it that the various sections do not depend on each other, making it possible for somebody not familiar with the entrails of SML to read the less technical sections on their own.

The type system of most modern functional programming languages is based on Milner's polymorphism. A compiler or interpreter usually checks (or infers) the types of functions and other values by directly inspecting the source code of a program. Here, another approach is taken: The program is first translated into code for a stack machine and then a non-standard interpreter applied to this code checks (or infers) the type of the corresponding values. This can be seen as an abstract interpretation of the object code of the program.

This paper solves problem #79 of RTA's list of open problems [14] — in the positive. If the rules of a TRS do not overlap w.r.t. substitutions of infinite terms then the TRS has unique normal forms. We solve the problem by reducing the problem to one of consistency for "similar" constructor term rewriting systems. For this we introduce a new proof technique. We define a relation ⇓ that is consistent by construction, and which — if transitive — would coincide with the rewrite system's equivalence relation =R. We then prove the transitivity of ⇓ by coalgebraic reasoning. Any concrete proof for instances of this relation only refers to terms of some finite coalgebra, and we then construct an equivalence relation on that coalgebra which coincides with ⇓.

It is well-known that the type system of ML is overly restrictive in its handling of recursion: certain intuitively sound emphterms do not pass ML's type-check. We formalise this intuition and show that the restriction is semantical: there are computable (semantical) emphfunctions which cannot be expressed by well-typed (syntactical) terms.

The original purpose of type systems for programming languages was to prevent certain forms of run-time errors, like using a number as a function. Some type systems go as far as guaranteeing the absence of run-time errors, e.g. the type system of Standard ML. One can call such a type system ``sound''. This raises the question of the dual notion of completeness, i.e. is everything typable that does not have run-time errors? Or, to put it in another way: does the type system restrict the expressive power of the underlying implementation in an undesirable way? To make this rather vague idea precise we define an abstract notion of ``type system'', together with general notions of soundness and completeness. We examine several type systems for these properties, for instance ?^? and PCF are both complete, but for very different reasons.