Legătura profundă care echivalează dovezi matematice și programe de calculator | Revista Quanta

Unele descoperiri științifice contează pentru că dezvăluie ceva nou - structura dublă elicoială a ADN-ului, de exemplu, sau existența găurilor negre. Cu toate acestea, unele revelații sunt profunde, deoarece arată că două concepte vechi, cândva gândite distincte, sunt de fapt aceleași. Luați ecuațiile lui James Clerk Maxwell care arată că electricitatea și magnetismul sunt două aspecte ale unui singur fenomen sau legătura dintre gravitație și relativitatea generală cu un spațiu-timp curbat.

Corespondența Curry-Howard face același lucru, dar pe o scară mai mare, legând nu doar concepte separate într-un domeniu, ci discipline întregi: Informatică și logica matematica. Cunoscut și sub denumirea de izomorfism Curry-Howard (un termen care înseamnă că există un fel de corespondență unu-la-unu între două lucruri), acesta stabilește o legătură între dovezile matematice și programele de calculator.

Simplu spus, corespondența Curry-Howard presupune că două concepte din informatică (tipuri și programe) sunt echivalente, respectiv, cu propoziții și demonstrații - concepte din logică.

O ramificare a acestei corespondențe este că programarea - adesea văzută ca un meșteșug personal - este ridicată la nivelul idealizat al matematicii. Scrierea unui program nu este doar „codificare”, ci devine un act de demonstrare a unei teoreme. Aceasta formalizează actul de programare și oferă modalități de a raționa matematic despre corectitudinea programelor.

Corespondența poartă numele celor doi cercetători care au descoperit-o în mod independent. În 1934, matematicianul și logicianul Haskell Curry a observat o asemănare între funcțiile din matematică și relația de implicare în logică, care ia forma afirmațiilor „dacă-atunci” între două propoziții.

Inspirat de observația lui Curry, logicianul matematic William Alvin Howard a descoperit o legătură mai profundă între calcul și logică în 1969, arătând că rularea unui program de calculator este mult ca simplificarea unei dovezi logice. Când rulează un program de calculator, fiecare linie este „evaluată” pentru a produce o singură ieșire. În mod similar, într-o demonstrație, începeți cu enunțuri complexe pe care le puteți simplifica (eliminând pași redundanți, de exemplu, sau înlocuind expresii complexe cu altele mai simple) până când ajungeți la o concluzie - o afirmație mai condensată și mai succintă derivată din multe declarații intermediare. .

În timp ce această descriere transmite un sens general al corespondenței, pentru a o înțelege pe deplin trebuie să învățăm puțin mai multe despre ceea ce oamenii de știință în informatică numesc „teoria tipurilor”.

Să începem cu un paradox celebru: într-un sat locuiește un frizer care îi rade pe toți bărbații care nu se bărbieresc singuri, și numai pe ei. Se rade frizerul? Dacă răspunsul este da, atunci nu trebuie să se radă singur (pentru că rade doar bărbații care nu se rad). Dacă răspunsul este nu, atunci trebuie să se radă singur (pentru că îi rade pe toți bărbații care nu se rad). Aceasta este o versiune informală a unui paradox descoperit de Bertrand Russell în timp ce încerca să stabilească bazele matematicii folosind un concept numit mulțimi. Adică, este imposibil să definiți o mulțime care să conțină toate seturile care nu se conțin fără a întâmpina contradicții.

Pentru a evita acest paradox, a arătat Russell, putem folosi „tipuri”. În linii mari, acestea sunt categorii ale căror valori specifice se numesc obiecte. De exemplu, dacă există un tip numit „Nat”, adică numere naturale, obiectele sale sunt 1, 2, 3 și așa mai departe. Cercetătorii folosesc de obicei două puncte pentru a indica tipul unui obiect. Numărul 7, de tip întreg, poate fi scris ca „7: Integer”. Puteți avea o funcție care preia un obiect de tip A și scuipă un obiect de tip B sau una care combină o pereche de obiecte de tip A și tip B într-un nou tip, numit „A × B”.

Prin urmare, o modalitate de a rezolva paradoxul este de a pune aceste tipuri într-o ierarhie, astfel încât să poată conține doar elemente de „nivel inferior” decât ele însele. Atunci un tip nu se poate contine, ceea ce evită autoreferenţialitatea care creează paradoxul.

În lumea teoriei tipurilor, demonstrarea faptului că o afirmație este adevărată poate arăta diferit de ceea ce suntem obișnuiți. Dacă vrem să demonstrăm că întregul 8 este par, atunci este o chestiune de a arăta că 8 este într-adevăr un obiect de un anumit tip numit „Even”, unde regula de apartenență este divizibil cu 2. După verificarea faptului că 8 este divizibil prin 2, putem concluziona că 8 este într-adevăr un „locuitor” de tip Even.

Curry și Howard au arătat că tipurile sunt fundamental echivalente cu propozițiile logice. Când o funcție „locuiește” într-un tip – adică atunci când poți defini cu succes o funcție care este un obiect de acel tip – arăți efectiv că propoziția corespunzătoare este adevărată. Deci, funcțiile care preiau o intrare de tip A și dau o ieșire de tip B, notate ca tip A → B, trebuie să corespundă unei implicații: „Dacă A, atunci B”. De exemplu, luați propoziția „Dacă plouă, atunci pământul este ud”. În teoria tipurilor, această propoziție ar fi modelată de o funcție de tipul „Plouă → Pământul este umed”. Formulările cu aspect diferit sunt de fapt aceleași din punct de vedere matematic.

Oricât de abstractă ar suna această legătură, ea nu numai că a schimbat modul în care practicienii de matematică și informatică gândesc despre munca lor, dar a condus și la mai multe aplicații practice în ambele domenii. Pentru informatică, oferă o bază teoretică pentru verificarea software-ului, procesul de asigurare a corectitudinii software-ului. Prin încadrarea comportamentelor dorite în termeni de propoziții logice, programatorii pot demonstra matematic că un program se comportă așa cum se așteaptă. De asemenea, oferă o bază teoretică puternică pentru proiectarea limbajelor de programare funcționale mai puternice.

Iar pentru matematică, corespondența a dus la nașterea lui asistenți de dovezi, numit și demonstratori de teoreme interactive. Acestea sunt instrumente software care ajută la construirea de dovezi formale, cum ar fi Coq și Lean. În Coq, fiecare pas al demonstrației este în esență un program, iar validitatea dovezii este verificată cu algoritmi de verificare a tipului. Matematicienii au folosit, de asemenea, asistenți de demonstrare - în special, Demonstrator de teoreme Lean — să formalizeze matematica, care presupune reprezentarea conceptelor, teoremelor și demonstrațiilor matematice într-un format riguros, verificabil de calculator. Acest lucru permite ca limbajul uneori informal al matematicii să fie verificat de computere.

Cercetătorii încă explorează consecințele acestei legături dintre matematică și programare. Corespondența originală Curry-Howard îmbină programarea cu un fel de logică numită logică intuiționistă, dar se dovedește că și mai multe tipuri de logică ar putea fi susceptibile de asemenea unificări.

„Ceea ce s-a întâmplat în secolul de la cunoștințele lui Curry este că continuăm să descoperim tot mai multe cazuri în care „sistemul logic X corespunde sistemului de calcul Y”,” a spus Michael Clarkson, un informatician la Universitatea Cornell. Cercetătorii au conectat deja programarea la alte tipuri de logică, cum ar fi logica liniară, care include conceptul de „resurse” și logica modală, care se ocupă de conceptele de posibilitate și necesitate.

Și deși această corespondență poartă numele lui Curry și Howard, ei nu sunt în niciun caz singurii care au descoperit-o. Acest lucru atestă natura fundamentală a corespondenței: oamenii o remarcă mereu și din nou. „Se pare că nu este o întâmplare că există o legătură profundă între calcul și logică”, a spus Clarkson.