תורת הטיפוסים
במתמטיקה, לוגיקה ומדעי המחשב, תורת הטיפוסים מתייחסת באופן כללי למחלקה של מערכות פורמליות, שבה לכל ערך יש טיפוס, המודד באופן מסוים את רמת המורכבות של האובייקט, והפעולות מוגבלות לערכים מטיפוס מסוים. שיטה זו אמנם מאפשרת פיתוח סביר של יסודות המתמטיקה, אבל החלוקה לטיפוסים קשיחה מדי, והגישה לא התקבלה על דעתם של רוב הלוגיקנים. תורת הטיפוסים באה לידי ביטוי גם בתחום מערכות הטיפוסים של שפות תכנות, ומשמשת במסגרת זו כבסיס מתמטי להוכחת תוכניות מחשב.
את תורת הטיפוסים הציג ברטרנד ראסל ב-1908, כמענה לפרדוקס שלו, שערער את יסודות תורת הקבוצות הנאיבית. לפי גישה זו, קבוצה הכוללת איברים מטיפוס מסוים, היא בהכרח בעלת טיפוס גבוה יותר - וכך נמנעת ההתייחסות העצמית העומדת ביסוד הפרדוקס. פיתוח מתמטי מסודר של תורת הטיפוסים ניתן לראשונה על ידי אלונזו צ'רץ' ב-1933.
שתי תורות טיפוסים ידועות שיכולות לשמש כבסיס למתמטיקה הן:
- תחשיב למדא של צ'רץ'.
- תורת הטיפוסים האינטואיציוניסטית של פר מרטין לוף.
היסטוריה
כיום, לתורת הטיפוסים יש יישומים רבים והיא משמשת בהרבה דיסציפלינות שונות. אפילו בתוך הלוגיקה והמתמטיקה, ישנם כמה סוגים שונים של תורות טיפוסים. הם משרתים מספר מטרות, ומנוסחות בדרכים שונות. אבל, לפני 1903, כאשר ראסל הציג לראשונה את תורת הטיפוסים[1], לא היו ניסוחים קודמים של שום תורת טיפוסים אחרת. רק מהמחצית השנייה של המאה העשרים ניתן לראות התפתחות של תיאוריות טיפוסים.
השימוש המפורש והפורמלי בטיפוסים (ולכן צורה מוקדמת של מה שמכונה כיום "תורת הטיפוסים") נועד במקור למנוע את הפרדוקסים שהתרחשו בלוגיקה ובמתמטיקה בסוף המאה ה-19 ותחילת המאה ה-20. אבל זו לא הייתה השיטה היחידה שפותחה למטרה זו. כלי נוסף להתחמקות מהפרדוקס היה כוונון עדין של תורת הקבוצות של קנטור[2][3] מאת ארנסט זרמלו[4], והתפיסה הלולאתית של קבוצה, שנבעה מאקסיומה הבסיסית של תורת הקבוצות של זרמלו-פראנקל.
הגישה של הימנעות מהפרדוקס בתורת הטיפוסים שונה לחלוטין מהגישה התיאורטית של תורת הקבוצות. ראשית, בגישה הטיפוסית, השפה משתנה על מנת להימנע מהפרדוקס, ולא האקסיומות. יתרה מזאת, מאז שהורחבה התיזה של צ'רץ' עם טיפוסים פשוטים ב-1940, תורת הטיפוסים המשיכה להתמקד ברעיון הפונקציה בלוגיקה ובמתמטיקה. מאז 1940, פונקציות נותרו אחד ממושאי המחקר העיקריים של תורת טיפוסים[5].
קישורים חיצוניים
- תורת הטיפוסים, באתר אנציקלופדיה בריטניקה (באנגלית)
הערות שוליים
- ^ Russell, Bertrand, 1872-1970., The principles of mathematics, Allen & Unwin, 1948
- ^ Georg Cantor, Beiträge zur Begründung der transfiniten Mengenlehre, Mathematische Annalen 46, 1895-11, עמ' 481–512 doi: 10.1007/bf02124929
- ^ Georg Cantor, [http://dx.doi.org/10.1007/bf01444205 Beitr�ge zur Begr�ndung der transfiniten Mengenlehre], Mathematische Annalen 49, 1897-06, עמ' 207–246 doi: 10.1007/bf01444205
- ^ E. Zermelo, [http://dx.doi.org/10.1007/bf01449999 Untersuchungen �ber die Grundlagen der Mengenlehre. I], Mathematische Annalen 65, 1908-06, עמ' 261–281 doi: 10.1007/bf01449999
- ^ Fairouz D. Kamareddine, A modern perspective on type theory : from its origins until today, Dordrecht: Kluwer Academic Publishers, 2004, מסת"ב 1-4020-2334-0
33762398תורת הטיפוסים