Substitution in non-wellfounded syntax with variable binding

Inspired from the recent developments in theories of non-wellfounded syntax (coinductively defined languages) and of syntax with binding operators, the structure of algebras of wellfounded and non-wellfounded terms is studied for a very general notion of signature permitting both simple variable binding operators as well as operators of explicit substitution. This is done in an extensional mathematical setting of initial algebras and final coalgebras of endofunctors on a functor category. The main technical tool is a novel concept of heterogeneous substitution systems.

Authors

• Ralph Matthes
• Tarmo Uustalu

Keywords

• Substitution
• Non-wellfounded syntax
• Variable binding
• Monad
• Functor category
• Final coalgebra
• Primitive corecursion