arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2210.15654

Reductions in Higher-Order Rewriting and Their Equivalence

Pablo Barenbaum·Eduardo Bonelli
View original source ↗Read source document ↗Export metadata ↓

Abstract

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink's, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (\b{eta}-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide. We also propose a standardization procedure, that computes a canonical representative of the permutation equivalence class of a rewrite.

Explore related subjects

cs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Pablo Barenbaum, Eduardo Bonelli. 2023-08-15. Reductions in Higher-Order Rewriting and Their Equivalence. https://arxiv.org/abs/2210.15654

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Probably correct row echelon form in the F4 algorithm

The computation of row echelon form is one of the main bottlenecks in the F4 algorithm. Several state of the art implementations use a probabilistic algorithm attributed to Monagan, Pearce, and Steel to accelerate this computation. Despite this, no bound on the probability that the algorithm returns an incorrect result appears to be available. In this paper, we provide such a bound. Furthermore, building on this result, we propose a Las-Vegas variant of the F4 algorithm and show experimentally that it can outperform deterministic F4 on some classical examples.

cs.SC↗
arXiv2026

Certified local rank and uniqueness barriers for a 48-term matrix-multiplication decomposition

We study replacements in fixed bilinear tensor decompositions, counting changes to complete rank-one summands, including output factors. The shortening frontier records the maximum rank defect of a fixed-size subset and determines the minimum length attainable within a change budget. For the rational 48-term Li--Wang--Hu decomposition \(D(2)\) of \(4\times4\) matrix multiplication over \(\mathbb{C}\), we prove rank radius at least 12, strong radius exactly 11, and border radius at least 8. Every shorter complex decomposition therefore changes at least thirteen original summands. An exact rational twelve-term replacement attains the equal-length barrier. The proofs combine exhaustive support reductions with saturated projected kernels and zero-corner completion arguments controlling arbitrary minimal competitors. A reduced-incidence argument transfers kernel certificates to tensor-space neighborhoods. A Laurent normal form gives strong radius exactly 11 for the sixteen-term core at every nonzero complex parameter. On a nonempty Zariski-open subset of the actual parameter curve, the rank radius is at least 12, the strong radius exactly 11, and the border radius at least 8. We also prove incomparability of the full Kothari--Moitra--Wein sufficient criterion and the Sylvester-equipped kernel criterion. These results describe local decomposition structure rather than a new rank bound for full matrix multiplication.

cs.SC↗
arXiv2026

Diversity of EML-type operators

The discovery of the EML operator, sufficient to evaluate the standard explicit purely transcendental elementary functions, has led to considerable interest and discussion across multiple scientific disciplines. However, most authors have focused on the binary EML itself, while numerous similar variants with slightly different properties are now known. This article attempts to close this gap by enumerating and classifying them. We also take this opportunity to clarify common misconceptions related to the EML operator. The principal goal, symbolic regression within an architecture as close as possible to proven neural networks which combine matrix multiplication with a single univariate non-linear activation function, remains beyond reach. Instead, we propose a Möbius layer, with rational functions replacing matrix operations, and showcase the recently discovered activation function eml(x,1/x), which allows exp(x) and ln(x) to be recovered separately, and hence all elementary functions to be evaluated within a rational generalization of the neural network.

cs.SC↗