Equivalence of Reductions in Higher-Order Rewriting

Higher-order rewriting is a symbiosis of two classical rewriting paradigms: the Lambda calculus, which features higher-order variables and variable binding, and first-order term rewriting, which features algebraic pattern matching. It is a powerful tool to study the meta-theory of declarative programming languages, such as Prolog and Haskell, on the one hand, and theorem provers and proof assistants, such as Isabelle, on the other. In this dissertation the notion of equivalence of reductions (for finite reductions) in higher-order rewrite systems (HRSs) is studied. Equivalence of reductions has been formalized for first-order term rewrite systems in various different ways. Here, I transform three of those formalizations to the higher-order case: • Permutation equivalence. Permutation equivalence is the formalization of the intuition that two reductions are equivalent if the one can be obtained from the other by iteratively permuting steps. I prove the property that every finite reduction (possibly containing multisteps) has a permutation equivalent proper reduction, that is, a reduction in which each step contracts exactly one redex. • Standardization equivalence. Standardization equivalence formalizes the idea that two reductions are equivalent if they have the same “standard” reduction, that is, a reduction in which the redexes are contracted in some standard order. In this thesis, we use the outermost-innermost order as standard order. In order to use standardization for formalizing equivalence of reductions, it is required that each (permutation) equivalence class of reductions contains a unique standard one. For the notion of standard used here, this is proved by giving two procedures which produce an equivalent standard reduction when given an arbitrary reduction: selection standardization and inversion standardization, which correspond to the weak and strong standardization of Klop, respectively. • Projection equivalence. If R and S are reductions, then the projection of R over S represents the reduction which contains the steps of R except the one which were also part of S. Projection equivalence captures the idea that two reductions are equivalent if the one projected over the other yields an empty reduction. The main result of this dissertation is that for local, orthogonal HRSs the three notions of equivalence coincide. An auxiliary result of this dissertation is the proof that HRSs enjoy finite family developments, meaning that in infinite reductions, there is no bound on the number of steps which were involved in creating a given symbol. This property is used to define the standardization procedures and has possible applications for proving termination of other HRSs.