Curry

Currying (az angol currying , néha - currying szóból ) - egy függvény átalakítása sok argumentumból függvénykészletté, amelyek mindegyike egy argumentum függvénye. Egy ilyen átalakítás lehetőségét először Gottlob Frege írásai jegyezték meg, amelyet Moses Scheinfinkel szisztematikusan tanulmányozott az 1920-as években, és Haskell Curryről, a kombinatorikus logika fejlesztőjéről nevezték el , amelyben alapvető az egyetlen érv függvényeire való redukálás.

Definíció

Két argumentum függvényében a curry operátor konverziót hajt végre – típus argumentumot vesz fel, és egy típus függvényt ad vissza . Intuitív módon egy függvény curry-je lehetővé teszi néhány argumentum javítását, miközben visszaadja a függvényt a többi argumentumból. Tehát a típus függvénye . $h\colon (A\time B)\to C$ $\lambda$ $\Lambda (h)\colon A\to (B\to C)$ $A$ ${\megjelenítési stílus (B\C)}$ $\lambda$ ${\megjelenítési stílus (A\idő B\-C)\- (A\- (B\-C))}$

A decurrying ( eng. uncurring ) inverz transzformációként kerül bevezetésre - a curried argumentum visszaállítása: függvényesetén a decurring operátorhajtja végre a transzformációt; a decurry operátor típusa. $k\colon A\to (B\to C)$ $\epsilon$ $\epsilon (k)\colon A\times B\to C$ ${\megjelenítési stílus (A\– (B\–C))\– (A\idő B\–C)}$

A gyakorlatban a currying lehetővé teszi egy olyan függvény figyelembevételét, amely nem kapta meg az összes megadott argumentumot. A curry operátor egyes programozási nyelvekbe be van építve, hogy lehetővé tegye a többhelyes függvények curriálását, az ilyen nyelvek leggyakoribb példái az ML és a Haskell . Minden nyelv, amely támogatja a lezárásokat , lehetővé teszi curry függvények írását.

Matematikai nézőpont

Az elméleti számítástechnikában a currying módot ad több argumentum függvényeinek vizsgálatára olyan nagyon egyszerű elméleti rendszereken belül, mint a lambda-számítás . A halmazelméletben a curry a halmazok és a halmazok közötti megfelelés . A kategóriaelméletben a curry az exponenciális univerzális tulajdonságából származik ; egy karteziánus zárt kategória helyzetében ez a következő megfeleléshez vezet. Bijekció van a bináris szorzatból származó morfizmusok és a morfizmusok exponenciálissá tétele között , amely természetes és a -hoz képest . Ez az állítás egyenértékű azzal a ténnyel, hogy a szorzatfunktor és a Hom-függvény adjunkt funktorok. $C^{A\times B}$ $\left(C^{B}\right)^{A}$ $f\colon (X\x Y)\-Z$ $g\colon X\to Z^{Y}$ $x$ $Z$

Ez a Descartes-féle zárt kategória , vagy általánosabban egy zárt monoid kategória kulcstulajdonsága . Az első elégséges a klasszikus logikához, de a második kényelmes elméleti alap a kvantumszámításhoz . A különbség az, hogy a Descartes-szorzat csak két objektumpárról tartalmaz információt, míg a monoidális kategória definíciójában használt tenzorszorzat alkalmas összefonódott állapotok leírására [1] .

A Curry-Howard levelezés szempontjából a curry funkciók megléte (típus lakhatóság és decurrying (típus lakhatóság ) egyenértékű egy logikai kijelentéssel ( a terméktípus a kötőszónak , a funkcionális típus pedig az implikációnak felel meg ). Curry és decurrying függvények Scott szerint folyamatosak . ${\megjelenítési stílus ((A\time B)\to C)\to (A\to (B\C)}$ ${\megjelenítési stílus (A\to (B\C)\to ((A\time B)\to C)}$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\-szer B$ $A-tól B-ig$

Currying programozási szempontból

A curryinget széles körben használják programozási nyelvekben , elsősorban azokban, amelyek támogatják a funkcionális programozási paradigmát . Egyes nyelveken a függvények alapértelmezés szerint curriáltak, azaz a többhelyes függvények magasabb rendű egyhelyes függvényekként vannak megvalósítva, és az argumentumok alkalmazása részleges alkalmazások sorozata .

Az első osztályú funkciókkal rendelkező programozási nyelvek általában műveleteket határoznak meg curry(a nézet aláírási A, B -> Cfunkciójának lefordítása aláírási funkcióvá A -> B -> C) és uncurry(a fordított transzformáció végrehajtása - a nézet aláírási funkciójának leképezése A -> B -> Caz űrlap kéthelyes függvényére A, B -> C). Ezekben az esetekben a részleges alkalmazási művelettel való kapcsolat átlátható papply: curry papply = curry.

Jegyzetek

↑ János c. Baez és Mike Stay, " Physics, Topology, Logic and Computation: A Rosetta Stone Archived 2013. május 15. at the Wayback Machine ", (2009) ArXiv 0903.0340 Archivált : 2014. július 20. at the Wayback Machine in New Structures for Physics , . Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlin, 2011, p. 95-174.

Irodalom

Benjamin Pierce. Típusok programozási nyelvekben / Per. angolból: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 p. — ISBN 978-5-7913-0082-9 .
Típuselmélet // Homotópia Típuselmélet: A matematika univalens alapjai . - Princeton : Institute for Advanced Study , 2013. - 603 p.