חשבון למבדה הוא מערכת פורמלית בלוגיקה מתמטית לביטוי חישובים מבוססי הפשטה ויישום פונקציות באמצעות כריכה והחלפת משתנים. זהו דגם אוניברסלי שניתן ליישם בעיצוב של כל מכונת טיורינג. חשבון הלמבדה הוצג לראשונה על ידי צ'רץ', מתמטיקאי מפורסם, בשנות ה-30.
המערכת מורכבת מבניית איברי למבדה וביצוע פעולות הפחתה עליהם.
הסברים ויישומים
האות היוונית למבדה (λ) משמשת בביטויי למבדה ובמונחי למבדה לציון הכריכה של משתנה בפונקציה.
ניתן לא להקליד או להקליד את חישוב למבדה. בגרסה הראשונה, ניתן להשתמש בפונקציות רק אם הן מסוגלות לקבל נתונים מסוג זה. מחשבי למבדה מוקלדים חלשים יותר, יכולים לבטא ערך קטן יותר. אבל, מצד שני, הם מאפשרים לך להוכיח דברים נוספים.
אחת הסיבות שיש כל כך הרבה סוגים שונים היא הרצון של מדענים לעשות יותר מבלי לוותר על ההזדמנות להוכיח משפטי חישוב למבדה חזקים.
למערכת יש יישומים בתחומים רבים ושונים של מתמטיקה, פילוסופיה, בלשנות ומדעי המחשב. קודם כל, חשבון הלמבדה הוא חשבון שמילא תפקיד חשוב בפיתוח תורת שפות התכנות. מערכות מיישמות את סגנונות היצירה הפונקציונלית. הם גם נושא חם למחקר בתיאוריה של קטגוריות אלה.
לבובות
חשבון הלמבדה הוצג על ידי המתמטיקאי אלונזו צ'רץ' בשנות ה-30 כחלק ממחקרו על יסודות המדע. המערכת המקורית הוכחה כלא עקבית מבחינה לוגית בשנת 1935 כאשר סטיבן קליין וג'יי ב. רוסר פיתחו את פרדוקס קליין-רוסר.
מאוחר יותר, בשנת 1936, צ'רץ' ייחד ופרסם רק את החלק הרלוונטי לחישובים, מה שנקרא כיום חשבון הלמבדה הלא מודפס. ב-1940 הוא גם הציג תיאוריה חלשה יותר אך עקבית מבחינה לוגית הידועה בשם מערכת הטיפוס הראשוני. בעבודתו הוא מסביר את כל התיאוריה במונחים פשוטים, כך שניתן לומר שצ'רץ' פרסם את חשבון למבדה עבור בובות.
עד שנות ה-60, כשהיחס שלו לשפות התכנות התברר, λ היה רק פורמליזם. הודות ליישומים של ריצ'רד מונטגו ובלשנים אחרים בסמנטיקה של השפה הטבעית, החשבון תפס מקום גאה הן בבלשנות והן במדעי המחשב.
מקור הסמל
למבדה אינו מייצג מילה או ראשי תיבות, הוא מגיע מהפניה במתמטיקה הראשית של ראסל ואחריה שני שינויים טיפוגרפיים. דוגמה לסימון: עבור פונקציה f עם f (y)=2y + 1 הוא 2ŷ + 1. וכאן אנו משתמשים ב-caret ("כובע") מעל y כדי לתייג את משתנה הקלט.
הכנסייה התכוונה במקור להשתמש בסמלים דומים, אך קובעי הכתיבה לא הצליחו למקם את סמל ה"כובע" מעל האותיות. אז במקום זאת הם הדפיסו אותו במקור בתור "/\y.2y+1". בפרק הבא של העריכה, הקלדניות החליפו את "/ \" בדמות דומה מבחינה ויזואלית.
מבוא לחישוב למבדה
המערכת מורכבת משפה של מונחים, שנבחרים על ידי תחביר פורמלי מסוים, ומערכת של כללי טרנספורמציה המאפשרים לבצע בהם מניפולציות. הנקודה האחרונה יכולה להיחשב כתיאוריה משוואה או כהגדרה אופרטיבית.
כל הפונקציות בחשבון למבדה הן אנונימיות, כלומר אין להן שמות. הם לוקחים רק משתנה קלט אחד, וקאריינג משמש ליישום עלילות עם מספר משתנים.
תנאי למבדה
תחביר החשבון מגדיר ביטויים מסוימים כתקפים ואחרים כבלתי חוקיים. בדיוק כמו מחרוזות שונות של תווים הן תוכניות C חוקיות וחלקן לא. הביטוי בפועל של חשבון הלמבדה נקרא "מונח הלמבדה".
שלושת הכללים הבאים מספקים הגדרה אינדוקטיבית שיכולה להיותחל על הבנייה של כל המושגים תקפים תחבירית:
משתנה x עצמו הוא מונח למבדה חוקי:
- אם T הוא LT ו-x אינו קבוע, אז (lambda xt) נקרא הפשטה.
- אם T וגם s הם מושגים, אז (TS) נקרא יישום.
שום דבר אחר אינו מונח למבדה. לפיכך, מושג תקף אם ורק אם ניתן להשיגו על ידי יישום חוזר של שלושת הכללים הללו. עם זאת, ייתכן שחלק מהסוגריים יושמטו בהתאם לקריטריונים אחרים.
הגדרה
ביטויי למבדה מורכבים מ:
- משתנים v 1, v 2, …, v n, …
- סמלים של הפשטה 'λ' ונקודה '.'
- סוגריים בסוגריים ().
ניתן להגדיר את הסט Λ באופן אינדוקטיבי:
- אם x הוא משתנה, אז x ∈ Λ;
- x אינו קבוע ו-M ∈ Λ, ואז (λx. M) ∈ Λ;
- M, N ∈ Λ, ואז (MN) ∈ Λ.
Designation
כדי לשמור על הסימון של ביטויי למבדה נקי, נעשה שימוש נפוץ במוסכמות הבאות:
- סוגריים חיצוניים הושמטו: MN במקום (MN).
- ההנחה היא שיישומים יישארו אסוציאטיביים: אפשר לכתוב MNP במקום ((MN) P).
- גוף ההפשטה משתרע ימינה יותר: λx. MN פירושו λx. (MN), לא (λx. M) N.
- רצף ההפשטות מצטמצם: λx.λy.λz. N יכול להיות λxyz. N.
משתנים חופשיים ומאוגדים
האופרטור λ מחבר את האי-קבוע שלו בכל מקום שהוא נמצא בגוף ההפשטה. משתנים שנכנסים לתחום נקראים קשורים. בביטוי λ x. M, החלק λ x מכונה לעתים קרובות קלסר. כאילו רומזים שהמשתנים הופכים לקבוצה בתוספת של X x ל-M. כל שאר הלא יציבים נקראים חופשיים.
לדוגמה, בביטוי λ y. x x y, y - קשור לא קבוע, ו-x - חופשי. וראוי גם לציין שהמשתנה מקובץ לפי ההפשטה ה"קרוב" שלו. בדוגמה הבאה, פתרון חשבון הלמבדה מיוצג על ידי מופע יחיד של x, הקשור לאיבר השני:
λ x. y (λ x. z x)
קבוצת המשתנים החופשיים M מסומנת כ-FV (M) ומוגדרת על ידי רקורסיה על מבנה האיברים באופן הבא:
- FV (x)={x}, כאשר x הוא משתנה.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
נוסחה שאינה מכילה משתנים חופשיים נקראת סגורה. ביטויי למבדה סגורים ידועים גם כקומבינטורים ושווים למונחים בלוגיקה קומבינטורית.
קיצור
המשמעות של ביטויי למבדה נקבעת לפי האופן שבו ניתן לקצר אותם.
ישנם שלושה סוגי חיתוכים:
- α-transform: שינוי משתנים קשורים (אלפא).
- β-reduction: החלת פונקציות על הארגומנטים שלהם (ביטא).
- η-transform: מכסה את הרעיון של הרחבה.
הנה זה גםאנחנו מדברים על השקילות המתקבלות: שני ביטויים הם β-שקולים אם ניתן להפוך אותם ל-β לאותו רכיב, ו-α / η-אקוויוולנטיות מוגדרות באופן דומה.
המונח redex, קיצור של reducible turnover, מתייחס לתת-נושאים שניתן לצמצם באחד מהכללים. חשבון למדה עבור בובות, דוגמאות:
(λ x. M) N הוא רדוקס בטא בביטוי להחלפת N ב-x ב-M. הרכיב שאליו מצטמצם רדוקס נקרא הרדוקציה שלו. ההפחתה (λ x. M) N היא M [x:=N].
אם x אינו פנוי ב-M, λ x. M x גם em-REDEX עם הרגולטור M.
α-transformation
שינויי שמות אלפא מאפשרים לך לשנות את השמות של משתנים קשורים. לדוגמה, x. x יכול לתת λ y. y. מונחים שנבדלים זה מזה רק בטרנספורמציה של אלפא אמורים להיות α שווה ערך. לעתים קרובות, כאשר משתמשים בחשבון למבדה, שווה ערך α נחשבים הדדיים.
הכללים המדויקים להמרת אלפא אינם טריוויאליים לחלוטין. ראשית, עם הפשטה זו, רק המשתנים המשויכים לאותה מערכת ישתנו. לדוגמה, התמרת האלפא λ x.λ x. x יכול להוביל ל- λ y.λ x. x, אך ייתכן שהדבר לא יוביל ל-λy.λx.y לאחרון יש משמעות שונה מהמקור. זה מקביל לרעיון של תכנות הצללה משתנה.
שנית, טרנספורמציה של אלפא אינה אפשרית אם היא תגרום ללכוד על ידי הפשטה אחרת שאינה קבועה. לדוגמה, אם תחליף את x ב-y ב-λ x.λ y. x, אז אתה יכול לקבלλy.λy. u, שאינו זהה בכלל.
בשפות תכנות עם היקף סטטי, ניתן להשתמש בהמרת אלפא כדי לפשט את רזולוציית השם. יחד עם זאת, לדאוג שהמושג משתנה לא יסווה את הייעוד באזור המכיל.
בתווי אינדקס של De Bruyne, כל שני מונחים שווה ערך לאלפא זהים מבחינה תחבירית.
Replacement
השינויים שנכתבו על ידי E [V:=R] הם תהליך החלפת כל המופעים החופשיים של המשתנה V בביטוי E במחזור R. ההחלפה במונחים של λ מוגדרת על ידי הלמבדה של הרקורסיה חישוב על מבנה המושגים כדלקמן (שים לב: x ו-y - משתנים בלבד, ו-M ו-N - כל ביטוי λ).
x [x:=N] ≡ N
y [x:=N] ≡ y if x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) אם x ≠ y, בתנאי ש-y ∉ FV (N).
להחלפה להפשטה של למבדה, לפעמים יש צורך לבצע α-טרנספורמציה של ביטוי. לדוגמה, זה לא נכון ש-(λ x. Y) [y:=x] מביא ל-(λ x. X) כי ה-x המוחלף היה צריך להיות חופשי, אבל בסופו של דבר נקשר. ההחלפה הנכונה במקרה זה היא (λ z. X) עד שקילות α. שימו לב שהחלפה מוגדרת באופן ייחודי עד למבדה.
β-reduction
הפחתת בטא משקפת את הרעיון של יישום פונקציה. בטא רדוקטיבי מוגדר במונחיםתחליף: ((X V. E) E ') הוא E [V:=E'].
לדוגמה, בהנחה של קידוד כלשהו 2, 7, ×, יש את הפחתת ה-β הבאה: ((λ n. N × 2) 7) → 7 × 2.
ניתן לראות בהפחתת ביתא זהה לרעיון של צמצום מקומי תחת ניכוי טבעי באמצעות איזומורפיזם קארי-הווארד.
η-transform
המרה זו מבטאת את הרעיון של הרחבה, שבהקשר זה היא ששתי פונקציות שוות כאשר הן נותנות את אותה תוצאה לכל הארגומנטים. המרה זו מחליפה בין λ x. (F x) ו-f בכל פעם ש-x לא נראה פנוי ב-f.
פעולה זו יכולה להיחשב זהה למושג השלמות המקומית בדדוקציה טבעית באמצעות האיזומורפיזם של קארי-הווארד.
צורות רגילות ומיזוג
עבור חשבון למבדה לא מודפס, כלל הפחתת β בדרך כלל אינו מנרמל חזק או חלש.
עם זאת, ניתן להראות שהפחתת β מתמזגת כאשר היא פועלת לפני טרנספורמציה α (כלומר, שתי צורות נורמליות יכולות להיחשב שוות אם מתאפשרת טרנספורמציה α מאחת לשנייה).
לכן, גם למונחים המנרמלים מאוד וגם למונחים המתואמים בצורה חלשה יש צורה נורמלית אחת. במונחים הראשונים, מובטחת שכל אסטרטגיית הפחתה תביא לתצורה טיפוסית. בעוד שבתנאים מנרמל חלש, ייתכן שחלק מאסטרטגיות הפחתה לא ימצאו את זה.
שיטות תכנות נוספות
יש הרבה ניבים של יצירה עבור חשבון הלמבדה. רבים מהם פותחו במקור בהקשר של שימוש במערכות כבסיס לסמנטיקה של שפת תכנות, תוך יישום יעיל של מבנה ברמה נמוכה. מכיוון שחלק מהסגנונות כוללים חשבון למבדה (או משהו דומה מאוד) כקטע, הטכניקות הללו מוצאות שימוש גם ביצירה מעשית, אך עשויות אז להיתפס כסתומות או זרות.
קבועים עם שם
בחשבון למבדה, ספריה לובשת צורה של קבוצה של פונקציות שהוגדרו קודם לכן, כאשר המונחים הם רק קבועים קונקרטיים. לחישוב טהור אין מושג של בלתי משתנים בשם, מכיוון שכל מונחי הלמבדה האטומיים הם משתנים. אבל אפשר גם לחקות אותם על ידי נטילת המשתנה כשם הקבוע, שימוש בהפשטה של למבדה כדי לקשור את הנדיף הזה בגוף, ויישום ההפשטה הזו להגדרה המיועדת. אז אם אתה משתמש ב-f כדי לייצג את M ב-N, תוכל לומר
(λ f. N) M.
מחברים מציגים לעתים קרובות מושג תחבירי כמו אפשר לאפשר כתיבה של דברים בצורה אינטואיטיבית יותר.
f=M עד N
על ידי שרשור הגדרות כאלה, אפשר לכתוב "תוכנית" חישוב למבדה כאפס הגדרות פונקציה או יותר ואחריהן איבר למבדה בודד, תוך שימוש בהגדרות אלו המרכיבות את עיקר התוכנית.
הגבלה בולטת של תביעה זו היא שהשם f אינו מוגדר ב-M,מאחר ש-M נמצא מחוץ לתחום המחייב של הפשטת הלמבדה f. המשמעות היא שלא ניתן להשתמש בתכונה של פונקציה רקורסיבית בתור M עם let. תחביר letrec המתקדם יותר, המאפשר לכתוב הגדרות פונקציות רקורסיביות בסגנון זה, משתמש בנוסף במקום זאת בקומבינטורים של נקודות קבועות.
אנלוגים מודפסים
סוג זה הוא פורמליזם מודפס המשתמש בסמל כדי לייצג הפשטה של פונקציה אנונימית. בהקשר זה, טיפוסים הם בדרך כלל אובייקטים בעלי אופי תחבירי המוקצים למונחי למבדה. האופי המדויק תלוי בחשבון המדובר. מנקודת מבט מסוימת, LI מוקלד יכול להיחשב כשכלולים של LI לא מודפס. אבל מצד שני, הם יכולים להיחשב גם בתור תיאוריה בסיסית יותר, וחשבון הלמבדה הלא מודפס הוא מקרה מיוחד עם סוג אחד בלבד.
Typed LI הם הבסיס של שפות תכנות ועמוד השדרה של שפות פונקציונליות כמו ML והאסקל. ובאופן עקיף יותר, סגנונות יצירה הכרחיים. חשבוני למבדה מודפסים ממלאים תפקיד חשוב בפיתוח מערכות סוגים לשפות תכנות. כאן, הקלדה בדרך כלל לוכדת את המאפיינים הרצויים של התוכנית, למשל, היא לא תגרום להפרת גישה לזיכרון.
חשבון למבדה מוקלדים קשורים קשר הדוק ללוגיקה מתמטית ולתורת ההוכחה באמצעות האיזומורפיזם של קארי-הווארד, וניתן לחשוב עליהם כעל שפה פנימית של מחלקות קטגוריות, למשל, אשרזה פשוט הסגנון של סגירות קרטזיות.
