Reference. ACGtk: A toolkit for developing and running abstract categorial grammars

Abstract categorial grammars (ACGs) is an expressive grammatical framework whose formal properties have been extensively studied. While it can provide its own account, as a grammar, of linguistic phenomena, it is known to encode several grammatical formalisms, including context-free grammars, but also mildly context-sensitive formalisms such as tree-adjoining grammars or m-linear context-free rewriting systems for which parsing is polynomial. The ACG toolkit we present provides a compiler, acgc, that checks and turns ACGs into representations that are suitable for testing and parsing, used in the acg interpreter. We illustrate these functionalities and discuss implementation features, in particular the Datalog reduction on which parsing is based, and the magic set rewriting techniques that can further be applied.

Cite

Cite as @Guillaume2024 (helia, typst) · \cite{Guillaume2024} (LaTeX)
BibTeX
bibtex · 16 lines
@inproceedings{Guillaume2024,
 title = {ACGtk: A Toolkit for Developing and Running Abstract Categorial Grammars},
 author = {Guillaume, Maxime and Pogodalla, Sylvain and Tourneur, Vincent},
 year = {2024},
 isbn = {978-981-97-2299-0},
 doi = {10.1007/978-981-97-2300-3_2},
 url = {https://doi.org/10.1007/978-981-97-2300-3_2},
 booktitle = {Functional and Logic Programming: 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15–17, 2024, Proceedings},
 pages = {13–30},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 location = {Kumamoto, Japan},
 keywords = {Abstract Categorial Grammars, Natural Language Processing, OCaml, Datalog},
 numpages = {18},
 abstract = {Abstract categorial grammars (ACGs) is an expressive grammatical framework whose formal properties have been extensively studied. While it can provide its own account, as a grammar, of linguistic phenomena, it is known to encode several grammatical formalisms, including context-free grammars, but also mildly context-sensitive formalisms such as tree-adjoining grammars or m-linear context-free rewriting systems for which parsing is polynomial. The ACG toolkit we present provides a compiler, acgc, that checks and turns ACGs into representations that are suitable for testing and parsing, used in the acg interpreter. We illustrate these functionalities and discuss implementation features, in particular the Datalog reduction on which parsing is based, and the magic set rewriting techniques that can further be applied.}
}
hayagriva YAML (typst)
yaml · 20 lines
Guillaume2024:
  type: article
  title: 'ACGtk: A Toolkit for Developing and Running Abstract Categorial Grammars'
  author:
  - Guillaume, Maxime
  - Pogodalla, Sylvain
  - Tourneur, Vincent
  date: 2024
  page-range: 13-30
  url: https://doi.org/10.1007/978-981-97-2300-3_2
  serial-number:
    doi: 10.1007/978-981-97-2300-3_2
    isbn: 978-981-97-2299-0
  abstract: Abstract categorial grammars (ACGs) is an expressive grammatical framework whose formal properties have been extensively studied. While it can provide its own account, as a grammar, of linguistic phenomena, it is known to encode several grammatical formalisms, including context-free grammars, but also mildly context-sensitive formalisms such as tree-adjoining grammars or m-linear context-free rewriting systems for which parsing is polynomial. The ACG toolkit we present provides a compiler, acgc, that checks and turns ACGs into representations that are suitable for testing and parsing, used in the acg interpreter. We illustrate these functionalities and discuss implementation features, in particular the Datalog reduction on which parsing is based, and the magic set rewriting techniques that can further be applied.
  parent:
    type: proceedings
    title: 'Functional and Logic Programming: 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15–17, 2024, Proceedings'
    publisher:
      name: Springer-Verlag
      location: Kumamoto, Japan
Cited by (1)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsers

We present Dependent Lambek Calculus (Lambek𝙳), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek𝙳, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek𝙳 using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb
Cites 32 works (1 here)
With notes (1)

The mathematics of sentence structure lambek58

DOI
External (31)
Guillaume2024 reference entries/refs/Guillaume2024/Guillaume2024.hel