HOR 2014 WORKSHOP PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. We show that Jay and Kesner’s dynamic pattern calculus can be embedded into a higher-order pattern rewriting systems in the sense of Nipkow. Metatheoretical results, such as confluence and standardisation, are shown to obtain for the dynamic pattern calculus as a consequence of this embedding. The embedding also opens a way to study the semantics of Jay’s programming language Bondi based on pattern matching.

ABSTRACT. It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.

ABSTRACT. We have now twice used the ``HACS'' compiler generator tool in an NYU graduate Compiler Construction class. HACS is based on a higher-order rewriting formalism, thus we have effectively been teaching students higher order rewriting techniques as the way to implement compilers. In this paper we report on how HACS matches specific rewriting notions to the techniques used by compiler writers, and where the main difficulties have been encountered in teaching these.

ABSTRACT. Some rewrite systems are not orthogonal, in that they do have critical peaks, but are very close to being orthogonal, in that for any given object there exists a partial function, called orthogonalisation, mapping the set of all redexes to an orthogonal subset and every multi-step to an equivalent one. Term rewrite systems having only trivial peaks, so-called weakly orthogonal systems with the lambda-beta-eta-calculus as prime example, are known to admit such an orthogonalisation. Here we characterise the term rewrite systems that admit orthogonalisation as those whose critical peaks are feeble, in that at least two out of the three terms in such a peak must be identical (generalising weak orthogonality).