פתיחת התפריט הראשי

רקעעריכה

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

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

תהי   הפונקציה  

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

 .

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

סימון למדאעריכה

סימון למדא הוא ביטוי מהצורה:

 

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

הפונקציה f היא הפונקציה המתאימה לכל   איבר   (כאשר f הוא כלל התאמה כלשהו).

כאשר:

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

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

 

הגדרה פורמליתעריכה

בצורה פורמלית, ביטוי למדא מוגדר בצורה הרקורסיבית הבאה:

  • כל משתנה (שמסומן בדרך כלל בתו או במחרוזת) הוא ביטוי למדא.
  • אם M,N הם ביטויי למדא, אז גם (MN) הוא ביטוי למדא (אפליקציה).
  • אם x הוא משתנה ו-M הוא ביטוי למדא אז (λx.M) הוא ביטוי למדא (אבסטרקציה).

נהוגים גם כמה כללי קיצור, המאפשרים השמטת סוגריים במקרה שהביטוי נשאר חד משמעי. למשל, אפשר להוריד את הסוגריים החיצוניים; אפשר להוריד סוגריים כשיש כמה אפליקציות ברצף (למשל (λx.λy.(M במקום ((λx.(λy.(M ) ואפשר להוריד סוגריים כאשר מפעילים כמה משתנים ברצף זה על זה משמאל לימין, כלומר xyz שקול ל (xy(z. כמו כן אפשר לסמן ביטוי כלשהו בשם, שמאפשר להשתמש אחר כך בשם הזה (כשהכוונה היא קיצור של הצבת השם). למשל, אם מגדירים A=λx.λy.xy, אז אפשר לרשום את הביטוי λz.AA כשהכוונה היא ל (λz.(λx.λy.xy)(λx.λy.xy

משתנים חופשיים הם משתנים שאינם מכומתים על ידי אף λ. פורמלית, הם מוגדרים בצורה הבאה:

  • בביטוי הכולל משתנה בלבד, המשתנה הזה חופשי
  • בביטוי הכולל אפליקציה של שני ביטויים, המשתנים החופשיים הם איחוד של המשתנים החופשיים בכל ביטוי.
  • בביטוי הכולל אפליקציה של ביטוי ומשתנה, המשתנים החופשיים הם המשתנים של הביטוי, מלבד המשתנה המכומת (אם היה חופשי לפני כן)

משתנה שאיננו חופשי נקרא קשור.
החשיבות של משתנים חופשיים היא בהצבות (שחשובות בכלל ביתא להלן): מותר להציב במקום משתנה ביטוי, רק אם אין משתנה חופשי בביטוי שיהפוך לקשור בעקבות ההצבה.

כללים לתחשיב למדאעריכה

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

כלל אלפאעריכה

כלל זה אומר ש

 

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

כלל בתאעריכה

כלל זה אומר ש

 

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

כלל אטהעריכה

כלל זה אומר ש

 

אם ורק אם

 

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

דוגמאותעריכה

אריתמטיקהעריכה

בעזרת תחשיב הלמדא אפשר להגדיר ולטפל בביטויים אריתמטיים. הדרך המקובלת היא זאת: את המספרים הטבעיים מגדירים בצורה הבאה:

  • ZERO = λf.λx.x
  • ONE = λf.λx.fx
  • (TWO = λf.λx.f(fx

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

כעת אפשר להגדיר פעולות חשבוניות:

  • עוקב: (SUCC=λn.λf.λx.f(nfx
  • חיבור: (ADD=λm.λn.λf.λx.mf(nfx
  • קודם: (PRED=λn.λf.λx.n(λg.λh.h(gf))(λy.x)(λy.y
  • חיסור: λm.λn. nPREDm
  • כפל: (λm.λn.λf.m(nf

למשל, נחשב את 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
וקיבלנו שתיים כמו שרצינו.

לוגיקהעריכה

את המשתנים הבוליאנים מסמנים בצורה הבאה:

  • TRUE=λx.λy.x
  • FALSE=λx.λy.y

היתרון של שיטה זאת היא שהביטוי הנפוץ "אם a החזר b ואם לא החזר c", שבשפות תכנות מסומן פעמים רבות כך: a?b:c, פשוט מאוד ליצוג בתחשיב למדא: abc.

כעת ניתן להגדיר קשרים ביניהם:

  • NOT=λf.λx.λy.fyx
  • AND=λf.λg.λx.λy.g(fxy)y
  • (OR=λf.λg.λx.λy.fx(gxy

וכן ביטויים לוגים שונים:

  • בדיקה האם משתנה הוא אפס: ISZERO=λn.n(λx.FALSE)TRUE
  • קטן-שווה: LE=λn.λm.ISZERO SUB nm
  • שוויון: (EQ=λn.λm.AND (LE nm)(LE mn

רקורסיהעריכה

פונקציות יכולות לפעול על עצמן, ועל כן לקבל את עצמן כארגומנט. אפשר לנצל זאת כדי לכתוב פונקציות ברקורסיה: <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

ראו גםעריכה

לקריאה נוספתעריכה

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

קישורים חיצונייםעריכה