מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

2.1. תזכורת – תחשיב היחסים

הסימנים של תחשיב היחסים

הסימנים מתחלקים ל-2 קבוצות:

סימנים לוגיים – סימנים המשותפים לכל השפות של תחשיב היחסים.
פרמטרים של השפה – מילון – סימנים המיוחדים לשפה.

הסימנים הלוגיים

כמתים: לכל $plot:\[\forall \]$ , קיים $plot:\[\exists \]$ .
קשרים של תחשיב הפסוקים: $plot:\[\left\{ { \to , \wedge , \vee ,\neg } \right\}\]$ .
סוגריים ופסיק.
סימן שוויון $plot:\[ \approx \]$ .
משתנים: $plot:\[\left\{ {{v_i}|i \in \mathbb{N}} \right\}\]$ .

מילון: פרמטרים של השפה

סימני קבועים אישיים מסומנים ב- $plot:\[{C_\alpha }\]$ כאשר $plot:\[\alpha \]$ אינדקס מספרי.
סימני יחס המסומנים ב- $plot:\[{R_{n,\alpha }}\]$ כאשר $plot:\[n,\alpha \in \mathbb{N}\]$ . $plot:\[n\]$ הוא מספר הארגומנטים ביחס ו- $plot:\[\alpha \]$ הוא אינדקס מספרי.
סימני פונקציה המסומנים ב- $plot:\[{F_{n,\alpha }}\]$ . $plot:\[n\]$ הוא מספר הארגומנטים ביחס ו- $plot:\[\alpha \]$ הוא אינדקס מספרי.

מילון: אוסף סימני יחס, סימני פונקציה וסימני קבועים אישיים, כאשר לכל סימן פונקציה ולכל סימן יחס ידוע מספר הארגומנטים. מילון מסומן לרוב באות $plot:\[\tau \]$ . לדוגמא: $plot:\[{\tau _0} = \left\langle {{R_{1,0}},{R_{1,1}},{F_{2,0}},{F_{2,3}},{C_2},{C_3}} \right\rangle \]$ .

מילון סופי הוא מילון המכיל מספר סופי של סימנים. מילון יחסי הוא מילון המכיל רק סימני יחס.

הגדרת אוסף הטענות בשפה

שלב 1:	הגדרת אוסף העצמים עליהם מדברים. שמות עצם אינם טענות שניתן לשאול עליהם נכון / לא נכון.
שלב 2:	נגדיר את אוסף הטענות בשפה שתיקראנה נוסחאות על סמך שמות העצם.

הגדרת אוסף שמות העצם

ההגדרה הינה באינדוקציה: (סימני פיסוק, משתנים $plot:\[ \cup \]$ קבועים)X.

קבוצת האטומים: סימני הקבועים מהמילון בתוספת המשתנים $plot:\[\left\{ {{v_i}|i \in \mathbb{N}} \right\}\]$ .

קבוצת הפעולות: לכל סימן פונקציה $plot:\[{F_{n,\alpha }}\]$ במילון נגדיר פעולה המקבלת שמות עצם $plot:\[{t_1},...,{t_n}\]$ ומוציאה כפלט את $plot:\[{F_{n,\alpha }}\left( {{t_1},...,{t_n}} \right)\]$ .

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

הגדרת אוסף הטענות/נוסחאות.

ההגדרה הינה באינדוקציה. קבוצת האטומים הינה אוסף סדרות הסימנים מהצורה $plot:\[{R_{n,\alpha }}\left( {{t_1},...,{t_n}} \right)\]$ כאשר $plot:\[{t_1},...,{t_n}\]$ שמות עצם, ו- $plot:\[{R_{n,\alpha }}\]$ הינו סימן יחס $plot:\[n\]$ -מקומי מהמילון. כל סדרת סימנים כזו תקרא נוסחה אטומית.

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

עבור הגדרת אוסף הנוסחאות נתייחס לסימן "=" כאל סימן יחס דו מקומי. דוגמא: $plot:\[F\left( {x,x} \right) = F\left( {x,y} \right)\]$ זוהי נוסחה אטומית.

קבוצת אוסף הפעולות מתחלקת לשני חלקים:

הפעלת הקשרים של תחשיב הפסוקים. אם $plot:\[\alpha ,\beta \]$ נוסחאות, אזי גם הביטויים הנ"ל הם נוסחאות: $plot:\[\left( {\alpha \wedge \beta } \right),\left( {\alpha \vee \beta } \right),\left( {\alpha \to \beta } \right),\left( {\neg \alpha } \right)\]$ .
הפעלת כמתים: לכל נוסחה $plot:\[\alpha \]$ ומשתנה $plot:\[x\]$ , גם $plot:\[\forall x\alpha \]$ ו- $plot:\[\exists x\alpha \]$ הן נוסחאות.

הערה: מניחים קדימות לכמתים: $plot:\[\forall {v_i}P\left( {{v_i}} \right) \to R\left( {{v_r}} \right) \equiv \left( {\forall {v_i}P\left( {{v_i}} \right)} \right) \to R\left( {{v_r}} \right)\]$

הבדלים בין סימני יחס לפונקציות

$plot:\[F\left( {F\left( {} \right)} \right)\]$ הינו שם עצם. $plot:\[R\left( {R\left( {} \right)} \right)\]$ לא מוגדר כחלק מתחשיב היחסים!

$plot:\[R\left( {F\left( {} \right)} \right)\]$ הינה נוסחה אטומית. $plot:\[F\left( {R\left( {} \right)} \right)\]$ לא קיים – אסור להפעיל סימני פונקציה על יחס.

$plot:\[R \to R\]$ מותר. $plot:\[F \to F\]$ - אסור. יש לתת סימני יחס בין הקשרים והכמתים.

$plot:\[\forall xR\]$ מותר. $plot:\[\forall xF\]$ אסור.

סמנטיקה לתחשיב היחסים - הגדרה אינטואיטיבית

בהינתן מילון $plot:\[\tau \]$ , $plot:\[\tau = \left\langle {{R_1},...,{R_m},{F_1},...,{F_k},{C_1}...,{C_l}} \right\rangle \]$ מבנה עבור $plot:\[\tau \]$ מוגדר כך:

$plot:\[M = \left\langle {{D^M},{R_1}^M,...,{R_m}^M,{F^M}_1,...,{F_k}^M,{C_1}^M...,{C_l}^M} \right\rangle \]$

כאשר $plot:\[{D^M}\]$ הוא התחום, $plot:\[{R_i}^M\]$ הוא הפירוש של סימן היחס $plot:\[{R_i}\]$ במבנה $plot:\[M\]$ , $plot:\[{F_i}^M\]$ הוא הפירוש של סימן הפונקציה $plot:\[{F_i}\]$ במבנה $plot:\[M\]$ , $plot:\[{C_i}^M\]$ הוא הפירוש של סימן הקבוע $plot:\[{C_i}\]$ במבנה $plot:\[M\]$ .

דוגמא: $plot:\[\tau = \left\langle {{R_{2,0}},{F_{1,0}},{C_0},{C_1}} \right\rangle \]$ . $plot:\[{M_2} = \left\langle {P\left( A \right), \subseteq ,{\text{completion}},\phi ,A} \right\rangle ,{M_1} = \left\langle {\mathbb{N}, \leqslant , + 1,2,3} \right\rangle \]$ .

בהינתן מבנה עבור מילון $plot:\[\tau \]$ , נגדיר השמה $plot:\[z\]$ המתאימה למשתנים ערכים מהתחום:

$plot:\[z:\left\{ {{v_i}|i \in \mathbb{N}} \right\} \to {D^M}\]$

נגדיר הרחבה של ההשמה $plot:\[z\]$ , שתתאים לכל שם עצם $plot:\[t\]$ מעל המילון $plot:\[\tau \]$ איבר בתחום שיסומן $plot:\[\bar z\left( t \right)\]$ .

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

בסיס: $plot:\[t\]$ משתנה $plot:\[\bar z\left( t \right) = z\left( t \right) \Leftarrow \]$ . $plot:\[t\]$ קבוע $plot:\[\bar z\left( {{c_i}} \right) = {c_i}^M \Leftarrow t = {c_i} \Leftarrow \]$ .

סגור: $plot:\[\bar z\left( {{F_{n,\alpha }}\left( {{t_1},...,{t_n}} \right)} \right) = F_{n,\alpha }^M\left( {\bar z\left( {{t_1}} \right),...,\bar z\left( {{t_n}} \right)} \right)\]$ .

משתנים חופשיים וקשורים

$plot:\[\forall {v_1}{R_{2,0}}\left( {{v_1},{v_1}} \right)\]$ - כל האיברים בתחום הם ביחס עם עצמם.
$plot:\[{R_{2,0}}\left( {{v_1},{v_1}} \right)\]$ - $plot:\[{v_1}\]$ ביחס $plot:\[{R_{2,0}}\]$ עם עצמו.

בדוגמא הראשונה אין צורך לדעת מה הערך של $plot:\[{v_1}\]$ בהשמה, ובנוסחה השניה כן. בנוסחה הראשונה $plot:\[{v_1}\]$ מופיע קשור (תחת השפעת הכמת), לכן הוא אינו מופיע בתרגום הנוסחה למילים ואין צורך לדעת את הערך שההשמה נתנה לו. בנוסחה השניה $plot:\[{v_1}\]$ חופשי.

טענה: תהי $plot:\[\alpha \]$ נוסחה מעל מילון $plot:\[\tau \]$ ו- $plot:\[M\]$ מבנה עבור $plot:\[\tau \]$ . אם $plot:\[{z_1}\]$ ו- $plot:\[{z_2}\]$ השמות ב- $plot:\[M\]$ המזדהות על המשתנים החופשיים ב- $plot:\[\alpha \]$ , אז ערך האמת של $plot:\[\alpha \]$ תחת $plot:\[{z_1}\]$ ותחת $plot:\[{z_2}\]$ זהה.

מסקנה: אם $plot:\[\alpha \]$ נוסחה ללא משתנים חופשיים, אז ערך האמת של $plot:\[\alpha \]$ אינו תלוי בהשמה.

הגדרה: נוסחה $plot:\[\alpha \]$ בלי משתנים חופשיים נקראת פסוק.

הגדרה פורמלית: נגדיר באינדוקציה על מבנה הנוסחה $plot:\[\alpha \]$ מתי $plot:\[{v_i}\]$ הוא משתנה חופשי ב- $plot:\[\alpha \]$ .

בסיס: נוסחאות אטומיות: $plot:\[{v_i}\]$ חופשי ב- $plot:\[\alpha \]$ אם $plot:\[{v_i}\]$ מופיע ב- $plot:\[\alpha \]$ .

סגור: קשרים: עבור $plot:\[ \circ \in \left\{ { \wedge , \vee , \to } \right\}\]$ , $plot:\[{v_i}\]$ חופשי ב- $plot:\[\left( {\alpha \circ \beta } \right)\]$ אם $plot:\[{v_i}\]$ חופשי ב- $plot:\[\alpha \]$ או $plot:\[{v_i}\]$ חופשי ב- $plot:\[\beta \]$ .

$plot:\[{v_i}\]$ חופשי ב- $plot:\[\left( {\neg \alpha } \right)\]$ אם $plot:\[{v_i}\]$ חופשי ב- $plot:\[\alpha \]$ .

כמתים: $plot:\[{v_i}\]$ חופשי ב- $plot:\[\forall {v_j}\alpha \]$ או ב- $plot:\[\exists {v_j}\alpha \]$ אם $plot:\[{v_i}\]$ חופשי ב- $plot:\[\alpha \]$ וגם $plot:\[i \ne j\]$ .

משתנה שאינו חופשי נקרא משתנה קשור.

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

הגדרת מבנה: בהינתן מילון $plot:\[\tau \]$ : $plot:\[\tau = \left\langle {{R_1},...,{R_m},{F_1},...,{F_k},{C_1},...,{C_l}} \right\rangle \]$ מבנה עבור $plot:\[\tau \]$ הוא:

$plot:\[M = \left\langle {{D^M},{R_1}^M,...,{R_m}^M,{F^M}_1,...,{F_k}^M,{C_1}^M...,{C_l}^M} \right\rangle \]$

כאשר $plot:\[{D^M}\]$ הוא התחום.

לכל $plot:\[1 \leqslant i \leqslant m\]$ אם $plot:\[{R_i}\]$ הוא סימן יחס $plot:\[n\]$ -מקומי אזי $plot:\[R_i^M \subseteq \underbrace {{D^M} \times ... \times {D^M}}_{n{\text{ times}}}\]$ , כלומר $plot:\[R_i^M\]$ הוא יחס $plot:\[n\]$ -מקומי מעל $plot:\[{D^M}\]$ .
לכל $plot:\[1 \leqslant i \leqslant k\]$ אם $plot:\[{F_i}\]$ סימן פונקציה $plot:\[n\]$ -מקומי אז $plot:\[F_i^M:\underbrace {{D^M} \times ... \times {D^M}}_{n{\text{ times}}} \to {D^M}\]$ , כלומר $plot:\[F_i^M\]$ מתארת מה הערך של $plot:\[{F_i}\]$ עבור כל $plot:\[n\]$ -יה סדורה של איברים מ- $plot:\[{D^M}\]$ .
לכל $plot:\[1 \leqslant i \leqslant l\]$ , מתקיים: $plot:\[C_i^M \in {D^M}\]$ .

ראינו כיצד בהינתן מבנה M מגדירים השמה $plot:\[z\]$ ב- $plot:\[M\]$ : $plot:\[z:\left\{ {{v_i}|i \in \mathbb{N}} \right\} \to {D^M}\]$ וראינו כיצד להרחיב את $plot:\[z\]$ כך שתתאים ערך מהתחום לכל שם עצם.

בהינתן נוסחה $plot:\[\alpha \]$ מעל מילון $plot:\[\tau \]$ , מבנה $plot:\[M\]$ והשמה $plot:\[z\]$ עבור $plot:\[M\]$ נסמן $plot:\[M\mathop \vDash \limits_z \alpha \]$ את הטענה ש- $plot:\[\alpha \]$ מסתפקת ב- $plot:\[M\]$ תחת $plot:\[z\]$ .

הגדרת ערך האמת: נגדיר באינדוקציה על מבנה $plot:\[\alpha \]$ מתי $plot:\[M\mathop \vDash \limits_z \alpha \]$ .

בסיס: $plot:\[\alpha \]$ נוסחה אטומית: $plot:\[\alpha = \left( {{t_1} \approx {t_2}} \right)\]$ עבור $plot:\[{t_1},{t_2}\]$ שמות עצם, $plot:\[M\mathop \vDash \limits_z \alpha \Leftrightarrow \bar z\left( {{t_1}} \right) = \bar z\left( {{t_2}} \right)\]$ .

כמו כן כאשר $plot:\[\alpha = R\left( {{t_1},...,{t_n}} \right)\]$ , עבור $plot:\[{t_1},...,{t_n}\]$ שמות עצם, $plot:\[M\mathop \vDash \limits_z \alpha \Leftrightarrow \left( {\bar z\left( {{t_1}} \right),...,\bar z\left( {{t_n}} \right)} \right) \in {R^M}\]$ .

סגור:

קשרים: מחשבים את ערך האמת בעזר טבלאות האמת. לכל נוסחה $plot:\[\alpha \]$ , מבנה $plot:\[M\]$ והשמה $plot:\[z\]$ , מתקיים כי $plot:\[M\mathop \vDash \limits_z \alpha \]$ או $plot:\[M\mathop \vDash \limits_z \neg \alpha \]$ אבל לא שניהם.
כמתים: נניח שלכל מבנה $plot:\[M'\]$ והשמה $plot:\[z'\]$ אנו יודעים האם $plot:\[M'\mathop \vDash \limits_{z'} \alpha \]$ . נרצה לדעת האם $plot:\[M\mathop \vDash \limits_z \forall {v_i}\alpha \]$ , $plot:\[M\mathop \vDash \limits_z \exists {v_i}\alpha \]$ למבנה והשמה מסויימים. בהינתן השמה $plot:\[z\]$ , משתנה $plot:\[{v_i}\]$ ואיבר $plot:\[d \in {D^M}\]$ , נגדיר השמה מתוקנת $plot:\[z\left[ {{v_i} \leftarrow d} \right]\]$ :

$plot:\[z\left[ {{v_i} \leftarrow d} \right]\left( {{v_j}} \right) = \left\{ {\begin{array}{*{20}{c}} {z\left( {{v_j}} \right)} \hfill & {i \ne j} \hfill \\ d \hfill & {i = j} \hfill \\ \end{array} } \right.\]$

נגדיר: לכל $plot:\[d \in {D^M}\]$ מתקיים $plot:\[M\mathop \vDash \limits_z \forall {v_i}\alpha \Leftrightarrow M\mathop \vDash \limits_{z\left[ {{v_i} \leftarrow d} \right]} \alpha \]$ .

קיים $plot:\[d \in {D^M}\]$ עבורו $plot:\[M\mathop \vDash \limits_z \exists {v_i}\alpha \Leftrightarrow M\mathop \vDash \limits_{z\left[ {{v_i} \leftarrow d} \right]} \alpha \]$ .