ในวิทยาการคอมพิวเตอร์การเรียกซ้ำแบบ คู่ขนาน (corecursion ) เป็นประเภทของการดำเนินการที่เป็นคู่ขนานกับการเรียกซ้ำเชิงโครงสร้าง (structural recursion)ในขณะที่การเรียกซ้ำจะใช้โครงสร้างข้อมูลโดยจัดการกับชั้นบนสุดก่อนแล้วจึงลงไปยังส่วนภายใน การเรียกซ้ำแบบคู่ขนานจะสร้างโครงสร้างข้อมูลโดยการกำหนดชั้นบนสุดก่อนแล้วจึงกำหนดส่วนภายใน การเรียกซ้ำแบบคู่ขนานมีความสำคัญอย่างยิ่งในภาษาแบบสมบูรณ์ (total languages)เนื่องจากช่วยให้สามารถเข้ารหัสการคำนวณที่ไม่สิ้นสุดได้ในบริบทที่ทุกฟังก์ชันต้องสิ้นสุด โดยได้รับการสนับสนุนจากโปรแกรมพิสูจน์ทฤษฎีบท Agda ^{[ 1 ]}และRocq ^{[ 2 ]}

ทั้งการเรียกซ้ำแบบแกนร่วม (corecursion) และการเรียกซ้ำ (recursion) สามารถมองได้ว่าเป็นการทำงานบนโครงสร้างข้อมูล แบบ ต้นไม้ ซึ่งรวมถึงโครงสร้างข้อมูลเช่น ลิสต์และสตรีมเป็นกรณีพิเศษ เนื่องจากการเรียกซ้ำต้องสิ้นสุด จึงทำงานได้เฉพาะกับต้นไม้ที่มีรากฐานที่ดี (well-founded tree) กล่าวคือไม่ลึกเป็นอนันต์ ซึ่งเรียกว่า ชนิด ข้อมูลหรือชนิดข้อมูลเริ่มต้นในทางกลับกัน การเรียกซ้ำแบบแกนร่วมจะสร้าง ชนิด ข้อมูลร่วมหรือชนิดข้อมูลสุดท้ายซึ่งรวมถึงต้นไม้ที่ลึกเป็นอนันต์ ชนิดข้อมูลร่วมไม่สามารถแสดงในหน่วยความจำได้โดยตรง ดังนั้นจึงมักถูกนำไปใช้โดยใช้ โครงสร้างข้อมูล แบบอ้างอิงตนเองหรือการประเมินแบบขี้เกียจ (lazy evaluation )

ในภาษาโปรแกรมทั้งหมดจำนวนธรรมชาติสามารถกำหนดได้ดังนี้ (โดยใช้ไวยากรณ์Haskell ^{[ a ]} ):

ข้อมูลNat = ศูนย์| Succ Nat

หลักการนี้กล่าวว่า จำนวนธรรมชาติทุกจำนวนจะเป็นศูนย์หรือเป็นจำนวนต่อจากจำนวนธรรมชาติที่มีอยู่แล้ว ตัวอย่างเช่น เลขหนึ่งแทนด้วย 0 Succ Zero, เลขสองแทนด้วย 0 Succ (Succ Zero), เลขสามแทนด้วยSucc (Succ (Succ Zero))และอื่นๆ

ถ้าเราตีความการประกาศข้างต้นในเชิงอุปนัยจำนวนธรรมชาติทั้งหมดจะถูกสร้างขึ้นด้วยวิธีนี้ และเราจะได้เซตของจำนวนธรรมชาติที่เราคุ้นเคย ที่สำคัญคือ เราสามารถเรียกซ้ำ^{[ b ]}บนเซตนี้ได้ ตัวอย่างเช่น เราสามารถใช้มันเพื่อสร้างรายการที่ทำซ้ำค่าได้หลายnครั้ง

repeat :: a -> Nat -> [ a ] ​​repeat x Zero = [] -- กรณีพื้นฐานrepeat x ( Succ n ) = x : repeat x n -- ขั้นตอนอุปนัย

โปรดสังเกตว่าการใช้ `if` นั้นrepeat x nมีความสำคัญอย่างยิ่ง—เราไม่สามารถเขียน `if` ได้repeat x (Succ n)เพราะนั่นคือฟังก์ชันที่เราพยายามกำหนด และดังนั้นมันจะวนลูปไปเรื่อยๆ โดยเฉพาะอย่างยิ่ง อินพุตจะต้องมีขนาดเล็ลง—หรือพูดให้ถูกคือลึกขึ้น หากมองในแง่ของโครงสร้างข้อมูล—ทุกครั้งที่เราเรียกซ้ำ

คำประกาศนี้อาจตีความได้ใน ลักษณะ อุปนัยร่วมซึ่งสามารถแสดงได้ดังนี้:

codata CoNat = ศูนย์| ซัคโคแนท

CoNatมีจำนวนธรรมชาติทั้งหมดที่Natมีโดยอัตโนมัติ แต่เนื่องจากโคดาต้าสามารถลึกได้อย่างไม่มีที่สิ้นสุด จึงมีเทอมพิเศษSucc (Succ (Succ (Succ …)))ที่ต่อเนื่องไปเรื่อยๆ อย่างไม่มีที่สิ้นสุด ซึ่งมักจะแสดงด้วย ∞ ^{[ 3 ]}สิ่งนี้เป็นเอกลักษณ์เฉพาะของจำนวนโคนาเจนต์ ดังนั้นจึงสามารถสร้างได้โดยใช้โคเรกชันเท่านั้น:

อินฟินิตี้:: CoNat อินฟินิตี้= Succ อินฟินิตี้

ในขณะที่การเรียกซ้ำ (recursion) กำหนดให้ค่าที่ป้อนเข้าไปในการเรียกซ้ำต้องมีขนาดเล็กลงทุกครั้ง การเรียกซ้ำแบบโคออร์ (corecursion) กำหนดให้ค่าที่ส่งออกมาจากการเรียกซ้ำต้องมีขนาดใหญ่ขึ้นทุกครั้ง นี่คือเหตุผลที่เราต้องเขียนSucc infinity; การเขียนแบบinfinity = infinityจะไม่ได้รับอนุญาตเพราะมันจะวนลูปไปเรื่อยๆ

เพื่อแสดงให้เห็นถึงความเป็นคู่กันระหว่างการเรียกซ้ำและการเรียกซ้ำร่วม เราสามารถห่อหุ้มสิ่งเหล่านี้ไว้ในฟังก์ชันสองฟังก์ชันrecคือ และcorecการมีอยู่ของฟังก์ชันเหล่านี้ พร้อมกับตัวสร้างปกติสองตัวของNatและCoNatระบุประเภทที่เกี่ยวข้องได้อย่างเฉพาะเจาะจง และด้วยเหตุนี้จึงอนุญาตให้เขียนรูปแบบการเรียกซ้ำและการเรียกซ้ำร่วมทั้งหมดใหม่โดยใช้ฟังก์ชันเหล่านี้^{[ 4 ]}

rec :: Nat -> ( Maybe c -> c ) -> c rec Zero f = f Nothing rec ( Succ n ) f = f ( Just ( rec n f ))corec :: ( c -> Maybe c ) -> c -> CoNat corec f base = case f base of Nothing -> Zero Just x -> Succ ( corec f x )

ในเชิงแนวคิดCoNatสามารถมองได้ว่าเป็นเครื่องสถานะ (state machine ) โดยที่cเป็นชนิดข้อมูลที่ห่อหุ้ม "สถานะปัจจุบัน" ฟังก์ชันc -> Maybe cเป็นฟังก์ชันการเปลี่ยนสถานะซึ่งจะส่งผลให้สิ้นสุดด้วยZeroหรือดำเนินการต่อด้วยSuccเราสามารถเขียนตัวอย่างข้างต้นใหม่โดยใช้ฟังก์ชัน ได้ดังนี้:

repeat x n = rec n ( \ s -> case s of Nothing -> [] Just a -> x : a ) infinity = corec ( \ () -> Just () ) ()

ตัวอย่างที่ซับซ้อนกว่าของข้อมูลร่วมคือต้นไม้ไบนารีซึ่งแต่ละโหนดจะเป็นโหนดใบที่เก็บข้อมูลบางอย่าง หรือเป็นโหนดกิ่งที่มีลูกสองตัวพอดี:

codata BinaryTree a = Leaf a | Branch ( BinaryTree a ) ( BinaryTree a )

ตัวอย่างนี้มีเทอมที่มีความลึกอนันต์อีกมากมายที่สามารถสร้างขึ้นได้โดยใช้การเรียกซ้ำร่วมเท่านั้น เช่น อาจมีความลึกอนันต์เฉพาะทางด้านซ้าย หรือทั้งสองด้าน หรือสลับกันระหว่างซ้ายและขวา:

infiniteLeft :: a -> BinaryTree a infiniteLeft x = Branch ( infiniteLeft x ) ( Leaf x )infiniteBoth :: BinaryTree a infiniteBoth = Branch infiniteBoth infiniteBothinfiniteAlternating :: a -> Bool -> BinaryTree a infiniteAlternating x False = Branch ( infiniteAlternating x True ) ( Leaf x ) infiniteAlternating x True = Branch ( Leaf x ) ( infiniteAlternating x False )

กล่าวอีกนัยหนึ่ง การเรียกซ้ำร่วมบนต้นไม้ไบนารีมีรูปแบบทั่วไปมากขึ้นโดยอิงจากตัวสร้างที่คล้ายกับ "เครื่องสถานะ":

corec :: ( c -> Either a ( c , c )) -> c -> BinaryTree a corec f base = case f base of Left x -> Leaf x Right ( x , y ) -> Branch ( corec f x ) ( corec f y )

ใน การตั้งค่า แบบพึ่งพาประเภทข้อมูลร่วมสามารถเข้ารหัสได้โดยใช้ประเภท M ซึ่งเป็นคู่ตรงข้ามกับประเภท Wเมื่อกำหนดประเภทAและตระกูลของประเภทB ที่มีดัชนีเป็น A แล้ว เราสามารถสร้างประเภท M ซึ่งแสดงถึงประเภทของต้นไม้ที่มีโหนดติดป้ายกำกับด้วยองค์ประกอบของAและโหนดลูกมีดัชนีเป็นเซตB ( a ) ในรหัสเทียม ประเภท M (และหลักการเรียกซ้ำร่วม) อาจถูกกำหนดได้ดังนี้:${\displaystyle {\mathsf {M}}_{a:A}B(a)}$

codata M a ( b :: a -> * ) = M { root :: a , branch :: b root -> M a b } corec :: ( c -> ( root :: a , b root -> c )) -> c -> M a b corec f base = let ( root , branch ) = f base in M ​​{ root = root , branch = \ i -> corec f ( branch i ) }

ตัวอย่างเช่น จำนวนธรรมชาติและจำนวนร่วมธรรมชาติ อาจถูกสร้างขึ้นเป็นฟังก์ชันประเภท W และ M ของฟังก์ชันเดียวกันได้:

f :: Bool -> * f False = Void -- กรณีศูนย์ (ไม่มีการแยกสาขา) f True = () -- กรณีสำเร็จ (มีการแยกสาขาหนึ่งสาขา)Nat = W Bool f CoNat = M Bool f

สามารถพิสูจน์ได้ว่า M-type มีอยู่ในโทโพอิพื้นฐาน จำนวนมาก และการมีอยู่ของ M-type เป็นผลมาจากการมีอยู่ของ W-type ^{[ 5 ]}

ส่วนข้างต้นแสดงให้เห็นว่ามีความเชื่อมโยงอย่างใกล้ชิดระหว่างจำนวนธรรมชาติและจำนวนร่วมธรรมชาติMaybe cและในทำนองเดียวกันระหว่างต้นไม้ไบนารีและEither a (c, c)ความเชื่อมโยงนี้มีความชัดเจนมากขึ้นโดยการแสดงว่าNatเป็นฟังก์ชันหนึ่งต่อหนึ่งทั่วถึงกับMaybe NatและCoNatกับMaybe CoNatโดยเฉพาะอย่างยิ่ง ฟังก์ชันหนึ่งต่อหนึ่งทั่วถึงนี้เชื่อมโยงกับ ZeroและNothingกับSucc nกล่าวJust nอีกนัยหนึ่งคือNatและCoNatเป็นจุดคงที่ ( จนถึงไอโซมอร์ฟิซึม ) ของแผนที่${\displaystyle X\mapsto X+1}$

ความแตกต่างระหว่างข้อมูลและโคดาต้าคือ ข้อมูลเป็นจุดคงที่ที่เล็กที่สุด ในขณะที่โคดาต้าเป็นจุดคงที่ที่ใหญ่ที่สุด ด้วยวิธีนี้ การเรียกซ้ำสามารถสรุปได้ว่า "องค์ประกอบทุกตัวของประเภทถูกสร้างขึ้นโดยตัวสร้างที่กำหนดเท่านั้น ( ZeroและSuccในกรณีของNat/ CoNat)" ในขณะที่โคดาต้ากล่าวว่า "ค่าทุกค่าที่สามารถวิเคราะห์ได้โดยใช้ตัวสร้างเป็นกรณีต่างๆ นั้นมีอยู่จริง"

จากมุมมองเชิงทฤษฎีหมวดหมู่CoNatสามารถกำหนดได้อย่างแม่นยำว่าเป็นโคอัลจีบราสุดท้ายของ เอน โดฟังก์ชัน^{[ 4 ]}เมื่อขยายคำจำกัดความนี้ เราจะได้ว่า: ${\displaystyle X\mapsto X+1}$

• มีฟังก์ชันอยู่ฟังก์ชันหนึ่งpred :: CoNat -> Maybe CoNat"Pred" ย่อมาจาก "predecessor" และโดยสัญชาตญาณแล้ว ฟังก์ชันนี้จะลบหนึ่งออกจากจำนวนโคเนเชอรัล หรือให้Nothingค่าอื่นแทน กล่าวอีกนัยหนึ่งคือpred Zero = Nothingและpred (Succ n) = Just nสิ่งนี้แสดงให้เห็นว่าCoNatเป็นโคอัลจีบราของฟังก์ชัน แต่ไม่จำเป็นต้องเป็นโคอัลจีบราสุดท้าย
• สำหรับทุกประเภทcและฟังก์ชันf :: c -> Maybe cจะมีฟังก์ชันหนึ่งcorec f :: c -> CoNatที่ทำให้ โดยpred (corec f x) = fmap (corec f) (f x)การแยกย่อยลงไปอีก ถ้าf x = Just yแล้วcorec f x = Succ (corec f y)ในขณะที่ถ้าf x = Nothingแล้วcorec f x = Zero—ซึ่งตรงกับนิยามของที่corecเราคุ้นเคยกันดี
• corecมีเอกลักษณ์ในความหมายต่อไปนี้: สำหรับฟังก์ชันอื่นใดg :: c -> CoNatที่สอดคล้องกับเงื่อนไข เช่นกันpred (g x) = fmap g (f x)สิ่งg x = corec f xนี้รับประกันว่าCoNatเป็นโคอัลจีบราสุดท้าย

Maybe cสามารถแทนที่ฟังก์ชันดังกล่าวด้วยฟังก์ชันอื่นใดก็ได้ในคำอธิบายข้างต้น เพื่อให้ได้นิยามของประเภทการเหนี่ยวนำร่วมอื่น ๆ

ไม่ใช่ฟังก์ชันทั้งหมดที่มีคอลจีบราสุดท้าย ตัวอย่างเช่นทฤษฎีบทของแคนเตอร์บอกเราว่าไม่มีเซตใดที่สามารถจับคู่กับเซตกำลังของมันได้ ดังนั้นฟังก์ชันเซตกำลังa -> Bool จึง ไม่มีคอลจีบราสุดท้าย อย่างไรก็ตาม ในกรณีของฟังก์ชันพหุนามหรือฟังก์ชันพหุนามผลหาร^{[ 6 ]}คอลจีบราสุดท้ายจะมีอยู่เสมอ ฟังก์ชันพหุนามเป็นฟังก์ชันที่สามารถแสดงในรูปแบบสำหรับประเภทαและตระกูลประเภทβ ( a ) ที่มีดัชนี αประเภท M คือการสร้างคอลจีบราสุดท้ายนี้อย่างแม่นยำ^{[ 5 ]}${\displaystyle \textstyle X\mapsto \sum _{a:\alpha }X^{\beta (a)}}$

แม้ว่าเราจะสามารถให้เหตุผลเกี่ยวกับชนิดข้อมูลแบบเหนี่ยวนำร่วมโดยใช้ความเป็นเอกลักษณ์ โดยตรงได้ แต่โดยทั่วไปแล้วการใช้ การเหนี่ยวนำร่วมcorecจะสะดวกกว่าซึ่งสามารถพิสูจน์ความเท่าเทียมกันของข้อมูลร่วมได้ กำหนดให้โคอัลจีบราสุดท้ายAของฟังก์ชันพหุนามF —เช่น— เรากล่าวว่าความสัมพันธ์เป็นการจำลองแบบคู่ขนานถ้าสำหรับทุกและสำหรับทุกโดยที่และหมายถึงแผนที่: ${\displaystyle \textstyle F(X)=\sum _{a:\alpha }X^{\beta (a)}}$${\displaystyle R\subseteq A\times A}$${\displaystyle (a,b)\in R}$${\displaystyle {\text{root}}(a)={\text{root}}(b)}$${\displaystyle {\text{branch}}(a,i)R{\text{branch}}(b,i)}$${\displaystyle i:B({\text{root}}(a))}$${\displaystyle {\text{root}}}$${\displaystyle {\text{สาขา}}}$

${\displaystyle {\begin{aligned}{\text{root}}&:A\rightarrow \alpha \\{\text{branch}}&:\prod _{a:A}\beta ({\text{root}}(a))\rightarrow A\end{aligned}}}$

หลักการของการเหนี่ยวนำร่วมระบุว่าสำหรับการจำลองแบบคู่ทั้งหมดRบนAและ, . ${\displaystyle (a,b)\in R}$${\displaystyle a=b}$

โดยทั่วไปแล้ว สำหรับแผนที่โคอัลจีบราความสัมพันธ์RบนAจะเป็นบิซิมูเลชันก็ต่อเมื่อมีฟังก์ชันที่สอดคล้องกับเงื่อนไขสำหรับทุกๆ ${\displaystyle {\text{get}}:A\rightarrow F(A)}$${\displaystyle f:R\rightarrow F(R)}$${\displaystyle (a,b)\in R}$

• ${\displaystyle {\text{get}}(a)=F(\pi _{1})(f(a,b))}$และ
• ${\displaystyle {\text{get}}(b)=F(\pi _{2})(f(a,b))}$,

โดยที่π ₁ และπ ₂ คือแผนที่การฉายภาพครั้งแรกและครั้งที่สองจะเห็นได้ว่ากรณีนี้เทียบเท่ากับกรณีพหุนามโดยการตั้งค่าความเท่าเทียมกันที่ต้องการสามารถแสดงได้ในรูปแผนภาพการสลับที่เช่นกัน: ${\displaystyle R\rightarrow A}$${\displaystyle f(a,b)=({\text{root}}(a),i\mapsto ({\text{branch}}(a,i),{\text{branch}}(b,i)))}$

การเหนี่ยวนำร่วมสามารถพิสูจน์ได้ง่ายจากความเป็นเอกลักษณ์ของcorec: π ₁ และπ ₂ ต่างก็มีคุณสมบัติที่กำหนดให้เท่ากับcorec fและจึงเท่ากัน ซึ่งแสดงให้เห็นว่า^{[ 4 ]}${\displaystyle a=\pi _{1}(a,b)=\pi _{2}(a,b)=b}$

เพื่อสาธิตการใช้การเหนี่ยวนำร่วม เราจะพิสูจน์คุณสมบัติพื้นฐานบางประการเกี่ยวกับการบวกบนจำนวนโคเนเชอรัล การบวกสามารถกำหนดได้เหมือนกับที่กำหนดไว้สำหรับจำนวนธรรมชาติ: ^{[ 3 ]}

เพิ่ม:: CoNat -> CoNat - > CoNat เพิ่มZero = a เพิ่มa ( Succ b ) = Succ ( เพิ่มa b )

คำจำกัดความนี้ แม้จะถูกต้อง แต่ก็ซ่อนความซับซ้อนบางอย่างไว้ เราอาจเขียนได้อีกแบบว่า:

เพิ่มศูนย์ศูนย์= ศูนย์เพิ่ม( Succ a ) ศูนย์= Succ ( เพิ่มa ศูนย์) เพิ่มa ( Succ b ) = Succ ( เพิ่มa b )

คำจำกัดความนี้ทำให้การแปลเป็นcorecเรื่องง่าย:

iterate :: ( CoNat , CoNat ) -> Maybe ( CoNat , CoNat ) iterate Zero Zero = Nothing iterate ( Succ a ) Zero = Just ( a , Zero ) iterate a ( Succ b ) = Just ( a , b )เพิ่มa b = corec วนซ้ำ( a , b )

เราสามารถพิสูจน์ได้โดยใช้การเหนี่ยวนำร่วมบนความสัมพันธ์(โดยที่คือเซตของจำนวนร่วมธรรมชาติ) ประการแรก จากนิยามของการบวก จะได้ว่า; ประการที่สอง ถ้าเราสมมติว่าอยู่ในรูปแบบสำหรับบางค่าaเราต้องแสดงว่า ก็อยู่ในรูปแบบนี้เช่นกัน เรามี: ดังนั้นและด้วยเหตุนี้จึงเป็นไปตามที่ต้องการ ${\displaystyle a+0=a}$${\displaystyle \{(a+0,a)|a\in \mathbb {N} ^{\infty }\}}$${\displaystyle \mathbb {N} ^{\infty }}$${\displaystyle a+0=0\iff a=0}$${\displaystyle (x+1,y+1)}$${\displaystyle (a+0,a)}$${\displaystyle (x,y)}$$${\displaystyle x+1=a+0=(y+1)+0=(y+0)+1}$$${\displaystyle x=y+0}$${\displaystyle (x,y)=(y+0,y)}$

เอกลักษณ์อาจได้รับการพิสูจน์ในทำนองเดียวกันโดยการเหนี่ยวนำร่วมบน(จำไว้ว่าความสัมพันธ์จะต้องรวมถึง); ในที่สุด การสลับที่ได้— —เป็นผลมาจากการเหนี่ยวนำร่วมที่ตรงไปตรงมาในทำนองเดียวกันบน^{[ 7 ]}${\displaystyle (a+1)+b=(a+b)+1}$${\displaystyle \{(((a+1)+b)-1,a+b)|a,b\in \mathbb {N} ^{\infty }\}}$${\displaystyle (0,0)}$${\displaystyle a+b=b+a}$${\displaystyle \{(a+b,b+a)|a,b\in \mathbb {N} ^{\infty }\}}$

หากโดเมนของการสนทนาคือหมวดหมู่ของเซตและฟังก์ชันทั้งหมด (เช่นในโปรแกรมพิสูจน์ทฤษฎีบทอย่าง Agda และ Rocq) ประเภทสุดท้าย (codata) อาจมี ค่าอนันต์ ที่ไม่เป็นไปตามกฎเกณฑ์ในขณะที่ประเภทเริ่มต้น (data) ไม่มี^{[ 8 ] [ 9 ]}ในทางกลับกัน หากโดเมนของการสนทนาคือหมวดหมู่ของลำดับบางส่วนที่สมบูรณ์และฟังก์ชันต่อเนื่องซึ่งสอดคล้องกับ ภาษาการเขียนโปรแกรม Haskell โดยประมาณ ประเภทสุดท้ายจะตรงกับประเภทเริ่มต้น และ coalgebra สุดท้ายและ algebra เริ่มต้นที่สอดคล้องกันจะก่อให้เกิด isomorphism ^{[ 10 ]}

การเรียกซ้ำแบบวงกลม (Corecursion) หรือที่เรียกว่าการเขียนโปรแกรมแบบวงกลมมีมาอย่างน้อยตั้งแต่ ( Bird 1984 ) ซึ่งให้เครดิตแก่John HughesและPhilip Wadlerรูปแบบทั่วไปมากขึ้นได้รับการพัฒนาใน ( Allison 1989 ) แรงจูงใจดั้งเดิมรวมถึงการสร้างอัลกอริทึมที่มีประสิทธิภาพมากขึ้น (อนุญาตให้ประมวลผลข้อมูลเพียงครั้งเดียวในบางกรณี แทนที่จะต้องประมวลผลหลายครั้ง) และการนำโครงสร้างข้อมูลแบบคลาสสิก เช่นรายการเชื่อมโยงสองทางและคิว มาใช้ในภาษาโปรแกรมเชิงฟังก์ชัน

• การจำลองแบบไบซิเมชั่น
• การเหนี่ยวนำร่วม
• การเรียกซ้ำ
• อนามอร์ฟิซึม