Formal Semantics and Abstract Properties of String Pattern Operations and Extended Formal Language Description Mechanisms

The classical view of semantics that we inherited from Montague is that natural languages are formal languages where semantics specifies the interpretations which can be associated with expressions of the language. In this context coercion might be seen as a slight but formally specifiable disturbance in the formal semantics which shows how the canonical interpretation of an expression can be modified by its linguistic context. In recent years an alternative to the formal language view of natural language has developed which sees the interpretation of language as a more local and dynamic process where the interpretation of expressions can be modified for the purposes of the utterance at hand. This presents linguistic semantics as a dynamic, somewhat chaotic, system constrained by the need to communicate. An interpretation of an expression will work in communication if it is close enough to other interpretations your interlocutor might be familiar with and there is enough evidence in the ambient context for her to approximate the interpretation you intended. On this view of language as a system in flux, coercion is not so much a disturbance in the semantic system but rather a regularization of available interpretations leading to a more predictable system. I will present some of the reasons why I favour the view of language in flux (but nevertheless think that the techniques we have learnt from formal semantics are important to preserve). I will look at some of the original examples of coercion discussed in the Pustejovskian generative lexicon and suggest that the possibilities for interpretation are broader than might be suggested by Pustejovsky’s original work. Finally, I will suggest that coercion can play a central role in compositional semantics taking two examples: (1) individual vs. frame-level properties and (2) dynamic generalized quantifiers and property coercion.

Download Full-text

Solving string constraints with Regex-dependent functions through transducers with priorities and variables

Proceedings of the ACM on Programming Languages ◽

10.1145/3498707 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-31

Author(s):

Taolue Chen ◽

Alejandro Flores-Lamas ◽

Matthew Hague ◽

Zhilei Han ◽

Denghang Hu ◽

...

Keyword(s):

Programming Languages ◽

Formal Language ◽

Formal Semantics ◽

Symbolic Execution ◽

Language Theory ◽

Regular Expressions ◽

Constraint Language ◽

Straight Line ◽

Finite State ◽

Lazy Semantics

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.

Download Full-text