The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
Dan Ghica, Huawei Research and Birmingham University, UK
Syntactic trinitarianism: terms, graphs, diagrams
The concept of 'syntax' is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call 'terms'. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this tutorial talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei.
Most of the material I will discuss is based on the recent tutorial paper "Hierarchical string diagrams and applications" jointly with Fabio Zanasi.
Aart Middeldorp, University of Innsbruck, Austria
Hydra Battles, Termination, and Transformations
The Battle of Hercules and Hydra is a combinatorial game introduced by Kirby and Paris. In an influential paper they proved that the termination of the Battle cannot be established in Peano arithmetic. Several authors have modeled the Battle as a term rewrite system. In this talk we review the various encodings and some of the termination techniques used to prove the termination of the ensuing rewrite systems.
In the context of functional programming/term normalization algorithms we discuss the optimization problem of constructing the result of a sequence of rewrite steps, without computing all the intermediate terms. From a rewrite system we construct a so-called creeper trace transducer, which reads a creeper trace while producing the desired answer. The transducer skips overlap between each pair of subsequent rules, and in some cases a part of the trace can be disregarded altogether.
In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.
When transforming a program into a more efficient version (for example by translating recursive functions into iterative ones), it is important that the input-output-behavior remains the same. One approach to assure this uses Logically Constrained Term Rewriting Systems (LCTRSs). Two versions of a program are translated into LCTRSs and compared in a proof system (Rewriting Induction). Proving their equivalence in this system often requires the introduction of a lemma. In this paper we present a new technique for generating invariants, using matrix calculations, and show how it can be combined with an existing method by Fuhs, Kop and Nishida to produce a lemma.
Python is a high level programming language that is strongly, but dynamically typed. In this paper we propose a type inference framework to compute types for the variables within a Python program by using static code analysis.
A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.