Book content

Skip to reader controlsSkip to navigationSkip to book detailsSkip to footer
5
nych,atezkoleirealizowanewmózguskładającegosięzwielkiej,aleskończonej
ilościkomórek(połączonychneuronówiglia).
Ciekawejestpodejściewspółczesnych(niestetynielicznych)matematykówiinfor-
matykówdotegoproblemu.
JakoprzykładmożnaprzytoczyćpróbyVladimiraA.Voevodsky1ijegoideiUni-
valentFoundationsofMathematicsorazHoTTczyliHomotopyTypeTheory2,tj.
związkuteoriitypówzteoriąhomotopiizapoczątkowanegoprzezSteveAwodey3.
Zjednejstrony,HoTTniewątpliwiedotyczypojęciaContinuum(toteoriahomo-
topii),zaśzdrugiej,jejzwiązkuzteoriątypów,awięcdotyczypodstawzarówno
Matematyki,jakiInformatyki.
Interesującemotywacjedoweryfikacjiważ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
dowodamiwzaawansowanejMatematycetakzłożone,żezdaniemV.Voevodsky,
potrzebnenarzędziawspomagające(automatycznesystemywnioskujące(ang.re-
asoner,proofassistant)opartenasystemachformalnych.WskazujeonnaCoq[20]
jakonanajbardziejzaawansowanysystemmogącywspomagaćpracęmatematyka.
Aleczytakiesystemy,opróczformalnejweryfikacjitwierdzenia,pomagająwzrozu-
mieniuistotytegotwierdzenia?Zastąpieniezrozumieniaprzezformalnąweryfikację
doprowadzidodegeneracjiMatematyki.Czyrzeczywiścietezaawansowanematema-
tycznekonstrukcje,tworzoneprzezwspółczesnychmatematykówiinformatyków,
takzłożone,żeniedostępnenietylkodlazwykłychludzialenawetdlasamych
matematyków,opróczkilkuwybranych,tychgenialnych?Czymożejesttak,żete
zaawansowanekonstrukcjedlategotrudne,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.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/