Kari

Currying (z angl . currying , někdy - currying ) - transformace funkce z mnoha argumentů na množinu funkcí, z nichž každá je funkcí jednoho argumentu. Možnost takové transformace byla poprvé zaznamenána ve spisech Gottloba Fregeho , systematicky studovaného Mosesem Scheinfinkelem ve dvacátých letech 20. století a pojmenovaného po Haskell Currym , vývojáři kombinatorické logiky , ve které je redukce na funkce jednoho argumentu zásadní.

Definice

Pro funkci dvou argumentů provede operátor curry převod – vezme argument typu a vrátí funkci typu . Intuitivně, curry funkce umožňuje opravit některé její argumenty a zároveň vrátit funkci ze zbývajících argumentů. Jedná se tedy o funkci typu . $h\colon (A\krát B)\to C$ $\lambda$ $\Lambda (h)\dvojtečka A\to (B\to C)$ $A$ $(B\to C)$ $\lambda$ $(A\times B\to C)\to (A\to (B\to C))$

Decurrying ( angl. uncurring ) je zaveden jako inverzní transformace - obnovující argument curried: pro funkci, decurring operátorprovede transformaci; typ operátora decurry je. $k\colon A\to (B\to C)$ $\epsilon$ $\epsilon (k)\dvojtečka A\krát B\to C$ $(A\to (B\to C))\to (A\times B\to C)$

V praxi vám currying umožňuje zvážit funkci, která neobdržela všechny poskytnuté argumenty. Operátor kari je zabudován do některých programovacích jazyků, aby bylo možné používat funkce na více místech, nejběžnějšími příklady takových jazyků jsou ML a Haskell . Všechny jazyky, které podporují uzávěry , vám umožňují psát curried funkce.

Matematické hledisko

V teoretické informatice poskytuje currying způsob, jak zkoumat funkce více argumentů ve velmi jednoduchých teoretických systémech, jako je lambda počet . V teorii množin je kari korespondence mezi množinami a . V teorii kategorií, currying přijde z univerzální vlastnosti exponenciály ; v situaci karteziánské uzavřené kategorie to vede k následující korespondenci. Existuje bijekce mezi sadami morfismů z binárního součinu a morfismy do exponenciály , která je přirozená vzhledem k a vzhledem k . Toto tvrzení je ekvivalentní tomu, že funktor součinu a funktor Hom jsou adjungované funktory. $C^{A\times B}$ $\left(C^{B}\right)^{A}$ $f\colon (X\krát Y)\to Z$ $g\colon X\to Z^{Y}$ $X$ $Z$

Toto je klíčová vlastnost kartézské uzavřené kategorie nebo, obecněji, uzavřené monoidní kategorie . První je zcela dostačující pro klasickou logiku, ale druhý je vhodným teoretickým základem pro kvantové výpočty . Rozdíl je v tom, že kartézský součin obsahuje pouze informaci o dvojici dvou objektů, zatímco tenzorový součin použitý v definici monoidální kategorie je vhodný pro popis entanglovaných stavů [1] .

Z pohledu Curry-Howardovy korespondence je existence currying funkcí (typ habitability a decurrying (typ habitability ) ekvivalentní logickému tvrzení ( typ produktu odpovídá konjunkci a funkční typ implikaci ). Currying a decurrying funkce jsou podle Scotta spojité . $((A\krát B)\to C)\to (A\to (B\to C)$ $(A\to (B\to C)\to ((A\krát B)\to C)$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\krát B$ $A až B$

Currying z programátorského hlediska

Currying je široce používán v programovacích jazycích , především v těch, které podporují funkční programovací paradigma . V některých jazycích jsou funkce standardně curried, to znamená, že funkce s více místy jsou implementovány jako funkce s jedním místem vyšších řádů a použití argumentů na ně je posloupností dílčích aplikací .

Programovací jazyky s prvotřídními funkcemi obvykle definují operace curry(překlad funkce podpisu pohledu A, B -> Cna funkci podpisu A -> B -> C) a uncurry(provádění zpětné transformace - mapování funkce podpisu pohledu na A -> B -> Cdvoumístnou funkci formuláře A, B -> C). V těchto případech je spojení s operací dílčí aplikace transparentní papply: curry papply = curry.

Poznámky

↑ John c. Baez a Mike Stay, " Fyzika, topologie, logika a výpočty: Rosetta Stone Archived 15 May 2013 at the Wayback Machine ", (2009) ArXiv 0903.0340 Archived 20 July 2014 at Wayback Machine in New Structures for Physics , , Bob Coecke, Lecture Notes in Physics sv. 813 , Springer, Berlín, 2011, s. 95-174.

Literatura

Benjamin Pierce. Typy v programovacích jazycích / Per. z angličtiny: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 s. — ISBN 978-5-7913-0082-9 .
Teorie typů // Homotopie Teorie typů: Univalentní základy matematiky . - Princeton : Institute for Advanced Study , 2013. - 603 s.