Skip to content

מספרי צ'רץ'

Haskell, מתמטיקה

גרסה באנגלית לפוסט כאן.

בואו נדבר על מספרים. אבל לא על המספרים ה"רגילים" שכולנו מכירים, אלא על יצוג אחר של מספרים, מספרים בקידוד צ'רץ'.
קידוד צ'רץ' היא דרך להציג את המספרים הטבעיים בתור פונקציות מסדר גבוה. פונקציה מסדר גבוה היא פונקציה שמקבלת פונקציה כלשהי כקלט, או מחזירה פונקציה כפלט. למעשה, אלה פונקציות שפועלות על פונקציות.
אחרי שהבנו מה זו פונקציה מסדר גבוה נגדיר את אופן הקידוד:
הקידוד יתאים למספר הטבעי nn את הפונקציה Cn(f,x)C_n(f, x) שמוגדרת כך:
CnC_n מקבלת שני פרמטרים. הראשון הוא פונקציה שמסומנת ב-ff וממפה איבר כלשהו מסוג TT אל איבר כלשהו מסוג TT. הפרמטר השני הוא איבר כלשהו ב-TT שנסמן ב-xx.
הפונקציה תחזיר את התוצאה של הפעלת ff על xx, nn פעמים בשרשרת. כלומר, פעם ראשונה נפעיל את ff על xx, בפעם השנייה נפעיל את ff על התוצאה של השלב הקודם (כלומר f(x)f(x)), וכך האלה nn פעמים. אם נרצה לכתוב את זה באופן פורמלי נכתוב את זה כך:

Cn(f,x)=f( ... f(n timesx) ... )n times=ff...fn times(x)=fn(x)\begin{aligned} C_n(f,x) & =\underbrace{f(\ ...\ f(}_{\text{\textit n times}}x\underbrace{)\ ...\ )}_{\text{\textit n times}} \\ & =\underbrace{f\circ f \circ ...\circ f}_{\text{\textit n times}}(x) \\ & =f^n(x) \end{aligned}

נסתכל על כמה דוגמאות בשביל להפוך את זה לפחות מופשט:
נגדיר את ff כך: f(x)=2xf(x)=2*x. ולכן בדוגמאות הבאות, הקבוצה שהזכרנו למעלה, TT, תהיה המספרים הממשיים (R\R).

  • C0C_0, זו הפונקציה שמותאמת למספר 00. התוצאה של C0(f,3)C_0(f, 3) תהיה 33. למה? כי הפעלנו את הפונקציה ff על 33 אפס פעמים, כלומר, לא הפעלנו, ולכן נשארו עם האיבר המקורי. למעשה, באופן כללי הפונקציה C0C_0 מחזירה את הפרמטר השני שלה כמו שהוא.
  • התוצאה של C1(f,3)C_1(f, 3) היא f(3)=23=6f(3)=2*3=6
  • התוצאה של C2(f,3)C_2(f, 3) היא f(f(3))=2(23)=12f(f(3))=2*(2*3)=12

אז הבנו איך הקידוד ממפה מספר טבעי לפונקציה. זה רק כיוון אחד. המיפוי ההפוך יותר פשוט. אם יש לנו פונקציה ChC_h שידוע לנו שהיא מקודדת מספר טבעי בקידוד צ'רץ', אבל אנחנו רוצים לגלות מהו אותו ה-hh, נחשב את הפונקציה עם f(x)=x+1f(x)=x+1 בתור פרמטר ראשון ו-00 בתור פרמטר שני. למה זה עובד? כי ChC_h תפעיל את ff על 00 hh פעמים, כלומר, תוסיף ל-00 את המספר hh, ולכן התוצאה תהיה hh.

אז המיפוי עובד לשני הכיוונים 🥳.
בואו נסמן את הפונקציה שמתאימה למספר nn את הפונקציה CnC_n ב-CEC_E. את הפונקציה שעושה את המיפוי ההפוך נסמן ב-CDC_D.
עכשיו נגדיר פעולות חיבור וכפל בין מספרי צ'רץ' שישמרו על המיפוי. כלומר, נרצה שיתקיים: CE(n+m)=CE(n)+CE(m)C_E(n + m)=C_E(n)+C_E(m) הסימון פה טיפה טריקי.
מה שקורה מצד שמאל זה חיבור רגיל בין שני טבעיים, nn ו-mm. על תוצאת החיבור מפעילים את CEC_E ומקבלים את הפונקציה Cn+mC_{n+m}.
מה שקורה מצד ימין זה שמפעילים את CEC_E על כל מספר טבעי בנפרד, מקבלים שתי פונקציות, CnC_n ו-CmC_m ומבצעים בינהן חיבור. זה לא חיבור בין מספרים, אלא בין פונקציות. ואת החיבור הזה, אנחנו נגדיר עכשיו.

למעשה, התוצאה של החיבור Cn+CmC_n+C_m צריכה להיות הפונקציה Cn+mC_{n+m}, כלומר, היא מקבלת כפרמטרים פונקציה ff וערך התחלתי xx ומפעילה את ff על xx סה"כ n+mn+m פעמים.
באותה הצורה נגדיר כפל. התוצאה של CnCmC_n*C_m היא הפונקציה CnmC_{n*m}.

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

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

השורה הראשונה מאפשרת את השימוש במילה forall. בשורה השנייה אנחנו מגדירים את CNumber ואומרים שהבנאי שלו נקרא Nr והוא מקבל פונקציה גנרית (שהמשתנה הגנרי שלה הוא t) מהצורה שהגדרנו מקודם.
אני אזכיר שבהסקל הטיפוס a -> b -> c מתאר פונקציה שמקבלת כפרמטר ראשון איבר מסוג a וכפרמטר שני איבר מסוג b ומחזירה איבר מסוג c.
אז מה שהגדרנו כאן זה תבנית לפונקציות CnC_n. שימו לב שזה לא אומר שכל הפונקציות שמתאימות לתבנית בהכרח מתארות מספרים טבעיים בקידוד צ'רץ', התבנית היא באופן כללי לפונקציות שמקבלות פונקציות ואיבר ומחזירות איבר.

בואו נשתמש בהגדרה בשביל להגדיר את 00, 11 ו-22 החדשים:

כמו שאמרנו מקודם, C0C_0 לא מפעילה את ff בכלל ומחזירה את xx כמו שהוא. C1C_1 מפעילה את ff על xx פעם אחת. ובאותו האופן, C2C_2 מפעילה פעמיים.
נניח שיש לנו עצם מסוג CNumber, וידוע שהוא קידוד של מפר טבעי כלשהו. איך נוכל לשחזר את המספר שהוא מייצג? כבר הזכרנו את זה למעלה, ובהסקל נכתוב את זה ככה:

השתמשנו בפונקציה עם הפרמטרים (+1) שמקבילה ל-f(x)=x+1f(x)=x+1 מלמעלה ו-0, וכך קיבלנו את המספר הטבעי שהפונקציה מייצגת. לפני שנממש את פונקציית החיבור, נממש אחת פשוטה יותר בשם succ. מה שהיא עושה זה לקבל עצם מסוג CNumber, ולהחזיר את העצם הבא אחריו ביצוג. כלומר, אם היא קיבלה את one היא תחזיר את two. הפונקציה הזו מקבילה לפונקצית העוקב של המספרים הטבעיים.

נניח שהפונקציה succ מקבלת CNumber שמתאר את הטבעי nn. אנחנו מגדירים כתוצאה פונקצייה חדשה שמקבלת פונקציה f ופרמטר x. היא תשתמש ב-a בשביל להפעיל את f על x nn פעמים, ואז תפעיל עוד פעם את f על התוצאה הסופית. וכך בעצם קיבלנו את העצם מסוג CNumber שמתאר את n+1n+1.
הערה קטנה: בשביל שהדבר הזה יתקמפל, חשוב להחליף את import Prelude שמופיע בראש הקוד, ב-import Prelude hiding (succ), כדי שהפונקציה המובנית succ לא תתנגש עם המימוש שלנו.

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

נניח ש-a ו-b מייצגים את n ו-m בהתאמה. הפונקציה שכתבנו מצד ימין משתמשת קודם ב-b בשביל להפעיל את f על x mm פעמים, ואז משתמשת ב-a בשביל להפעיל על התוצאה את f עוד nn פעמים. סה"כ היא מפעילה את f על x n+mn+m פעמים, שזה בדיוק מה שרצינו.
אבל אנחנו מסוגלים לכתוב את זה יותר יפה. יש לנו את הפונקציה a שיודעת להפעיל פונקציות על איבר כלשהו nn פעמים. למה לא שנשתמש בה בשביל להפעיל את succ על Nr b וככה למצוא את ה-CNumber שמתאר את n+mn+m. למה זה הגיוני? כי אם מפעילים את succ על b פעם אחת מקבלים את ה-CNumber שמייצג את m+1m+1.
ולכן אם נפעיל את succ על b nn פעמים באמצעות a נקבל את ה-CNumber שמייצג את m+nm+n.

יש דרך אפילו יותר קצרה לכתוב את זה, והיא:

אבל אנחנו לא מנסים להגיע לקצרנות, אלא לקריאות 😊

נשאר לנו לממש רק פונקציית הכפל! אציין שזה תרגיל נהדר בעיניי וכדאי לכם לנסות לפתור אותו בעצמכם. כמובן שאתם יכולים פשוט להסתכל על התשובה בהמשך, אבל יהרס כל הכיף 🙃
אנחנו רוצים להשתמש עוד פעם ב-a בשביל לחשב את ה-CNumber החדש. נעשה את זה ככה:

נעבור שלב שלב. התוצאה add (Nr b) היא פונקציה שמקבלת CNumber כלשהו ומחברת אליו את Nr b. אנחנו משתמשים ב-a בשביל לחבר ל-zero, ה-CNumber שמייצג את 00, את b nn פעמים. בסה"כ הפעלנו על zero את succ mm פעמים בכל הפעלה של add (Nr b) וסה"כ nmn*m פעמים. ולכן קיבלנו את ה-CNumber שמייצג את nmn*m.

באותה צורה אפשר להגדיר חזקה! אבל אותה אני לא אסביר, אלא פשוט אראה את הקוד:

אפשר להמשיך עם זה גם לטטרציה אבל נראה לי שהקונספט הובן 😊