תחשיב למדא

מתוך ויקיפדיה, האנציקלופדיה החופשית
קפיצה אל: ניווט, חיפוש
Incomplete-document-purple.svg יש להשלים ערך זה: ערך זה עשוי להיראות מלא ומפורט, אך עדיין חסר בו תוכן מהותי. סיבה: עוסק רק בפורמליזם ולא במודל החישובי. ייתכן שתמצאו פירוט בדף השיחה.
הנכם מוזמנים להשלים את החלקים החסרים ולהסיר הודעה זו. שקלו ליצור כותרות לפרקים הדורשים השלמה, ולהעביר את התבנית אליהם.

תחשיב למדא (לעתים גם: תחשיב למְבְּדאאנגלית: Lambda calculus]) הוא צורה לוגית-פורמלית ריגורוזית להצגה וטיפול בפונקציות במתמטיקה ומדעי המחשב. תחשיב למדא הוא נושא בעל חשיבות בלוגיקה מתמטית (תורת הטיפוסים), יסודות המתמטיקה, מדעי המחשב התאורטיים, בתכנות פונקציונלי ובמערכות הוכחה אוטומטיות.

רקע[עריכת קוד מקור | עריכה]

פונקציה היא שלשה \ ( f , A , B ) כאשר A הוא תחום ההגדרה, B הוא הטווח (A ו-B הן קבוצות) ואילו f הוא יחס מעל \ A \times B שמכיל את הזוגות הסדורים מהצורה \ \left( a , f(a) \right). היחס f נקרא לעתים (באופן לא פורמלי) "כלל התאמה".

כאשר עובדים עם פונקציה נהוג לסמן או לרשום:

תהי \ f : A \to B הפונקציה  \ f(x) (למשל, באנליזה מתמטית של פונקציות ממשיות: \ f(x) = x^2 )...

אבל זו צורת רישום בזבזנית ולא מדויקת, שכן מבחינה לוגית,  \ f(x) הוא לא פונקציה אלא מספר כלשהו! למרות שהסימונים המקובלים כיום הם לא חד-משמעיים, הם נפוצים בגלל ההרגל והנוחות שבהם.

הערה: בספרי אלגברה מופשטת נהוג הסימון הבא:

 f : \begin{array}{rcl} A & \longrightarrow & B \\ a & \longmapsto & f(a) \end{array}

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

תחשיב הלמדא[עריכת קוד מקור | עריכה]

תחשיב הלמדא הוא ביטוי מהצורה:

\ f = \lambda  x \in A  .  f(x) \in B

שמשמעותו היא:

הפונקציה f היא הפונקציה המתאימה לכל \ x \in A איבר \ f(x) \in B (כאשר f הוא כלל התאמה כלשהו).

כאשר:

  • הכמת "למדא" מציין שמדובר בכלל התאמה.
  • האיבר הראשון אחרי הלמדא הוא תחום ההגדרה של הפונקציה.
  • האיבר שאחרי הנקודה הוא כלל התאמה, שבדרך כלל מוצג כביטוי של x. בשביל להיות פורמליים יש לציין מאיזה טווח לקוח ביטוי זה, אבל מאחר שזה לרוב ברור מההקשר נוהגים להשמיטו. ביישומים רבים, נוח להניח שהטווח של f הוא פשוט התמונה שלה \ \mathrm{Im}(f) .

הערה: נהוג גם הסימון

\ f = \lambda  x \in A  :  f(x) \in B

מאחר שהסימון עם הנקודה הוא בעייתי מאחר שקשה לראות את הנקודה (ולכן מעדיפים לרשום נקודתיים).

דוגמה: את הפונקציה של שורש ריבועי נרשום כך:

\ \sqrt{} = \lambda  x \in [0 , \infty )  .  \sqrt{x} \in [0 , \infty )

הכללות[עריכת קוד מקור | עריכה]

אפשר להכליל את תחשיב הלמדא כדי לדון בפונקציות רבות משתנים ובפונקציה של פונקציה.

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

כללים לתחשיב למדא[עריכת קוד מקור | עריכה]

קיימים כללים לוגיים פורמליים המאפשרים מניפולציות וטיפול בפונקציות באמצעות תחשיב למדא.

כלל אלפא[עריכת קוד מקור | עריכה]

כלל זה אומר ש

\ \lambda x . f(x) = \lambda y . f(y)

ומשמעותו הוא ש"למדא" הוא כמת לוגי קושר. כלומר, מותר לשנות את השם של המשתנה הקשור, כל עוד לא מחליפים את שמו לשם של משתנה המופיע חופשית.

כלל בתא[עריכת קוד מקור | עריכה]

כלל זה אומר ש

\ \left( \lambda x . f(x) \right)(a) = f(a)

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

כלל אטה[עריכת קוד מקור | עריכה]

כלל זה אומר ש

\ \lambda x . f(x) = \lambda x . g(x)

אם ורק אם

\ \forall a \in A \ : \quad \left( \lambda x . f(x) \right)(a) = \left( \lambda x . g(x) \right)(a)

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

ראו גם[עריכת קוד מקור | עריכה]

לקריאה נוספת[עריכת קוד מקור | עריכה]