בתשובה לתוהה, 14/12/06 20:46
ההוכחה הזאת פשוט דבילית 424584
קח דוגמה בC:

void func(int c)
{
printf("%d\n", (getch() == 'a') ? c : 0);
}

משתמש בc או לא, זה תלוי בקלט. c אמנם מוזכר, אבל לא בהכרח משתמשים בו.
ההוכחה הזאת פשוט דבילית 424586
התוכנה משתמשת בו בתגובה לקלט מסוים = התוכנה משתמשת בו,
כנראה ששכחת שבעית העצירה שואלת אם התוכנה עוצרת בתגובה לקלט מסוים, לא בתגובה לכל קלט שהוא.
ההוכחה הזאת פשוט דבילית 424598
זה נכון. רציתי לתת דוגמה נגדית לדוגמה שלך בקשר לקומפיילר שיודע אם משתמשים במשתנה או לא -- הוא באמת לא יכול לדעת.
ההוכחה הזאת פשוט דבילית 424602
"הקומפיילר יודע שאתה לא משתמש במשתנה באותה משמעות שהוא יודע אם האות A נמצאת או לא נמצאת בקוד שכתבת"

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

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

אם אתה מעדיף לשאול את המרצה בקורס, אני הכתובת. באופן כללי, התשובה שלי תהיה: "תשאל את גדי, הוא יודע בדיוק על מה הוא מדבר".
ההוכחה הזאת פשוט דבילית 424612
יופי, בקיצר, לך או לגדי יש הוכחה לזה?
ההוכחה הזאת פשוט דבילית 424616
אבל אין כאן בכלל מה להוכיח. התוכנית עשויה להשתמש במשתנה, ועשויה לא להשתמש במשתנה, בהתאם לקלט. תשובה שמבוססת על ראיית התוכנית בלבד ללא התחשבות בקלט תהיה שגויה ביחס לחלק מהקלטים, ונכונה בקשר לשאר. זה דומה לשאלה האם השערת הרצף (שהזכרתי במקום אחר בדיון) נכונה או לא נכונה - היא יכולה להיות שניהם, זה תלוי באקסיומות.

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

halt(machine m,machine_code u,input x)

if m = u return Error illigal input

else return true if machine stops on x, false otherwise.

בלתי אפשרי למימוש.
ההוכחה הזאת פשוט דבילית 424626
אני לא בטוח שאני מבין את התפקיד של u,m כאן. אתה משתמש בהם בצורה מפורשת רק בשורה השנייה. בשורה השלישית אתה מדבר על "machine" - מה זה? זה m? זה u? זה שניהם גם יחד? מה הם מייצגים?
ההוכחה הזאת פשוט דבילית 424628
טוב סליחה ננסח את זה בדיוק כמו שאתה נסחת (חשבתי שזה היה הניסוח המקורי ולא בדקתי)

halt (Machine m,Input I)

if m = I return Error in input

else return true if m stops on i, false otherwise
ההוכחה הזאת פשוט דבילית 424631
ראשית, שים לב שהאלגוריתם הזה לא פותר את בעיית העצירה. קיימים קלטים שעליהם הוא מחזיר פלט שגוי (למעשה, "Error in input" הוא בכלל לא פלט לגיטימי - אנחנו מצפים לקבל "כן" או "לא" כתשובה, ולא שום דבר אחר).

שנית, בוא נניח שקיים אלגוריתם כזה. אני אבנה אלגוריתם S שהולך ככה: הוא מקבל קלט שנסמן בתור M1, מגדיר בתור M את הקלט בלי התו האחרון שלו, ומחשב את
halt(M,M1)

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

עכשיו, איך יתנהג S על הקלט S1, כש-S1 הוא הקידוד של S ועוד התו "1" בסוף?
ההוכחה הזאת פשוט דבילית 424633
ממה התחלנו, אמרנו שאותי מענין אם אפשר לבנות תוכנה שתבדוק אם התוכנה שלי עוצרת על קלט מסוים, נניח שאפשר לבנות תוכנה כזאת במגבלה שאני לא יכול לתת לה בתור קלט את התוכנה עצמה, זה מספיק טוב (למעשה מדהים) בשבילי. אז כשמתיימרים להוכיח לי שאי אפשר לעשות את זה, וההוכחה היא שאם התוכנה שלי היא גם הקלט אז יש בעיות, זה בעיני סתם רמאות זולה - בעצם לא הוכחת שאי אפשר לעשות את מה שבאמת מענין אותי אם אפשר לעשות.

לגבי מה ששאלת, לא הבנתי מה הבעיה, מה שיוצא לנו מההגדרה שלך זה

S (S + 1)
M = S
if Halt(S,S+1) loop
else halt.

מה הבעיה פה? תהיה בדיקה אם
S
עוצר על
S + 1
ואם כן הוא לא יעצור, ואם לא הוא יעצור..
ההוכחה הזאת פשוט דבילית 424634
אה או קי סליחה הבנתי, טוב... אז נשנה את האלגוריתם ל

Halt(Machine M,Input I)
if M = I return Error
S = CallingAlgorithm(Halt)
S1 = CallintAlgorithmInput(S)
while S do
if S = M and S1 = I return Error
S = CallingAlgorithm(S)
end while
return true if M stops on I false otherwise

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

מה זה "CallingAlgorithm"? לי נראה שאתה חושב כאן במונחים של תכנות, לא של מכונות טיורינג. בפרט, אתה מניח שיש מעין מחסנית קריאות או משהו דומה, ולכן אפשר לדעת מה האלגוריתם שקרא לך. במכונות טיורינג זה לא הולך ככה - האלגוריתם S לא "קורא" לאלגוריתם Halt (אם הוא היה עושה את זה, חלק מהקלט ל-Halt - במובלע - היה משתנה נוסף, שמכיל את זהות האלגוריתם הקורא) - הוא פשוט מבצע אותו. תחשוב על זה כאילו העתיקו את כל הקוד של Halt לתוך S (כמו inline ב-++C).

אבל חוץ מכל זה, אני מודה שאני לא ממש מבין את האלגוריתם שאתה מציג. בפרט, מה עושה השורה
S = CallingAlgorithm(S)
? זה נראה כאילו אתה מנסה לעלות מעלה במחסנית הקריאות - אבל הרי אין שם כלום (כי אף אחד לא באמת "קורא" ל-S). גם התנאי

while S do

לא ברור לי, הרי S הוא לא משתנה בוליאני. אתה מניח ש-CallingAlgorithm מחזיר 0 כשהוא מגיע לסוף מחסנית הקריאות? אם כן, בכל הלולאה אין טעם, כי היא תעצור אחרי הפעם הראשונה.

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

------
השלב הבא שלך כנראה יהיה זה: תגיד "אוקיי, אז אני מעוניין שתוכיח לי שלא קיים אלגוריתם שמקבל: א) את המכונה שקראה לו. ב) את הקלט שעליו המכונה הזו נקראה. ג) את המכונה שהוא צריך לבדוק. ד) את הקלט שעליו צריך לבדוק את המכונה הזו". אז תיכנס לתמונה בעיה נוספת - שני הקלטים הראשונים, כאמור, יכולים להיות מועברים רק על ידי מכונת הטיורינג הקוראת (הם לא נוצרים בצורה אוטומטית). את המכונה הזו אף אחד לא מכריח להעביר את הקלטים ש*לדעת Halt* צריכים להיות שם - היא יכולה להעביר מה שבא לה. מכיוון ש-Halt לא יכול לדעת אם שיקרו לו או לא, הוא תמיד חייב לענות כאילו לא שיקרו לו, ולכן כל הבדיקה לא אפקטיבית.
ההוכחה הזאת פשוט דבילית 424644
זאת היתה הפשטה (פסוודו קוד) אם תרצה אכתוב קוד יותר מדויק, אין בעיה לעשות את זה, אבל זאת לא הפואנטה, הפואנטה היא שמחשב אמיתי כן יכול לעבור על כל הפונקציות שקראו לפונקציה HALT עד לפונקציה הראשית (main) וככה לבדוק שאתה לא מנסה לרמות אותו עם הטריק הזה.

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

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

לכן אין ממש טעם בכל הדיון הזה. אם כל מה שמעניין אותך הוא תוכניות מחשב "אמיתיות", הדיון הזה לא בשבילך. כדי שהוא יעניין אותך, אולי כדאי לעבור לבעייה של Wang tiling - במקרה שלה הרבה יותר ברור עד כמה לומר "טוב, לא נשאל על ריצוף אינסופי אלא על ריצוף של שטח סופי" מוציא את העוקץ מכל העניין.
ההוכחה הזאת פשוט דבילית 424649
תראה אתה זה שטענת במאמר שאף מחשב שקיים או שיהיה קיים אי פעם לא יוכל לפתור את הבעיה הזאת, כלומר דברת לא סתם על מחשב ספציפי, אלא על האמאמא של המחשבים הספציפיים (כל מחשב ספציפי שאי פעם יתקיים) אז הבעיה היא ברעש שאתה עושה, שמטעה אנשים (אפילו כאלה שמתכנתים לפרנסתם שלא לדבר על סתם תמימים..) שאתה באמת מוכיח כאן מגבלה של המחשבים שהם מכירים בעולם (או שיכירו בעתיד) ולא סתם מתפלסף..
ההוכחה הזאת פשוט דבילית 424650
מה שטענתי אכן נכון; אף מחשב שקיים או שיהיה לא יכול לפתור את הבעיה הזו. הוא *כן* יכול לפתור בעיות שדומות לה אבל פשוטות יותר, כמו זו שהצגת.

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

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

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

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

אם אתה מתעניין בעיקר בצד המעשי, אני משער שכדאי לך להמתין עד אשר (ואם) יפורסם המאמר שעוסק בהבדל שבין ניתן לחישוב יעיל, ובין לא ניתן לחישוב יעיל - שם הגישה הננקטת היא דווקא גישת בית הלל (גם דברים שמעשית יהיה מאוד קשה לחשב עשויים להיחשב ל''קלים לחישוב'').
ההוכחה הזאת פשוט דבילית 424658
אין הבדל, ברור שאין תשובה לשאלה אם תוכנה עוצרת או לא עוצרת כשאתה מרשה לה לעצור או לא לעצור בהתאם לתשובה...
ההוכחה הזאת פשוט דבילית 424660
כאן הטעות שלך. יש תשובה לשאלה, אלא שהתוכנה לא מסוגלת לחשב אותה בעצמה.
ההוכחה הזאת פשוט דבילית 424661
זה לא מדויק, התוכנה יודעת לחשב אותה היא פשוט אומרת ההיפך ממה שקורה.. (אז אתה יכול לקרוא לזה חישוב ברברס..)
ההוכחה הזאת פשוט דבילית 424664
לא. מכיוון שההוכחה מראה שאין Q שפותר את הבעיה, התוכנה לא יודעת לחשב את זה. זכור שיצאנו מתוך גישה של הנחה בשלילה.
ההוכחה הזאת פשוט דבילית 424666
אז הגענו לשלב שבו הראנו שאם יש Q כזה ואנחנו מרשים לתוכנה לשאול את זה על עצמה אז יש אופציה ליצור "באג" שבו התוכנה תגיד שהיא לא עוצרת כשהיא כן עוצרת, ושהיא עוצרת כשהיא לא עוצרת. הוכחנו גם שאין אפשרות לתקן את הבאג (שיווצר רק כשישאלו את התוכנה על עצמה ולא כשישאלו אותה על אחרות) האופציה היחידה תהיה להוציא הודעת שגיאה על קלט לא חוקי, דבר אחד לא הוכחנו וזה שאי אפשר לבנות את Q.
ההוכחה הזאת פשוט דבילית 424670
זה לא "באג". זו סתירה, שמראה ש-Q פשוט לא עושה את מה שהנחנו שהיא עושה.

אני חושב שהדיון הזה מיצה את עצמו - אין לי חשק להתחיל דיון 1571 חדש.
ההוכחה הזאת פשוט דבילית 424678
או, הללויה.

באמת תהיתי למה אתה עד פעם מתוכח עם טרחן שלא מבין טענות לפני שהוא מתוכח איתן. המר בחור לא מבין הוכחה פשוטה של reduction ad absurdum וחושב שמדובר בטריקים "דבילים" ולא מעניינים. זה הרגע לשלוח אותו לקורס בלוגיקה בסיסית, לא לנהל איתו דיון.
ההוכחה הזאת פשוט דבילית 424683
הרבה יותר קל לא לנהל דיון מלחשוב שאולי משהו דפוק אצלך
ההוכחה הזאת פשוט דבילית 424693
דיון ניתן לא לנהל גם ע''י כתיבת המון מלל.
ההוכחה הזאת פשוט דבילית 424685
בקורס ללוגיקה כבר הייתי, תודה. גם הוכחות כאלו ראיתי לא מעט, ההבדל הוא שהן אף פעם לא טענו שמשתמע מהן יותר ממה שהוכיחו מהן.

לצערי אתה לא הבנת כל כך את הדיון, בעצם היתה פחות או יותר הסכמה שלא ממש מצליחים להוכיח את מה שמשתמע (גם עבור אנשים כמוך מסתבר), אלא משהו שולי בהרבה מבחינה מעשית (ייתכן שמשמעותי מאוד מבחינה פילוסופית, בעיני לא אבל אני לא פילוסוף). מכיוון שהוסכם שמדובר בהתפלספות ניסיתי בסוף קצת להתפלסף איתה בחזרה כדי להראות שלמקל יש 2 קצוות, אבל אני לא מתכוון לגרור אנשים לדיונים שאין להם ענין בהם (אפילו אם רגע לפני זה הם טענו שזה בעיקר מה שמענין אותם ולא הקטע המעשי) אז נראה שנפסיק כאן.
ההוכחה הזאת פשוט דבילית 424687
לא הוסכם שמדובר ב''התפלספות''. העולם לא מתחלק לשני סוגי בחינות - מעשית ו''פילוסופית''.
ההוכחה הזאת פשוט דבילית 424689
נשגב מבינתי איפה הוכחת שבדיקות לא יכולות לעקוף את הטריק, להיפך אמרת שאפשר לפתור את הבעיה ככה רק שזאת לא אותה הבעיה אלא בעיה יותר קלה, אז בסדר, אותי מענינת הבעיה המעשית של אם תוכנה תוכל לבדוק לי את התוכנה שלי ולראות אם היא הולכת להתקע ואותך כנראה מענינים יותר פרדוקסים לוגיים בסגנון השקרן, כנראה בגלל זה אתה מצליח להסכים ולא להסכים בעת ובעונה אחת לפי משב הרוח.

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

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

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

אבל זה מיצה את עצמו.
מה, פה זה slashdot? 424690
שאלות כמו הקשר בין מדעי המחשב לבין תכנות מעשי הן אכן שאלות מעניינות (אותי לפחות). לנהל אותן ע"י התחרבשויות רטוריות, רעש, צלצולים והתלהמויות לא נחוצות כמו "ההוכחה הזאת פשוט דבילית" או "אתה חייב לעשות לך מנהג ולהפסיק לקשקש" זה כבר סיפור אחר ואלה הדגלים הראשונים שמציינים שבעצם מדברים עם טרחן. הדגלים הנוספים הם שמתקבל הרושם שהוא לא ממש סגור על מה הוא כן מנסה לטעון.

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

הלהט הריגשי בדיון בו ניתן לברר יחדיו אם טענה היא נכונה, לא נכונה או שלא ניתן לענות עליה (כרגע או בכלל), הוא מאוד מוזר בעיני.
מה, פה זה slashdot? 424692
הסיבה ללהט הרגשי הוא ששמעתי על ה''הוכחה'' הזאת לפני שראיתי אותה והדבר הזה עשה עלי רושם מאוד חזק וגרם לי לחשוב הרבה על המשמעויות שלו וגם להתלהב מאוד מהעובדה שאפשר להוכיח כזה דבר (כמו שחשבתי שהוכיחו) כגודל הציפיה כך גם גודל האכזבה שהיתה לי כשלמדתי אותה, למרות שעברו כמה שנים מאז, התחושה המאוד חזקה שהיתה לי אז, תחושה שרימו אותי, חוזרת כל פעם שאני שומע עליה שוב ולכן הרגשיות שבה אני מנהל את הדיון עליה.
Reset 424696
אז נשים את תחושות העלבון והרגשות רגע בצד, אם אפשר.

בקצרה, בפשטות ובדיוק, מה אתה טוען?
Reset 424709
כבר כתבתי, הבעיה היא אם אפשר למצוא אלגוריתם שיגיד אם אלגוריתם אחר עוצר על קלט מסוים, ההוכחה של טיורינג אומרת שלא מכיוון שאם האלגוריתם הזה יקבל כקלט את עצמו זה ייצור פרדוקס, אז אני אומר, או קי אז אסור לו לקבל את עצמו כקלט. עכשיו אפשר למצוא אלגוריתם כזה? מה שמענין באמת זה אם אפשר למצוא אלגוריתם, וההתחכמויות של אבל אם הוא יקבל את עצמו כקלט יהיה פרדוקס פחות מענינות. וכמו שנזכרתי לא מזמן, זה די דומה לפרדוקס ראסל, אחרי שמתמטיקאים שמעו עליו הם יכלו לזרוק את כל תורת הקבוצות כי היא יצרה פרדוקסים או להחליט שקבוצת ראסל היא קבוצה לא חוקית, נחש מה הם החליטו?
Reset 424715
רצית - קיבלת.
האלגוריתמים שלי מכיל משוואה דיופונטית פולינומיאלית ומחפש לה פיתרון בטבעיים ע''י השיטה המתוחכמת של ניחוש לא סדור. יכול להיות שימצא פתרון, יכול להיות שלא, בשום שלב לא ניתן להגיד שלא קיים פתרון (כי יש עוד מספרים שלא ניסינו). אם קיים אלגוריתם המסוגל לקבוע האם התוכנה עוצרת, אזי הוא פתר את השאלה האם קיים פתרון בטבעיים עבור המשוואה הנתונה, מה שסותר הוכחה הרבה יותר ''מתמטית'' מבחינתך (כבר קישרו אליה בדיון הזה), הבעיה העשירית של הילברט.
Reset 424717
הבעיה האהובה עלי היא וריאציה על Wang tiling - נניח שיש לנו אוסף כלשהו של אבני כמו-טטריס (כלומר, כמו האבנים שיש בטטריס אבל יכולות להיות מכל גודל שהוא, לא רק 4), האם ניתן לרצף את המישור כולו באמצעות עותקים של איברים מהאוסף?

מתברר שגם אלגוריתם כללי לפתרון הבעיה הזו לא קיים.

(הרחבה על מה זה לעזאזל "אבן כמו-טטריס" - Polyomino [Wikipedia])
Reset 424807
במבט ראשון נדמה לי שאפשר לחלק את הבעיה לשני חלקים:
שיטה ראשונה לריצוף המישור - צור צורה הניתנת לגיבוש ‏1 באמצעות אבנים מהאוסף. אני מניח שבהינתן אוסף סופי של צורות אפשר להסיק האם קיימת צורה כזו (רק מניח, אין לי באמת את הכלים המתמטיים להתמודד עם הבעיה). אבל בעצם מי מבטיח לי שצורה אחת מספיקה, אולי דרושות כמה צורות כדי למלא את כל החללים (כמו כדורגל) ? היות ובניגוד לצורה הראשונה אנחנו לא מחפשים מינימום מחזורי, אין שום סיבה לשים מגבלה על הגודל, מה שגורם לי לחפש מחזור שיכול להיות אינסופי (זה עלול לקחת קצת זמן).
שיטה שניה - מצא שיטה (או אולי לפעמים אפילו אין שיטה מסודרת) להמשיך להרכיב עוד ועוד צורות בלי רווחים עד אינסוף. אני מניח שכאן לב הבעיה.

אתה יכול לקשר לסקיצה של ההוכחה ?

1 שאפשר להמשיך אותה מכל צדדיה ביחידות חוזרניות מבלי להשאיר רווחים.

[אילו היו חמש דקות של נסיון להתמודד עם בעיה שאין לי את הכלים להתמודד איתה]
Reset 424823
אני לא בטוח מה אתה מנסה לעשות - לי זה נראה כאילו אתה מנסה דווקא לפתור את הבעיה. אם אתה מנסה להוכיח שהיא לא פתירה דרך גישת "בואו ננסה לפתור ונראה איפה אנחנו נתקעים", זו לא הדרך הנכונה.

להוכיח שאין אלגוריתם למציאת ריצוף על ידי אבני "כמו-טטריס" זה לא כל כך קשה אם כבר יש לך הוכחה שאין ריצוף על ידי Wang tiling - פשוט עושים רדוקציה (כלומר, מראים דרך לתרגם בעיית ריצוף עם Wang tiles לבעיית ריצוף עם "כמו-טטריס"). זה תרגיל נחמד לחשוב איך אפשר לעשות את זה - ואני בטוח שיש כמה דרכים (הדרך שאני חשבתי עליה טיפה שונה מהדרך שבה הוכיחו את זה לראשונה, אבל בשורה התחתונה זה אותו הדבר).

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

Berger, R. (1966). "The undecidability of the domino problem", Memoirs Amer. Math. Soc. 66(1966).

והרעיון הוא רדוקציה מבעיית הכרעה במכונות טיורינג (אם איני טועה, ממש מבעיית העצירה עצמה). אם היא זמינה לך, אתה יכול גם להעיף מבט בחוברת של קורס החישוביות של הטכניון, שנכתבה על ידי עודד גולדרייך - הוא מדגים שם משהו כמעט זהה.
Reset 424858
נדמה לי שהם מרחיקים טיפה מעבר לבעיה שהגדרת, אבל העקרון דומה.
Reset 424719
ואולי יהיה לך אלגוריתם שידע להגיד כן/לא בכל מקרה שניתן לכתוב אלגוריתם, ו"אני לא יכול לדעת" במקרים האחרים?
Reset 424720
תרגום טענת התוהה:
קיימת מ"ט H כך שבהניתן כל קידוד של מ"ט <M> (כך ש- M שונה מ-H) וקלט K, אז H מכריעה אם M עוצרת על K.

זו הטענה?
Reset 424721
הניסוח שלך יצא לא לגמרי מדויק, תזכר בניסוח המקורי (הקלט הוא המכונה M)

בכל מקרה, לא טענתי שהיא קיימת, כל מה שטענתי זה שההוכחה שהובאה במאמר, לא מוכיחה שהיא לא קיימת.

ברור כמו שאמרו פה שמכונה שתוכל לעשות את זה אבסולוטית (וגם להגיד מתי אי אפשר לדעת, בעקבות ההערה של קהלת) תהיה בעצם סוג של גאון מתמטי, אז אני באמת בספק אם אפשר (מעשית) לנסח אלגוריתם שבעצם יבטא את מהות החשיבה המתמטית. למרות שזה מענין תאורטית, וגם מעשית כמה אפשר להתקרב לזה.
Reset 424722
אאל''ט, הניסוח שלי, בניגוד לאלה שלך, הוא מדויק וחד משמעי. אתה אולי מתכוון שלא בדיוק לכך התכוונת. נסח בבקשה בשפה הנ''ל את הטענה שלך, כך שהיא תהיה טענה מדויקת ואז נמשיך משם.
Reset 424723
באיזה שפה אתה רוצה שאני אנסח לך את המילים ההוכחה שמופיעה במאמר לא מוכיחה שאלגוריתם לא קיים? (נתתי פסוודו קוד די מדויק של האלגוריתם שאליו אני מתכוון, דפדף קצת למעלה)
Reset 424754
בשפה חד משמעית, בדיוק כמו שאני ניסחתי טענה. זה לא קשה, זה פשוט עלול לעזור לנו להחליט אם מה שאתה טוען הוא נכון או לא ולכן אתה נזהר. ''די מדויק'' (שזה אותו דבר כמו ''לא מדויק'') זה לא מספיק בשביל לנהל דיון בנושא.

תקעת את הדגל השדמי השלישי והאחרון (יצירת לולאה אינסופית בדיון ע''י הפניה לתגובה קודמת שכתבת ושאליה כבר התיחסו, במקום לענות במשפט אחד תשובה פשוטה ומדויקת לבקשה פשוטה ומדויקת).
שדמית 101 424755
מה השניים הראשונים?
שדמית 101 424763
1) הפרובוקציה.
שלב גיוס הקהל: האביר שמעיז למוטט את מגדל הקלפים.

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

2) ריקוד השדים.
שלב ההתחרבשויות, ההתעקשויות, גסות הרוח והתיקונים העצמיים הבלתי נגמרים.

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

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

3) ה-LOOP.
הרעבת השדים וסגירת המעגל.

אם מנסים לנטרל את הרעש הלבן, להמנע מהמלכודת שהיא הרטוריקה והשפה הטבעית ולתקשר רק ברמת הטענות החד משמעיות שמשתמשות במושגים החד משמעיים בתחום, מקבלים מייד הפניות לתגובות קודמות בדיון הארוך, במקום תשובה קצרה וחד משמעית.
Reset 424756
טוב אתה רשאי לפרוש
Reset 424724
אפשר לצאת מהשאלה של התוהה ולהגיע לשאלה "מעניינת". למשל, נניח שאנו מסתכלים על קבוצת כל המ"ט הקיימות ועל כל הקלטים שאורכם קטן מאורך נתון כלשהו (X תווים). האם אז קיים אלגוריתם שפותר את בעיית העצירה? (שימו לב שלא הגבלתי את אורך התכנית אלא את אורך הקלט).
הסיבה שהשאלה הזאת נראית מעניינת בעיני היא שאז באמת ההוכחה של טיורינג לא עובדת (נראה לי) כי הקלט לא יכול להיות זהה או שקול לתוכנה.
Reset 424725
אפשר להראות משהו הרבה יותר חזק: אפילו לגבי הקלט 0 בלבד אי אפשר להכריע באופן כללי אם M עוצרת עליו או לא.

למה? בוא נניח שאפשר (יש אלגוריתם Q שעושה את זה), אז אני אראה לך איך לפתור את בעיית העצירה. אתה נותן לי M וקלט x, ואני בונה מכונה חדשה, M_x, שמה שהיא עושה הוא זה: היא *מתעלמת* מהקלט שלה, ובמקום זה כותבת את x על סרט הקלט, חוזרת לתחילתו, ומכאן ואילך מתנהגת כמו M. כלומר, M_x היא פשוט דרך להריץ את M על x בלי ש-x יתקבל כקלט.

עכשיו, ברור ש-M_x עוצרת על 0 (או כל קלט אחר) אם ורק אם M עוצרת על x. אז פשוט נחזיר את התשובה ש-Q מחזיר - פתרנו את בעית העצירה.
Reset 424903
זה רעיון מעניין, אם אתה יכול להמשיך איתו. לא סתם החליטו שקבוצת ראסל היא לא-חוקית, אלא החליפו את הגדרת הקבוצה: לא עוד "אוסף של איברים", אלא הגדרה מפורטת של צרמלו-פרנקל מה זה קבוצה ומה זה לא. אתה יכול למצוא הגדרה אלטרנטיבית ומצומצמת יותר ממכונת-טיורינג לתוכנה?
Reset 424907
לא חסרות כאלו; יש המוני סוגים שונים ומשונים של מכונות טיורינג עם מגבלות עליהן. מגבלה שכבר ציינתי לא מעט בדיון היא מגבלה על הזיכרון; אם עבור מכונת טיורינג, הזיכרון המקסימלי שהיא משתמשת בו בריצה על קלט הוא פונקציה (ניתנת לחישוב) של גודל הקלט, אפשר לפתור את בעיית העצירה עבור המכונה הזו.
שואל ועונה 424914
הבעיה שהצגתי קודם (חיפוש פתרון למשוואה) משתמשת בכמות סופית של זיכרון (אין צורך לזכור פתרונות קודמים, פחות יעיל אבל עדין עובד), איך מיישבים את הסתירה ?
ראוי לציין שהמכונה שלי משתמשת ביכולת להגריל מספרים אקראיים, תכונה שלא באמת קיימת במ"ט (בעצם אפשר לראות בזה הוכחה לכך שמ"ט לעולם לא תוכל להגריל מספרים אקראיים)
שואל ועונה 424918
בעצם טעיתי. הגבלה על גודל הזיכרון מגבילה את גודל המספר המנוחש.
שואל ועונה 424934
...ובעיקר את אורכו.
שואל ועונה 424958
כבר ענית היטב לעצמך. רק הערה קטנה: לא קשה להוכיח שגם מכונת טיורינג *אי דטרמיניסטית* (מושג שעליו ארחיב, אם בכלל, במאמר המשך למאמר ההמשך) לא חזקה יותר ממכונת טיורינג רגילה - ואי דטרמיניזם, מבחינה רעיונית, הוא יותר חזק מאקראיות "סתם" (אם כי זה לא כל כך פשוט - במכונות אקראיות מרשים לפעמים למכונה לטעות - ובפרט, יש מכונה אקראית שפותרת את בעיית העצירה בהסתברות 1/2).
שואל ועונה 424959
מחכה בקוצר רוח.
מה, פה זה slashdot? 424838
עד שכתבת "למרות שעברו כמה שנים מאז" חשבתי שאתה בן שמונה עשרה וקצת, בוגר מצטיין של קורס תכנות, בעל נסיון ביישום אי אילו אלגוריתמים לא טריויאליים (כולל quicksort עם הקצאה דינמית של זכרון, יה, יה) ומרגיש שהעולם בקצות אצבעותיו. חשבתי אפילו לתת לך עצה קטנה ממרום גילי, בקשר לכותרות מסוג "ההוכחה הזאת היא דבילית": כאשר ההוכחה מקובלת על המון אנשים בלתי דבילים בעליל, הסיכוי שכולם טועים באופן טריויאלי בלי לשים לב למה שנראה לך ברור מאליו - הסיכוי הזה לא גדול במיוחד. זה לא אומר, חלילה, שצריך לקבל את דבריהם בלי הרהור וערעור, אבל כדאי לצאת מההנחה ש*אתה* לא מבין כאן משהו יסודי, לא שכל האחרים דבילים, ולנסות לברר מה באמת הולך כאן. כאשר בוחרים בסגנון שלך, רוב הסיכויים הם שיתברר שבדיון הזה הדביליות היא לא בהוכחה.

אבל מה? מסתבר שאתה לא כל-כך צעיר, כך שאם לא למדת את זה עד היום כנראה גם לא תלמד. בהצלחה בסטארט-אפ.
מה, פה זה slashdot? 424863
התכוונת בהצלחה בסטנד-אפ.
מה, פה זה slashdot? 424842
לא הבנתי. ממה התאכזבת?
ההוכחה הזאת פשוט דבילית 424999
הנה שאלה ש(עוד) לא מיצתה את עצמה: הוכח שאי אפשר להכריע את בעית העצירה בקבוצת כל מ"ט שלא מקבלות קלט.
ההוכחה הזאת פשוט דבילית 425003
זה דומה למשהו שכבר אמרתי במקום אחר: נניח שאנחנו רוצים לפתור את בעית העצירה עבור מכונה M וקלט x, ויש לנו Q שמכריע אותה עבור מכונות שלא מקבלות קלט. אני בונה מכונה Mx שלא מקבלת קלט ומה שהיא עושה הוא לכתוב על הסרט שלה את x ואז להריץ את M, ומעביר אותה ל-Q.

אבל הרדוקציה הפרטנית הזו די מיותרת, כי משפט רייס (שלא הוזכר במאמר) כולל גם את המקרה הזה.
ההוכחה הזאת פשוט דבילית 425005
תמיד יש את הבעיה הזו כשמשלימים דיונים עם עשרות+ תגובות: או שתגיב ותחרמופף או שתקרא קודם את הכל ותשכח על מה רצית להגיב.
ההוכחה הזאת פשוט דבילית 424900
אבל התוהה,
"אם מישהו שטוען שהוא תמיד משקר משקר", מקרה הידוע בשם פרדוקס השקרן, זהו לב ההוכחה של אי היכולת לפתור את בעית העצירה.

התוכנית שגדי הציג עוצרת (משקרת) אם היא לא עוצרת (אומרת אמת) ולהפך.

האם נסכים לסכם גם כאן בוואלה?
ההוכחה הזאת פשוט דבילית 424651
מקריאת תגובותיך נראה לי שאינך עומד על ההבדל המהותי בין מדעי המחשב לבין תיכנות מעשי על כל הישומים המסחריים שלו. כמו שמישהו (פון ניומן ?) פעם ניסח זאת - "מחשבים קשורים למדעי המחשב כמו שטלסקופ קשור לאסטרונומיה".
ההוכחה הזאת פשוט דבילית 424656
אדסחר דייקסטרה:

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

אלגוריתם יאללה_בלאגן
א. N=4
ב. בדוק האם N הוא סכום של שני מספרים ראשוניים.
ג. אם כן:
ג1. N=N+2
ג2. חזור לשלב ב.
ד. אם לא: הדפס "השערת גולבך שגויה" וסיים.

שים לב, יאללה_באלגן בודק את השערת גולדבך (כל מס' זוגי גדול מ 2 הוא סכום של שני ראשוניים). אם ההשערה נכונה (ואף אחד לא הצליח עדיין להוכיח או להפריך את זה), יאללה_באלגן לעולם לא יעצור. כך, שאם אתה מצליח להריץ את התוכנית שלך ו*לקבל תשובה נכונה*, פתרת את אחת הבעיות הקשות במתמטיקה. כל מה שנשאר הוא להראות את התשובה למתמטיקאי, ואז אתה תהיה אדם עשיר ומפורסם (בהנתן, כמובן, שלא תמות בשיבה טובה לפני שהתוכנית שלך תחזיר תשובה).

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

זה אגב מעלה שאלה מעניינת (בעיניי). האם במדעי המחשב מוצאים לפעמים הוכחות לא-קונסטרוקטיביות לקיומם של אלגוריתמים?
ההוכחה הזאת פשוט דבילית 424772
התוהה הביא אלגוריתם שפותר את בעיית העצירה. אם כך, זה ממש בקטנה בשבילו להביא אלגוריתם שבודק מקרה פרטי מאד: האם יאללה_בלאגן עוצר. בתור התחלה, הוא יכול להביא את האלגוריתם הכללי שלו.

נראה לי שאולי ע"י מקרה פרטי, יהיה אפשר להמחיש לתוהה היכן הטעות שלו.
ההוכחה הזאת פשוט דבילית 424774
הוא לא הביא אלגוריתם כזה, אלא רק הציע שיטת ''שיפוץ'' לאלגוריתם אפשרי. יש בצורת הניסוח שלו בעיות פורמליות, אבל הרעיון הבסיסי דווקא לגיטימי (הוכחנו שאי אפשר לפתור את בעיית העצירה - הטוען תהה האם ניתן לפתור אותה עבור כל קלט שאינו ''המכונה הקוראת, הקלט של המכונה הקוראת'')
ההוכחה הזאת פשוט דבילית 424775
אני מקבל את התיקון. אבל למה שלא יתחיל במקרה הפרטי שלי? אם הוא לא רוצה להיות עשיר ומפורסם אני מוכן לקחת את העונש הזה על עצמי. שיעשה את זה רק בשביל האתגר.
ההוכחה הזאת פשוט דבילית 424776
אם הבנת למה הוא התכוון בדיוק, אתה מוכן לנסח במקומו את הטענה עם "התיקונים"? (אותך אני מבין)

מהי בדיוק "בעיית העצירה תג" עליה אנו מדברים? האם לא קל לבצע ממנה רדוקציה אל בעיית העצירה ה"רגילה"?
ההוכחה הזאת פשוט דבילית 424780
יותר משזו בעיה, זה "אתגר" - תוכיח לי שלא קיים אלגוריתם Q שפותר את בעית העצירה עם הקלטים M, x תחת ההנחה שאם אלגוריתם S כלשהו משתמש ב-Q הוא מעביר לו כקלט גם את המידע על עצמו ועל הקלט שהוא עצמו קיבל.

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

בהתחלה התוהה הציג גרסה פשוטה יותר של האתגר: להוכיח שלא ניתן לפתור את בעיית העצירה גם אם מגבילים את הקלטים להיות מהצורה M,x כאשר M שונה מ-x. אפשר להוכיח באופן ישיר שגם אלגוריתם לפתרון הבעיה הזו לא קיים (הראיתי איך קודם), אבל גם רדוקציה מבעיית העצירה לבעיה הזו (שים לב: לא בכיוון ההפוך) קל להדגים: אם קיבלת M ו-x תעביר אותם לאלגוריתם הפלאי אם M שונה מ-x. אחרת, שנה את M בצורה שתחזיר מכונה שקולה (למשל, תוסיף עוד מצב פנימי שלא מגיעים אליו אף פעם) ואז תעביר את הקלט לאלגוריתם הפלאי.
ההוכחה הזאת פשוט דבילית 424804
כן, כמובן שלא בכיוון ההפוך. אני קצת חלוד. תודה!
ההוכחה הזאת פשוט דבילית 424779
רעיונות דומים צצים מדי פעם גם לגבי משפט גדל (אולי אפשר להכריע כל טענה פרט לטענות השקולות ל"אני לא יכיחה"? או פרט לטענות מתייחסות-לעצמן? או פרט לטענות מתייחסות-לעצמן-בעקיפין?)

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

התשובה המתוחכמת יותר היא שכבר יש, בכל המקרים, דוגמאות מאוד קונקרטיות של בעיות הכרעה או עצירה וכו' שהן בלתי-פתירות. לדוגמה, אם נדון רק במכונות טיורינג המנסות לפתור משוואות דיופנטיות בדרך הפשוטה ביותר (לסרוק פתרונות אפשריים), גם את בעיית העצירה עבור היקום המאוד מצומצם הזה לא ניתן לפתור. זה כבר משפט הרבה יותר קשה, אבל הוא (מה לעשות) גם נכון, והוא בוודאי הרבה יותר חזק מהטענה הנדונה: התוהה מנסה לסלק רק את האלכסון (מכונה=קלט), ואילו כאן סילקנו את האלכסון ועוד הרבה יותר (כמעט את כל המכונות וכמעט את כל הקלטים), ואפילו זה לא מספיק.
ההוכחה הזאת פשוט דבילית 573906
Proving Program Termination, B. Cook et al., CACM v54 n5, May 2011

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

"In our new problem statement we will still require that a termination proving tool will always return answers that are correct, but we will not necessarily require an answer. If the termination prover cannot prove or disprove termination, it should return 'unknown."'
ההוכחה הזאת פשוט דבילית 581351
עוד לא קראתי את המאמר, אבל אני חושב שמתפספסת כאן נקודה (לא בהכרח במאמר אלא בפרשנות של מה זה אומר). אנחנו *לא רוצים* לשנות את בעיית העצירה כך שתהיה פתירה. יש לא מעט וריאציות שאפשר להציע על בעיית העצירה כך שתהיה פתירה, אבל אנחנו דווקא רוצים את הניסוח הלא פתיר. לא כי בעיית העצירה בפני עצמה כל כך מעניינת, אלא כי מה שנובע מאי הפתירות שלה (למשל, אי הפתירות של הבעיה העשירית של הילברט או של בעיית ריצופי וואנג) מעניין.

אגב, ה-

In contrast to popular belief, proving termination is not always impossible.

שמופיע בתחילת המאמר

קצת חצוף. אלו לא חדשות חדשות...

חזרה לעמוד הראשי המאמר המלא

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים