Picture map of Europe with pins indicating European capital cities

Open Access research with a European policy impact...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by Strathclyde researchers, including by researchers from the European Policies Research Centre (EPRC).

EPRC is a leading institute in Europe for comparative research on public policy, with a particular focus on regional development policies. Spanning 30 European countries, EPRC research programmes have a strong emphasis on applied research and knowledge exchange, including the provision of policy advice to EU institutions and national and sub-national government authorities throughout Europe.

Explore research outputs by the European Policies Research Centre...

Positive inductive-recursive definitions

Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik (2013) Positive inductive-recursive definitions. In: Algebra and Coalgebra in Computer Science. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, Berlin, pp. 19-33. ISBN 9783642402050

Full text not available in this repository. Request a copy from the Strathclyde author


We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.