Treść książki
Przejdź do opcji czytnikaPrzejdź do nawigacjiPrzejdź do informacjiPrzejdź do stopki
5
nych,atezkoleisąrealizowanewmózguskładającegosięzwielkiej,aleskończonej
ilościkomórek(połączonychneuronówiglia).
Ciekawejestpodejściewspółczesnych(niestetynielicznych)matematykówiinfor-
matykówdotegoproblemu.
Zjednejstrony,HoTTniewątpliwiedotyczypojęciaContinuum(toteoriahomo-
topii),zaśzdrugiej,jejzwiązkuzteoriątypów,awięcdotyczypodstawzarówno
Matematyki,jakiInformatyki.
InteresującesąmotywacjedoweryfikacjiważnychtwierdzeńwMatematyceinspi-
rowaneosobistymdoświadczeniemV.Voevodsky.Wzaawansowanychwąskichtema-
tykach,tylkoniewielkagrupamatematykówmożeewentualniesprawdzićpoprawność
dowodówtwierdzeńrozwiązującychważneproblemy.Alenawetwtedyzdarzająsięsy-
tuacje,kiedybardzotrudnojestrozstrzygnąćczydowódtwierdzeniajestnieoprawny,
czyteżniepoprawnyjestkontrprzykładdlategotwierdzenia.Konstrukcjezwiązanez
dowodamiwzaawansowanejMatematycesątakzłożone,żezdaniemV.Voevodsky,
potrzebnesąnarzędziawspomagające(automatycznesystemywnioskujące(ang.re-
jakonanajbardziejzaawansowanysystemmogącywspomagaćpracęmatematyka.
Aleczytakiesystemy,opróczformalnejweryfikacjitwierdzenia,pomagająwzrozu-
mieniuistotytegotwierdzenia?Zastąpieniezrozumieniaprzezformalnąweryfikację
doprowadzidodegeneracjiMatematyki.Czyrzeczywiścietezaawansowanematema-
tycznekonstrukcje,tworzoneprzezwspółczesnychmatematykówiinformatyków,są
takzłożone,żesąniedostępnenietylkodlazwykłychludzialenawetdlasamych
matematyków,opróczkilkuwybranych,tychgenialnych?Czymożejesttak,żete
zaawansowanekonstrukcjedlategosątrudne,ponieważniejestjasneichugruntowa-
nie,czyliichsensniejestjednoznacznieokreślony,ajedynieopisanywformalizmie
teoriomnogościowymlubwteoriikategorii?
Wydajesię,żerozwójMatematykiosiągnąłjużtakistan,żebezjawnegojej
ugruntowania(okazujesię,żerównieżiInformatyki)dalszyrozwójjestbardzotrudny,
jeśliwogólemożliwy.
Rozwójkomputerów,technologiiinformacyjnychorazsamejInformatykijestim-
ponującywostatnichlatach.Faktyczniezmieniłonnaszącywilizacjęiwpływaobecnie
wznaczącysposóbnażycieprawiekażdegoczłowieka.Patrzącodstronywyłącznie
naukowej,dokonałosiętozasprawągenialnieprostejarchitekturykomputeraprzy-
pisywanejJohnowivonNeumannowi,ale(jakonsamtostwierdził)opracowanejna
podstawiekoncepcjiuniwersalnejmaszynyTuringa.Komputer,wedługtejarchitektu-
ry,przetwarzabajtywbardzoprostysposób.Programskładasięzsekwencjiinstruk-
cji.Sątoinstrukcjepobraniabajtówzpamięcidorejestrówprocesoraorazprosty
zestawinstrukcjidoprzetwarzaniatychbajtów.Instrukcjetemogązmieniaćflagi,tj.
1theInstituteforAdvancedStudy(IAS)inPrinceton,N.J.http://www.math.ias.edu/
~vladimir/
2http://homotopytypetheory.org/
3http://www.andrew.cmu.edu/user/awodey/
