Higher-order theories
Logic in Computer Science
2008-09-09 v2
Abstract
We extend our approach to abstract syntax (with binding constructions) through modules and linearity. First we give a new general definition of arity, yielding the companion notion of signature. Then we obtain a modularity result as requested by Ghani and Uustalu (2003): in our setting, merging two extensions of syntax corresponds to building an amalgamated sum. Finally we define a natural notion of equation concerning a signature and prove the existence of an initial semantics for a so-called representable signature equipped with a set of equations.
Cite
@article{arxiv.0704.2900,
title = {Higher-order theories},
author = {Andre' Hirschowitz and Marco Maggesi},
journal= {arXiv preprint arXiv:0704.2900},
year = {2008}
}