Advertisement
Published in:
2011 | OriginalPaper | Chapter
Constructing List Homomorphisms from Proofs
Authors : Yun-Yan Chi, Shin-Cheng Mu
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.