New Scientist - Leta 1976 sta dva matematika, Appel in Haken, dokazala več kot sto let star problem barvanja zemljevidov (zanima nas najmanj koliko barv moramo uporabiti, da za vsako "državo" velja, da se z nobeno izmed sosed ne ujema v barvi, torej da se nikjer ne stikata dve enako obarvani). No, skoraj dokazala. Težava je bila v tem, da sta pravzaprav le omejila prostor rešitev in nato nad preostanek nagnala računalnik. Čudo tehnike je mlelo in mlelo ter na koncu izplunilo 4 (zavedam se, da do 42 manjka samo ena 2, ampak vseeno se pretvarjajmo, da je podobnost povsem naključna).
Vse lepo in prav, če se v dvatisoč in še nekaj letih matematika ne bi že malo izrodila in začela težiti k (platonski) popolnosti. Po svoje imajo puristi prav. "Zavihajmo rokave in upajmo na najboljše" pristop se vsekakor ne more meriti z eleganco nekajvrstičnih dokazov. Ako bi to novico pisal nekaj dni nazaj, bi mi preostalo le še, da zapadem v že tisočkrat prežvečene debate, češ, je indukcija sprejemljivo orodje? Smo lahko gotovi, da dani program kje ne skriva enklave ščurkov? In tako naprej, nazaj, okoli ovinka in po hribu navzgor vse do zgodnjih jutranjih ur.
Ampak vse to je preteklost! Gonthier in Werner sta dokaz, torej algoritem uporabljen za preiskovanje prostora rešitev, prenesla ("prenesla" se morda ne sliši kot kdo ve kakšen dosežek, ampak v resnici zahteva popolno abstrakcijo tako problema kot rešitve, kar ni mačji kašel) v Coq, jezik za preverjanje logičnih izjav. Pravovernejšega dokaza od povsem abstraktnega formalno-logičnega sistema si težko zaželimo. V kolikor v njunem delu ne najdejo kakšne resne napake, s tem kritikom računalnikov ne ostane več veliko streliva.
Rezultat sam ni pretirano presunljiv, Appel in Haken sta imela prav. Precej bolj presunljive so možnosti, ki jih orodja kot je Coq odpirajo. Microsoft (Gonthier je zaposlen v njihovem raziskovalnem centru na Cambridgu) tako namerava s formalizacijo programske logike zdesetkati populacijo hroščev v svojih izdelkih še preden jih prvič prevedejo.
Na novico nas je opozoril snow. Naj mu vsi hrošči v kodi poginejo!
Če se ne motim izhaja problem barv iz teorije grafov. Gledaš torej samo 2 sosednji državi - abstraktno si to predstavljamo kot vozlišča (predstavljajo države) in povezave med njimi (ki pomeni da državi mejita ena na drugo)....zdaj pa "barvamo" vozlišča, in gledamo da sta vedno različni barvi na dveh sosednjih, torej takih, ki sta med sabo povezani...
..nekaj takega (direktno iz glave)...
Aja, pozabil sm pohvaliti OwcA-o za odlično novico :)
Microsoft (Gonthier je zaposlen v njihovem raziskovalnem centru na Cambridgu) tako namerava s formalizacijo programske logike zdesetkati populacijo hroščev v svojih izdelkih še preden jih prvič prevedejo.
Men se tole zdi le prenos problemov/napak na en abstraktni nivo više. Zakaj bi bil pa opis programa v kakšnem višjem/bolj abstraktnem nivoju kej bol odporn na napake? Ko bo to delal si bodo pač omislil še en višji nivo ki bo kontroliral tega etc. Profita pa dejansko ni nobenega.
Rad bi videl človeka ki bo kar na hitro logično pravilno opisal delovanje recimo kakega drajverja etc. Vsak, ki je kdaj kak bol resn program pisal/dizajniral, ve, da hudič tiči v detajlih. Abstrakcija pa velikokrat pomeni ravno odstranjevanje detajlov, ki ti potem povsem nepričakovano skačejo v hrbet.
Nekaj napak tako gotovo odkriješ, četudi so povečini tako očitne, da bi jih tudi kartkotrajno testiranje odkrilo, imaš s tem še vedno ta proces vsaj do neke mere avtomatiziran in standariziran.
Owca, se strinjam, sigurno se najde kej. Ampak problem pa je da tem ko sestavš takšen abstraktni opis sistema, kompleksnost celga sistema le še povečaš. In kar naenkrat nucaš še močnejša orodja da vse skup kontroliraš. Vsekakor se najdejo področja kjer je to koristno ampak za splošen softver (ala MS stuff) se počasi kaže da pretirana formalizacija ne prinaša nekega profita (hint: agilne metode).
Pred dvema tednoma sem v The Economistu ( klik) zasledil članek, ki obravnava to tematiko.
Owca, sicer kul novica, ampak se bojim, da iz nje ni jasno razvidno, kaj točno sploh želiš do-povedat, kakšen pomen ima to "odkritje". Priporočam v branje.
Zgleda, da bi bilo kar dosti dela. No, za Avstalijo, Novo Zelandjio, pa se kaj ze ves, da lahko izberes, kar hoces.
Sicer pa, zdaj ko vemo, da je resitev 4. A bi se dalo to resiti z rekurzijo, da bi sel pac od Protugalske proti vzhodu, na voljo bi si vzel 4 barve, in poskusal priti cim dlje. Ce prides do konca, pol je 4 dovolj.
In kako bi znal da si jih pobarval optimalno? Tako na blef bi sigurno vsaj nekaj barv več porabu kot je potrebno. Še pri dost manjših grafih ni to tako enostavno.
Caki, gre se za to, da pobarvas vsako drzavo z eno od 4 barv. Zdej, s katero zacnes je vseeno. Recimo, Portugalska naj bo rumena, potem Spanija zelena, naprej Andora spet rumena. Pride Francija, je rdeca. Potem pa gledas poti naprej. Recimo, da se drzis serverne obale. Tam gor je pol menda Nizozemska, v eno barvo, ki ni enaka Franciji, potem naprej je menda Nemcija, in tako naprej. Recimo, do Rusije. Pa se vrnes nazaj na Francijo in poskusa tiste drzave ob severu, ki se niso pobarvane. In barvas tako navzdol. Ce ne gre vec, se pa vracas. Mogoce bi slo, no.
Zigga, IMHO je bistven pri tej novici dokaz da je dejansko ena mašina sposobna česa takega...da gre za nek napredek tudi na tem področju, ki predstavlja težak posel celo običajnim glavam, kaj šele "butastim" mašinam.
Tistih nekaj potencialnih bugov, ki jih ima pa bo sčasoma zginilo na poti k univerzalni mašini za dokazovanje izrekov...
> Men se tole zdi le prenos problemov/napak na en abstraktni nivo više. Zakaj bi bil pa opis programa v kakšnem višjem/bolj abstraktnem nivoju kej bol odporn na napake? Ko bo to delal si bodo pač omislil še en višji nivo ki bo kontroliral tega etc. Profita pa dejansko ni nobenega.
Ja res, C#/python/... je cisto brezveze, gremo nazaj na 1010011101.
In ko prideš do držav a la ZDA, Rusija, Azerbajdžan, Hrvaška itd., ki imajo dele ozemlja odrezane od matice (Aljaska, Kaliningrad, Naxičevan, Dubrovnik)? Da kake Francije (Gvajana, en otoček pri Kanadi, Tahiti, Nova Kaledonija, kos Antarktike....) niti ne omenjamo....
Avtorji poročila "CyberInsecurity: The Cost of Monopoly" so mnenja, da bodo neuspešni tudi poiskusi podjetja Microsoft da izboljša varnost svojih sistemov, če bo stranski učinek tega še večje priklepanje uporabnikov nanje. Problem je namreč monokultura.
Poleg tega s kompleksnostjo sistema narašča število napak v njemu. Odpravljanje napak pa kompleksnost še poveča. Zato izboljševanje varnosti ni linearno - potrebno je več sredstev za izboljšanje varnosti bolj kompleksnega sistema.
Primer: SP2, kjer je odpravljanje napak povzročilo nove.
> Poleg tega s kompleksnostjo sistema narašča število napak v njemu.
To sploh ni nujno res. Kompleksnost NIKAKOR ne pomeni nujno, da je napak več, lahko jih je tudi precej manj. Zelo kompleksni sistemi so poljubno verjetno brez napake.
Sej to si ni tako težko predstavljat. Poleg osnovnega sistema še en kup skrutinerjev, ki lovijo vsako napako in zaustavijo sistem, kakor hitro se kakšna pojavi.
Spontani splav v zgodnji nosečnosti recimo, je živ primer tega principa.
Sej to si ni tako težko predstavljat. Poleg osnovnega sistema še en kup skrutinerjev, ki lovijo vsako napako in zaustavijo sistem, kakor hitro se kakšna pojavi.
In od kje se vzamejo ti skrutinerji? Če je to avtomatika, je takoj del sistema in dodatna kompleksnost, ki jo je treba vzdrževat. Edin učinkovit poznan način za zmanjšanje napak, je zmanjšanje kompleksnosti in primeren pristop k delu.
> OwcA, > Mnja, saj je samo neskončno mnogo mogočih grafov.
Kako ti prideš to neskončno mnogo grafov, ko pa jaz dojemam le enega in edinega. Namreč gre za graf tipa planarne topologije, ki se jo povzame iz geometrijskih relacij, za katere velja pogoj, da se sosednji državi stikata ob meji, meja pa je lahko tudi meddržavna stoječa površinska voda. To se prevede na logične relacije med elementi grafa, geometrijo pa se popolnoma odpiše. Ostane le topološki opis relacij med elementi grafa, tj. med vozlišči, vejami in ploskvami (node, edge, face). Lege ploskev, ki jih obdajajo veje, so opredeljene glede na stran veje, pri čemer mora imeti veja opredeljeno usmerjenost. Vozlišče predstavlja tro- ali večmejo (ali točko mejitve para držav na vodno površino ), veja razmejuje par držav ali meddržavno vodno površino. Ploskev pa je ali država ali pa meddržavna vodna površina (identitete držav oz. meddržavnih vodnih površin referenciramo na ploskve). V primeru države Vatikan je veja dejansko zaključena same vase (ima eno vozlišče). Dejansko dobimo preprost logični model, ki matematično nima povsem nič skupnega z geometrijo. To je povsem nekaj običajnega pri modeliranju prostorskih podatkov v sistemih GIS (navadno se še vedno ločeno ohranijo geometrijski zapisi, če že ne zaradi drugega, pa zaradi grafičnega uporabniškega vmesnika za prikaz in urejanje vektorskih podatkov). Torej, množica držav in meddržavnih vodnih površin je povezana lahko le na en in edini možen s planarno topologijo opredeljen način.
Za rešitev naloge je potrebno izdelati primeren algoritem, ki podatke jemlje iz tega topološkega modela.
OwcA, morda razpoznaš ti še kakšno drugo planarno topologijo, torej planarni graf?
Če hočeš nekaj induktivno dokazati moraš preiskati cel prostor rešitev. Topološko je to seveda samo en genus 0 prostor, ampak razrezov (kart) je pa neskončno in pregledati moraš vse.
Abstrakcija problema je dvorezen meč. Na eni razsloji problem v nekakšno hierarhijo laže obvladljivih podproblemov, po drugi pa zakoliči strukturo hierarhije. Tako se poenostavi problem hkrati pa omeji maneverski prostor. Na takšni osnovi je bil izveden razslojen komunikacijskim odel ISO OSI, znotraj programskih jezikov objektno programiranje, opisni jeziki (npr. za programiranje central, kjer se lahko na pol grafično napiše SPECIFIČEN!!! algoritem), upravljanje avtomobila, državno upravne ureditve ...
Tako ministru za gospodarstvo ni potrebno skrbeti, iz kakšnega materiala mora biti šrauf (vem, da zalše zveni vijak, a se šrauf navadno lepše zateguje) in s kakšnim navorom ga mora zategniti nek delavec v strojnem podjetju. Bo pa usoda tega delavca precej odvisna od kritičnih odločitev ministrov, pa tudi ali bo povprečen delavec zategoval šraufe v tanke ali v turbine hidroelektrarn. Na višjem abstrakcijskem sloju imaš bolj posreden in manj določen vpliv na spodnje sloje. Ravno zato minister ne bo mogel neposredno odločati o zategovanju šraufuv - omejitev manevrskega prostora le na njegovo domeno. Dispečer v logističnem centru govori, kam naj šoferji dostavijo robo, ne ukvarja pa se s tem, kdaj naj kdo pritisne na gas, kuplungo ali žlajf. S tem pa se zagotovi, da vsak proces deluje le v svoji domeni in v interakciji z njemu podrejeno in nadrejeno domeno - nič dlje. Ugotavljanje napak v takšnem sistemu je veliko lažje, nadzorovati pa je seveda potrebno vse sloje, pri čemer državna ureditev navadno odpove.
Pri programiranju so zadeve z abstrakcijo zelo podobne. Nizkonivojske funkcije, ki so neposredni ukazi procesorju, ne smejo biti neposredno povezani s funkcijami, ki jih vnaša programer. Prav tako je mogoče ustvarjati skulpture struktur, podobno kot iz lego kock. Večja kot je abstrakcija, enostavno zapišemo porblem, a imamo na razpolago manj izraznih sredstev - pride do večjega vpliva vkalupljanja v standardne spodne sloje. Detajlov izvedbe ne bomo mogli opredeliti, za to bo poskrbelo razvojno okolje ali izvajalni sistem. Če malce osvetlim primerjavo: primer neabstraktnosti s popolno neposrednostjo bi bil, če bi Janša vsaki čistilki posebej rekel, da naj npr. z dvigom pokrova školjke in z uporabo ščetke s krožnibi gibi spuca školjo, vsakemu zidarju, kako naj se loti zidave itd. Seveda bi tako vodil državo kot celoto, a vendar sigurno precej manj uspešno kot sedaj, napak pa bi kar mrgolelo. To je podobno kot bi operacijski sistem napisali v strojnem jeziku z neposredno obravnavo vseh sodelujočih komponent - totalna zbrka. Velik del k abstrakciji je pripomoglo ločevanje strojne od programske opreme z vmesnim softverom - drajverji. Tudi jedro operacijskega sistema je ločeno od programov. Primer je tudi uporaba objektnega koncepta - očitno vzeto iz koncepta legic.
V bistvu lahko tudi v kompleksnem sistemu zmanjšaš št. napak. Vendar je potrebno nesorazmerno večje število energije za odpravo enakega števila napak kot v nekompleksnem sistemu.
K MSju pa prištejemo še marketinški boj (izdelke hitro ven, brez obsežnih priskusov) in priklepanje uporabnikov - dva velika minusa za varnost.
Sej je dokej na izi skapirat, da so 4 barve zadosti...
če ima država samo 2 sosedi rabiš 3 barve: levo, desno pa sebe če ma država 3 sosede rabiš 4 barve: prvo, drugo, tretjo pa sebe če pa ima 4 sosede pa rabiš spet samo 3 barve: zgornja+spodnja, leva+desna in sebe itd...
Ni ravno velka znanost, sam mašinerija ki to pofarba mora biti dokaj vztrajna. Hitrost itaq samo mi ljudje hočemo, compu se jebe kolk mileniumov računa, da je odgovor življenja, vesolja in vsega... 42
Fijavz? Hehe, sem ga imel. Pa je dostikrat tako zgledalo, da on rece "no, imamo A in potem se jasno vidi kako se dobi B". Jaz sem pa med A in B videl samo en klif pa morje polno morskih psov do obzorja. Sem pa vseeno spacal devetko
Kako pa ti misliš, da je bilo najenostavneje dokazat, da so 4 barve dovolj? You guessed it. Nobena država nima "pet-meje". Trivialen dokaz, pa vseeno deluje.
