Reference. Categorial and categorical grammars
Cite
Cited by (2)
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.
Closed Categories and Categorial Grammar dougherty-1993
Cites 22 works (4 here)
With notes (4)
Introduction to Higher-Order Categorical Logic lambek_scott_1986
Formal Philosophy: Selected Papers of Richard Montague Montague1974-MONFPS
Categories for the Working Mathematician maclane_1971
External (18)
- The Semantics of Variety in Categorial Grammar (1983)
- A PRODUCTION GRAMMAR FOR HINDI KINSHIP TERMINOLOGY (1983)
- Lambek's Categorial Grammars (1982)
- Semantique doctrinale appliquee (1982)
- A MATHEMATICIAN LOOKS AT LATIN CONJUGATION (1979)
- Syntax and semantics: A categorical view (1970)
- Deductive systems and categories II. Standard constructions and closed categories (1969)
- Deductive systems and categories (1968)
- Lectures on Rings and Modules (1966)
- Closed Categories (1966)
- Eindeutigkeit und Mehrdeutigkeit formaler Sprachen (1966)
- On the Calculus of Syntactic Types (1961)
- Contributions to a Mathematical Analysis of the English Verb Phrase (1959)
- Combinatory Logic I (1958)
- A Quasi-Arithmetical Notation for Syntactic Description (1953)
- General Theory of Natural Equivalences (1945)
- A formulation of the simple theory of types (1940)
- Die syntaktische Konnexitat (1935)