Free Σ-Monoids: A Higher-Order Syntax with Metavariables
The notion of Σ-monoids is proposed by Fiore, Plotkin and Turi, to give abstract algebraic model of languages with variable binding and substitutions. In this paper, we give a free construction of Σ-monoids. The free Σ-monoid over a given presheaf serves a well-structured term language involving binding and substitutions. Moreover, the free Σ-monoid naturally contains interesting syntactic objects which can be viewed as “metavariables” and “environments”. We analyse the term language of the free Σ-monoid by relating it with several concrete systems, especially the λ-calculus extended with contexts.
KeywordsFunction Symbol Monoidal Category Object Variable Binding Signature Construction Rule
Unable to display preview. Download preview PDF.
- [FPT99]Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. 14th Annual Symposium on Logic in Computer Science, pp. 193–202 (1999)Google Scholar
- [GU03]Ghani, N., Uustalu, T.: Explicit substitutions and higher order syntax. In: Proceedings of 2nd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2003, pp. 135–146 (2003)Google Scholar
- [Ham03]Hamana, M.: Term rewriting with variable binding: An initial algebra approach. In: Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003). ACM Press, New York (2003)Google Scholar
- [Plo00]Plotkin, G.: Another meta-language for programming with bound names modulo renaming. In: Winter Workshop in Logics, Types and Rewriting, Heriot-Watt University (February 2000) (Lecture slides)Google Scholar
- [San98]Sands, D.: Computing with contexts: A simple approach. In: Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II). Electronic Notes in Theoretical Computer Science, vol. 10 (1998)Google Scholar