Parsing as Deduction Revisited: Using an Automatic Theorem Prover to Solve an SMT Model of a Minimalist Parser (2022)

Abstract: We introduce a constraint-based parser for Minimalist Grammars (MG), implemented as a working computer program, that falls within the long established “Parsing as Deduction” framework. The parser takes as input an MG lexicon and a (partially specified) pairing of sound with meaning - i.e. a word sequence paired with a semantic representation - and, using an axiomatized logic, declaratively deduces syntactic derivations (i.e. parse trees) that comport with the specified interface conditions. The parser is built on the first axiomatization of MGs to use Satisfiability Modulo Theories (SMT), encoding in a constraint-based way the principles of minimalist syntax. The parser operates via a novel solution method: it assembles an SMT model of an MG derivation, translates the inputs into SMT formulae that constrain the model, and then solves the model using the Z3 SMT-solver, a high-performance automatic theorem prover; as the SMT-model has finite size (being bounded by the inputs), it is decidable and thus solvable in finite time. The output derivation is then recovered from the model solution. To demonstrate this, we run the parser on several representative inputs and examine how the output derivations differ when the inputs are partially vs. fully specified. We conclude by discussing the parser’s extensibility and how a linguist can use it to automatically identify: (i) dependencies between input interface conditions and principles of syntax, and (ii) contradictions or redundancies between the model axioms encoding principles of syntax.

## introduction minimalist theories of syntax consider the human language faculty (hlf) as a computational system capable of deriving from a finite lexicon and a single combinatorial operation, an unbounded set of hierarchical syntactic structures, pairing sounds (typically word sequences) with meaning representations (chomsky, 1995). (in more technical language, the hlf pairs phonological forms [pf], where a pf is an encoding of information relevant to how a brain-internal structured expression gets pronounced, signed, etc, with logical forms [lf], where an lf is a structured semantic representation, e.g. predicate-argument structure.) this study introduces a novel computational model for the hlf, implemented as a working computer program, @xcite that takes the form of a constraint-based parser for minimalist grammars (mg), grounded in the (first) axiomatization of minimalist syntax using satisfiability modulo theories (smt). @xcite working within the "parsing as deduction" framework (pereira and warren, 1983), the parser is a logic program that uses an automatic theorem prover to answer the question: can a given lexicon yield a syntactic structure that encodes a given lf and/or pf? more specifically, the parser takes as input an mg lexicon and a (partial) specification of lf and pf interface conditions (i.e. constraints over the lf and pf encoded in a syntactic structure), and it outputs the set of mg derivations (i.e. syntactic structures) that the (input) lexicon can generate and that satisfy the (input) interface conditions. the parser operates by first constructing an smt model of a lexicon and an smt model of derivation, with the two models linked by shared free variables to form an smt model of a minimalist parser. next, the parser converts the inputs into constraints, expressed as smt-formulae, that augment the smt model and serve to constrain the space of model solutions. finally, the parser obtains its output by using the z3 smt-solver, 3 a (modern) high-performance automatic theorem prover, to check whether the smt model is satisfiable -if it is, the smt-solver enumerates valid model-interpretations from which the parser recovers the (output) set of minimalist derivations. notably, this model of hlf is declarative, and so encompasses both semantic parsing and natural language generation. e.g. one can use the parser to generate language by: (i) inputting a lexicon and lf constraints; (ii) ordering the parser to "solve for syntax" and recover a derivation from the modelsolution; and (iii) obtaining the (output) generated pf from the recovered derivation. (here the inputs are known quantities and the derivation is an unknown quantity being solved for.) moreover, our model for hlf can be used to run experiments in which the input interface conditions are partially specified and the smt-solver is instructed to identify dependencies between the principles of syntax (encoded in the parser) and the features in the input lexicon -in this way, one can determine whether (and how) the syntactic principles and the lexicon do not adequately constrain a derivation to compensate for the absent (lf or pf) interface conditions. the remainder of this study is organized as follows. first, §2 reviews key principles of minimalist syntax and how they are modeled using mgs. next, §3 reviews related prior work within the parsing as deduction framework, which this study seeks to extend, and that motivates our approach. then, §4, §5 and §6 present the three key contributions of this study: §4 details the deductive parsing procedure, showing how the z3 smt-solver can be used to identify satisfiable interpretations of an smt model of a minimalist parser; §5 details the smt model of the minimalist parser, its underlying axiomatization of minimalist syntax, and how the model is constrained by user specified inputs; §6 details application of the parser to a representative set of example inputs and analyzes the output derivations, showing how the parser functions even when the input interface conditions are only partially specified. finally, §7 discusses how: (i) the smt model of the parser may be extended, and (ii) the parser can help linguists identify dependencies and contradictions between the model axioms encoding principles of syntax and the logical constraints derived from the input interface conditions. ## background: minimalist grammars we opted to model minimalist syntax using the minimalist grammar (mg) formalism (stabler, figure 1 : the parser outputs an mg derivation of "what has the man eaten?" that satisfies the lf & pf interface conditions in i 1 (of ## related work: parsing as deduction we have developed an mg parser within the parsing as deduction framework, which was first described by pereira and warren (1983), who showed how an axiomatization of a context-free grammar could be combined with a logical deduction engine to formulate a chart parser as a logic program. as pereira notes, key advantages of this framework include: (i) a connection between the deductions that yield a syntactic structure and the inferences needed to extract a semantic interpretation from said structure; (ii) the ability to handle filler-gap dependencies without altering the basic design of a chart parser. the parsing as deduction framework has since been employed to construct parsers for a variety of grammatical formalisms, including lexicalized context-free grammars, tree adjoining grammars, combinatory categorical grammars, and dependency grammars. @xcite notably, this framework has been used to develop parsers that model government and binding (gb) theory (a predecessor of minimalist syntax) by encoding principles of syntax within a system of axioms that mirrors the modular structure of gb theory (chomsky, 1981; johnson, 1989; fong, 1991). normally, these parsers employ prolog, the defacto language for constraint logic programming (clp). @xcite however, we leverage recent advances in the performance of automated theorem provers for smt, which enhances clp by enabling us to focus entirely on formulating (declarative) model axioms while the computer is free to decide how best to deduce a model solution (de moura and bjørner, checking the smt model. the procedure uses the smt-solver's model-checking routine (i.e. decision procedure) to determine whether there exists a satisfiable interpretation of the model (i.e. the conjunction of the smt-formulae in s) -if one exists, the procedure recovers it from the solver, and then (automatically) reconstructs an mg derivation from the (recovered) model interpretation. the procedure then pushes onto s a constraint (i.e. an smt-formula) that prohibits the interpretation of m d from being equivalent to any previously recovered (satisfiable) model interpretations; foot_9 this model-checking process is then run again to try and recover a (new) alternative mg derivation -this process is repeated until the solver cannot identify a (new) satisfiable model interpretation (because all model-solutions have already been identified). output. the procedure outputs the set of mg derivations that were reconstructed from the recovered (satisfiable) model interpretations -each (output) derivation accords with the (input) interface conditions, i, and can be generated from the (input) lexicon, l. finally, we illustrate the parsing procedure with a worked out example. consider the procedure taking as input the lexicon in ## specification of the smt model this section details the smt models of the mg derivation and mg lexicon -these models make up the heart of the parser introduced in this study. @xcite these models consist of: (i) uninterpreted (i.e. free) finite sorts that represent model-objects such as words, syntactic features, categories, nodes in a derivation tree, etc; (ii) uninterpreted (free) functions that establish relationships between modelobjects by mapping members of one or more sorts to another sort; (iii) model axioms -i.e. smtformulae -that constrain the valuation an smtsolver may assign to each uninterpreted function. 17 (see fig. 2 for a summary of the sorts and functions that make up the model.) crucially, since the model of the parser has finite size (being bounded by the input parameter, p), we can explicitly quantify all of the smt formulae in the model, thereby yielding a decidable model that is solvable in finite time. we turn first to the smt model of the lexicon. when constructing this model, the parsing procedure scans the input lexicon and instantiates several finite sorts: σ, that models the set of pfs; f, that models the set of feature-labels (e.g. {x, y, p, q}); and the lexicon node sort, ω, that models the syntactic features appearing in the input lexicon. @xcite the lexicon node sort is organized into disjoint subsets referred to as lexicon node sequences, with each subset corresponding to one of the distinct lexical feature sequences appearing in the input lexicon. @xcite among the uninterpreted functions in the lexicon model, one plays an especially critical role: the @xcite a complete, formal definition of these smt models, including all model axioms, may be found in ch. 2 of (indurkhya, 2021a); see appendix a for notes on reproducibility. @xcite all model axioms are written using propositional logic extended with (quantifier-free) theories of: (i) uninterpreted functions, (ii) pseudo-boolean constraints, and (iii) arithmetic. next we turn to the smt model of the derivation, which is composed of a finite sort, n, that models the nodes in the derivation. the derivation takes the form of a multi-dominance tree 23 that is formed by augmenting the derivation tree with additional edges corresponding to the movement of phrases via internal merge (see fig. 1 ). members of n are sub-divided into derivation node sequences, with each sequence corresponding to the projection of a lexical head within the derivation; 24 an important exception to this is a single member of n, ⊥, that serves as a null-value target for uninterpreted functions. the model's uninterpretable functions include: (a) a unary function, p, that maps each node in a derivation node sequence to its successor node (in that sequence). (b) a unary function, h, that maps each @xmath0.e. beginning) of the derivation node sequence to which x belongs; a derivation node @xmath1. (c) a binary function, m, that models merge: next the parsing procedure translates each of the (input) interface conditions (ics) into smtformulae that constrain the smt model of the derivation. lf ics stipulating (subject-predicate) agreement and the assignment of θ-roles (i.e. semantic roles) to arguments are translated into model constraints (i.e. smt-formulae) that require specific local hierarchical relations be established by merge, 27 and the sentence type (i.e. declarative vs. interrogative) is translated into model constraints that dictate which type of complementizer, c ques. or c decl. , heads the sentence. pf ics are translated into constraints that require the subject-verb-object (svo) ordering of the derived tree, in which all phrasal-movement and head-movement has taken place, match the linear order of words in the input sentence. @xcite notably, the smt-formulae encoding lf constraints are entirely separate from the smt-formulae encoding pf constraints. finally, the smt models of the lexicon and the derivation are connected by an uninterpreted function, µ, that maps each derivation node sequence to a lexicon node sequence, subject to the constraints: (i) µ • @xmath2, which lines up each projection in the derivation with a lexical feature sequences (for a lexical entry) in the lexicon; (ii) β ω • µ = β n , which ensures that each lexical head in a derivation has the same category as the lexical entry it originates from. (fig. 3 depicts these constraints and others as commutative diagrams.) there are also model-axioms that further restrict µ by requiring that pairs of nodes merged via em or im map to selectional or licensing features (respectively). ## parsing with partially specified inputs we validated the parsing procedure, and in particular the smt-models it constructs, by using it to parse each pair of interface conditions in if the input is limited to the pf ics in i 1 , the parser can output a derivation (see fig. 4 ) in which "the man" is the internal argument (as it merges with "eaten") and "what" is the external argument (as it merges with the light-verb, v). this alternative derivation is possible because the external and internal arguments are selected using the same feature, =y, and swapping where the two arguments merge into the vp-shell structure compels the axiom encoding the uniformity of θ-assignment hypothesis to assign semantic roles (to the arguments) that yield an incorrect reading of "what has the man eaten?" one solution is to refine the (selection) labels of nominal phrases (np) to encode θ-roles; however, the model must be updated to propagate np-labels to determiners (and complementizers and relative pronouns), or else the lexicon will grow untenably by multiplying out the determiners for each distinct selection label. conversely, if the input is instead limited to the lf ics in i 1 , then the parser can output a derivation (see fig. 5 ) where the auxiliary verb "has" is not raised because t -to-c head-movement is compelled by pf ics (and not by lf ics); consequently, the surfaced form, "what the man has eaten?", is ungrammatical. one solution is to add axioms that model economy conditions (collins, 2001), so that t -to-c head-movement may be omitted if doing so leaves the surfaced form unchanged. ## conclusion we have introduced an mg parser that is a computational model of hlf and is grounded in an smt-model encoding a novel axiomatization of minimalist syntax. the parser uses the z3 smtsolver, an automatic theorem prover, to answer the question: can the input lexicon yield a derivation that satisfies the input lf and pf interface conditions? in this way, parsing is translated into an (smt) decision problem, with model solutions corresponding to the derivations output by the parser. we demonstrated that the parser, implemented within the parsing as deduction framework, can operate on partially specified interface conditions. @xcite figure 4 : a derivation yielded by the parser, using the lexicon in this flexibility of the parser can be leveraged to observe when: (i) output derivations do not accord with the prescriptions of modern theories of minimalist syntax -inspecting these derivations can yield clues about how interface conditions and linguistic constraints cooperate to rule out derivations prohibited by the theory; (ii) the parser fails to output any derivation despite the theory prescribdesign enables it to operate on partially specified inputs, with the smt-solver in effect solving for the unspecified inputs (in addition to the derivation itself). e.g. if we specify the lf and pf interface conditions, but not the lexicon, then the parser will constrain the smt model of the derivation using the interface conditions, but will not constrain the smt model of the lexicon since no input lexicon was specified -then when the smt-solver obtains a satisfiable interpretation of the smt model of the parser, we can (automatically) recover from the interpretation of the lexicon model an mg lexicon that yields a derivation that satisfies the specified interface conditions. moreover, if we augment the parser by connecting multiple smt models of derivations, each constrained by a different pairing of interface conditions, to a single smt model of a lexicon, then the composite smt model can be used to infer an mg that can, for each pair of interface conditions, yield a derivation that satisfies that pairing -notably, this approach aligns with earlier work that used logic grammars to infer a lexicon (rayner et al., 1988). see (indurkhya, 2020) and (indurkhya, 2022) for detailed discussions of how augmenting the parser in this manner can yield instantaneous and incremental (respectively) computational models of language acquisition. figure 5 : a derivation yielded by the parser, using the lexicon in finally, a key advantage of this parser is that it enables a division of labor: the smt-solver is tasked with carrying out the logical deductions needed to find a model solution, leaving the linguist free to: (i) extend the parser, with the modular design of the smt-model enabling related sets of axioms to be modified without impacting the remainder of the model; foot_13 (ii) investigate how principles of syntax cooperate to constrain the space of derivations, and identify redundant principles that may be dropped to yield a simpler theory of syntax.