Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 155-174 |
| Number of pages | 20 |
| Journal | Theoretical Computer Science |
| Volume | 327 |
| Issue number | 1-2 |
| DOIs | |
| Publication status | Published - 25 Oct 2004 |
Bibliographical note
Funding Information: We are grateful to Felix Joachimski for discussions and encouragement and to Andreas Abel for hinting at the counterexample of powerlists. R. Matthes’ participation in ETAPS’03 was partially financed by an EC HSC grant. T. Uustalu’s research was supported by the Portuguese Foundation for Science and Technology under grant No. PRAXIS/C/EEI/ 14172/98 and by the Estonian Science Foundation under grant No. 5567. The visit of T. Uustalu to LMU München in Jan. 2002 was financed by the Graduiertenkolleg “Logik in der Informatik” of the Deutsche Forschungsgemeinschaft; his participation in ETAPS’03 was possible thanks to a travel grant from the Estonian Information Technology Foundation.Other keywords
- Final coalgebra
- Functor category
- Monad
- Non-wellfounded syntax
- Primitive corecursion
- Substitution
- Variable binding