Loading AI tools
מוויקיפדיה, האנציקלופדיה החופשית
תחשיב למדא (לעיתים גם: תחשיב למְבְּדא באנגלית: Lambda calculus) הוא צורה לוגית-פורמלית ריגורוזית להצגה וטיפול בפונקציות במתמטיקה ומדעי המחשב. תחשיב למדא הוא נושא בעל חשיבות בלוגיקה מתמטית (תורת הטיפוסים), יסודות המתמטיקה, מדעי המחשב התאורטיים, בתכנות פונקציונלי ובמערכות הוכחה אוטומטיות.
תחשיב למדא הוא מודל חישובי שעל פי תזת צ'רץ'-טיורינג הוא שלם טיורינג.
פונקציה היא שלשה כאשר A הוא תחום ההגדרה, B הוא הטווח (A ו-B הן קבוצות) ואילו f הוא יחס מעל שבו לכל יש יחיד שעבורו . היחס f נקרא לעיתים (באופן לא פורמלי) "כלל התאמה".
בכתיבה מתמטית חופשית מתארים לפעמים פונקציה בנוסח
אבל זו צורת רישום לא מדויקת, שכן מבחינה לוגית הוא מספר (אם כי x אינו ידוע). מקובל גם תיאור בסגנון
ברם, לצורכי לוגיקה וניתוח הוכחות באמצעות מחשב יש למצוא ביטוי לוגי-פורמלי חד-משמעי שיתאר פונקציה. ביטוי זה הוא סימון למדא.
סימון למדא הוא ביטוי מהצורה:
שמשמעותו היא:
כאשר:
דוגמה: את הפונקציה של שורש ריבועי נרשום כך:
בצורה פורמלית, ביטוי למדא מוגדר בצורה הרקורסיבית הבאה:
נהוגים גם כמה כללי קיצור, המאפשרים השמטת סוגריים במקרה שהביטוי נשאר חד משמעי. למשל, אפשר להוריד את הסוגריים החיצוניים; אפשר להוריד סוגריים כשיש כמה אפליקציות ברצף (למשל (λx.λy.(M במקום ((λx.(λy.(M ) ואפשר להוריד סוגריים כאשר מפעילים כמה משתנים ברצף זה על זה משמאל לימין, כלומר xyz שקול ל (xy(z. כמו כן אפשר לסמן ביטוי כלשהו בשם, שמאפשר להשתמש אחר כך בשם הזה (כשהכוונה היא קיצור של הצבת השם). למשל, אם מגדירים A=λx.λy.xy, אז אפשר לרשום את הביטוי λz.AA כשהכוונה היא ל (λz.(λx.λy.xy)(λx.λy.xy
משתנים חופשיים הם משתנים שאינם מכומתים על ידי אף λ. פורמלית, הם מוגדרים בצורה הבאה:
משתנה שאיננו חופשי נקרא קשור.
החשיבות של משתנים חופשיים היא בהצבות (שחשובות בכלל ביתא להלן): מותר להציב במקום משתנה ביטוי, רק אם אין משתנה חופשי בביטוי שיהפוך לקשור בעקבות ההצבה.
קיימים כללים לוגיים פורמליים המאפשרים מניפולציות וטיפול בפונקציות באמצעות תחשיב למדא.
כלל זה אומר ש
ומשמעותו הוא ש"למדא" הוא כמת לוגי קושר. כלומר, מותר לשנות את השם של המשתנה הקשור, כל עוד לא מחליפים את שמו לשם של משתנה המופיע חופשית.
כלל זה אומר ש
ומשמעותו היא שהפעלה של הפונקציה על איבר כלשהו מחזירה את התמונה של אותו איבר לפי כלל ההתאמה של הפונקציה. במילים אחרות, זה כלל הצבה לחישוב הערך שמחזירה הפונקציה.
כלל זה אומר ש
משמעותו היא ששתי פונקציות בעלות אותו תחום הגדרה A הן זהות אם ורק אם הן זהות עבור כל הערכים בתחום הגדרה זה.
בעזרת תחשיב הלמדא אפשר להגדיר ולטפל בביטויים אריתמטיים. הדרך המקובלת היא זאת: את המספרים הטבעיים מגדירים בצורה הבאה:
וכן הלאה. כלומר, מספר טבעי מקבל פונקציה ומשתנה ומפעיל את הפונקציה על המשתנה מספר פעמים כמספר הטבעי הזה.
כעת אפשר להגדיר פעולות חשבוניות:
למשל, נחשב את 1+1:
כיוון שהפעולה PLUS פועלת על ONE ועל ONE, אנחנו רוצים לחשב את PLUS ONE ONE (הדרך בתחשיב למדא להפעיל פונקציה על שני משתנים היא להפעיל אותה עליהם בזה אחר זה)
כלומר, אנחנו רוצים לחשב את (λm.λn.λf.λx.mf(nfx))(λf.λx.fx)(λf.λx.fx)
נשתמש בכלל ביתא כדי לפשט את הביטוי ככל הניתן:
(λm.λn.λf.λx.mf(nfx))(λf.λx.fx)(λf.λx.fx)
(λn.λf.λx.(λf.λx.fx)f(nfx))(λf.λx.fx)
(λf.λx.(λf.λx.fx)f((λf.λx.fx)fx
(λf.λx.(λf.λx.fx)f(fx
(λf.λx.f(fx
וקיבלנו שתיים כמו שרצינו.
את המשתנים הבוליאניים מסמנים בצורה הבאה:
היתרון של שיטה זאת היא שהביטוי הנפוץ "אם a החזר b ואם לא החזר c", שבשפות תכנות מסומן פעמים רבות כך: a?b:c, פשוט מאוד ליצוג בתחשיב למדא: abc.
כעת ניתן להגדיר קשרים ביניהם:
וכן ביטויים לוגים שונים:
פונקציות יכולות לפעול על עצמן, ועל כן לקבל את עצמן כארגומנט. אפשר לנצל זאת כדי לכתוב פונקציות ברקורסיה: <f=(λx.x)λr.<term כאשר term הוא הפונקציה f שמשתמשת בעצמה בתור rr.
למשל, נגדיר את פעולת העצרת:
((FACTORIAL=(λx.x)λr.λn.(EQUAL n 0)ONE(MULT n rr(SUB n ONE
תחשיב למדא עומד ביסודו של התכנות הפונקציונלי שבו פונקציות מקבלות פונקציות כארגומנטים ומחזירות פונקציות אחרות תוך שהן מפעילות את הארגומנטים זה על זה.
בנוסף, שפות תכנות רבות מאפשרות הגדרת פונקציה אנונימית בעזרת ביטויי למדא. למשל, בשפת פייתון ניתן להגדיר את פונקציית הזהות בצורה אנונימית כך: lambda x:x
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.