תחשיב למדא

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

רקע

פונקציה היא שלשה $\ (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:A\to B$

$a\mapsto f(a)$

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

תחשיב הלמבדא

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

$\ 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 הן זהות אם ורק אם הינן זהות עבור כל הערכים בתחום הגדרה זה.

ראו גם

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

לקריאה נוספת

• ארנון אברון, מבוא למתמטיקה בדידה, הוצאת אוניברסיטת תל אביב
• The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Revised Edition H.P. Barendregt, Publisher: North Holland; Revised edition (November 15, 1985)