בתשובה לאינקוגניטו, 27/12/09 19:05
יש אמת מעבר למילים. 532229
א. לשפה קוראים רובי, ובאנגלית Ruby. תוכל למצוא פרטים נוספים ב: http://www.ruby-lang.org/ ר' גם http://tryruby.org/ .
למזלך הגדרתה (או לפחות המימוש הסטנדרטי שלה) לא סובלת מ־overflow של מספרים. בהרבה שפות מחשבים מקובלות, היית נופל כבר כאן.

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

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

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

ה. צודק, אני משועמם. אתה לא משועמם?
יש אמת מעבר למילים. 532231
ב. למעשה, ברובי אין פעולת ++.

ועכשיו שברתי את שיא הנטפוק האיילי של כל הזמנים.
יש אמת מעבר למילים. 532233
א. תודה
ב. מעולם לא ראיתי איך תוכנת רובי כתובה, אני משער שאם היא לא כתובה יותר מדי מוזר אני אדע להגיד אם היא נכונה וגם אם לא, לא מדובר שקשה מדי לכתוב גם באסמבלר.
ג. בסדר, זה לא כאילו ההוכחה הזאת באמת חשובה ( אני מניח שאתה לומד שn+1>n בתואר השני או משהו כזה).
ד. גם ההוכחה הרגילה שלכל מספר יש ריבוע היא די מסובכת אבל זה לא הענין.
ה. לנהל ויכוחים לא נגמרים עם תש"חיסט? כן. להוכיח שn+1>n בלי להשתמש בהנחת האינדוקציה? זה לא. גם לי יש גבולות.
יש אמת מעבר למילים. 532237
ב. לא נכון. לא ידוע אלגוריתם כללי לבדיקת נכונות של תוכנית

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

אתה מאמין למה שכתבתי כאן?

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

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

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

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

בינתיים הצלחת להעלות לא מעט טענות שנראו לך נכונות והתבררו כשגויות. אולי יש משהו בפורמליזם.
יש אמת מעבר למילים. 532249
א. לא כל תכנית, אבל את היישום של פלוס 1 אני כנראה אצליח לזהות. וחוץ מזה מדובר בבערך שלוש שורות באסמבל כך שאפילו אני יכול לכתוב את זה.
ג. גם לי נוח להסתמך על משפטים פורמליים, זה לא סותר את מה שאמרתי.
יש אמת מעבר למילים. 532250
א. זה רק מוריד את השאלה לרמת הפשטה נמוכה יותר. אתה מניח שהמימוש של המעבד נכון. אתה חושב שאתה מסוגל להבדיל בין שתי מכונות וירטואליות שבאחת מהן יש באג קטן המימוש של אותו קוד אסמבלי לבין מכונה אחרת שבה אין באג כזה? (בלי לדעת מראש מה שגוי).
יש אמת מעבר למילים. 532252
לא, אני לא יכול.
מצד שני אני לא מבין מה הנקודה שלך. אתה יודע כמה מאמרים יש שכל החישובים הסטטיסטיים נעשו על ידי מחשב? ומתוכם כמה נעשו על ידי אנשים ששפת התכנות היחידה שהם מכירים זה spss ?
גם הם לא יכולים להבדיל בין קוד נכון לשגוי, אז מה?
יש אמת מעבר למילים. 532256
הם מקווים לטוב.

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

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

אבל יש גם דרך יותר פשוטה: אני אפעיל את האלגוריתם הבא:

א. בקש מאינקוגניטו להראות את נכונות הטענה לגבי x
ב. טען: "ההוכחה לגבי המספרים עד x לא מספיקה לי - לא בדקת שהמחשב מחשבר נכון גם את הערך x+1".
ג. הגדל את x ב־1
ד. חזור ל־א'

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

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

לא כתבתי שיש לי הוכחה או שאני יכול למצוא אחת. אמרתי שאני *מבין* ש n+1>n. כל הנקודה שלי היא שיש דברים שאני יודע שהם נכונים גם בלי הוכחות.
יש אמת מעבר למילים. 532262
זה לא נכון תמיד בשעון שלי.

הבעיה היא שמתמטיקה (גם המעשית) זימנה לנו לא מעט תוצאות לא אינטואיטיביות.

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

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

#include <stdio.h>
int main() {
float f;
for (f=0; ; f++) { printf("%f\n", f); }
return 0; }

הפלט:

0.000000
1.000000
2.000000
...
16777214.000000
16777215.000000
16777216.000000
16777216.000000
16777216.000000

(וישאר תקוע על הערך הזה)

לפרטים נוספים:

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

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