Anamorphismus - Anamorphism

In der Computerprogrammierung ist ein Anamorphismus eine Funktion, die durch wiederholte Anwendung der Funktion auf ihr vorheriges Ergebnis eine Sequenz erzeugt. Sie beginnen mit einem Wert A und wenden eine Funktion f darauf an, um B zu erhalten. Dann wenden Sie f auf B an, um C zu erhalten, und so weiter, bis eine Abschlussbedingung erreicht ist. Der Anamorphismus ist die Funktion, die die Liste von A, B, C usw. generiert. Sie können sich den Anamorphismus als Entfaltung des Anfangswerts in eine Folge vorstellen.

Die obige Beschreibung des Laien kann formaler in der Kategorientheorie formuliert werden : Der Anamorphismus eines koinduktiven Typs bezeichnet die Zuordnung einer Koalgebra zu ihrem eindeutigen Morphismus zur endgültigen Koalgebra eines Endofunktors . Diese Objekte werden in der funktionalen Programmierung als Unfolds verwendet .

Das kategorische Dual (auch bekannt als das Gegenteil) des Anamorphismus ist der Katamorphismus .

Anamorphismen in der funktionalen Programmierung

In der funktionalen Programmierung , eine Anamorphismus ist eine Verallgemeinerung des Begriffs entfaltet sich auf coinductive Listen . Formal sind Anamorphismen generische Funktionen , die ein Ergebnis eines bestimmten Typs kokursiv konstruieren können und die durch Funktionen parametrisiert werden, die den nächsten einzelnen Schritt der Konstruktion bestimmen.

Der betreffende Datentyp wird als größter Fixpunkt ν X definiert. FX eines Funktors F . Aufgrund der universellen Eigenschaft finaler Koalgebren gibt es einen eindeutigen Koalgebra-Morphismus A → ν X . FX für jede andere F- Koalgebra a: A → FA . Somit kann man Funktionen von einem Typ A _in_ einen koinduktiven Datentyp definieren, indem man eine Koalgebra-Struktur a auf A spezifiziert .

Beispiel: Potenziell unendliche Listen

Als Beispiel wird der Typ von potentiell unendlichen Listen (mit Elementen eines festen Typs value ) als Fixpunkt [Wert] = ν X angegeben. value × X + 1 , dh eine Liste besteht entweder aus einem Wert und einer weiteren Liste oder ist leer. Eine (Pseudo-) Haskell -Definition könnte so aussehen:

data [value] = (value:[value]) | []

Es ist der Fixpunkt des Funktors F value, wobei:

data Maybe a = Just a | Nothing
data F value x = Maybe (value, x)

Man kann leicht überprüfen, dass der Typ tatsächlich [value]isomorph zu F value [value]ist und somit [value]der Fixpunkt ist. (Beachten Sie auch, dass in Haskell der kleinste und der größte Fixpunkt von Funktoren zusammenfallen, daher sind induktive Listen dasselbe wie koinduktive, potenziell unendliche Listen.)

Der Anamorphismus für Listen (dann normalerweise als unfold bekannt ) würde eine (potenziell unendliche) Liste aus einem Zustandswert erstellen. Normalerweise nimmt die Abwicklung einen Zustandswert xund eine Funktion an f, die entweder ein Paar aus einem Wert und einem neuen Zustand oder ein Singleton ergibt, um das Ende der Liste zu markieren. Der Anamorphismus würde dann mit einem ersten Startwert beginnen, berechnen, ob die Liste fortgesetzt oder endet, und im Falle einer nicht leeren Liste den berechneten Wert dem rekursiven Aufruf des Anamorphismus voranstellen.

Eine Haskell-Definition einer Entfaltung oder eines Anamorphismus für Listen, genannt ana, lautet wie folgt:

ana :: (state -> Maybe (value, state)) -> state -> [value]
ana f stateOld = case f stateOld of
            Nothing                -> []
            Just (value, stateNew) -> value : ana f stateNew

Mit ana können wir nun ganz allgemeine Funktionen implementieren , zum Beispiel einen Countdown:

f :: Int -> Maybe (Int, Int)
f current = let oneSmaller = current - 1
            in   if oneSmaller < 0
                   then Nothing
                   else Just (oneSmaller, oneSmaller)

Diese Funktion dekrementiert eine ganze Zahl und gibt sie gleichzeitig aus, bis sie negativ ist, und markiert dann das Ende der Liste. Entsprechend ana f 3wird die Liste berechnet [2,1,0].

Anamorphismen auf anderen Datenstrukturen

Ein Anamorphismus kann für jeden rekursiven Typ nach einem generischen Muster definiert werden, das die zweite Version von ana für Listen verallgemeinert .

Zum Beispiel die Abwicklung für die Baumdatenstruktur

 data Tree a = Leaf a | Branch (Tree a) a (Tree a)

ist wie folgt

 ana :: (b -> Either a (b, a, b)) -> b -> Tree a
 ana unspool x = case unspool x of
                   Left a          -> Leaf a
                   Right (l, x, r) -> Branch (ana unspool l) x (ana unspool r)

Um die Beziehung zwischen dem rekursiven Typ und seinem Anamorphismus besser zu sehen, beachten Sie, dass Treeund Listwie folgt definiert werden kann:

 newtype List a = List {unCons :: Maybe (a, List a)}

 newtype Tree a = Tree {unNode :: Either a (Tree a, a, Tree a))}

Die Analogie zu anaerscheint durch Umbenennung bin ihrer Art:

 newtype List a = List {unCons :: Maybe (a, List a)}
 anaList ::       (list_a       -> Maybe (a, list_a)) -> (list_a -> List a)

 newtype Tree a = Tree {unNode :: Either a (Tree a, a, Tree a))}
 anaTree ::       (tree_a       -> Either a (tree_a, a, tree_a)) -> (tree_a -> Tree a)

Bei diesen Definitionen hat das Argument für den Konstruktor des Typs denselben Typ wie der Rückgabetyp des ersten Arguments von ana, wobei die rekursiven Erwähnungen des Typs durch ersetzt werden b.

Geschichte

Eine der ersten Veröffentlichungen, die den Begriff eines Anamorphismus im Kontext der Programmierung einführte, war der Artikel Functional Programming with Bananas, Lenses, Envelopes and Stacheldraht von Erik Meijer et al. , das im Kontext der Programmiersprache Squiggol stand .

Anwendungen

Funktionen wie zipund iteratesind Beispiele für Anamorphismen. zipnimmt ein Paar von Listen, sagen wir ['a','b','c'] und [1,2,3] und gibt eine Liste von Paaren zurück [('a',1),('b',2) ,('c',3)]. Iteratenimmt ein Ding x und eine Funktion f von solchen Dingen zu solchen und gibt die unendliche Liste zurück, die durch wiederholte Anwendung von f entsteht, dh die Liste [x, (fx), (f (fx)), ( f (f (fx))), ...].

 zip (a:as) (b:bs) = if (as==[]) || (bs ==[])   -- || means 'or'
                      then [(a,b)]
                      else (a,b):(zip as bs) 
 
 iterate f x = x:(iterate f (f x))

Um dies zu beweisen, können wir beides mit unserer generischen Abwicklung implementieren ana, mit einer einfachen rekursiven Routine:

 zip2 = ana unsp fin
    where
    fin (as,bs) = (as==[]) || (bs ==[]) 
    unsp ((a:as), (b:bs)) = ((a,b),(as,bs))

 iterate2 f = ana (\a->(a,f a)) (\x->False)

In einer Sprache wie Haskell sind selbst die abstrakten Funktionen fold, unfoldund analediglich definierte Begriffe, wie wir aus den obigen Definitionen gesehen haben.

Anamorphismen in der Kategorientheorie

In der Kategorientheorie sind Anamorphismen das kategorische Dual von Katamorphismen (und Katamorphismen sind das kategorische Dual von Anamorphismen).

Das bedeutet Folgendes. Angenommen ( A , fin ) ist eine finale F- Koalgebra für einen Endofunktor F einer bestimmten Kategorie in sich. Somit ist fin ein Morphismus von A nach FA , und da angenommen wird, dass er endgültig ist, wissen wir, dass immer dann, wenn ( X , f ) eine weitere F- Koalgebra ist (ein Morphismus f von X nach FX ), ein eindeutiger Homomorphismus h von ( X , f ) bis ( A , fin ), die ein morphism ist h von X zu A , so dass fin . h = Fh . f . Dann bezeichnen wir für jedes solche f mit ana f diesen eindeutig spezifizierten Morphismus h .

Mit anderen Worten, wir haben die folgende definierende Beziehung, wenn einige feste F , A und fin wie oben angegeben sind:

Notation

Eine in der Literatur zu findende Notation für ana f ist . Die verwendeten Brackets werden als Linsenbrackets bezeichnet , nach denen Anamorphismen manchmal als Linsen bezeichnet werden .

Siehe auch

Verweise

Externe Links