Anamorfisme - Anamorphism

For anden anvendelse, se Anamorphosis (disambiguation) .
For ikke at forveksle med katamorfisme .

I computerprogrammering er en anamorfisme en funktion, der genererer en sekvens ved gentagen anvendelse af funktionen til dens tidligere resultat. Du begynder med en vis værdi A og anvender en funktion f på den for at få B. Derefter anvender du f til B for at få C og så videre, indtil en afslutningsbetingelse er nået. Anamorfismen er den funktion, der genererer listen over A, B, C osv. Du kan tænke på anamorfismen som at udfolde den oprindelige værdi i en sekvens.

Ovenstående lægmandsbeskrivelse kan angives mere formelt i kategoriteori : anamorfismen af en koinduktiv type angiver tildeling af en kulgebra til dens unikke morfisme til den endelige kulgebra af en endofunktor . Disse objekter bruges i funktionel programmering som udfoldelser .

Den kategoriske dobbelte (aka modsatte) af anamorphism er catamorphism .

Anamorfismer i funktionel programmering

I funktionel programmering , en anamorphism er en generalisering af begrebet udfolder på coinductive lister . Formelt set er anamorfismer generiske funktioner, der corecursively kan konstruere et resultat af en bestemt type, og som parametreres af funktioner, der bestemmer det næste enkelt trin i konstruktionen.

Den pågældende datatype er defineret som det største faste punkt ν X. FX af en functor F . Ved den endelige coalgebras universelle egenskab er der en unik kulgebra morfisme A → ν X. FX for enhver anden F -coalgebra a: A → FA . Således kan man definere funktioner fra en type A _into_ en coinductive datatype ved at angive en coalgebra struktur en på A .

Eksempel: Potentielt uendelige lister

Som et eksempel, typen af potentielt uendelige lister (med elementer af en fast type, værdi er) angives som fikspunkt [value] = ν X. værdi × X + 1 , dvs. en liste består enten af ​​en værdi og en yderligere liste, eller den er tom. En (pseudo-) Haskell -definition kan se sådan ud: 

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

Det er funktorens faste punkt F value, hvor: 

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

Man kan let kontrollere, at typen faktisk [value]er isomorf for F value [value], og dermed [value]er det faste punkt. (Bemærk også, at i Haskell falder de mindste og største fixpunkter for funktorer sammen, derfor er induktive lister det samme som koinduktive, potentielt uendelige lister.)

Den anamorphism for lister (så normalt kendt som udfolde ) ville bygge en (potentielt uendelig) liste fra en tilstand værdi. Typisk tager udfoldelsen en tilstandsværdi xog en funktion, fder giver enten et par af en værdi og en ny tilstand eller en singleton for at markere slutningen af ​​listen. Anamorfismen ville derefter begynde med et første frø, beregne, om listen fortsætter eller slutter, og i tilfælde af en ikke -undantaget liste, forberede den beregnede værdi til det rekursive opkald til anamorfismen.

En Haskell -definition af en udfoldelse eller anamorfisme for lister, kaldet ana, er som følger: 

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

Vi kan nu implementere ganske generelle funktioner ved hjælp af ana , for eksempel en nedtælling: 

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

Denne funktion vil reducere et helt tal og udsende det på samme tid, indtil det er negativt, på hvilket tidspunkt det vil markere slutningen af ​​listen. Tilsvarende ana f 3beregner listen [2,1,0].

Anamorfismer på andre datastrukturer

En anamorfisme kan defineres for enhver rekursiv type i henhold til et generisk mønster, der generaliserer den anden version af ana til lister.

For eksempel udfoldelsen for trædatastrukturen 

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

er som følgende 

 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)

For bedre at se forholdet mellem den rekursive type og dens anamorfisme skal du bemærke, at Treeog Listkan defineres således: 

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

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

Analogien med anavises ved at omdøbe bi sin type: 

 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)

Med disse definitioner har argumentet til konstruktøren af ​​typen den samme type som returtypen for det første argument for ana, med de rekursive omtaler af typen erstattet med b.

Historie

En af de første publikationer, der introducerede forestillingen om en anamorfisme i forbindelse med programmering, var papiret Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire af Erik Meijer et al. , som var i sammenhæng med programmeringssproget Squiggol .

Ansøgninger

Funktioner kan lide zipog iterateer eksempler på anamorfismer. ziptager et par lister, siger ['a', 'b', 'c'] og [1,2,3] og returnerer en liste med par [('a', 1), ('b', 2) , ('c', 3)]. Iteratetager en ting, x og en funktion, f, fra sådanne ting til sådanne ting, og returnerer den uendelige liste, der kommer fra gentagen anvendelse af f, dvs. listen [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))

For at bevise dette kan vi implementere både ved hjælp af vores generiske udfoldning anaved hjælp af en simpel rekursiv rutine: 

 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)

I et sprog som Haskell, selv de abstrakte funktioner fold, unfoldog anablot defineret udtryk, som vi har set fra definitionerne ovenfor.

Anamorfismer i kategoriteori

I kategoriteori er anamorfismer den kategoriske dual af katamorfismer (og katamorfismer er den kategoriske dual af anamorfismer).

Det betyder følgende. Antag ( A , fin ) er en sidste F -coalgebra for en eller anden endofunktor F i en eller anden kategori i sig selv. Således, finne er en morphism fra A til FA , og da det antages at være endelig ved vi, at når ( X , f ) er en anden F -coalgebra (a morphism f fra X til FX ), vil der være en unik homomorfi h fra ( X , f ) til ( A , fin ), det er en morfisme h fra X til A, så fin . h = Fh . f . Så for hver sådan f betegner vi med ana f, at unikt specificeret morfisme h .

Med andre ord har vi følgende definerende forhold givet nogle faste F , A og fin som ovenfor:

Notation

En notation for ana f fundet i litteraturen er . De anvendte beslag er kendt som linsebeslag , hvorefter anamorfier undertiden omtales som linser .

Se også

Referencer

eksterne links