Abstract syntax

Abstract syntax describes a program or logical theory in terms that are syntactical, yet abstracted from a sequence of symbols. It is most familiar to programmers in the form of abstract syntax trees , although abstract syntax need not take of the form of a tree, nor should every expression tree be considered abstract syntax.

Abstract syntax is intermediate between concrete syntax and the invariant notion of program/theory that emerges from categorical logic.

Categorical abstract syntax

The most famous use of category theory in PLT/logic is to give an invariant, or presentation-independent, description of programs/theories. However, category theory can also provide the mathematics for abstract syntax.

Variable binding

Marcelo Fiore and others give an abstract syntax for variable binding, based on presheaf categories and with roots in in Kelly’s clubs.

  • Fiore, Plotkin, Turi, 1999: Abstract syntax and variable binding (doi)
    • Influential paper whose “fundamental idea is to turn contexts [of variables] into the ‘index category’ of presheaves”
    • Connection to species and operads described in: Fiore, 2005, invited talk: Mathematical models of computational and combinatorial structures (doi)
  • Tanaka, 2000: Abstract syntax and variable binding for linear binders (doi)
    • Adapts (Fiore et al, 1999) from cartesian to linear setting
  • Tanaka & Power, 2006: Pseudo-distributive laws and axiomatics for variable binding (doi)
    • Conference version: Tanaka & Power, 2005: A unified category-theoretic formulation of typed binding signatures (doi)
    • Talk: Power, 2007: Abstract syntax: substitution and binders (doi)
    • Extension from variable binding to binding signatures: Power & Tanaka, 2005: Binding signatures for generic contexts (doi)
  • Fiore, 2008: Second-order and dependently-sorted abstract syntax (doi)
    • Part II gives abstract syntax for dependent types, as found in GATs

Term graphs

  • Garner, 2012: An abstract view on syntax with sharing (doi, arxiv)
    • Generalizes abstract syntax for term trees based on initial algebras of endofunctors to term graphs, or term trees with sharing
    • Sec. 1 has useful review of previous work