TY - JOUR
T1 - Substitution in non-wellfounded syntax with variable binding
AU - Matthes, Ralph
AU - Uustalu, Tarmo
N1 - Funding Information:
1 Attending ETAPS’03 was partially financed by an EC HSC grant. 2 [email protected] 3Supported 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 work was largely done while the author was with Dep. de Informática, Universidade do Minho, Braga, Portugal. His visit to LMU München in Jan. 2002 was financed by the Graduiertenkolleg “Logik in der Informatik” of the Deutsche Forschungsge-meinschaft. Attending ETAPS 2003 was made possible by a travel grant from the Estonian Information Technology Foundation. 4 [email protected]
PY - 2003/7
Y1 - 2003/7
N2 - 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. In the non-wellfounded case, the fundamental operation of substitution is more beneficially defined in terms of primitive corecursion than coiteration.
AB - 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. In the non-wellfounded case, the fundamental operation of substitution is more beneficially defined in terms of primitive corecursion than coiteration.
KW - Final coalgebra
KW - Functor category
KW - Monad
KW - Non-wellfounded syntax
KW - Primitive corecursion
KW - Substitution
KW - Variable binding
UR - http://www.scopus.com/inward/record.url?scp=0942302122&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(04)80639-X
DO - 10.1016/S1571-0661(04)80639-X
M3 - Conference article
AN - SCOPUS:0942302122
SN - 1571-0661
VL - 82
SP - 191
EP - 205
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1
T2 - CMCS'03, Coalgebraic Methods in Computer Science Satellite Event for ETAPS 2003)
Y2 - 5 April 2003 through 6 April 2003
ER -