|
||||
|
||||
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."'
|
|
||||
|
||||
עוד לא קראתי את המאמר, אבל אני חושב שמתפספסת כאן נקודה (לא בהכרח במאמר אלא בפרשנות של מה זה אומר). אנחנו *לא רוצים* לשנות את בעיית העצירה כך שתהיה פתירה. יש לא מעט וריאציות שאפשר להציע על בעיית העצירה כך שתהיה פתירה, אבל אנחנו דווקא רוצים את הניסוח הלא פתיר. לא כי בעיית העצירה בפני עצמה כל כך מעניינת, אלא כי מה שנובע מאי הפתירות שלה (למשל, אי הפתירות של הבעיה העשירית של הילברט או של בעיית ריצופי וואנג) מעניין. אגב, ה- In contrast to popular belief, proving termination is not always impossible. שמופיע בתחילת המאמרקצת חצוף. אלו לא חדשות חדשות... |
חזרה לעמוד הראשי | המאמר המלא |
מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
RSS מאמרים | כתבו למערכת | אודות האתר | טרם התעדכנת | ארכיון | חיפוש | עזרה | תנאי שימוש | © כל הזכויות שמורות |