Pith. sign in

REVIEW 1 cited by

Preservation theorems for Tarski's relation algebra

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2305.04656 v5 pith:2J5R6AMJ submitted 2023-05-08 cs.LO

classification cs.LO
keywords fragmentgeneratedfinitelyfinitefunction-preservingoperationsalgebraantidomain
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary structures). The function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable function-preserving operations). Similarly, the total-function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable total-function-preserving operations). In contrast, the forward-looking function-preserving fragment is finitely generated by composition, intersection, antidomain, and preferential union. Similarly, the forward-and-backward-looking injective-function-preserving fragment is finitely generated by composition, intersection, antidomain, inverse, and an `injective union' operation.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Algebras for Deterministic Computation Are Inherently Incomplete

    cs.PL 2024-11 accept novelty 8.0 of 10

    No finite set of regular control-flow operations generates the deterministic fragment of Kleene Algebra with Tests, so GKAT and all its finite regular extensions remain expressively incomplete.

Pith tools