פונקציית קורי

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

פונקציית Curry היא פונקציה המקבלת פונקציה דו-מקומית $f:A\times B\to C$ ומחזירה פונקציה שמחזירה פונקציה ${\text{Curry}}\left(f\right):A\to (B\to C)$ . באופן פורמלי, קל להגדיר את פונקציית קורי באמצעות תחשיב למדא. באופן אינטואיטיבי, פונקציית קורי היא פונקציה שבמקום להכניס מספר קלטים ב"בת-אחת" בפונקציה המקורית, יוצרת ממנה פונקציה שבה מכניסים את הקלטים אחד אחרי השני, כך שבשלבי הביניים לפני הכנסת הקלט האחרון, יש לנו פונקציה עם פחות משתנים (ראו דוגמאות).

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

הגדרה

נגדיר את $Curry$ בעזרת כתיב למדא:

$Curry:(A\times B\to C)\to (A\to (B\to C))$

$Curry=\lambda f\in A\times B\to C.\lambda a\in A.\lambda b\in B.f(<a,b>)$

תהי $f:A\times B\to C$ פונקציה, בכתיב למדא היא "תירשם" כך:

f=\lambda \left\langle a,b\right\rangle \in A\times B.f\left(\left\langle a,b\right\rangle \right)

אזי פונקציית קורי מתאימה ל-f את הפונקציה הבאה

Curry(f)=\lambda a\in A.\lambda b\in B.f\left(\left\langle a,b\right\rangle \right)

שזו פונקציה המקבלת איבר ב-A ומחזירה פונקציה מ-B ל-C, כלומר: לכל $a\in A$ מוחזרת הפונקציה

(Curry(f))(a)=[\![{\mbox{ }}b\mapsto f(a,b){\mbox{ }}]\!]

קיים גם התהליך ההפוך, שנקרא ${\text{UnCurry}}$ או ${\text{Curry}}^{-1}$ , שלוקח פונקציה $g:A\to (B\to C)$ והופך אותה לפונקציה $Curry^{-1}(g):A\times B\to C$ .

Curry^{\mathrm {-1} }=\lambda g\in A\to (B\to C).\lambda \left\langle a,b\right\rangle \in A\times B.(g(a))(b)

תהליכים אלה הופכיים אחד לשני ומהם מסיקים את האיזומורפיזם הבא:

\left(A\times B\to C\right)\cong \left(A\to (B\to C)\right)

\mathrm {Hom} \left(A\times B,C\right)\cong \mathrm {Hom} \left(A,\mathrm {Hom} (B,C)\right)

פונקציית קורי היא התאמה חד-חד-ערכית ועל בין

A\times B\to C

לבין

A\to (B\to C)

ומכך נובע שוויון עוצמות: לכל

A,B,C

קבוצות

\left|A\times B\to C\right|=\left|A\to (B\to C)\right|

. דבר זה מוכיח את משפט אריתמטיקת העוצמות

{\left|C\right|}^{\left(\left|A\right|\cdot \left|B\right|\right)}={\left({\left|C\right|}^{\left|B\right|}\right)}^{\left|A\right|}

דוגמאות

דוגמה 1

תהי $f:\mathbb {R} \times \mathbb {R} \to \mathbb {R}$ , למשל: $f(x,y)=x+y$ . בסימון למדא נכתוב אותה כך:

f=\lambda x,y.x+y

אזי פונקציית קורי שלה היא

Curry(f)=\lambda x.\lambda y.x+y

לדוגמה:

f(3,4)=3+4=7

בעוד ש-

(Curry(f))(3)=\lambda y.3+y

וזו פונקציה במשתנה y שבו אפשר להציב ערכים, למשל:

(((Curry(f))(3))(4)=(\lambda y.3+y)(4)=3+4=7

.

דוגמה 2

תהי D הפונקציה הבאה: היא מקבלת פונקציה ממשית $f:\mathbb {R} \to \mathbb {R}$ ומספר ממשי $x\in \mathbb {R}$ ומחזירה את ערך הנגזרת של f בנקודה x, כלומר את $f'(x)$ . לכן אפשר לרשום: $D(f,x)=f'(x)$ כאשר $D:(\mathbb {R} \to \mathbb {R} )\times \mathbb {R} \to \mathbb {R}$ .

נסתכל על פונקציית קורי של D, זו פונקציה המקבלת פונקציה ממשית $f:\mathbb {R} \to \mathbb {R}$ ומחזירה את הפונקציה הנגזרת שלה $f':\mathbb {R} \to \mathbb {R}$ שהיא פונקציה המקבלת מספר ממשי $x\in \mathbb {R}$ ומחזירה את ערך הנגזרת ב-x. כלומר: $(Curry(D))(f)=[\![x\mapsto f'(x)]\!]$ כאשר $Curry(D):(\mathbb {R} \to \mathbb {R} )\to (\mathbb {R} \to \mathbb {R} )$ .