תחשיב למדא – הבדלי גרסאות

נוספו 52 בתים ,  לפני 9 שנים
הכללת "תחשיב למדא" ו"תחשיב למבדא" בשורת הפתיחה, ושינוי כל המופעים של "למבדא" בערך ל"למדא" בהתאם לערכים בוויקיפדיה (כולל זה) והדיון בדף השיחה.
מ (←‏רקע: מיקוד קישור פנימי)
(הכללת "תחשיב למדא" ו"תחשיב למבדא" בשורת הפתיחה, ושינוי כל המופעים של "למבדא" בערך ל"למדא" בהתאם לערכים בוויקיפדיה (כולל זה) והדיון בדף השיחה.)
{{השלמה|כל הערך=כן|סיבה=עוסק רק בפורמליזם ולא במודל החישובי}}
'''תחשיב למדא''' (לעתים גם: '''תחשיב למְבְּדא''' (ב[[אנגלית]]: Lambda calculus)) הוא צורה לוגית-פורמלית [[ריגורוזיות|ריגורוזית]] להצגה וטיפול ב[[פונקציה|פונקציות]] ב[[מתמטיקה]] ו[[מדעי המחשב]]. תחשיב למבדאלמדא הוא נושא בעל חשיבות ב[[לוגיקה מתמטית]] ([[תורת הטיפוסים]]), [[יסודות המתמטיקה]], [[מדעי המחשב]] התאורטיים, ב[[תכנות פונקציונלי]] וב[[מערכת הוכחה אוטומטית|מערכות הוכחה אוטומטיות]].
 
== רקע ==
: <math>a \mapsto f(a)</math>
 
ברם, לצורכי [[לוגיקה]] וניתוח הוכחות באמצעות [[מחשב]] יש למצוא ביטוי לוגי-פורמלי חד-משמעי שיתאר פונקציה. ביטוי זה הוא תחשיב הלמבדאהלמדא.
 
== תחשיב הלמבדאהלמדא ==
תחשיב הלמבדאהלמדא הוא ביטוי מהצורה:
: <math>\ f = \lambda x \in A . f(x) \in B </math>
שמשמעותו היא:
: הפונקציה f היא הפונקציה המתאימה לכל <math>\ x \in A</math> איבר <math>\ f(x) \in B</math> (כאשר f הוא כלל התאמה כלשהו).
כאשר:
* הכמתה[[כמת]] "[[למבדא|למבדאלמדא]]" מציין שמדובר בכלל התאמה.
* האיבר הראשון אחרי הלמבדאהלמדא הוא [[תחום הגדרה|תחום ההגדרה]] של הפונקציה.
* האיבר שאחרי הנקודתיים הוא כלל התאמה, שבדרך כלל מוצג כביטוי של x. בשביל להיות פורמליים יש לציין מאיזה [[טווח של פונקציה|טווח]] לקוח ביטוי זה, אבל מאחר שזה לרוב ברור מההקשר נוהגים להשמיטו. ביישומים רבים, נוח להניח שהטווח של f הוא פשוט ה[[תמונה (מתמטיקה)|תמונה]] שלה <math>\ \mathrm{Im}(f)</math> .
 
== הכללות ==
 
אפשר להכליל את תחשיב הלמבדאהלמדא כדי לדון בפונקציות רבות משתנים ובפונקציה של פונקציה.
 
ראוי בנושא זה לציין את [[פונקציית קורי]] שבאמצעותה מראים שההגדרה של פונקציה בשני משתנים שקולה להגדרה של פונקציה של פונקציה במשתנה אחד.
 
== כללים לתחשיב למבדאלמדא ==
 
קיימים כללים לוגיים פורמליים המאפשרים מניפולציות וטיפול בפונקציות באמצעות תחשיב למבדאלמדא.
 
=== כלל אלפא ===
כלל זה אומר ש
: <math>\ \lambda x . f(x) = \lambda y . f(y) </math>
ומשמעותו הוא ש"למבדאלמדא" הוא [[כמת לוגי]] קושר. כלומר, מותר לשנות את השם של המשתנה הקשור, כל עוד לא מחליפים את שמו לשם של משתנה המופיע חופשית.
 
=== כלל בתא ===