Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Constructing List Homomorphisms from Proofs
verfasst von : Yun-Yan Chi, Shin-Cheng Mu
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.