Generalising and dualising the third list-homomorphism theorem

Shin-Cheng Mu and Akimasa Morihata. In the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), pages 385-391.
[PDF]

The third list-homomorphism theorem says that a function is a list homomorphism if it can be described as an instance of both a foldr and a foldl. We prove a dual theorem for unfolds and generalise both theorems to trees: if a function generating a list can be described both as an unfoldr and an unfoldl, the list can be generated from the middle, and a function that processes or builds a tree both upwards and downwards may independently process/build a subtree and its one-hole context. The point-free, relational formalism helps to reveal the beautiful symmetry hidden in the theorem.

Leave a Comment

Your email address will not be published. Required fields are marked *