### Paramorphisms

Paramorphisms correspond to the concept of primitive recursion. A paramorphism can be defined in terms of products and catamorphisms

or characterised by the universal property

It is a (strict) specialisation of the generalised tupling transformation mentioned before. I didn't get the statement about generalised tupling precise enough at the beginning, so I was confused by why the universal property of paramorphisms can be a bidirectional implication, until I realised that the statement of general tupling can be proven to be bidirectional:

Once the full-fledged tupling rule is established, the universal property of paramorphisms follows as an easy corollary since `id = cata α`

.

--

It took me more time than I expected...

Labels: Program Derivation

<< 回到主頁