Für foldr haben wir das Fusionsgesetz : Wenn f streng ist, f a = b und
f (g x y) = h x (f y) für alle x, y , dann f . foldr g a = foldr h b .
Wie kann man ein ähnliches Gesetz für foldr1 entdecken / ableiten? (Es kann natürlich nicht einmal die gleiche Form annehmen - bedenke, dass beide Seiten auf [x] handeln.)
Sie können freie Sätze verwenden, um Aussagen wie das Fusionsgesetz abzuleiten. Die Automatische Generierung von freien Theoremen funktioniert für Sie, Die folgende Anweisung wird automatisch abgeleitet, wenn Sie foldr1 oder den Typ (a -> a -> a) -> [a] -> a eingeben.
Wenn f strict und f (p x y) = q (f x) (f y)) für alle x und y haben Sie f (foldr1 p z) = foldr1 q (map f z)) . Das heißt, im Gegensatz zu Ihrer Aussage über foldr erhalten Sie auf der rechten Seite ein zusätzliches map f .
Beachten Sie auch, dass das freie Theorem für foldr etwas allgemeiner ist als Ihr Fusionsgesetz und daher dem Gesetz für foldr1 ziemlich ähnlich sieht. Nämlich für die strikten Funktionen g und f wenn g (p x y) = q (f x) (g y)) für alle x und y dann g (foldr p z v) = foldr q (g z) (map f v)) .
Ich weiß nicht, ob etwas für foldr1 befriedigend sein wird. [Ich denke] Es ist nur definiert als
Lassen Sie uns zuerst erweitern, was Sie oben haben, um an der gesamten Liste zu arbeiten,
%Vor%für foldr1, könnte man sagen,
%Vor% um in foldr1 zu rekondensieren, können Sie eine imaginäre Funktion erstellen, die f auf das linke Element abbildet, für ein Ergebnis von
Tags und Links haskell functional-programming