Structural induction

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

א) בסיס האינדוקציה- המקרה הכי בסיסי ופשוט שבו קל להראות שהטענה נכונה.
ב) הנחת האינדוקציה- הנחה כללית שהטענה נכונה עבור מקרה כלשהו.
ג) צעד האינדוקציה- צ״ל שאם נוסיף צעד לאיבר שידוע שעליו הטענה מתקיימת אז גם האיבר החדש מקיים את הטענה.

אינדוקציה מתמטית

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

לדוגמה נגדיר את הקבוצה הבאה

בעצם $A=\{3n|n\in \mathbb{N}\}$ .

נרצה להוכיח ש ${\mathrm{\forall }}_{3n\in A}:3|a$ . קל להוכיח זאת באינדוקציה מתמטית. הבסיס יהיה $a=3$ וההנחה תהיה שמתקיים עבור $a\in A$ כלשהו וקל להסביר למה עבור $a+3$ הטענה גם מתקיימת.

הגדרה: $P(a)$ מוגדר להיות פרדיקט (טענה שמחזירה true או false ) כלשהו על $a$ במקרה הזה $3|a$ .

נשים לב: היינו יכולים להגדיר את $a$ כאיבר מהצורה $3n$ ולהוכיח באינדוקציה מתמטית עם הבסיס $n=1$

אינדוקציה מבנית

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

נניח שיש לנו $A$ קבוצה של איברים שנוצרה מהגדרה רקורסיבית, נרצה להוכיח שמתקיים פרדיקט $P$ לכל איבר בקבוצה. כלומר : ${\mathrm{\forall }}_{a\in A}:P(A)=\text{ true }$ .

בסיס האינדוקציה: נראה ש $P$ מתקיים עבור איבר הבסיס.
הנחת האינדוקציה: נניח $P(a)$ עבור $a\in A$ כללי.
צעד האינדוקציה: אם הטענה נכונה לאיבר $a\in A$ אז הטענה נכונה לאיברים ש״נובעים״ ממנו לפי כללי הרקורסיה.

לדוגמה - עבור הדוגמה של אינדוקציה מתמטית ממקודם הבסיס יהיה האיבר $3$ וכמובן שמתקיים $3|3$ .
ההנחה תהיה $P(a)$ עבור $a$ כלשהו כלומר $3|a$ . האיבר הבא הוא $a+3$ ולכן טריוויאלי שהוא מקיים $3|a+3$ .

דוגמה 2:
נגדיר קבוצה $A$ כ

נרצה להוכיח את הטענה ש ${\mathrm{\forall }}_{(a,b)\in A}:9|(a+b)$ כלומר $P(a,b):9|(a,b)$ .

בסיס האינדוקציה: איברי הבסיס הנ״ל מקיימים את הדרוש שכן סכומם הוא $9$.
הנחת האינדוקציה: נניח $P(a,b)$ עבור $(a,b)\in A$
צעד האינדוקציה: מההנחה מתקיים $9|a+b$ נתבונן באיברים הבאים בתור: $(a+5,b+4),(a,b+9)$
נסמן $a+b=9k$ שכן הסכום מתחלק ב$9$ . מתקיים ש $a+5+b+4=9k+9=9(k+1)$ שכמובן מתחלק ב$9$. ועבור האיבר השני $a+b+9=9k+9=9(k+1)$ שבאותו אופן מתחלק ב$9$

אינדוקציה מבנית על עצים בינאריים

נוכיח טענה באמצעות אינדוקציה מבנית על עץ בינארי מלא. נרצה להוכיח את הטענה שכמות העלים שווה לכמות הקודקודים הפנימיים בעץ ועוד אחד.

לשם נוחות נסמן: $e(t)$ - פונקציה המחזירה את כמות העלים בעץ , $b(t)$ - פונקציה המחזירה את כמות הקודקודים הפנימיים בעץ. צ״ל ש $e(t)=b(t)+1$

בסיס: עבור עץ $T$ עם קודקוד בודד מתקיים $e(T)=1$ ו $b(T)=0$ ולכן מתקיים הדרוש.
הנחה: עבור עץ $T_1$ מתקיים $e(T_1)=b(T_1)+1$ וכנ״ל עבור עץ $T_2$.

צעד: נגדיר $T$ שהוא עץ עם קודקוד שורש ותת עץ ימני שהוא $T_2$ ותת עץ שמאלי שהוא $T_1$. מתקיים :

מתקיים גם ש

כאשר התוספת $1$ היא בגלל קודקוד השורש. אם נציב במשוואה למעלה נקבל $e(T)=b(T)+1$ כדרוש .

אינדוקציה מבנית על דקדוק חסר הקשר

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

Production Rules:

Backus-Naur Form (BNF):

Derivation Rules:

כאשר הסימון של כללי גזירה הוא ״מלמעלה אפשר לגזור את מה שכתוב למטה״.

כעת נייצג את הקבוצה $M$ באופן הבא:

ובאמצעות כללי גזירה :

נרצה להוכיח ש $\mathbb{N}=M$ על ידי הכלה דו כיוונית באמצעות אינדוקציה מבנית.

$\leftarrow$ : $M\subseteq N$ -
בסיס - עבור איברי הבסיס של $M$ שהם $(0,S(0))$ נקבל ש $0\in N$ מהגדרה וגם מכלל הגזרה השני של המספרים הטבעיים $\frac{}{\frac{0\in N}{S(0)\in N}}$ .

הנחת האינדוקציה- יהי $x\in M\cap N$ .

צעד- אם $x\in M$ אזי $S(S(x))\in M$ ונרצה להראות שזה שייך גם ל $N$ . קל להראות זאת באמצעות אותם כללי גזירה $x\in N|S(x)\in N|S(S(x))\in N$ כלומר הפעלת כלל הגזירה $succ$ פעמיים.

$\to$ $M\supseteq N$ -
בסיס - איבר הבסיס של $N$ הוא $0$ ומכלל הגזירה מתקיים שהוא אכן ב $M$

הנחה - יהי $x\in M\cap N$ .

צעד- עבור $x\in N$ מתקיים ש $S(x)\in N$ ונרצה להוכיח שגם הוא שייך ל $M$. כיוון ש $x\in M$ מתקיים ש $S(S(x))\in M$.

נשים לב שנתקלנו במבוי סתום, שכן לא ניתן לגזור מתוך החוקים של $M$ את $S(x)$ .

מה עושים? הפתרון הוא להוכיח טענה חזקה יותר באמצעות אינדוקציה מבנית, במקרה הזה הפתרון הוא להוכיח ש ${\mathrm{\forall }}_{x\in N}:x\in M\wedge S(x)\in M$ . הסיבה שזה עובד היא בגלל כלל גזירה של $M$ שלא ניצלנו אותו שהוא הכלל $one$ .

אם נרצה להוכיח את הנ״ל נוכל להראות ש $S(0)\in M$ בקלות כי $0\in M$ .
הכוח פה כעת הוא בהנחת האינדוקציה שכן נקבל $x\in N\cap M\wedge S(x)\in M$ וכעת בצעד יותר קל לנו להוכיח את הדרוש.

ביטויים אריתמטיים

נגדיר דקדוק חסר הקשר שיוצר ביטויים מתמטיים עם מספרים טבעיים והאופרטורים $+,\ast ,()$

או באמצעות סדרת כללי הגזירה

נשים לב שהדקדוק הוא רב משמעי, למשל נראה ש $(5+3)\ast 2+5\in E$ באמצעות עץ גזירה

אינדוקציה מבנית על פונקציות ב OCaml

נגדיר את הפונקציה הבאה בOCaml

let rec m = fun t -> match t with
	| Leaf(a) -> Leaf(a)
	| Node(t1,t2) -> Node(m(t2), m(t1))

פונקציה שעושה mirror לעץ בינארי (החלפה בין הילדים) ונרצה להוכיח את הטענה הבאה : ${\mathrm{\forall }}_T:m(m(T))=T$ כאשר $T$ הוא עץ בינארי.

נראה כעת כיצד להוכיח באמצעות אינדוקציה מבנית:
בסיס- t=Leaf(a) עבור עלה כלשהו, לפי הגדרת $m$ נקבל ש $m(t)=t$ ולכן $m(m(t))=t$ .

הנחה- יהיו $t1,t2$ מטיפוס $tree$ ונניח $m(m(t_1))=t_1,m(m(t_2))=t_2$

צעד- $t=Node(t_1,t_2)$ ומתקיים

כדרוש