תחשיב למדא

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

רקע

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

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

תהי $\ f:A\to B$ הפונקציה $\ f(x)=x^{2}$

אבל זו צורת רישום לא מדויקת, שכן מבחינה לוגית $\ f(x)=x^{2}$ הוא מספר (אם כי 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 הן זהות אם ורק אם הן זהות עבור כל הערכים בתחום הגדרה זה.

ראו גם

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

לקריאה נוספת

מדיה וקבצים בנושא תחשיב למדא בוויקישיתוף

• ארנון אברון, מבוא למתמטיקה בדידה, הוצאת אוניברסיטת תל אביב
• 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)