קואינדוקציה

במדעי המחשב, קואינדוקציה היא טכניקה להגדרה והוכחה של תכונות הנוגעות למערכות עצמים שמקיימות תכונות מסוימות של אינטראקציה בין העצמים בהן.

קואינדוקציה היא ההיפוך המתמטי של אינדוקציה מבנית.^{[דרוש מקור]} טיפוסים המוגדרים באופן קואינדוקטיבי נקראים קודאטה (codata) והם בדרך כלל מבני נתונים אינסופיים, כגון זרמים.

כהגדרה או מפרט, קואינדוקציה מתארת כיצד ניתן "לבחון" אובייקט, וכיצד "לפרק" או "לשבור" אותו לאובייקטים פשוטים יותר. כטכניקת הוכחה, ניתן להשתמש בה כדי להראות שמשוואה מתקיימת בכל המימושים האפשריים של מפרט כזה.

כדי ליצור ולתפעל קודאטה, משתמשים בדרך כלל בפונקציות קורקורסיביות, בשילוב עם הערכה עצלנית. במונחים לא רשמיים, במקום להגדיר פונקציה על ידי התאמת דפוסים בכל אחד מהמרכיבים האינדוקטיביים, מגדירים את פלט כל אחד מה"משמידים" או "הבוחנים" על תוצאת הפונקציה.

תיאור

ב - ניתנת הגדרה תמציתית הן של עקרון האינדוקציה והן של עקרון הקואינדוקציה. אמנם ערך זה אינו עוסק בעיקר באינדוקציה, אך יש ערך בהתבוננות בצורות המוכללות של שתיהן בבת אחת. על מנת לתאר את העקרונות, נדרשות מספר הקדמות.

הקדמות

תהי $U$ קבוצה ותהי $F$ פונקציה מונוטונית $2^{U}\rightarrow 2^{U}$, כלומר:

$X\subseteq Y\Rightarrow F(X)\subseteq F(Y)$

אלא אם צוין אחרת, ההנחה היא כי $F$ מונוטונית.

X נקראת F-סגורה אם $F(X)\subseteq X$

X נקראת F-עקבית אם $X\subseteq F(X)$

X נקראת נקודת שבת אם $X=F(X)$

ניתן להבין מונחים אלו אינטואיטיבית באופן הבא. נניח ש-$X$ היא קבוצה של קביעות, ו-$F(X)$ היא הפעולה שמחזירה את ההשלכות של $X$. אז $X$ היא F-סגורה כאשר לא ניתן להסיק יותר ממה שכבר נטען, בעוד $X$ היא F-עקבית כאשר כל הקביעות בה נתמכות על ידי קביעות אחרות (כלומר, אין "הנחות לא-F-לוגיות").

משפט קנאסטר-טרסקי קובע כי נקודת השבת הקטנה ביותר של $F$ (המסומנת ב-$\mu F$) מתקבלת על ידי החיתוך של כל הקבוצות ה-F-סגורות, בעוד שנקודת השבת הגדולה ביותר (המסומנת ב-$\nu F$) מתקבלת על ידי האיחוד של כל הקבוצות ה-F-עקביות. כעת נוכל לציין את עקרונות האינדוקציה והקואינדוקציה.

הגדרה

עקרון האינדוקציה : אם $X$ היא F-סגורה, אז $\mu F\subseteq X$

עקרון הקואינדוקציה : אם $X$ היא F-עקבית, אז $X\subseteq \nu F$

דיון

העקרונות, כפי שהוצהרו, מעט לא ברורים, אך ניתן לחשוב עליהם בצורה מועילה בדרך הבאה. נניח שאנו רוצים להוכיח תכונה של כל האיברים של $\mu F$. לפי עקרון האינדוקציה, די להראות שקיימת קבוצה F-סגורה $X$ שעבור כל איבר בה מתקיימת התכונה. באופן הופכי, נניח שאנו רוצים להראות $x\in \nu F$. אז מספיק להציג קבוצה F-עקבית אשר $x$ שייך לה.

דוגמאות

הגדרת קבוצה של טיפוסי נתונים

הבה נתבונן בדקדוק הבא של טיפוסי נתונים:

$T=\bot \;|\;\top \;|\;T\times T$

כלומר, קבוצת הטיפוסים כוללת את "הטיפוס התחתון" $\bot$, "הטיפוס העליון" $\top$, ורשימות (לא הומוגניות). ניתן לזהות את הטיפוסים הללו עם המחרוזות מעל האלפבית $\Sigma =\{\bot ,\top \}$. תהי $\Sigma ^{*}$ קבוצת כל המחרוזות מעל $\Sigma$. נתבונן בפונקציה $F:2^{\Sigma ^{*}}\rightarrow 2^{\Sigma ^{*}}$:

$F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}$

בהקשר הזה, $x\times y$ פירושו "ההרכבה של המחרוזת $x$ והמחרוזת $y$." כעת עלינו להגדיר את קבוצת סוגי הנתונים שלנו כנקודת שבת של $F$, אבל זה משנה אם נבחר את הנקודה הקטנה ביותר או את הגדולה ביותר.

נניח שהגדרנו את $\mu F$ כקבוצת טיפוסי הנתונים שלנו. באמצעות עקרון האינדוקציה, נוכל להוכיח את הטענה הבאה:

כל טיפוסי הנתונים ב-$\mu F$ הם סופיים

כדי להגיע למסקנה זו, נסתכל על קבוצת כל המחרוזות הסופיות מעל $\Sigma$. ברור כי $F$ לא יכולה לייצר מחרוזת אינסופית במקרה זה, לכן מתקבל כי הקבוצה הזו F-סגורה והמסקנה נובעת מאליה.

עכשיו ניקח במקום את $\nu F$ כקבוצת טיפוסי הנתונים שלנו. ברצוננו להשתמש בעקרון הקואינדוקציה כדי להוכיח את הטענה הבאה:

הטיפוס $\bot \times \bot \times \cdots$ שייך ל-$\nu F$

כאן $\bot \times \bot \times \cdots$ מציין את הרשימה האינסופית המורכבת לחלוטין מעותקים של $\bot$. על מנת להשתמש בעקרון הקואינדוקציה, נתבונן בקבוצה:

$\{\bot \times \bot \times \cdots \}$

הקבוצה הזו מתבררת כ-F-עקבית, ולכן $\bot \times \bot \times \cdots \in \nu F$. קביעה זו תלויה בקביעה החשודה ש-

$\bot \times \bot \times \cdots =\bot \times \bot \times \cdots \times \bot \times \bot \times \cdots$

ההצדקה הפורמלית לכך היא טכנית ומסתמכת על פירוש מחרוזות כסדרות, כלומר פונקציות מסוג $\mathbb {N} \rightarrow \Sigma$. באופן אינטואיטיבי, הטיעון דומה לטיעון כי $0.{\bar {0}}1=0$ (ראו שבר מחזורי).

טיפוסי נתונים קואינדוקטיביים בשפות תכנות

נתבונן בהגדרה הבאה של זרם:^{[דרוש מקור]}

data Stream a = S a (Stream a)

-- Stream "destructors"
head (S a astream) = a
tail (S a astream) = astream

נראה כי זו הגדרה שאינה מבוססת היטב, אך היא בכל זאת שימושית בתכנות וניתן להשתמש בה באופן הגיוני. בכל אופן, זרם הוא רשימה אינסופית של איברים שניתן לבחון את הראשון מהם, או להחסיר את האיבר הזה כדי לקבל זרם נוסף.

קשר עם קואלגברות-F

ראו תורת הקטגוריות

נבחן את האנדופונקטור $F$ בקטגוריית הקבוצות:

$F(x)=A\times x$

$F(f)=\langle \mathrm {id} _{A},f\rangle$

לקואלגברת-F הסופית $\nu F$ מיוחס המורפיזם הבא:

$\mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F$

ממנו נובעת קואלגברה נוספת $F(\nu F)$ עם המורפיזם $F(\mathrm {out} )$. מכיוון ש-$\nu F$ סופית, קיים מורפיזם יחיד

${\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F$

כך ש-

$\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)$

ההרכבה ${\overline {F(\mathrm {out} )}}\circ \mathrm {out}$ יוצרת הומומורפיזם נוסף של קואלגברות-F, $\nu F\rightarrow \nu F$. מאחר ש-$\nu F$ סופית, הומומורפיזם זה הוא יחיד, ולכן זהה ל-$\mathrm {id} _{\nu F}$. בסך הכל מתקבל:

${\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}$

$\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}$

זוהי עדות לאיזומורפיזם $\nu F\simeq F(\nu F)$, המצביע במונחים קטגוריים על העובדה ש-$\nu F$ היא נקודת שבת של $F$, ומצדיק את הסימון.

זרם כקואלגברה סופית

נראה כי

Stream A

היא הקואלגברה הסופית של הפונקטור $F(x)=A\times x$. נתבונן במימושים הבאים:

out astream = (head astream, tail astream)
out' (a, astream) = S a astream

ניתן לראות בקלות שהם הופכיים אחד של השני, ועדים לאיזומורפיזם. עיינו בהפנייה לפרטים נוספים.

קשר עם אינדוקציה מתמטית

נדגים כיצד עקרון האינדוקציה כולל את מושג האינדוקציה המתמטית. תהי $P$ תכונה כלשהי של מספרים טבעיים. נבחר בהגדרה הבאה של אינדוקציה מתמטית:

$P(0)\land (P(n)\Rightarrow P(n+1))\Rightarrow P(\mathbb {N} )$

כעת נבחן את הפונקציה $F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }$:

$F(X)=\{0\}\cup \{x+1:x\in X\}$

ניתן לראות בקלות יחסית כי $\mu F=\mathbb {N}$. לכן, לפי עקרון האינדוקציה, אם ברצוננו להוכיח תכונה כלשהי $P$ של $\mathbb {N}$, די להראות ש-$P$ היא F-סגורה. בפירוט, הדרישה היא:

$F(P)\subseteq P$

כלומר,

$\{0\}\cup \{x+1:x\in P\}\subseteq P$

זוהי בדיוק ההגדרה של ההגדרה של אינדוקציה מתמטית כפי שציינו אותה.

לקריאה נוספת

ספרי לימוד

• Davide Sangiorgi (2012). Introduction to Bisimulation and Coinduction. Cambridge University Press.
• Davide Sangiorgi and Jan Rutten (2011). Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.

כתבי מבוא

• Andrew D. Gordon (1994). "A Tutorial on Co-induction and Functional Programming"
• Bart Jacobs and Jan Rutten (1997). A Tutorial on (Co)Algebras and (Co)Induction (קישור חלופי) — מתאר אינדוקציה וקואינדוקציה בבת אחת
• Eduardo Giménez and Pierre Castéran (2007). "A Tutorial on [Co-Inductive Types in Coq"]
• Coinduction — מבוא קצר

ערך זה הוא יתום, כלומר אין ערכים במכלול שמקשרים אליו. אתם מוזמנים לתרום למכלול ולקשר אליו מכמה מהערכים שמכילים את המונח "קואינדוקציה".

הערך באדיבות ויקיפדיה העברית, קרדיט,
רשימת התורמים
רישיון cc-by-sa 3.0

קואינדוקציה37641347Q4227156