Sciweavers

Share
APLAS
2011
ACM

Constructing List Homomorphisms from Proofs

7 years 6 months ago
Constructing List Homomorphisms from Proofs
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 effort constructing the proof is thus not wasted, and the resulting program is guaranteed to be correct.
Yun-Yan Chi, Shin-Cheng Mu
Added 12 Dec 2011
Updated 12 Dec 2011
Type Journal
Year 2011
Where APLAS
Authors Yun-Yan Chi, Shin-Cheng Mu
Comments (0)
books