Corecursion

Inom datavetenskap är corecursion en typ av operation som är dubbel till rekursion . Medan rekursion fungerar analytiskt, börjar på data längre från ett basfall och bryter ner det i mindre data och upprepar tills man når ett basfall, corecursion fungerar syntetiskt, utgår från ett basfall och bygger upp det, och producerar iterativt data längre bort från ett basfall. basfallet. Enkelt uttryckt använder corecursive algoritmer den data som de själva producerar, bit för bit, allt eftersom de blir tillgängliga och behövs för att producera ytterligare bitar av data. Ett liknande men distinkt begrepp är generativ rekursion som kan sakna en bestämd "riktning" som är inneboende i korekursion och rekursion.

Där rekursion tillåter program att arbeta på godtyckligt komplexa data, så länge de kan reduceras till enkla data (basfall), tillåter corecursion program att producera godtyckligt komplexa och potentiellt oändliga datastrukturer, såsom strömmar, så länge som det kan produceras från enkla data (basfall) i en sekvens av ändliga steg. Där rekursion kanske inte avslutas och aldrig når ett bastillstånd, startar corecursion från ett bastillstånd och producerar sålunda efterföljande steg deterministiskt, även om den kan fortsätta på obestämd tid (och alltså inte avslutas under strikt utvärdering), eller så kan den konsumera mer än den producerar och blir därför icke- produktiv . Många funktioner som traditionellt analyseras som rekursiva kan alternativt, och utan tvekan mer naturligt, tolkas som corekursiva funktioner som avslutas i ett givet skede, till exempel återfallsrelationer som den faktoriella.

Corecursion kan producera både ändliga och oändliga datastrukturer som resultat, och kan använda självrefererande datastrukturer. Corecursion används ofta i samband med lat utvärdering , för att endast producera en ändlig delmängd av en potentiellt oändlig struktur (istället för att försöka producera en hel oändlig struktur på en gång). Corecursion är ett särskilt viktigt begrepp inom funktionell programmering , där corecursion och codata tillåter totala språk att arbeta med oändliga datastrukturer.

Exempel

Corecursion kan förstås i motsats till rekursion, som är mer bekant. Medan corecursion främst är av intresse för funktionell programmering, kan det illustreras med imperativ programmering, vilket görs nedan med hjälp av generatorfunktionen i Python. I dessa exempel används lokala variabler och tilldelas värden imperativt (destruktivt), även om dessa inte är nödvändiga i corecursion i ren funktionell programmering. I ren funktionell programmering, snarare än att tilldela till lokala variabler, bildar dessa beräknade värden en oföränderlig sekvens, och tidigare värden nås genom självreferens (senare värden i sekvensen refererar till tidigare värden i sekvensen som ska beräknas). Uppgifterna uttrycker helt enkelt detta i imperativparadigmet och specificerar explicit var beräkningarna sker, vilket tjänar till att förtydliga expositionen.

Faktoriell

Ett klassiskt exempel på rekursion är att beräkna faktorn , som definieras rekursivt av 0! := 1 och n! := n × (n - 1)! .

För att rekursivt beräkna sitt resultat på en given ingång, anropar en rekursiv funktion (en kopia av) sig själv med en annan ("mindre" på något sätt) indata och använder resultatet av detta anrop för att konstruera sitt resultat. Det rekursiva samtalet gör detsamma, om inte basfallet har nåtts. Sålunda utvecklas en anropsstack i processen. Till exempel, för att beräkna fac(3) , anropar detta rekursivt i sin tur fac(2) , fac(1) , fac(0) ("avveckling" av stacken), vid vilken punkt rekursionen slutar med fac(0) = 1 , och sedan lindas stacken av i omvänd ordning och resultaten beräknas på vägen tillbaka längs anropsstacken till den initiala anropsramen fac(3) som använder resultatet av fac(2) = 2 för att beräkna slutresultatet som 3 × 2 = 3 × fac(2) =: fac(3) och slutligen returnera fac(3) = 6 . I det här exemplet returnerar en funktion ett enda värde.

Denna stackavveckling kan förklaras, och definierar faktorialet corecursively , som en iterator , där man börjar med fallet $1=:0!$ , från detta startvärde konstruerar sedan faktoriella värden för ökande tal 1, 2, 3... som i ovanstående rekursiva definition med "tidspil" omvänd, så att säga, genom att läsa den baklänges som $n!\times (n+1)=:(n+1)!$ . Den sålunda definierade corekursiva algoritmen producerar en ström av alla faktorialer. Detta kan konkret implementeras som en generator . Symboliskt, om man noterar att beräkning av nästa faktorvärde kräver att man håller reda på både n och f (ett tidigare faktorvärde), kan detta representeras som:

n,f=(0,1):(n+1,f\ gånger (n+1))

eller i Haskell ,

       0 (  \  (  n  ,  f  )  ->  (  n  +  1  ,  f  *  (  n  +  1  )))  `  iterera  `  (  ,  1  )

betyder, "med början från $n,f=0,1$ $n+1, f\ gånger (n+1)$ i varje steg beräknas nästa värden som ". Detta är matematiskt ekvivalent och nästan identiskt med den rekursiva definitionen, men $+1$ understryker att faktorvärdena byggs upp , framåt från startfallet, snarare än att beräknas efter att först ha gått bakåt, ner till basfallet, med en $-1$ minskning Den direkta utsignalen från den corecursiva funktionen innehåller inte bara det faktoriella ${\displaystyle n!}-$ värden, men inkluderar också för varje värde hjälpdata för dess index n i sekvensen, så att ett specifikt resultat kan väljas bland dem alla, när och när det behövs.

Det finns ett samband med denotationssemantik , där denotationerna av rekursiva program byggs upp korkursivt på detta sätt.

I Python kan en rekursiv faktoriell funktion definieras som:

    
    
       0
         
    
              def  factorial  (  n  :  int  )  ->  int  :  """Rekursiv faktoriell funktion."""  if  n  ==  :  return  1  else  :  return  n  *  factorial  (  n  -  1  )

Detta kan sedan kallas till exempel som factorial(5) för att beräkna 5! .

En motsvarande corecursive generator kan definieras som:

 
    
       0 
     
         
                   def  factorials  ():  """Corecursive generator."""  n  ,  f  =  ,  1  medan  True  :  ger  f  n  ,  f  =  n  +  1  ,  f  *  (  n  +  1  )

Detta genererar en oändlig ström av factorials i ordning; en ändlig del av den kan produceras av:

  
       0 
       
         
                   def  n_factorials  (  k  :  int  ):  n  ,  f  =  ,  1  medan  n  <=  k  :  ger  f  n  ,  f  =  n  +  1  ,  f  *  (  n  +  1  )

Detta kan sedan kallas för att producera factorials upp till 5! via:

   
     för  f  i  n_faktorer  (  5  ):  print  (  f  )

Om vi bara är intresserade av en viss faktor, kan bara det sista värdet tas, eller så kan vi smälta samman produktionen och åtkomsten till en funktion,

  
       0 
       
                  
      def  nth_factorial  (  k  :  int  ):  n  ,  f  =  ,  1  medan  n  <  k  :  n  ,  f  =  n  +  1  ,  f  *  (  n  +  1  )  ger  f

Som lätt kan ses här är detta praktiskt taget likvärdigt (bara genom att ersätta avkastningen med den enda avkastningen där) med ackumulatorargumenttekniken för svansrekursion , avlindad till en explicit loop. Således kan man säga att begreppet corecursion är en förklaring av utförandet av iterativa beräkningsprocesser genom rekursiva definitioner, där så är tillämpligt.

Fibonacci-sekvens

På samma sätt kan Fibonacci-sekvensen representeras som:

a,b=(0,1):(b,a+b)

Eftersom Fibonacci-sekvensen är en återkommande relation av ordning 2, måste den korkursiva relationen spåra två på varandra följande termer, med $(b,-)$ som motsvarar förskjutning ett steg framåt, och $(-,a+b)$ som motsvarar beräkning av nästa term. Detta kan sedan implementeras enligt följande (med parallell tilldelning ):

 
       0 
     
         
               def  fibonacci_sequence  ():  a  ,  b  =  ,  1  medan  True  :  ger  a  a  ,  b  =  b  ,  a  +  b

I Haskell,

        0  map  fst  (  (  \  (  a  ,  b  )  ->  (  b  ,  a  +  b  ) )  `  iterera  `  (  ,  1  )  )

Trädpassering

Trädpassering via ett djup-först- tillvägagångssätt är ett klassiskt exempel på rekursion. Dubbelt, bredd-först- traversal kan mycket naturligt implementeras via corecursion.

Utan att använda rekursion eller corecursion specifikt, kan man korsa ett träd genom att börja vid rotnoden, placera dess underordnade noder i en datastruktur och sedan iterera genom att ta bort nod efter nod från datastrukturen samtidigt som varje borttagen nods barn placeras tillbaka i den datastrukturen. . Om datastrukturen är en stack (LIFO), ger detta genomgång av djupet-först, och om datastrukturen är en kö (FIFO), ger detta genomgång av bredd-först.

Med hjälp av rekursion kan en (efterbeställning) genomgång av djupet-först implementeras genom att starta vid rotnoden och rekursivt korsa varje underträd i tur och ordning (underträdet baserat på varje underordnat nod) – det andra underträdet börjar inte bearbetas förrän första underträdet är klart. När väl en lövnod nås eller barnen till en grennod har förbrukats, besöks själva noden (t.ex. värdet på själva noden matas ut). I det här fallet fungerar anropsstacken (av de rekursiva funktionerna) som den stack som itereras över.

Med hjälp av corecursion kan en bredd-först-traversering implementeras genom att börja vid rotnoden, mata ut dess värde, sedan bredd-först korsa underträden – dvs. skicka vidare hela listan med underträd till nästa steg (inte ett enda underträd , som i det rekursiva tillvägagångssättet) – i nästa steg mata ut värdet för alla deras rotnoder, sedan skicka vidare deras underträd, etc. I det här fallet fungerar generatorfunktionen, ja själva utdatasekvensen, som kö. Som i faktorexemplet (ovan), där hjälpinformationen för indexet (vilket steg ett var vid, n ) trycktes framåt, förutom den faktiska utmatningen av n !, är i detta fall hjälpinformationen för de återstående underträden skjuts framåt, utöver den faktiska produktionen. Symboliskt:

v,t=([],[FullTree]):(RootValues(v,t),ChildTrees(t))

vilket betyder att man vid varje steg matar ut listan med värden för rotnoder och fortsätter sedan till underträden. Att bara generera nodvärdena från den här sekvensen kräver helt enkelt att slänga de extra underordnade träddata, sedan förenkla listan med listor (värdena grupperas initialt efter nivå (djup); utjämning (avgruppering) ger en platt linjär lista). I Haskell,

                concatMap  fst  (  (  \  (  v  ,  t  )  ->  (  rootValues  v  t  ,  childTrees  t  ))  `  iterate  `  (  [ ]  ,  fullTree  )  )

Dessa kan jämföras enligt följande. Den rekursiva genomgången hanterar en lövnod (längst ner ) som basfall (när det inte finns några underordnade, mata bara ut värdet), och analyserar ett träd i underträd, korsar var och en i tur och ordning, vilket så småningom resulterar i bara lövnoder – faktiska blad noder och grennoder vars barn redan har behandlats (avskuren nedan ). Däremot hanterar den corecursive traversalen en rotnod (överst ) som basfall (gid en nod, mata först ut värdet), behandlar ett träd som syntetiserat av en rotnod och dess underordnade, och producerar sedan som hjälputgång en lista över underträd vid varje steg, som sedan är indata för nästa steg – barnnoderna för den ursprungliga roten är rotnoderna i nästa steg, eftersom deras föräldrar redan har behandlats (avskuren ovan ) . I den rekursiva traversalen finns det en distinktion mellan lövnoder och grennoder, medan det i den corecursive traversalen inte finns någon distinktion, eftersom varje nod behandlas som rotnoden till det underträd som den definierar.

Särskilt, givet ett oändligt träd, kommer den korskursiva bredd-första-traverseringen att korsa alla noder, precis som för ett finit träd, medan den rekursiva djup-första-traverseringen kommer att gå nedför en gren och inte korsa alla noder, och faktiskt om den korsar postorder , som i det här exemplet (eller i ordning), kommer den inte att besöka några noder alls, eftersom den aldrig når ett löv. Detta visar användbarheten av corecursion snarare än rekursion för att hantera oändliga datastrukturer.

I Python kan detta implementeras enligt följande. Den vanliga efterbeställningens djup-först genomgång kan definieras som:

 
    
        
        
        
         def  df  (  nod  ):  """Post-order depth-first traversal."""  om  noden  inte  är  Ingen  :  df  (  nod  .  left  )  df  (  nod  .  right  )  print  (  nod  .  value  )

Detta kan sedan anropas av df(t) för att skriva ut värdena för trädets noder i post-order djup-första ordning.

Den bredd-första corecursive generatorn kan definieras som:

 
    
      
     
          
           
                
                 
                
                
           def  bf  (  träd  ):  """Bredth-first corecursive generator."""  tree_list  =  [  träd  ]  medan  tree_list  :  new_tree_list  =  [  ]  för  träd  i  tree_list  :  om  träd  inte  är  Inget  :  avkastningsträd  .  värde  ny_trädlista  .  lägg till  (  träd  .  vänster  )  new_tree_list  .  lägg till  (  träd  .  höger  )  trädlista  =  ny_trädlista

Detta kan sedan anropas för att skriva ut värdena för trädets noder i bredd-första ordning:

   
     för  i  i  bf  (  t  ):  skriv ut  (  i  )

Definition

Initiala datatyper kan definieras som den minsta fixpunkten ( upp till isomorfism ) av någon typekvation; isomorfismen ges då av en initial algebra . Dubbelt kan slutliga (eller terminala) datatyper definieras som den största fixpunkten i en typekvation; isomorfismen ges sedan av en slutlig koalgebra .

Om diskursdomänen är kategorin av mängder och totala funktioner, kan slutliga datatyper innehålla oändliga, icke välgrundade värden, medan initialtyper inte gör det. Å andra sidan, om diskursdomänen är kategorin av fullständiga partiella ordningar och kontinuerliga funktioner , som ungefär motsvarar Haskell -programmeringsspråket, så sammanfaller sluttyper med initialtyper, och motsvarande slutliga koalgebra och initiala algebra bildar en isomorfism.

Corecursion är då en teknik för att rekursivt definiera funktioner vars intervall (kodomän) är en slutlig datatyp, dubbelt med det sätt som vanlig rekursion rekursivt definierar funktioner vars domän är en initial datatyp.

Diskussionen nedan ger flera exempel i Haskell som särskiljer corecursion. Grovt sett, om man skulle överföra dessa definitioner till kategorin uppsättningar, skulle de fortfarande vara korekursiva. Denna informella användning överensstämmer med befintliga läroböcker om Haskell. Exemplen som används i den här artikeln är före försöken att definiera corecursion och förklara vad det är.

Diskussion

Regeln för primitiv corecursion på codata är den dubbla till den för primitiv rekursion på data. Istället för att gå ner på argumentet genom att mönstermatcha på dess konstruktorer (som anropades innan , någonstans, så att vi får ett färdigt datum och kommer till dess ingående underdelar, dvs. "fält"), stiger vi på resultatet genom att fylla i dess "destruktorer" (eller "observatörer", som kommer att anropas efteråt , någonstans - så vi anropar faktiskt en konstruktor och skapar en annan bit av resultatet som ska observeras senare). Således skapar corecursion (potentiellt oändlig) kodata, medan vanlig rekursion analyserar (nödvändigtvis ändlig) data. Vanlig rekursion kanske inte är tillämplig på koddata eftersom den kanske inte avslutas. Omvänt är corecursion inte strikt nödvändig om resultattypen är data, eftersom data måste vara ändliga.

I "Programming with streams in Coq: a case study: the Sieve of Eratosthenes" finner vi

                    
     

             
                     

               
          hd  (  conc  a  s  )  =  a  tl  (  conc  a  s  )  =  s  (  sil  p  s  )  =  om  div  p  (  hd  s  )  så  sil  p  (  tl  s  )  annars  konc  (  hd  s  )  (  sil  p  (  tl  s  ))  hd  (  primtal  s  )  =  (  hd  s  )  tl  (  primtal  s  )  =  primtal  (  sikt  (  hd  s  )  (  tl  s  ))

där primtal "erhålls genom att tillämpa primtalsoperationen på strömmen (Enu 2)". Efter ovanstående notation kan sekvensen av primtal (med en släng 0 som prefix) och talströmmar som successivt siktas, representeras som

p,s=(0,[ 2..]):(hd(s),sil(hd(s),tl(s)))

eller i Haskell,

        0  (  \  (  p  ,  s  @  (  h  :  t  ))  ->  (  h  ,  sikt  h  t  ))  `  iterera  `  (  ,  [  2  ..  ])

Författarna diskuterar hur definitionen av sikt inte garanteras alltid vara produktiv och kan fastna t.ex. om den anropas med [5,10..] som den initiala strömmen.

Här är ett annat exempel i Haskell. Följande definition ger listan över Fibonacci-tal i linjär tid:

  0         fibs  =  :  1  :  zipMed  (  +  )  fibs  (  svansfiber  )  _

Denna oändliga lista beror på lat utvärdering; element beräknas efter behov, och endast finita prefix representeras någonsin explicit i minnet. Denna funktion tillåter algoritmer på delar av koddata att avslutas; sådana tekniker är en viktig del av Haskell-programmering.

Detta kan också göras i Python:

      

  
       

 
     
           
             
         
          
      0  
     

    
     från  itertools  importera  tee  ,  chain  ,  islice  ,  imap  def  add  (  x  ,  y  ):  return  x  +  y  def  fibonacci  ():  def  deferred_output  ():  för  i  i  output  :  yield  i  resultat  ,  c1  ,  c2  =  tee  (  deferred_output  () ,  3  )  parad  =  imap  (  add  ,  c1  ,  islice  (  c2  ,  1  ,  None  ))  output  =  kedja  ([  ,  1  ],  parad  )  returnera  resultat  för  i  i  islice  (  fibonacci  (),  20  ):  print  (  i  )

Definitionen av zipWith kan infogas, vilket leder till detta:

  0     
  
          fibs  =  :  1  :  nästa  fibs  där  nästa  (  a  :  t  @  (  b  :  _  ))  =  (  a  +  b  )  :  nästa  t

Det här exemplet använder en självrefererande datastruktur . Vanlig rekursion använder sig av självreferensfunktioner , men rymmer inte självrefererande data. Detta är dock inte väsentligt för Fibonacci-exemplet. Det kan skrivas om enligt följande:

   0
       fibs  =  fibgen  (  ,  1  )  fibgen  (  x  ,  y  )  =  x  :  fibgen  (  y  ,  x  +  y  )

Detta använder endast självreferensfunktion för att konstruera resultatet . Om det skulle användas med strikt listkonstruktor skulle det vara ett exempel på skenande rekursion, men med icke-strikt listkonstruktor producerar denna bevakade rekursion gradvis en obestämd lista.

Corecursion behöver inte producera ett oändligt objekt; en corecursive kö är ett särskilt bra exempel på detta fenomen. Följande definition producerar en bredd-första genomgång av ett binärt träd i linjär tid:

                 

        
   
  
          

      0                                        
                            
                    dataträd  a  b  =  Blad  a  |  _  Gren  b  (  Träd  a  b  )  (  Träd  a  b  )  bftrav  ::  Träd  a  b  ->  [  Träd  a  b  ]  bftrav  träd  =  kö  där  kö  =  träd  :  gen  1  kö  gen  p  =  []  gen  len  (  Blad  _  :  s  )  =  gen  (  len  -  1  )  s  gen  len  (  Gren  _  l  r  :  s  )  =  l  :  r  :  gen  (  len  +  1  )  s

Denna definition tar ett initialt träd och producerar en lista med underträd. Den här listan har dubbla syften som både kö och resultat ( gen len p producerar sina utgående lenskåror efter dess ingångsbakåtpekare, p , längs kön ). Det är ändligt om och endast om det initiala trädet är ändligt. Köns längd måste spåras explicit för att säkerställa uppsägning; detta kan säkert elimineras om denna definition endast tillämpas på oändliga träd.

Ett annat särskilt bra exempel ger en lösning på problemet med bredd-först-märkning. Funktionsetiketten besöker varje nod i ett binärt träd på ett brett första sätt och ersätter varje etikett med ett heltal, varje efterföljande heltal är större än det förra med ett . Denna lösning använder en självrefererande datastruktur, och det binära trädet kan vara ändligt eller oändligt.

         
   
    
         

                   
                                
                    
                                
                                        
                                        etikett  ::  Träd  a  b  ->  Träd  Int  Int  label  t  =  t  ′  där  (  t  ′  ,  ns  )  =  go  t  (  1  :  ns  )  go  ::  Träd  a  b  ->  [  Int  ]  ->  (  Träd  Int  Int  ,  [  Int  ])  go  (  Leaf  _  )  (  n  :  ns  )  =  (  Leaf  n  ,  n  +  1  :  ns  )  go  (  Gren  _  l  r  )  (  n  :  ns  )  =  (  Gren  n  l  ′  r  ′  ,  n  +  1  :  ns  "  )  där  (  l  "  ,  ns  "  )  =  go  l  ns  (  r  "  ,  ns  "  )  =  go  r  ns  "

En apomorfism (som en anamorfism , till exempel unfold ) är en form av corecursion på samma sätt som en paramorphism (som en catamorphism , som fold ) är en form av rekursion.

Coq proof-assistenten stöder corecursion och coinduction med hjälp av CoFixpoint-kommandot .

Historia

Corecursion, kallad cirkulär programmering, dateras åtminstone till ( Bird 1984 ), som krediterar John Hughes och Philip Wadler ; mer allmänna former utvecklades i ( Allison 1989 ). De ursprungliga motiveringarna inkluderade att producera mer effektiva algoritmer (tillåta 1 pass over data i vissa fall, istället för att kräva flera pass) och implementera klassiska datastrukturer, såsom dubbellänkade listor och köer, i funktionella språk.

Se även

Anteckningar

Bird, Richard Simpson (1984). "Använda cirkulära program för att eliminera flera genomgångar av data". Acta Informatica . 21 (3): 239–250. doi : 10.1007/BF00264249 . S2CID 27392591 .
Allison, Lloyd (april 1989). "Cirkulära program och självrefererande strukturer" . Programvara: Övning och erfarenhet . 19 (2): 99–109. doi : 10.1002/spe.4380190202 . S2CID 21298473 .
Geraint Jones och Jeremy Gibbons (1992). Linjär-tid-bredd-först-trädalgoritmer: En övning i aritmetiken av veck och blixtlås ( Teknisk rapport). Inst för datavetenskap, University of Auckland.
Jon Barwise ; Lawrence S Moss (juni 1996). Onda cirklar . Centrum för studier av språk och information. ISBN 978-1-57586-009-1 . Arkiverad från originalet 2010-06-21 . Hämtad 2011-01-24 .
Lawrence S Moss; Norman Danner (1997). "På grunderna för Corecursion". Logic Journal of the IGPL . 5 (2): 231–257. CiteSeerX 10.1.1.40.4243 . doi : 10.1093/jigpal/5.2.231 .
Kees Doets; Jan van Eijck (maj 2004). Haskell-vägen till logik, matematik och programmering . King's College Publications. ISBN 978-0-9543006-9-2 .
David Turner (2004-07-28). "Total funktionell programmering" . Journal of Universal Computer Science . 10 (7): 751–768. doi : 10.3217/jucs-010-07-0751 .
Jeremy Gibbons; Graham Hutton (april 2005). "Bevismetoder för corecursive program" . Fundamenta Informaticae . 66 (4): 353–366.
Leon P Smith (2009-07-29), "Lloyd Allison's Corecursive Queues: Why Continuations Matter" , The Monad Reader (14): 37–68
Raymond Hettinger (2009-11-19). "Recept 576961: Teknik för cyklisk iteration" .
MB Smyth och GD Plotkin (1982). "Den kategoriteoretiska lösningen av rekursiva domänekvationer" (PDF) . SIAM Journal on Computing . 11 (4): 761–783. doi : 10.1137/0211062 . S2CID 8517995 .
Leclerc, Francois; Paulin-Mohring, Christine (1993). Programmering med strömmar i Coq: A Case Study: the Sieve of Eratosthenes . Typer för bevis och program: Internationell workshop TYPER '93. Springer-Verlag New York, Inc. s. 191–212. ISBN 978-3-540-58085-0 .