Abstract Syntax: Substitution and Binders


Power, J., 2007. Abstract Syntax: Substitution and Binders. Electronic Notes in Theoretical Computer Science, 173, pp. 3-16.

Related documents:

PDF (Power_ENTCS_2007_173_3.pdf) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (776kB) | Preview


    We summarise Fiore et al's paper on variable substitution and binding, then axiomatise it. Generalising their use of the category F of finite sets to model untyped cartesian contexts, we let S be an arbitrary pseudo-monad on Cat and consider op(S1): this generality includes linear contexts, affine contexts, and contexts for the Logic of Bunched Implications. Given a pseudo-distributive law of S over the (partial) pseudo-monad Tcoc−=[op(−),Set] for free cocompletions, one can define a canonical substitution monoidal structure on the category [op(S1),Set], generalising Fiore et al's substitution monoidal structure for cartesian contexts: this provides a natural substitution structure for the above examples. We give a concrete description of this substitution monoidal structure in full generality. We then give an axiomatic definition of a binding signature, then state and prove an initial algebra semantics theorem for binding signatures in full generality, once again extending the definitions and theorem of Fiore et al. A delicate extension of the research includes the category Pb(Injop,Set) studied by Gabbay and Pitts in their quite different analysis of binders, which we compare and contrast with that of Fiore et al.


    Item Type Articles
    CreatorsPower, J.
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementPower_ENTCS_2007_173_3.pdf: NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, vol 173, 2007, DOI 10.1016/j.entcs.2007.02.024
    ID Code26515


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...