Free Σ-Monoids: A Higher-Order Syntax with Metavariables

  • Makoto Hamana
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3302)


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.


Function Symbol Monoidal Category Object Variable Binding Signature Construction Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [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
  3. [Ham01]
    Hamana, M.: A logic programming language based on binding algebras. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 243–262. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. [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
  5. [HO01]
    Hashimoto, M., Ohori, A.: A typed context calculus. Theoretical Computer Science 266, 249–271 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  6. [Mac71]
    Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971)CrossRefzbMATHGoogle Scholar
  7. [Mas99]
    Mason, I.A.: Computing with contexts. Higher-Order and Symbolic Computation 12(2), 171–201 (1999)CrossRefzbMATHGoogle Scholar
  8. [Pit03]
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  9. [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
  10. [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
  11. [SSB99]
    Sato, M., Sakurai, T., Burstall, R.: Explicit environments. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 340–354. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. [SSK01]
    Sato, M., Sakurai, T., Kameyama, Y.: A simply typed context calculus with first-class environments. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, pp. 359–374. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. [SSKI03]
    Sato, M., Sakurai, T., Kameyama, Y., Igarashi, A.: Calculi of meta-variables. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003 and KGC. LNCS, vol. 2803, pp. 484–497. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. [Tal93]
    Talcott, C.L.: A theory of binding structures and applications to rewriting. Theoretical Computer Science 112(1), 99–143 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  15. [UPG03]
    Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003 and KGC. LNCS, vol. 2803, pp. 513–527. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Makoto Hamana
    • 1
  1. 1.Department of Computer ScienceGunma UniversityJapan

Personalised recommendations