Globoka povezava, ki enači matematične dokaze in računalniške programe | Revija Quanta

Nekatera znanstvena odkritja so pomembna, ker razkrivajo nekaj novega - na primer dvojno vijačno strukturo DNK ali obstoj črnih lukenj. Vendar so nekatera razkritja globoka, ker kažejo, da sta dva stara koncepta, ki sta se nekoč mislila za različna, v resnici enaka. Vzemimo enačbe Jamesa Clerka Maxwella, ki kažejo, da sta elektrika in magnetizem dva vidika enega samega pojava, ali splošna relativnostna povezava gravitacije z ukrivljenim prostorom-časom.

Korespondenca Curry-Howard počne enako, vendar v večjem obsegu, saj ne povezuje le ločenih konceptov znotraj enega področja, temveč celotne discipline: Računalništvo in matematična logika. Znan tudi kot Curry-Howardov izomorfizem (izraz, ki pomeni, da obstaja nekakšna korespondenca ena proti ena med dvema stvarema), vzpostavlja povezavo med matematičnimi dokazi in računalniškimi programi.

Preprosto povedano, korespondenca Curry-Howard trdi, da sta dva koncepta iz računalništva (vrste in programi) enakovredna predlogom in dokazom – konceptom iz logike.

Ena od razvejanosti tega dopisovanja je, da je programiranje – ki se pogosto obravnava kot osebna obrt – povzdignjeno na idealizirano raven matematike. Pisanje programa ni le »kodiranje«, postane dejanje dokazovanja izreka. To formalizira dejanje programiranja in ponuja načine za matematično sklepanje o pravilnosti programov.

Korespondenca je poimenovana po dveh raziskovalcih, ki sta jo neodvisno odkrila. Leta 1934 je matematik in logik Haskell Curry opazil podobnost med funkcijami v matematiki in implikacijskim razmerjem v logiki, ki je v obliki stavkov "če-potem" med dvema predlogoma.

Navdihnjen s Curryjevim opazovanjem je matematični logik William Alvin Howard leta 1969 odkril globljo povezavo med računanjem in logiko ter pokazal, da je izvajanje računalniškega programa podobno poenostavitvi logičnega dokaza. Ko se računalniški program izvaja, je vsaka vrstica "ocenjena", da se ustvari en izhod. Podobno pri dokazu začnete s kompleksnimi izjavami, ki jih lahko poenostavite (na primer z odpravo odvečnih korakov ali zamenjavo kompleksnih izrazov s preprostejšimi), dokler ne pridete do zaključka – bolj zgoščene in jedrnate izjave, izpeljane iz številnih vmesnih izjav. .

Medtem ko ta opis izraža splošen pomen korespondence, se moramo, da bi jo popolnoma razumeli, naučiti nekaj več o tem, čemur računalničarji pravijo »teorija tipov«.

Začnimo s slavnim paradoksom: V vasi živi brivec, ki brije vse moške, ki se sami ne brijejo, in samo njih. Ali se brivec brije sam? Če je odgovor pritrdilen, potem se ne sme briti sam (ker brije samo moške, ki se ne brijejo). Če je odgovor ne, potem se mora sam obriti (ker obrije vse moške, ki se ne obrijejo). To je neformalna različica paradoksa, ki ga je odkril Bertrand Russell, medtem ko je poskušal postaviti temelje matematike z uporabo koncepta, imenovanega množice. To pomeni, da je nemogoče definirati množico, ki vsebuje vse množice, ki ne vsebujejo same sebe, ne da bi naleteli na protislovja.

Da bi se izognili temu paradoksu, je pokazal Russell, lahko uporabimo »tipe«. V grobem so to kategorije, katerih posebne vrednosti se imenujejo objekti. Na primer, če obstaja vrsta z imenom »Nat«, kar pomeni naravna števila, so njeni objekti 1, 2, 3 in tako naprej. Raziskovalci običajno uporabljajo dvopičje za označevanje vrste predmeta. Število 7, celoštevilskega tipa, lahko zapišemo kot "7: Celo število." Lahko imate funkcijo, ki vzame objekt tipa A in izpljune objekt tipa B, ali funkcijo, ki združi par predmetov, ki sta bila tipa A in tipa B, v nov tip, imenovan »A × B«.

Eden od načinov za razrešitev paradoksa je torej ta, da te tipe postavimo v hierarhijo, tako da lahko vsebujejo samo elemente »nižje ravni« od sebe. Potem tip ne more vsebovati samega sebe, kar se izogne ​​samonanašanju, ki ustvarja paradoks.

V svetu teorije tipov lahko dokazovanje, da je izjava resnična, izgleda drugače, kot smo vajeni. Če želimo dokazati, da je celo število 8 sodo, potem moramo dokazati, da je 8 res objekt določenega tipa, imenovanega »Sodo«, kjer je pravilo za pripadnost deljivo z 2. Ko preverimo, da je 8 deljivo po 2 lahko sklepamo, da je 8 res »prebivalec« tipa Even.

Curry in Howard sta pokazala, da so tipi v osnovi enakovredni logičnim predlogom. Ko funkcija »naseljuje« tip - to je, ko lahko uspešno definirate funkcijo, ki je objekt tega tipa - dejansko pokažete, da je ustrezna propozicija resnična. Torej funkcije, ki sprejmejo vhod tipa A in dajo izhod tipa B, označene kot tip A → B, morajo ustrezati implikaciji: "Če A, potem B." Na primer, vzemite predlog "Če dežuje, potem so tla mokra." V teoriji tipov bi bil ta predlog modeliran s funkcijo tipa »Raining → GroundIsWet«. Različne formulacije so v resnici matematično enake.

Naj se ta povezava sliši še tako abstraktno, ni samo spremenila razmišljanja praktikov matematike in računalništva o svojem delu, ampak je privedla tudi do več praktičnih aplikacij na obeh področjih. Za računalništvo predstavlja teoretične temelje za preverjanje programske opreme, proces zagotavljanja pravilnosti programske opreme. Z oblikovanjem želenega vedenja v smislu logičnih predlogov lahko programerji matematično dokažejo, da se program obnaša v skladu s pričakovanji. Zagotavlja tudi močno teoretično podlago za oblikovanje zmogljivejših funkcionalnih programskih jezikov.

In za matematiko je dopisovanje privedlo do rojstva dokazni pomočniki, imenovani tudi interaktivni dokazovalci izrekov. To so programska orodja, ki pomagajo pri konstruiranju formalnih dokazov, kot sta Coq in Lean. V Coq je vsak korak dokaza v bistvu program, veljavnost dokaza pa se preverja z algoritmi za preverjanje tipa. Matematiki uporabljajo tudi dokazne pomočnike - zlasti Lean dokazilo izrek — formalizirati matematiko, kar vključuje predstavitev matematičnih konceptov, izrekov in dokazov v strogem, računalniško preverljivem formatu. To omogoča, da včasih neformalni jezik matematike preverijo računalniki.

Raziskovalci še vedno raziskujejo posledice te povezave med matematiko in programiranjem. Izvirna Curry-Howardova korespondenca združuje programiranje z nekakšno logiko, imenovano intuicionistična logika, vendar se je izkazalo, da bi bilo takšnim poenotenjem lahko primernih tudi več vrst logike.

"V stoletju od Curryjevega vpogleda se je zgodilo to, da nenehno odkrivamo vedno več primerov, kjer 'logični sistem X ustreza računalniškemu sistemu Y'," je dejal. Michael Clarkson, računalniški znanstvenik na univerzi Cornell. Raziskovalci so programiranje že povezali z drugimi vrstami logike, kot sta linearna logika, ki vključuje koncept »virov«, in modalna logika, ki se ukvarja s konceptoma možnosti in nujnosti.

In čeprav ta korespondenca nosi Curryjevo in Howardovo ime, nikakor nista edina, ki sta jo odkrila. To potrjuje temeljno naravo korespondence: ljudje jo vedno znova opažajo. »Zdi se, da ni naključje, da obstaja globoka povezava med računanjem in logiko,« je dejal Clarkson.