מערכת מיזאר

מערכת מיזאר

פרדיגמות	תכנות הצהרתי
תאריך השקה	1973
מתכנן	אנדז'יי טריבולץ
הושפעה על ידי	Automath
mizar.uwb.edu.pl

מערכת מיזאר (בפולנית: System Mizar) מורכבת משפה פורמלית לכתיבת הגדרות והוכחות מתמטיות, יחד עם מסייע הוכחה (אנ'), המסוגל לבדוק הוכחות הכתובות בשפה זו, וספרייה של מתמטיקה פורמלית, שבה ניתן להשתמש בהוכחה של משפטים חדשים. המערכת מתוחזקת ומפותחת על ידי פרויקט מיזאר, בעבר בניהולו של מייסדו, אנדז'יי טריבולץ (Andrzej Trybulec).

בשנת 2009 הספרייה המתמטית של מיזאר הייתה הגוף הקוהרנטי הגדול ביותר של מתמטיקה פורמלית קפדנית שקיים.

היסטוריה

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

הפרויקט מפותח ומתוחזק על ידי קבוצות מחקר באוניברסיטת ביאליסטוק בפולין, אוניברסיטת אלברטה בקנדה ואוניברסיטת שינשו ביפן. בעוד שבודק ההוכחה של מיזאר נשאר קנייני, הספרייה המתמטית של מיזאר - הגוף הנכבד של מתמטיקה פורמלית שהוא אימת - היא בעלת רישיון קוד פתוח.^[1]

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

שפת מיזאר

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

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

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

הספרייה המתמטית של מיזאר

הספרייה המתמטית של מיזאר (Mizar Mathematical Library - MML) כוללת את כל המשפטים שאליהם יכולים המחברים להתייחס במאמרים חדשים שנכתבים. לאחר אישור בודק ההוכחה, הם מוערכים בהמשך בתהליך של ביקורת עמיתים לתרומה וסגנון מתאים. אם יתקבלו, הם מתפרסמים בכתב העת Formalized Mathematics^[4] ומתווספים ל-MML.

רוחב

נכון ליולי 2012, MML כללה 1,150 מאמרים שנכתבו על ידי 241 מחברים. במצטבר, אלה מכילים יותר מ-10,000 הגדרות צורניות של עצמים מתמטיים וכ-52,000 משפטים שהוכחו על עצמים אלה. יותר מ-180 משפטים נודעים נהנו כך מקודיפיקציה פורמלית.^[5] כמה דוגמאות הן משפט האן-בנך, הלמה של קניג, משפט נקודת השבת של בראואר, משפט השלמות של גדל ומשפט העקום של ז'ורדן.

רוחב הכיסוי הזה הוביל חלק^[6] להציע את מיזאר כאחת הקירובים המובילים לאוטופיית ה-QED של קידוד כל ליבת המתמטיקה בצורה הניתנת לאימות מחשב.

זמינות

כל מאמרי MML זמינים בצורת PDF כמאמרים של כתב העת Journal of Formalized Mathematics. הטקסט המלא של ה-MML מופץ עם בודק מיזאר וניתן להורדה חופשית מאתר מיזאר. בפרויקט מתמשך^[7] הספרייה הפכה לזמינה גם בפורמט ויקי ניסיוני^[8] המאפשר עריכות רק כאשר הן מאושרות על ידי בודק מיזאר.

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

מבנה לוגי

ה-MML בנוי על האקסיומות של תורת הקבוצות של טרסקי-גרותנדיק (אנ'). למרות שמבחינה סמנטית כל האובייקטים הם קבוצות, השפה מאפשרת להגדיר ולהשתמש בטיפוסים חלשים תחבירית. לדוגמה, ניתן להכריז על קבוצה מטיפוס Nat רק כאשר המבנה הפנימי שלה תואם רשימה מסוימת של דרישות. בתורה, רשימה זו משמשת כהגדרה של המספרים הטבעיים והקבוצה של כל הקבוצות התואמות לרשימה זו מסומנת כ-NAT.^[9] יישום טיפוסים זה מבקש לשקף את הדרך שבה רוב המתמטיקאים חושבים באופן פורמלי על סמלים,^[10] וכך מייעל את הקודיפיקציה.

בודק ההוכחות מיזאר

הפצות של בודק ההוכחות מיזאר (Mizar Proof Checker) לכל מערכות ההפעלה העיקריות זמינות להורדה בחינם באתר Mizar Project. השימוש בבודק ההוכחות הוא חינם לכל מטרה לא מסחרית. הוא כתוב ב-Free Pascal וקוד המקור זמין לכל חברי איגוד משתמשי מיזאר.^[11]

לקריאה נוספת

• מרכוס דו סוטוי, תוכנת היצירתיות - איך לומדת הבינה המלאכותית לכתוב, לצייר ולחשוב, תרגמה: מיכל קירזנר-אפלבוים, ספרי עליית הגג וידיעות ספרים, 2022, עמ' 273–283.

קישורים חיצוניים

• אתר האינטרנט הרשמי של מערכת מיזאר (באנגלית)

• Matuszewski, Roman; Piotr Rudnicki (2005). "Mizar: the first 30 years" (PDF). Mechanized Mathematics and Its Applications. 4.

הערות שוליים

1. Mailing list announcement referring to the open-sourcing of MML
2. Wiedijk, Freek (2008). "Formal Proof--Getting Started" (PDF). Notices of the AMS. 55 (11): 1408–1414.
3. Wiedijk, Freek. "The "de Bruijn factor"". נבדק ב-24 ביולי 2018.
4. אתר האינטרנט הרשמי של Formalized Mathematics
5. "A list of named theorems in the MML". נבדק ב-22 ביולי 2012.
6. Wiedijk, Freek (2007). "The QED Manifesto Revisited" (PDF). From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric. 10 (23).
7. The MathWiki project homepage form
8. The MML in wiki form
9. Grabowski, Adam; Artur Kornilowicz; Adam Naumowicz (2010). "Mizar in a Nutshell". Journal of Formalized Reasoning. 3 (2): 152–245.
10. Taylor, Paul (1999). Practical Foundations of Mathematics. Cambridge University Press. ISBN 9780521631075. אורכב מ-המקור ב-2015-06-23. נבדק ב-2012-07-24.
11. אתר האינטרנט הרשמי של Association of Mizar Users