מספרי צ'רץ'

06.01.2020 — Haskell, Math — 7 min read

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

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

\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}

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

$C_0$ , זו הפונקציה שמותאמת למספר $0$ . התוצאה של $C_0(f, 3)$ תהיה $3$ . למה? כי הפעלנו את הפונקציה $f$ על $3$ אפס פעמים, כלומר, לא הפעלנו, ולכן נשארו עם האיבר המקורי. למעשה, באופן כללי הפונקציה $C_0$ מחזירה את הפרמטר השני שלה כמו שהוא.
התוצאה של $C_1(f, 3)$ היא $f(3)=2*3=6$
התוצאה של $C_2(f, 3)$ היא $f(f(3))=2*(2*3)=12$

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

אז המיפוי עובד לשני הכיוונים 🥳.
בואו נסמן את הפונקציה שמתאימה למספר $n$ את הפונקציה $C_n$ ב- $C_E$ . את הפונקציה שעושה את המיפוי ההפוך נסמן ב- $C_D$ .
עכשיו נגדיר פעולות חיבור וכפל בין מספרי צ'רץ' שישמרו על המיפוי. כלומר, נרצה שיתקיים: $C_E(n + m)=C_E(n)+C_E(m)$ הסימון פה טיפה טריקי.
מה שקורה מצד שמאל זה חיבור רגיל בין שני טבעיים, $n$ ו- $m$ . על תוצאת החיבור מפעילים את $C_E$ ומקבלים את הפונקציה $C_{n+m}$ .
מה שקורה מצד ימין זה שמפעילים את $C_E$ על כל מספר טבעי בנפרד, מקבלים שתי פונקציות, $C_n$ ו- $C_m$ ומבצעים בינהן חיבור. זה לא חיבור בין מספרים, אלא בין פונקציות. ואת החיבור הזה, אנחנו נגדיר עכשיו.

למעשה, התוצאה של החיבור $C_n+C_m$ צריכה להיות הפונקציה $C_{n+m}$ , כלומר, היא מקבלת כפרמטרים פונקציה $f$ וערך התחלתי $x$ ומפעילה את $f$ על $x$ סה"כ $n+m$ פעמים.
באותה הצורה נגדיר כפל. התוצאה של $C_n*C_m$ היא הפונקציה $C_{n*m}$ .

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

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

1{-# LANGUAGE RankNTypes #-}
2newtype CNumber = Nr (forall t. (t -> t) -> t -> t)

GitHub

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

בואו נשתמש בהגדרה בשביל להגדיר את $0$ , $1$ ו- $2$ החדשים:

1zero = Nr (\ f x -> x )
2one = Nr (\ f x -> f x )
3two = Nr (\ f x -> f (f x) )

GitHub

כמו שאמרנו מקודם, $C_0$ לא מפעילה את $f$ בכלל ומחזירה את $x$ כמו שהוא. $C_1$ מפעילה את $f$ על $x$ פעם אחת. ובאותו האופן, $C_2$ מפעילה פעמיים.
נניח שיש לנו עצם מסוג CNumber, וידוע שהוא קידוד של מפר טבעי כלשהו. איך נוכל לשחזר את המספר שהוא מייצג? כבר הזכרנו את זה למעלה, ובהסקל נכתוב את זה ככה:

1eval :: CNumber -> Int
2eval (Nr n) = n (+1) 0

GitHub

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

1succ :: CNumber -> CNumber
2succ (Nr a) = Nr (\ f x -> f (a f x) )

GitHub

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

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

1add :: CNumber -> CNumber -> CNumber
2add (Nr a) (Nr b) = Nr (\ f x -> a f (b f x))

GitHub

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

1add :: CNumber -> CNumber -> CNumber
2add (Nr a) (Nr b) = a succ (Nr b)

GitHub

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

1add :: CNumber -> CNumber -> CNumber
2add (Nr a) = a succ

GitHub

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

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

1mult :: CNumber -> CNumber -> CNumber
2mult (Nr a) (Nr b) = a (add (Nr b)) zero

GitHub

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

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

1pow :: CNumber -> CNumber -> CNumber
2pow (Nr a) (Nr b) = b (mult a) one

GitHub

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