הצגת המקור של הדף "תחשיב למדא"

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

תחשיב למדא הוא [[מודל חישובי]] שעל פי [[תזת צ'רץ'-טיורינג]] הוא [[שלמות טיורינג|שלם טיורינג]].

== רקע ==

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

בכתיבה מתמטית חופשית [[סימון מתמטי#סימונים מקובלים|מתארים]] לפעמים פונקציה בנוסח
: תהי <math>\ f : A \to B</math> הפונקציה <math> \ f(x) = x^2</math>
אבל זו צורת רישום לא מדויקת, שכן מבחינה לוגית <math> \ f(x)=x^2</math> הוא מספר (אם כי x אינו ידוע). מקובל גם תיאור בסגנון
: <math> f : \begin{array}{rcl} A & \longrightarrow & B \\ a & \longmapsto & f(a) \end{array}</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>\ \sqrt{} = \lambda x \in [0, \infty ) . \sqrt{x} \in [0, \infty ) </math>

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

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

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

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

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

ביטוי למדה שיש בו לפחות משתנה חופשי אחד נקרא ביטוי פתוח, בעקבות "נוסחה פתוחה" {{אנ|Open_formula}} בלוגיקה. ביטוי שאין בו משתנים חופשיים נקרא ביטוי סגור.

חשיבות המשתנים החופשיים היא בהצבות שחשובות ב[[#כלל_בטא|כלל בטא]] להלן, כאשר מחליפים רק משתנים חופשיים, ואף לא משתנה קשור.

כמו כן ב[[#כלל_אלפא|כלל אלפא]] מותר לשנות משתנה מכומת באבסטרקציה, רק אם אין משתנה חופשי בביטוי שיהפוך לקשור בעקבות השינוי.

== כללים לתחשיב למדא ==

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

=== כלל אלפא ===

כלל זה אומר ש
: <math>\ \lambda x. f(x) = \lambda y. f(y) </math>
ומשמעותו הוא ש"למדא" הוא כמת לוגי קושר. כלומר, מותר לשנות את השם של המשתנה הקשור, כל עוד לא מחליפים את שמו לשם של משתנה המופיע חופשית.

=== כלל בטא ===

כלל זה אומר ש
: <math>\ \left(\lambda x. f(x) \right)(a) = f(a) </math>
ומשמעותו היא שהפעלה של הפונקציה על איבר כלשהו מחזירה את התמונה של אותו איבר לפי כלל ההתאמה של הפונקציה. במילים אחרות, זה כלל הצבה לחישוב הערך שמחזירה הפונקציה.

=== כלל אטא ===

כלל זה אומר ש
: <math>\ \lambda x. M x = M </math>
כאשר <math>x</math> אינו חופשי ב <math>M</math>. הרי שעל פי כלל בטא, <math>\ \left(\lambda x. M x \right)(a) = M a </math> עבור כל a במקרה כזה.

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

כלל זה מבטא את העיקרון הלוגי של שוויון בהרחבה, אשר על פיו
: <math>\ g = f </math>
[[אם ורק אם]]
: <math>\ \forall a \in A \ : \quad g(a) = f(a) </math>
משמעותו היא ששתי פונקציות בעלות אותו תחום הגדרה A נחשבות זהות אם ערכיהן זהים עבור כל ערך וערך ב[[תחום הגדרה]] זה.

==דוגמאות==
===ביטויים ידועים===
כמה ביטויי למדה בסיסיים ידועים גם תחת שמות מקובלים, של מה שנקרא "קומבינטורים {{אנ|SKI combinator calculus}}",
*I = λx.x
*K = λx.λy.x
*S = λf.λg.λx.fx(gx)
*B = λf.λg.λx.f(gx)
*C = λf.λg.λx.fxg
*W = λ.fλx.fxx
*U = λx.xx

===אריתמטיקה===
ניתן להגדיר ביטויי למדא המבטאים את הערכים והפעולות האריתמטיים. הדרך המקובלת היא זאת: את הביטויים ל[[מספר טבעי|מספרים הטבעיים]] מגדירים בצורה הבאה:
* ZERO = λf.λx.x
* ONE = λf.λx.fx
* TWO = λf.λx.f(fx)
* THREE = λf.λx.f(f(fx))
וכן הלאה. כלומר, ביטוי של מספר כלשהו מפעיל את הפונקציה הניתנת לו, f, את אותו מספר פעמים של המספר עצמו, ברצף, החל מהערך הנוסף x, יהיו f ו-x אשר יהיו. לדוגמה,
* TWO f x = f(fx)
עבור כל f ו-x. כלומר, ה-f מופעל פעמיים ברצף החל מה x.

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

בהגדרות שלמעלה רואים בבירור ש
* THREE = λf.λx.f(TWO f x)
ובכלל, על ידי [[הפשטה]] מקבלים הגדרה [[הכללה_(מתמטיקה)|כללית]] של פעולת המספר העוקב SUCC שמקיימת משוואה
* THREE = SUCC TWO = λf.λx.f(TWO f x) = (λn.λf.λx.f(n f x)) TWO
פעולת ההפשטה, ה[[אבסטרקציה (מדעי המחשב)|אבסטרקציה]] בצעד האחרון, מייצרת בהתאם את ביטוי הלמדה הסגור מסוג אבסטרקציה, וכך מתקבלת מעצמה ההגדרה
* עוקב: SUCC = λn.λf.λx.f(n f x)
או בעברית, "המספר העוקב של n מפעיל n פעמים ברצף את הפונקציה f החל מהערך x, ואז מפעיל את הפונקציה פעם אחת נוספת. ביחד, n + 1 פעמים."

תחת אותה השיטה מגדירים גם פעולות חשבוניות נוספות,
* [[חיבור]]: ADD = λm.λn.m SUCC n = λm.λn.λf.λx.mf(nfx)
* [[כפל]]: MULT = λm.λn.λf.λx.m(nf)x
* [[חזקה (מתמטיקה)|חזקה]]: EXPT = λb.λn.λf.λx.nbfx
* קודם: PRED = λnfx.n(λri.i(rf))(Kx)I
* [[חיסור]]: SUB = λmn.n PRED m
* [[חצי]]: HALF = λnfx.n(λrif.i(rfi))(K(Kx))If
* [[עצרת (מתמטיקה)|עצרת]]: FACT = λnf.n(λra.a(r(SUCC a)))(Kf)ONE

למשל, PRED THREE f x הופך ל-I(f(f(Kxf))) כלומר f(fx) כלומר אותה התוצאה כמו של TWO f x, עבור כל f ו-x. ובכלל ניתן לראות ש
: PRED (SUCC n) f x =
: SUCC n (Xf) (Kx) I =
: Xf (n (Xf) (Kx)) I =
: I (n (Xf) (Kx) f) =
: I (f (f (... (f (Kxf)) ...))) =
: n f x
מכיוון ש Xfri = i(rf) ולכן Xfrf = f(rf) וכמובן Kxf = x.
השתמשנו בקיצור כתיבה X = λf.λr.λi.i(rf).

כמו כן,
: PRED ZERO f x = ZERO (Xf) (Kx) I = KxI = x = ZERO f x
: PRED (PRED ZERO) f x = PRED ZERO (Xf) (Kx) I = K(Kx)II = x = ZERO f x
וכן הלאה, לכל f ו-x.

אך בעצם ניתן להסיק PRED ZERO = ZERO כבר מהמשוואה הראשונה לפי כלל [[#כלל_אטא|צימצום אטא]],
ולקבל ישירות
: PRED (PRED ZERO) = PRED ZERO = ZERO
וכן הלאה לכל מספר הפעלות של פעולת הקודם על ZERO, משמע עבור כל המספרים השליליים, שהם תמיד יהיו אפס תחת הקידוד הזה.

לדוגמה, נחשב את 1+1:{{ש}}
כיוון שהפעולה ADD פועלת על ONE ועל ONE, אנחנו רוצים לחשב את ADD ONE ONE. הדרך בתחשיב למדא להפעיל פונקציה על שני משתנים היא להפעיל אותה עליהם בזה אחר זה.{{ש}}
כלומר, אנחנו רוצים לחשב את
: T = ADD ONE ONE
: T = (λm.λn.λf.λx.mf(nfx)) (λg.λy.gy) (λr.λq.rq)
נשתמש בכלל בטא כדי לצמצם את הביטוי ככל הניתן:
: T = (λn.λf.λx.(λg.λy.gy)f(nfx)) (λr.λq.rq)
: T = λf.λx.(λg.λy.gy)f((λr.λq.rq)fx)
: T = λf.λx.(λy.fy)((λr.λq.rq)fx)
: T = λf.λx.(λy.fy)((λq.fq)x)
: T = λf.λx.(λy.fy)(fx)
: T = λf.λx.f(fx)
וקיבלנו TWO כמו שרצינו.

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

כעת ניתן להגדיר קשרים ביניהם:
* IF = λa.λb.λc.abc
* NOT = λf.λx.λy.fyx
* AND = λf.λg.λx.λy.f(gxy)y
* OR = λf.λg.λx.λy.fx(gxy)

וכן ביטויים לוגיים שונים עבור ערכים אריתמטיים:
* בדיקה האם ערך הוא אפס: ISZERO = λn.n (λx.FALSE) TRUE
* בדיקה האם ערך הוא לא אפס: NONZERO = λn.n (λx.TRUE) FALSE
* קטן-שווה: LE = λn.λm.ISZERO (SUB n m)
* שוויון: EQ = λn.λm.AND (LE nm) (LE m n)
ואכן,
* NONZERO n = NOT (ISZERO n) = NOT (n (λx.FALSE) TRUE) =
* n (λx.NOT FALSE) (NOT TRUE) = n (λx.TRUE) FALSE

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

: <R = (λx.x x) λg.<term

כאשר <term> משתמש בהפעלה עצמית (g g) לצורך קריאה רקורסיבית. כך g מופעל על עצמו ומקבל את (ההעתק של) עצמו וכך יכול להשתמש בו.

למשל, כך נוכל להגדיר את פעולת ה[[עצרת (מתמטיקה)|עצרת]] בצורה רקורסיבית:

: R = (λx.x x) λg.λn.ISZERO n ONE (MULT n ((g g) (PRED n)))

(λx.x x) ידוע כ"קומבינטור '''U''' {{אנ|SKI_combinator_calculus#Self-application_and_recursion}}",

: U = λx.x x

את תבנית ההפעלה העצמית (g g) עצמה גם ניתן להפשיט ולזקק, עד לקבלת "קומבינטור '''Y''' {{אנ|Fixed-point combinator#Y combinator}}", 

: R = U λg.λn.ISZERO n ONE (MULT n ((&#x0332;g&#x0332; &#x0332;g&#x0332;)&#x0332; (PRED n))) 

: R = U λg.(λ&#x0332;r&#x0332;.λn.ISZERO n ONE (MULT n (&#x0332;r&#x0332; (PRED n)))) (g g)

: R = (λ&#x0332;f&#x0332;.U λg.&#x0332;f&#x0332; (g g)) (λr.λn.ISZERO n ONE (MULT n (r (PRED n))))

זאת אומרת,

: F = λr.λn.ISZERO n ONE (MULT n (r (PRED n)))

: Y = λf.Uλg.f (g g)

: R = YF

כלומר,

: H = λf.λg.f (g g)

: Y = λf.U(Hf)

: R = YF = U(HF) = HF(HF) = F(HF(HF)) = F(YF) = FR

דהיינו '''Y''' אכן מייצר [[נקודת שבת]] עבור הארגומנט שלו. וכאשר '''F''' הוא ביטוי למדא המצפה לפונקציה {{אנ|Higher-order_function}} כארגומנט ראשון שלו להשתמש בה לצורך חישוב רקורסיבי, נקודת השבת שלו
'''R'''='''YF'''='''F(YF)'''='''FR'''
היא אכן הפונקציה הרקורסיבית עבור '''F''', כי הרי רקורסיה משמעותה שימוש באותה פונקציה עצמה לצורך חישוב רקורסיבי.

במילים אחרות, כאשר '''F''' מהווה ביטוי למדה לחישוב של '''''צעד אחד''''' לפני חישוב המשך r כלשהו, נקודת השבת שלו r='''R''' היא החישוב הרקורסיבי '''R''' בשלמותו המבצע את מספר הצעדים הבלתי מוגבל של '''F''',

: '''R''' = '''FR''' = '''F'''('''FR''') = '''F'''('''F'''('''FR''')) = '''F'''('''F'''('''F'''(...)))

לפי הצורך, כנדרש על פי ערך הפרמטר הנוסף n.

את '''Y''' ניתן גם לבטא כמחרוזת של קומבינטורים, בכמה דרכים, למשל

'''Y''' = '''WS'''('''BWB''') = '''BU'''('''CBU''') = '''SSCBU''' = '''BU'''('''SB'''('''KU''')) = '''SSI'''('''S'''('''S'''('''KS''')'''K''')('''K'''('''SII''')))'''

<!-- Y = WS(BWB) = BU(CBU) = BU(SB(KU)) = SSI(S(S(KS)K)(K(SII)))
                   BU(CBU) = SB(CB)U = SSCBU
  -->
כולן מבטאות את אותו ביטוי הלמדה הנ"ל ובעצם מתארות את אותו הדבר. קיימים עוד מספר בלתי מוגבל של קידודי קומבינטורים אחרים, שונים מהותית, שמייצרים גם הם את נקודת השבת עבור הארגומט שלהם ומשיגים את אותה המטרה אך בדרכים אחרות, שונות ומגוונות.

==בתכנות==
תחשיב למדא עומד ביסודו של [[תכנות פונקציונלי|התכנות הפונקציונלי]] שבו פונקציות מקבלות פונקציות כארגומנטים ומחזירות פונקציות אחרות תוך שהן מפעילות את הארגומנטים זה על זה.

בנוסף, שפות תכנות רבות מאפשרות הגדרת פונקציה אנונימית בעזרת ביטויי למדא. למשל, בשפת [[פייתון]] ניתן להגדיר את פונקציית הזהות בצורה אנונימית כך: lambda x:x

== ראו גם ==
* [[פונקציה]]
* [[לוגיקה]]
* [[כמת לוגי]]
* [[תחשיב הפרדיקטים]]
* [[תכנות פונקציונלי]]

== לקריאה נוספת ==
{{ויקישיתוף בשורה}}
* [[ארנון אברון]], [https://web.archive.org/web/20070306163611/http://www.cs.tau.ac.il/~odedr/book_discrete_math/bdida_all.pdf '''מבוא למתמטיקה בדידה'''], הוצאת [[אוניברסיטת תל אביב]]
* '''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)

==קישורים חיצוניים==
* {{MathWorld}}

{{בקרת זהויות}}

[[קטגוריה:ערכים שבהם תבנית בריטניקה אינה מתאימה]]
[[קטגוריה:לוגיקה מתמטית]]
[[קטגוריה:ארצות הברית: המצאות]]