<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>
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 (S1)^o^p: 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 T"c"o"c-=[(-)^o^p,Set] for free cocompletions, one can define a canonical substitution monoidal structure on the category [(S1)^o^p,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(Inj^o^p,Set) studied by Gabbay and Pitts in their quite different analysis of binders, which we compare and contrast with that of Fiore et al.
Theoretical Computer Science, Computer Science(all)
Theoretical Computer Science, Computer Science(all)
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |