Cutting Languages Down to Size

Programming languages and other formal languages (e.g. data representation languages like JSON) are often described via a context-free formal grammar, e.g. in the Extended Backus–Naur form that can be automatically processed by tools like Yacc and Bison. These languages tend to grow over time, as more features are added and the language covers more application cases. On the one hand, this makes the language more powerful. But on the other hand, this often makes the language harder to understand and harder to implement, increasing the barrier to entry for new developers.

This problem can, of course, be addressed by manually maintaining simplified or partial grammars. However, this creates not only a maintenance overhead, but may also lead to undesired and even unnoticed divergences of the full and the simplified grammar. Instead, we propose to use automatically extraction of self-contained parts of a formal grammar to create simpler sub-languages.

Our particular use case is the TPTP syntax for automated theorem proving tools. TPTP defines a family of languages, from pure first-order clause normal form (CNF) and full first order (FOF) via typed first-order (TFF), eventually to typed higher-order logic (THF). The language can be used to write both input problems (i.e. lists of logical formulae), but also derivations (where some of the formulas are input formulas, and the others are justified by reference to existing formulas and some mechanism for deriving the former from the latter. Most of the extensions are modular and even conservative (i.e. FOF is mostly a superset of CNF, and normally FOF is used as shorthand for CNF+FOF), and we are interested in e.g. extracting just a grammar for CNF or CNF+FOF. We are also interested extracting languages that do not allow certain features, e.g. a language in which only the pure input format in specified, not logical derivations. The task of this thesis is the design of a tool that performs this extraction and presents the result in a format that is both machine readable, but also friendly to use for human users.

One approach to this would be to a) select a given non-terminal node as the start symbol for the new grammar and b) block the undesired productions starting at certain non-terminal symbols. The tool can then start at the selected new start symbol and follow all legal transition to collect the remaining reachable grammar. It can also clean-up the resulting grammar by inlining rules for non-terminals with only a single production. An outstanding solution would also heuristically associate comments with grammar productions, and keep the comments referring to the remaining productions in place.

There are several possible tools with different levels of convenience for the user:

• A basic command line tool which accepts a grammar file and a control file listing blocked productions, and that then produces the reduced grammar in the form of a new grammar file. In agile terms, this would be the minimal viable product.
• The same, with maintaining of comments.
• The same, but with (optional) inlining of single-alternative rules.
• A visualization tool (e.g. based on Graphviz) visualizing the full and the reduced grammar.
• A GUI tool allowing the user to interactively select which productions should be blocked and dynamically visualizing the resulting new grammar. Preferably, this would use the command line version in the background and be able to generate and export not only the reduced grammar, but also the control file.

The topic will be co-supervised by Stephan Schulz and Geoff Sutcliffe, who will be available (via email or video conference) to discuss pearticulars of the TPTP grammar, its format and applications. It is suitable for one or two students - in the case of two students we expect not only the command line tool, but also a usable GUI.

Literature

Weblinks

• The full TPTP syntax
• PLY (Python Lex-Yacc) is an Open Source Python implementation of Lex/Yacc and may be useful for extracting the parser for Yacc/Bison grammars