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
<< 回到主頁