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. +more 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.

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ě. +more 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. +more 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č.

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.

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. +more 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. +more 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. +more 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 , 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 .

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ů. +more 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. +more Hindleym a J. P. Seldinem), North-Holland Publishing Company, Amsterdam 1972.

Reference

Kategorie:Američtí logici Kategorie:Američtí matematici Kategorie:Matematici 20. +more století Kategorie:Absolventi Harvardovy univerzity Kategorie:Absolventi Univerzity v Göttingenu Kategorie:Narození v roce 1900 Kategorie:Narození 12. září Kategorie:Úmrtí v roce 1982 Kategorie:Úmrtí 1. září Kategorie:Muži.