Paramorphisms
- 1 September 1992
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 4 (5) , 413-424
- https://doi.org/10.1007/bf01211391
Abstract
“Catamorphisms” are functions on an initial data type (an inductively defined domain) whose inductive definitional pattern mimics that of the type. These functions have powerful calculation properties by which inductive reasoning can be replaced by equational reasoning. This paper introduces a generalisation of catamorphisms, dubbed “paramorphisms”. Paramorphisms correspond to a larger class of inductive definition patterns; in fact, we show that any function defined on an initial type can be expressed as a paramorphism. In spite of this generality, it turns out that paramorphisms have calculation properties very similar to those of catamorphisms. In particular, we prove a Unique Extension Property and a Promotion Theorem for paramorphisms.Keywords
This publication has 6 references indexed in Scilit:
- Data structures and program transformationScience of Computer Programming, 1990
- Do-it-yourself type theoryFormal Aspects of Computing, 1989
- Constructing a calculus of programsPublished by Springer Nature ,1989
- Lectures on Constructive Functional ProgrammingPublished by Springer Nature ,1989
- An Introduction to the Theory of ListsPublished by Springer Nature ,1987
- How to prove algebraic inductive hypotheses without inductionPublished by Springer Nature ,1980