Treść książki
Przejdź do opcji czytnikaPrzejdź do nawigacjiPrzejdź do informacjiPrzejdź do stopki
14
ROZDZIAŁ1.PRZEGLĄDHISTORYCZNY
Zdrugiejstrony,konstruktywnepodejściawrazzichrozwojemicorazbardziej
teoriarekursji),stałysięosobnymidziałamiMatematykiizaczęłystosowaćcoraz
bardziejwyrafinowaneabstrakcje,którychsenszczasembyłgubiony.Owszembył
onobecnyuichtwórcówwpostaciintuicji,dlaprzykładu,wznakomitejmonografii
oderwaneodichoryginalnegoznaczenia,tj.odtychintuicji,itracąsens.
WpołowieXXwiekupowstałateoriakategoriigłównienapotrzebydynamicznie
rozwijającejsięwtedytopologiialgebraicznej.Kategoriajestdefiniowanajakokolek-
cjaobiektówistrzałek(nazywanychteżmorfizmami)pomiędzy(niektórymi)obiek-
tami.Strzałkimogąbyćskładaneasocjacyjnie,odpowiadatokompozycjifunkcji,a
dlakażdegoobiektujeststrzałka(identyczność)odniegodoniegosamego.Możeto
byćuważanezaabstrakcjępojęciafunkcjinawyższympoziomie.Wteoriimnogości,
kluczowympojęciemjestrelacjanależeniaelementudozbioru.Wteoriikategorii,
kluczowympojęciemjestmorfizm.Teoriakategoriimiałabyćtymiwłaściwymipod-
stawamidlaMatematyki.
Wydajesię,żedobrympodsumowaniembadańnadpodstawamiMatematykipro-
wadzonychwpierwszejpołowieXXwiekumogąbyćgorzkiesłowa,któreHermann
foundationsof(logicand)mathematics.”Dyskusjeikontrowersje,gorącenapoczątku
XXwieku,powolizamieraływnastępnychdekadach.Przeważyłpopularny,również
obecnie,pogląd:“”Don}tworry,justdomathematicsbyprovingtheorems...”.A
kryzysnarastał.
ObecnietoczysiędyskusjawokółHomotpyTypeTheory:UnivalentFoundations
ofMathematics(HoTT),gdziepodstawowympojęciemjesthomotopytype(typhomo-
topiny)jakozłożonaabstrakcyjnastrukturanawiązującadopojęciagroupoidwteorii
kategorii.HoTTbazujenaformalizmieteoriitypówwprowadzonejprzezMartin-L"
ofa
(lata70-teXXwieku)mającejbyćpodstawądlaMatematyki,przynajmniejtejkon-
struktywnej,dlaktórejkonstrukcjaobiektupolegałanaprzedstawieniudowodu,że
takiobiektistnieje.
TymczasemwInformatyce(itechnologiachinformacyjnych)powstająnowejęzyki
programowania,któreodwołująsiębezpośredniodozaawansowanychiabstrakcyjnych
pojęćmatematycznychiswobodnieoperująfunkcjamiwysokiegorzędu(funkcjonała-
mi)takjakzwykłymiobiektami.
OilemaszynaTuringajestwystarczającymmodelemdlaobliczeńpierwszegorzę-
du,toniebardzowiadomoczymsąfunkcjonałyiobliczenianawyższychrzędach.
Programowanienietylkojakoprzetwarzaniebajtów,alerównieżjakoprzetwarza-
niematematycznychstrukturwysokiegorzędu,tomeritumtegocopostulowałJohn
dyTuringa.Powstałe,tzw.funkcyjnejęzykiprogramowania(np.Haskell,F#,czy
Scala)realizująobliczenianawyższychpoziomach(tj.nafunkcjonałach)wsposób
symbolicznypoprzezprzepisywanietermów.
Czymsąfunkcjonałyijakiejestichugruntowanie,żebymożnabyłoprzeprowa-
dzaćnanichbezpośrednieobliczeniaidalszekonstrukcje?Jesttobardzotrudny
problem,patrzG"
