Archive for the 'Initial algebras' Category

Monadic presentations of untyped lambda-terms using inductive datatypes

By Thorsten Altenkirch and Bernhard Reus, from CSL 1999, available from Thorsten Altenkirch’s website:

We present a definition of untyped lambda-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended a Kleisli triple, which is a concise way to verify the substitution laws for lambda-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed lambda-calculus using dependent types, and show that this is an instance of a generalisation of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.


Term rewriting with variable binders: an initial algebra approach

By Makoto Hamana, from PPDP 2003, available from Makoto Haman’s website:

We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner; firstly we present the term language, then formulate equational logic, and finally define rewrite systems by two styles: rewrite logic and pattern matching styles. The novelty of this development is that we follow an initial algebra approach in an extended notion of Σ-algebras in various functor categories. These are based on Fiore-Plotkin Turi’s presheaf semantics of variable binding and Lüth-Ghani’s monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs are initial algebras in suitable categories. Finally, we discuss our design choice of BTRSs from a semantic perspective.