On the Expressive Power of String Constraints
summary
Classifies 20 string-logics built from concatenation, word-equality, length arithmetic and language membership and shows which express which formal languages. Key claims: encodes Turing computations so concatenation plus visibly-pushdown membership already captures all recursively enumerable languages (satisfiability undecidable), while many pure word-equation fragments do not. Proof tools: reductions from Turing machines and a combinatorial unanchored blocks pumping lemma that produces counterexamples to expressibility. Gives concrete separations (e.g. which combos can express a^n b^n or ww).
AI-written summary · about
chapters (8)
- 0:00Start
- 5:31String Solving
- 7:17String Constraints
- 12:33Quick Recap
- 14:58Research Questions
- 17:42Focus: Theories with Word Equations
- 19:27Showing Inexpressibility: A Pumping Argument
- 25:35Separation and Grouping of the Theories: Expressive Power
related talks
01h 24mIntroduction to Constraint Logic Programming
01h 01mDatalog and Equality Saturation
41mOptimizing Relational Programs I
18mParikh's Theorem Made Symbolic
17mFixpoints for the Masses: Programming with First-Class Datalog Constraints
20mThe Decision Problem for Regular First Order Theories
01h 02mAlgebraic Structures in Logic and Query Evaluation 3
01h 08mAlgebraic Structures in Logic and Query Evaluation 4