SPINDLE : Spinning Raw Text into Lambda Terms with Graph Attention (2023)

Abstract: This paper describes SPINDLE, an open source Python module, providing an efficient and accurate parser for written Dutch that transforms raw text input to programs for meaning composition expressed as λ terms. The parser integrates a number of breakthrough advances made in recent years. Its output consists of hi-res derivations of a multimodal type-logical grammar, capturing two orthogonal axes of syntax, namely deep function-argument structures and dependency relations. These are produced by three interdependent systems: a static type-checker asserting the well-formedness of grammatical analyses, a state-of-the-art, structurally-aware supertagger based on heterogeneous graph convolutions, and a massively parallel proof search component based on Sinkhorn iterations. Packed in the software are also handy utilities and extras for proof visualization and inference, intended to facilitate end-user utilization.

## introduction the transparency and formal well-behavedness of lambda calculi make them the ideal format for expressing compositional structures, a fact that has been duly emphasized by parsers and tools with a predominant focus on semantics. lambda calculi form a key ingredient of type-logical grammars, where they find use as the computational counterpart of a so-called grammar logic, a substructural logic of the intuitionistic linear variety that is designed to capture (aspects of) natural language syntax and semantics @xcite . for typelogical grammars, the curry-howard isomorphism guarantees a straightforward passage between logical rules, type constructors and term-forming operators; put simply, parse ≡ proof ≡ program, and category ≡ proposition ≡ type. the modus operandi 1 stylized spind 2 λe and standing for spindle parses into dependency-decorated λ expressions. source code and user instructions can be found at https://github.com/ konstantinoskokos/spindle . by extension, words may only combine in a strict, well-typed manner, forming larger phrases in the process. parsing becomes a process of logical deduction, at the end of which the result (a proof) gives rise to a recipe for meaning assembly (a program). this program is turned into executable code as soon as one plugs in appropriate interpretations for the lexical constants (words) and for the term operations (composition instructions). the set-up is general-purpose in that it readily accommodates different choices for these interpretations; valid targets can for instance be found in (truth-conditional) formal semantics, distributionalcompositional models @xcite , or tableau-based theorem provers @xcite . in this work, we are interested in what happens prior to semantic execution; that is, we abstract away from lexical semantics and seek to reveal the compositional recipe underlying a natural language utterance. to that end, we employ a type grammar aimed at capturing two different syntactic axes, only rarely observed together in the wild: functionargument structures and dependency relations. to procure a derivation from an input phrase, we design and implement a system combining three distinct but communicating components. component number one is the implementation of the grammar's type system -it comes packed with a number of useful facilities, most important being a static type checker that verifies the syntactic well-formedness of the analyses construed. component number two is a supertagger responsible for assigning a type to each input word -the tagger is formulated on the basis of a hyper-efficient heterogeneous graph convolution kernel that boasts state-of-the-art accuracy among categorial grammar datasets. the third and last component is a neural permutation module that exploits the linearity constraint of the target logic to simplify proof search as optimal transport learning @xcite -this reformulation allows for a massively parallel and easily optimizable implementation. the three components alternate roles through the processing pipeline, switching between phases of low level linear algebra routines and high level logical reasoning (gpu and cpu intensive, respectively). their integration yields a lightspeed-fast and highly accurate neurosymbolic parser, neatly packaged and made publicly available. ## conclusion & future work thus concludes the demonstration tour of spind 2 λe: a unique neurosymbolic parser that can accurately and efficiently convert raw text into λ expressions. unlike cheaper alternatives, these λ expressions are not structureless ad-hoc imitations produced from arbitrary decoding, but executable, type-safe and 100% guaranteed correct programs. the software focuses on dutch, but the universality of the intuitionistic linear core allows easy cross-lingual adaptation that essentially boils down to retraining with a new type lexicon; a french implementation is currently in the works @xcite . as to what the future holds, the intention is to keep the module synchronized and up-to-date with aethel: any upcoming major release of the latter will be reflected in an update of the former (be it soft patching or retraining). compatibility aside, planned features include deploying the module as a web service, compiling it as a stand-alone package and documenting the annotations (so as to be more inclusive towards the type-uninitiated). any performance, stability or efficiency improvements stemming from related research or moments of engineering inspiration are also likely to find their way to the user-facing front. contributions and feedback are always welcome.