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.
Higher-order theories / André, Hirschowitz; Marco, Maggesi. - ELETTRONICO. - (2007), pp. 1-12.
Higher-order theories
Marco Maggesi
2007
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.File | Dimensione | Formato | |
---|---|---|---|
2008-Higher-Order Theory.pdf
accesso aperto
Tipologia:
Altro
Licenza:
Tutti i diritti riservati
Dimensione
170.27 kB
Formato
Adobe PDF
|
170.27 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.