Karry

Currying (fra engelsk currying , nogle gange - currying ) - transformationen af en funktion fra mange argumenter til et sæt funktioner, som hver er en funktion af et argument. Muligheden for en sådan transformation blev først bemærket i Gottlob Freges skrifter , systematisk studeret af Moses Scheinfinkel i 1920'erne og opkaldt efter Haskell Curry , udvikleren af kombinatorisk logik , hvor reduktion til funktioner af et argument er grundlæggende.

Definition

For en funktion af to argumenter udfører curry-operatoren en konvertering - den tager et type-argument og returnerer en funktion af type . Intuitivt giver curry en funktion dig mulighed for at rette nogle af dens argumenter, mens du returnerer funktionen fra de resterende argumenter. Således er en funktion af typen . $h\colon (A\ gange B)\til C$ $\lambda$ $\Lambda (h)\colon A\to (B\to C)$ $EN$ $(B\to C)$ $\lambda$ $(A\ gange B\to C)\to (A\to (B\to C))$

Decurrying ( eng. uncurring ) introduceres som en invers transformation - gendannelse af curried-argumentet: for en funktiondecurry-operatorentransformationen; typen af decurry-operatør er. $k\colon A\to (B\to C)$ $\epsilon$ $\epsilon (k)\colon A\times B\to C$ $(A\to (B\to C))\to (A\time B\to C)$

I praksis giver currying dig mulighed for at overveje en funktion, der ikke modtog alle de angivne argumenter. Curry-operatøren er indbygget i nogle programmeringssprog for at tillade, at funktioner på flere steder kan curry, de mest almindelige eksempler på sådanne sprog er ML og Haskell . Alle sprog, der understøtter lukninger , giver dig mulighed for at skrive curry-funktioner.

Matematisk synspunkt

I teoretisk datalogi giver currying en måde at undersøge funktioner af flere argumenter inden for meget simple teoretiske systemer såsom lambda-regningen . I mængdelære er currying en overensstemmelse mellem sæt og . I kategoriteori kommer currying fra den eksponentielle universelle egenskab ; i situationen med en kartesisk lukket kategori fører dette til følgende korrespondance. Der er en bijektion mellem sæt af morfismer fra et binært produkt og morfismer til en eksponentiel , der er naturlig med hensyn til og med hensyn til . Dette udsagn svarer til det faktum, at produkt- og Hom-funktionerne er sammenhængende funktioner. $C^{A\times B}$ $\left(C^{B}\right)^{A}$ $f\colon (X\ gange Y)\til Z$ $g\colon X\to Z^{Y}$ $x$ $Z$

Dette er en nøgleegenskab for en kartesisk lukket kategori eller mere generelt en lukket monoidal kategori . Den første er ganske tilstrækkelig til klassisk logik, men den anden er et praktisk teoretisk grundlag for kvanteberegning . Forskellen er, at det kartesiske produkt kun indeholder information om et par af to objekter, mens det tensorprodukt, der anvendes i definitionen af en monoidal kategori , er velegnet til at beskrive sammenfiltrede tilstande [1] .

Set fra Curry-Howard-korrespondancens synspunkt er eksistensen af currying-funktioner (type beboelighed og decurrying (type beboelighed ) ækvivalent med et logisk udsagn ( produkttype svarer til konjunktion og funktionel type til implikation ). Currying og decurrying-funktioner er kontinuerlige ifølge Scott . $((A\ gange B)\til C)\til (A\til (B\til C)$ $(A\to (B\to C)\to ((A\time B)\to C)$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\ gange B$ $A til B$

Spændende fra et programmeringssynspunkt

Currying er meget udbredt i programmeringssprog , primært dem, der understøtter det funktionelle programmeringsparadigme . På nogle sprog er funktioner curried som standard, det vil sige, multi-place-funktioner er implementeret som single-place- funktioner af højere orden , og anvendelsen af argumenter på dem er en sekvens af delvise applikationer .

Programmeringssprog med førsteklasses funktioner definerer normalt operationer curry(oversættelse af en visningssignaturfunktion A, B -> Ctil en signaturfunktion A -> B -> C) og uncurry(udførelse af den omvendte transformation - tilknytning af en visningssignaturfunktion til en A -> B -> Cto-steds funktion af formularen A, B -> C). I disse tilfælde er forbindelsen med den delvise applikationsoperation gennemsigtig papply: curry papply = curry.

Noter

↑ John c. Baez og Mike Stay, " Physics, Topology, Logic and Computation: A Rosetta Stone Archived 15 May 2013 at the Wayback Machine ", (2009) ArXiv 0903.0340 Arkiveret 20. juli 2014 på Wayback Machine in New Structures for Physics , red. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlin, 2011, s. 95-174.

Litteratur

Benjamin Pierce. Typer i programmeringssprog / Pr. fra engelsk: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 s. — ISBN 978-5-7913-0082-9 .
Typeteori // Homotopi Typeteori: Matematiks univalente grundlag . - Princeton : Institute for Advanced Study , 2013. - 603 s.