TY - JOUR

T1 - Category Theoretic Semantics for Typed Binding Signatures with Recursion

AU - Power, John

AU - Tanaka, M

PY - 2008

Y1 - 2008

N2 - We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and ωCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad T_{fp} on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [F, Set] to [(SA)^{op}, V^{A}]. We define a substitution monoidal structure on [(SA)^{op}, V^{A}], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previouswork by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.

AB - We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and ωCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad T_{fp} on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [F, Set] to [(SA)^{op}, V^{A}]. We define a substitution monoidal structure on [(SA)^{op}, V^{A}], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previouswork by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.

UR - http://www.scopus.com/inward/record.url?scp=50249102644&partnerID=8YFLogxK

UR - http://www.metapress.com/content/7224025073182m45/?p=5af41a9b342449e9ba1f34fd2ddd442e&pi=4

M3 - Article

VL - 84

SP - 221

EP - 240

JO - Fundamenta Informaticae

JF - Fundamenta Informaticae

SN - 0169-2968

IS - 2

ER -