תורת הטיפוסים

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

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

שתי תורות טיפוסים ידועות שיכולות לשמש כבסיס למתמטיקה הן:

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

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

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

ברטרנד ראסל הציע את הרעיון ב-1908. הוא רצה למנוע בעיה שבה ההגדרות יוצרות סתירה. אלונזו צ'רץ' ארגן את הרעיון בצורה מדעית ב-1933.

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