פונקציית קורי – הבדלי גרסאות

תוכן שנמחק תוכן שנוסף
שורה 13:
: <math>f = \lambda <a,b> \in A\times B . f(<a,b>)</math>
אזי פונקציית קורי מתאימה ל-f את הפונקציה הבאה
: <math>f^\mathrm{Cu} = \lambda a \in A . \lambda b \in B . f(a,b) \in C</math>
שזו פונקציה המקבלת איבר ב-A ומחזירה פונקציה מ-B ל-C, כלומר: לכל <math>a \in A</math> מוחזרת הפונקציה
: <math>f^\mathrm{Cu}(a) = [\![ \mbox{ } b \mapsto f(a,b) \mbox{ } ]\!]</math>
 
קיים גם התהליך ההפוך, שנקרא UnCurry או <math>Curry^\mathrm{-1}</math> , שלוקח פונקציה <math>g: A \to (B \to C)</math> והופך אותה לפונקציה <math>g^\mathrm{UnCu} : A \times B \to C</math>.
: <math>Curry^\mathrm{-1} = \lambda g\in A \to (AB \to BC).\lambda <a,b> \in A \times B . (g(a))(b)</math>
: תהליכים אלה הופכיים אחד לשני ומהם מסיקים את ה[[איזומורפיזם]] הבא:
: <math>\left( A \times B \to C \right) \cong \left( A \to (B \to C) \right)</math>