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

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

4.4.6.1. קבוצה מבוססת היטב

הגדרה: קבוצה מבוססת היטב (Well founded set) היא קבוצה עם יחס (יכול להיות חלקי) $plot:$\left( {W, > } \right)$$ שבה לא קיימת סדרה יורדת אינסופית. כלומר לא קיימת סדרה אינסופית $plot:${w_0},{w_1},{w_2},... \in W$$ כך שמתקיים $plot:${w_0} > {w_1} > {w_2} > {w_3}...$$ .

תזכורת:

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

דוגמאות לקבוצות מבוססות היטב:

$plot:$\left( {\mathbb{N}, > } \right)$$ כאשר המספרים הם המספרים בסדר הרגיל.
בהינתן קבוצה סופית ויחס הכלה, הקבוצה $plot:$\left( {p\left( A \right), \supset } \right)$$ הינה קבוצה מבוססת היטב.
$plot:$\left( {N \times N, > } \right)$$ - $plot:$\left( {n',m'} \right) > \left( {n,m} \right) \Leftrightarrow \left( {n' > m} \right) \vee \left( {n' = n \wedge m' > m} \right)$$ (יחס סדר לקסיקוגרפי) גם קבוצה מבוססת היטב.

לאחר שבחרנו זוג התחלתי $plot:$\left( {{n_0},{m_0}} \right)$$ נוכל אומנם לרדת ל $plot:$\left( {{n_0} - 1,{m_1}} \right)$$ כך ש $plot:${m_1}$$ גדול כרצוננו, אולם הוא עדין סופי, ולכן אפשר לשים לכל היותר $plot:${m_1}$$ איברים עד שנאלץ לרדת ל $plot:${n_0} - 2$$ וכך בסופו של דבר, הסדרה חייבת להיות סופית.

דוגמאות לקבוצות שאינן מבוססות היטב:

$plot:$\left( {{\mathbb{R}^ + }, > } \right)$$ - אינה קבוצה מבוססת היטב – למשל ניתן לבחור בסדרה: $plot:${r_1},\frac{{{r_1}}}{2},\frac{{{r_1}}}{4},...$$
$plot:$\left( {p\left( A \right), \supset } \right)$$ עבור אינסופית אינה קבוצה מבוססת היטב – למשל אם $plot:$A = \mathbb{N}$$ נבחר $plot:${A_0} = \mathbb{N},{A_{i > 0}} = {A_{i - 1}}\backslash \left\{ i \right\}$$