Free Σ-monoids: A higher-order syntax with metavariables

Abstract. 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.