To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Unnesting of copatterns… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Unnesting of copatterns

Chapter in book
Authors A. Setzer
Andreas Abel
B. Pientka
D. Thibodeau
Published in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISBN 9783319089171
Publisher Springer
Publication year 2014
Published at Department of Computer Science and Engineering (GU)
Language en
Keywords abstract reduction system , algebraic data types , ARS , coalgebras , codata , conservative extension , copattern matching , Pattern matching , strong normalisation , weak normalisation
Subject categories Computer and Information Science


Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e. the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong and weak normalisation: a term of the original language is strongly/weakly normalising in one language if and only if it is so in the other. In the proof we develop more general criteria which guarantee that extensions of abstract reduction systems are conservative and preserve strong or weak normalisation. © 2014 Springer International Publishing Switzerland.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?