-
Projections for infinitary rewriting
Authors:
Carlos Lombardi,
Alejandro Ríos,
Roel de Vrijer
Abstract:
Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order, left-linear term rewriting are described in the Terese book, chapter 8. In a previous work, we defined an extension of the finitary proof-term formalism, that allows…
▽ More
Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order, left-linear term rewriting are described in the Terese book, chapter 8. In a previous work, we defined an extension of the finitary proof-term formalism, that allows to describe contractions in infinitary first-order term rewriting, and gave a characterisation of permutation equivalence.
In this work, we discuss how projections of possibly infinite rewrite sequences can be modeled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting described in Terese, Section 8.7. We extend this characterisation to infinitary rewriting and also refine it, by describing precisely the role that structural equivalence plays in the development of the notion of projection. The characterisation we propose yields a definite expression, i.e. a proof term, that describes the projection of an infinitary reduction over another.
To illustrate the working of projections, we show how a common reduct of a (possibly infinite) reduction and a single step that makes part of it can be obtained via their respective projections. We show, by means of several examples, that the proposed definition yields the expected behavior also in cases beyond those covered by this result. Finally, we discuss how the notion of limit is used in our definition of projection for infinite reduction.
△ Less
Submitted 22 September, 2016; v1 submitted 25 May, 2016;
originally announced May 2016.
-
On abstract normalisation beyond neededness
Authors:
Eduardo Bonelli,
Delia Kesner,
Carlos Lombardi,
Alejandro Rios
Abstract:
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first…
▽ More
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A.Melliès in his PhD thesis. The theorem states that multistep strategies reducing so called necessary and never-grip** sets of redexes at a time are normalising in any ARS. Grip** refers to an abstract property reflecting the behavior of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.
△ Less
Submitted 9 May, 2016; v1 submitted 5 December, 2014;
originally announced December 2014.
-
Proof terms for infinitary rewriting, progress report
Authors:
Carlos Lombardi,
Alejandro Ríos,
Roel de Vrijer
Abstract:
We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity.
Our main use of proof terms is in a definition of permutation e…
▽ More
We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity.
Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects.
A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.
△ Less
Submitted 12 February, 2014; v1 submitted 10 February, 2014;
originally announced February 2014.
-
A standardisation proof for algebraic pattern calculi
Authors:
Delia Kesner,
Carlos Lombardi,
Alejandro Ríos
Abstract:
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Taka…
▽ More
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Takahashi and Crary for lambda-calculus. The proof is based on the fact that any development can be specified as a sequence of head steps followed by internal reductions, i.e. reductions in which no head steps are involved.
△ Less
Submitted 17 February, 2011;
originally announced February 2011.
