Loughborough University
Browse

On the expressive power of string constraints

Download (368.27 kB)
conference contribution
posted on 2023-01-13, 10:12 authored by Joel DayJoel Day, Vijay Ganesh, Nathan Grewal, Florin Manea

We investigate properties of strings which are expressible by canonical types of string constraints. Specifically, we consider a landscape of 20 logical theories, whose syntax is built around combinations of four common elements of string constraints: language membership (e.g. for regular languages), concatenation, equality between string terms, and equality between string-lengths. For a variable x and formula f from a given theory, we consider the set of values for which x may be substituted as part of a satisfying assignment, or in other words, the property f expresses through x. Since we consider string-based logics, this set is a formal language. We firstly consider the relative expressive power of different combinations of string constraints by comparing the classes of languages expressible in the corresponding theories, and are able to establish a mostly complete picture in this regard. Secondly, we consider the question of deciding whether the language or property expressed by a variable/formula in one theory can be expressed in another theory. We establish several negative results which are relevant to preprocessing and normalisation of string constraints in practice. Some of our results have strong connections to important open problems regarding word equations and the theory of string solving.

Funding

German Research Foundation (Deutsche Forschungsgemeinschaft, DFG), by the project with number 466789228

History

School

  • Science

Department

  • Computer Science

Published in

Proceedings of the ACM on Programming Languages

Volume

7

Issue

POPL

Pages

278 - 308

Source

50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)

Publisher

Association for Computing Machinery

Version

  • VoR (Version of Record)

Rights holder

© Owner/Author

Publisher statement

This is an Open Access Article. It is published by Association for Computing Machinery under the Creative Commons Attribution 4.0 International Licence (CC BY). Full details of this licence are available at: https://creativecommons.org/licenses/by/4.0/

Acceptance date

2022-11-08

Publication date

2023-01-11

Copyright date

2023

eISSN

2475-1421

Language

  • en

Location

Boston, Massachusetts, United States

Event dates

15th January 2023 - 21st January 2023

Depositor

Dr Joel Day. Deposit date: 13 January 2023

Article number

10

Usage metrics

    Loughborough Publications

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC