Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi

Masahito Hasegawa

In Proc. 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97), Springer LNCS 1210 (1997) 196-213

Abstract

Cyclic sharing (cyclic graph rewriting) has been used as a practical technique for implementing recursive computation efficiently. To capture its semantic nature, we introduce categorical models for lambda calculi with cyclic sharing (cyclic lambda graphs), using notions of computation by Moggi / Power and Robinson and traced monoidal categories recently introduced by Joyal, Street and Verity. The former is used for representing the notion of sharing, whereas the latter for cyclic data structures.

Our new models, which are shown to be sound and complete for the cyclic lambda calculi, provide a semantic framework for understanding recursion created from cyclic sharing, which includes traditional models for recursion created from fixed points as special cases. Our cyclic lambda calculus then serves as a uniform language for this wider range of models of recursive computation.

[gzipped ps file][pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page