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

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

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

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

• תחשיב למדא של צ'רץ'.
• תורת הטיפוסים האינטואיציוניסטית של פר מרטין לוף.

ערך זה הוא קצרמר בנושא מדעי המחשב. אתם מוזמנים לתרום למכלול ולהרחיב אותו.