Haskell Brooks Curry

Haskell Brooks Curry (12. září 1900 Millis, Massachusetts – 1. září 1982 State College, Pensylvánie) byl americký matematik a logik. Je znám především díky své práci v oboru kombinatorické logiky. Je také autorem Curryho paradoxu a Curryho–Howardova isomorfismu. Jsou po něm pojmenovány tři programovací jazyky: Haskell, Brook a Curry, jakož i technika přeměny funkce v matematice a matematické informatice zvaná currying.

Životopis

Narodil se v městečku Millis ve státě Massachusetts v rodině profesora řečnictví Samuela Silase Curryho a jeho ženy Anny Baright Curryové. Od roku 1916 studoval medicínu na Harvardově univerzitě, ale později přešel na studium matematiky. Po dokončení tohoto studia v roce 1920 studoval dva roky elektrotechniku na Massachusettském technologickém institutu a poté se vrátil studovat fyziku na Harvard, kde roku 1924 získal magisterský titul. V té době se započal jeho zájem o matematickou logiku, poté co se seznámil s dílem Principia Mathematica autorů Alfreda Northe Whiteheada a Bertranda Russella, v němž se autoři snaží odvodit veškeré matematické pravdy z dobře definovaného souboru axiomů a odvozovacích pravidel zapsaných aparátem symbolické logiky. Curry zůstal na Harvardu a začal pracovat na svém doktorátu v oboru matematika. Zatímco jeho školitel George David Birkhoff jej směřoval k práci na diferenciálních rovnicích, on se dál zajímal stále víc o logiku. V roce 1927, zatímco pracoval jako instruktor na Princetonské univerzitě, objevil práci Mosese Schönfinkela o kombinatorické logice. Schönfinkel v ní předjímal mnohé z jeho vlastního výzkumu. Curry následně přešel na Göttingenskou univerzitu, kde mohl spolupracovat s Heinrichem Behmannem a Paulem Bernaysem, kteří byli obeznámeni s Schönfinkelovou prací. Curryho konzultantem se stal David Hilbert. V roce 1930 obdržel Haskell Brooks Curry titul Ph.D. s disertační prací o kombinatorické logice.^[2]

V roce 1928 se Curry oženil s Marii Virginií Wheatleyovou. Po dokončení disertační práce se manželé v roce 1929 přestěhovali do univerzitního města State College v Pensylvánii, kde Curry přijal místo na Pensylvánské státní univerzitě. Setrval zde po následujících 37 let. V období 1931/1932 strávil rok na Chicagské univerzitě v rámci národního výzkumného stipendia a v období 1938/1939 rok v Institutu pro pokročilá studia v Princetonu. Bezprostředně po válce pracoval v letech 1945 až 1946 na projektu ENIAC. V rámci Fulbrightova stipendia spolupracoval s Robertem Feysem v belgické Lovani na zdejší Katolické univerzitě. Po odchodu z Pensylvánské univerzity v roce 1966 přijal Curry místo na Amsterdamské univerzitě. V roce 1970, po dokončení druhého dílu pojednání o kombinatorické logice, odešel z Amsterdamu a vrátil se do State College v Pensylvánii, kde 1. září 1982 zemřel.

Vědecká práce

Těžištěm jeho práce bylo dokázat vztahy a souvislosti kombinatorické logiky s matematikou. Ke konci roku 1933 se z korespondence s americkým logikem Johnem Rosserem dozvěděl o Kleene-Rosserově paradoxu. Paradox, rozpracovaný Rosserem a Stephenem Kleenem, prokázal nesoudržnost řady souvisejících formálních systémů včetně lambda kalkulu.

Curry se v podstatě stal zakladatelem kombinatorické logiky, z níž vzešel jeden styl funkcionálního programovacího jazyka. Síla a rozsah kombinatorické logiky jsou dost podobné lambda kalkulu Alonza Churche.

V roce 1947 popsal jeden z prvních programovacích jazyků vyšší úrovně a připravil první popis postupu při převádění obecných aritmetických výrazů do kódu pro jednoadresový počítač.^[3]

Přednášel na Harvardu, na Princetonu a v letech 1929–1966 na Pensylvánské státní univerzitě.

V roce 1942 publikoval Curryho paradox.

V roce 1966 se stal profesorem logiky a její historie a filozofie exaktních věd na Amsterodamské univerzitě. Stal se tak následníkem nizozemského filozofa a logika Everta Willema Betha.^[4]

Curry také psal a učil o matematické logice obecně, jeho učení v této oblasti vyvrcholilo v roce 1963 publikováním Základů matematické logiky. Jeho oblíbenou filozofií matematiky byl formalismus (viz Obrysy formalistické filozofie matematiky, v čemž následoval svého mentora Hilberta, avšak jeho dílo svědčí o značné filozofické zvídavosti a o nepředpojatosti vůči intuicionistické logice.

Přínos pro programovací jazyky

Po tomto logikovi byl pojmenován významný funkcionální programovací jazyk Haskell.

Haskell Curry popsal a poprvé použil princip, který byl po něm nazván curryfikace (anglicky currying). Jedná se o rozložení libovolné funkce o dvou argumentech na funkci jednoho argumentu vracející funkci druhého argumentu. Výhodnost této funkce je patrná v případě, že první argument je v řadě výpočtů pevný, zatímco druhý argument může nabývat různých hodnot. Zápis této funkce v jazyku Scheme:

 (define curry+
   (lambda (c)
     (lambda (x)
       (+ x c))))

Vyhodnocení této funkce: jedná se o funkci, která bude vracet další funkci jako výsledek své aplikace. Funkce curry+ má pouze jediný argument. Při aplikaci funkce curry+ bude vyhodnoceno její tělo, jímž je tento lambda výraz. Jeho vyhodnocením vznikne funkce jednoho argumentu, která bude vrácena jako výsledná hodnota aplikace curry+.

V případě aplikace (define f (curry+ 10)) bude na symbol f navázána hodnota vzniklá vyhodnocením (curry+ 10). Při vyhodnocování tohoto výrazu dojde k aplikaci uživatelsky definované funkce curry+ s argumentem 10. Při její aplikaci vznikne prostředí P, jehož předkem bude globální prostředí (protože v něm vznikla curry+) a ve kterém bude na symbol c navázána hodnota 10. V prostředí P bude vyhodnoceno tělo funkce curry+, to jest výraz (lambda (x) (+ x c)). Jeho vyhodnocením vznikne funkce <(x),(+ x c),P>, která je vrácena jako výsledek aplikace curry+. Tím pádem bude po vyhodnocení prvního výrazu na symbol f navázána funkce <(x),(+ x c),P>.^[5]

V Haskellu, který používá curryfikaci, můžeme funkci dvou argumentů volat s jedním argumentem. Výsledek je, podobně jako v minulém odstavci, funkce zbylých argumentů. Je reprezentována pomocí uzávěru, angl. closure, ve kterém se zapamatují už zadané argumenty funkce. Výsledek získáme až po vyhodnocení uzávěru.

Hlavní publikace

• Grundlagen der Kombinatorischen Logik (Základy kombinatorické logiky) American Journal of matematics, The Johns Hopkins University Press 1930
• Outlines of a formalist philosophy of mathematics (Nástin formalistické filozofie matematiky), Elsevier Science, Amsterdam 1951
• A theory of formal deducibility (Teorie formální odvoditelnosti), University of Notre Dame Press 1952
• Combinatory Logic I (Kombinatorická logika I – s Robertem Feysem), North-Holland Publishing Company, Amsterdam 1958
• Combinatory Logic II (Kombinatorická logika II – s J. R. Hindleym a J. P. Seldinem), North-Holland Publishing Company, Amsterdam 1972

Reference

V tomto článku byl použit překlad textu z článku Haskell Curry na anglické Wikipedii.