Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

APLAS

2011

ACM

2011

ACM

The well-known third list homomorphism theorem states that if a function h is both an instance of foldr and foldl, it is a list homomorphism. Plenty of previous works devoted to constructing list homomorphisms, however, overlook the fact that proving h is both a foldr and a foldl is often the hardest part which, once done, already provides a useful hint about what the resulting list homomorphism could be. In this paper we propose a new approach: to construct a possible candidate of the associative operator and, at the same time, to transform a proof that h is both a foldr and a foldl to a proof that h is a list homomorphism. The eﬀort constructing the proof is thus not wasted, and the resulting program is guaranteed to be correct.

Related Content

Added |
12 Dec 2011 |

Updated |
12 Dec 2011 |

Type |
Journal |

Year |
2011 |

Where |
APLAS |

Authors |
Yun-Yan Chi, Shin-Cheng Mu |

Comments (0)