String Rewriting Systems: Brief Introduction and Sample of Open Problems

Assaf Kfoury

Home/Archive/arXiv

arXiv · 2608.19397

String Rewriting Systems: Brief Introduction and Sample of Open Problems

Assaf Kfoury

View original source ↗Read source document ↗Export metadata ↓

Abstract

This document is the result of pulling together small parts of different lecture notes I have written over several decades for first-year graduate-level courses -- typically with the title Formal Methods -- which included many other topics of mathematical logic and theoretical computer science. After combining these materials, I updated the references and adjusted the text to account for progress accomplished in the intervening years. The sample of open problems in the last section is a small collection of special cases that are still unresolved up until the date of this writing.

Explore related subjects

cs.LO

Keep this discovery

BibTeX RIS

Assaf Kfoury. 2026-09-05. String Rewriting Systems: Brief Introduction and Sample of Open Problems. https://arxiv.org/abs/2608.19397

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

Discover connections

cs.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

A categorical formulation of Kraus' paradox

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT↗

arXiv2026

Univalence without function extensionality

It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of the univalence axiom, asserting that the wild category formed by the universe is univalent, which we call categorical univalence. We show that categorical univalence does not imply function extensionality by an analysis of Von Glehn's polynomial model construction, which produces models of Martin-Löf type theory that always refute function extensionality. We find in particular that when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.

cs.LO↗

arXiv2026

Quantified propositional calculi and narrow implicit proofs

In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.

cs.LO↗