TY - GEN

T1 - Generalising and dualising the third list-homomorphism theorem

T2 - 16th ACM SIGPLAN International Conference on Functional Programming, ICFP'11

AU - Mu, Shin Cheng

AU - Morihata, Akimasa

PY - 2011/10/19

Y1 - 2011/10/19

N2 - 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.

AB - 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.

KW - Program derivation

KW - Third list homomorphism theorem

UR - http://www.scopus.com/inward/record.url?scp=80054060919&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80054060919&partnerID=8YFLogxK

U2 - 10.1145/2034773.2034824

DO - 10.1145/2034773.2034824

M3 - Conference contribution

AN - SCOPUS:80054060919

SN - 9781450308656

T3 - Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP

SP - 385

EP - 391

BT - ICFP'11 - Proceedings of the 2011 ACM SIGPLAN International Conference on Functional Programming

Y2 - 19 September 2011 through 21 September 2011

ER -