A mélyhivatkozás matematikai bizonyítékok és számítógépes programok egyenlővé tétele | Quanta Magazin

Egyes tudományos felfedezések azért számítanak, mert valami újat tárnak fel – például a DNS kettős spirális szerkezetét vagy a fekete lyukak létezését. Egyes kinyilatkoztatások azonban mélyrehatóak, mert azt mutatják, hogy két régi fogalom, amelyeket egyszer külön gondoltak, valójában ugyanaz. Vegyük James Clerk Maxwell egyenleteit, amelyek azt mutatják, hogy az elektromosság és a mágnesesség egyetlen jelenség két aspektusa, vagy az általános relativitáselmélet összefüggése a gravitáció és a görbe téridő között.

A Curry-Howard levelezés ugyanezt teszi, de nagyobb léptékben, nem csupán egy területen belüli különálló fogalmakat kapcsol össze, hanem egész tudományágakat: Computer Science és a matematikai logika. Curry-Howard izomorfizmusként is ismert (ez azt jelenti, hogy két dolog között van valamiféle egy az egyhez megfelelés), kapcsolatot hoz létre a matematikai bizonyítások és a számítógépes programok között.

Egyszerűen fogalmazva, a Curry-Howard levelezés azt állítja, hogy a számítástechnikából származó két fogalom (típusok és programok) egyenértékű a propozíciókkal és a bizonyítékokkal – a logikai fogalmakkal.

Ennek a megfelelésnek az egyik következménye, hogy a programozást – amelyet gyakran személyes mesterségnek tekintenek – a matematika idealizált szintjére emelik. Egy program megírása nem csupán „kódolás”, hanem egy tétel bizonyításának aktusává válik. Ez formalizálja a programozást, és lehetőséget biztosít a programok helyességének matematikai érvelésére.

A levelezést a két kutatóról nevezték el, akik egymástól függetlenül fedezték fel. 1934-ben Haskell Curry matematikus és logikus hasonlóságot észlelt a matematikában a függvények és a logikai implikációs kapcsolat között, amely „ha-akkor” állítások formáját ölti két állítás között.

William Alvin Howard matematikus-logikus, Curry megfigyelései alapján 1969-ben mélyebb kapcsolatot fedezett fel a számítás és a logika között, megmutatva, hogy egy számítógépes program futtatása olyan, mint egy logikai bizonyítás egyszerűsítése. Amikor egy számítógépes program fut, minden sor „kiértékelésre kerül”, hogy egyetlen kimenetet adjon. Hasonlóképpen, a bizonyítás során összetett állításokkal kezd, amelyeket leegyszerűsíthet (például a redundáns lépések kiiktatásával, vagy az összetett kifejezések egyszerűbbekkel való helyettesítésével), amíg el nem jut egy következtetésre – egy sűrítettebb és tömörebb állításra, amely sok közbenső állításból származik. .

Bár ez a leírás a megfelelés általános értelmét közvetíti, annak teljes megértéséhez egy kicsit többet kell megtudnunk arról, amit az informatikusok „típuselméletnek” neveznek.

Kezdjük egy híres paradoxonnal: Egy faluban él egy borbély, aki megborotválja az összes férfit, aki nem borotválja magát, és csak őket. A borbély borotválja magát? Ha a válasz igen, akkor nem szabad borotválkoznia (mert csak azokat a férfiakat borotválja, akik nem borotválják meg magukat). Ha a válasz nem, akkor le kell borotválkoznia (mert minden férfit leborotvál, aki nem borotválja magát). Ez egy informális változata annak a paradoxonnak, amelyet Bertrand Russell fedezett fel, amikor a halmazoknak nevezett fogalom segítségével megpróbálta megteremteni a matematika alapjait. Vagyis lehetetlen olyan halmazt definiálni, amely az összes olyan halmazt tartalmazza, amelyek nem tartalmazzák önmagukat, anélkül, hogy ellentmondásokba ütköznének.

Russell megmutatta, hogy ezt a paradoxont ​​elkerüljük, használhatunk „típusokat”. Nagyjából ezek olyan kategóriák, amelyek meghatározott értékeit objektumoknak nevezzük. Például, ha létezik egy „Nat” nevű típus, ami természetes számokat jelent, akkor az objektumai 1, 2, 3 stb. A kutatók általában kettőspontot használnak az objektum típusának megjelölésére. Az egész típusú 7-es szám a következőképpen írható fel: „7: Integer”. Lehet olyan függvény, amely egy A típusú objektumot vesz, és egy B típusú objektumot köp ki, vagy egy olyan funkciót, amely az A és B típusú objektumok párját kombinálja egy új típusba, az úgynevezett „A × B”.

A paradoxon feloldásának egyik módja tehát az, hogy ezeket a típusokat hierarchiába helyezzük, így csak náluk „alacsonyabb szintű” elemeket tartalmazhatnak. Ekkor egy típus nem tudja visszatartani magát, ami elkerüli a paradoxont ​​létrehozó önreferenciát.

A típuselmélet világában az állítás igazának bizonyítása másképp nézhet ki, mint amit megszoktunk. Ha azt akarjuk bizonyítani, hogy a 8-as egész szám páros, akkor meg kell mutatnunk, hogy a 8 valóban egy bizonyos típusú „Páros” objektum, ahol a tagság szabálya osztható 2-vel. Miután ellenőriztük, hogy a 8 osztható-e 2-vel azt a következtetést vonhatjuk le, hogy a 8 valóban az Even típusú „lakója”.

Curry és Howard megmutatta, hogy a típusok alapvetően egyenértékűek a logikai kijelentésekkel. Amikor egy függvény „lakozik” egy típusban – vagyis amikor sikeresen definiálhat egy függvényt, amely az adott típusú objektum –, akkor hatékonyan megmutatja, hogy a megfelelő állítás igaz. Tehát azoknak a függvényeknek, amelyek A típusú bemenetet vesznek fel, és B típusú kimenetet adnak, A → B típusként jelölve, meg kell felelniük egy következménynek: „Ha A, akkor B”. Vegyük például a következőt: „Ha esik az eső, akkor nedves a föld.” A típuselméletben ezt a tételt egy „Raining → GroundIsWet” típusú függvény modellezné. A különbözőnek tűnő megfogalmazások matematikailag valójában ugyanazok.

Bármilyen elvontnak is hangzik ez a kapcsolat, nemcsak megváltoztatta azt, ahogyan a matematika és az informatika művelői gondolkodnak a munkájukról, hanem számos gyakorlati alkalmazáshoz is vezetett mindkét területen. A számítástechnika számára elméleti alapot ad a szoftverellenőrzéshez, a szoftverek helyességét biztosító folyamathoz. Azáltal, hogy a kívánt viselkedést logikai állításokkal keretezi, a programozók matematikailag tudják bizonyítani, hogy egy program a várt módon viselkedik. Erős elméleti alapot is biztosít erősebb funkcionális programozási nyelvek tervezéséhez.

A matematika esetében pedig a levelezés vezetett a születéshez bizonyítási segédek, más néven interaktív tételbizonyítók. Ezek olyan szoftvereszközök, amelyek segítik a formális bizonyítékok készítését, mint például a Coq és a Lean. A Coq-ban a bizonyítás minden lépése lényegében egy program, és a bizonyítás érvényességét típus-ellenőrző algoritmusok ellenőrzik. A matematikusok bizonyítási asszisztenseket is használtak – nevezetesen a Karcsú tétel bizonyító — a matematika formalizálása, amely magában foglalja a matematikai fogalmak, tételek és bizonyítások szigorú, számítógéppel ellenőrizhető formátumban történő megjelenítését. Ez lehetővé teszi a matematika olykor informális nyelvezetének számítógépek általi ellenőrzését.

A kutatók még mindig vizsgálják a matematika és a programozás közötti kapcsolat következményeit. Az eredeti Curry-Howard levelezés egyfajta logikával olvasztja a programozást, amit intuicionista logikának neveznek, de kiderül, hogy több logikatípus is alkalmas lenne az ilyen egyesítésekre.

„A Curry felismerése óta eltelt évszázadban az történt, hogy egyre több olyan esetet fedezünk fel, amikor „X logikai rendszer az Y számítási rendszernek felel meg” – mondta. Michael Clarkson, a Cornell Egyetem informatikusa. A kutatók már összekapcsolták a programozást más típusú logikákkal, például a lineáris logikával, amely magában foglalja az „erőforrások” fogalmát, és a modális logikát, amely a lehetőség és a szükség fogalmával foglalkozik.

És bár ez a levelezés Curry és Howard nevét viseli, korántsem ők az egyedüliek, akik felfedezték. Ez bizonyítja a levelezés alapvető természetét: az emberek újra és újra észreveszik. „Úgy tűnik, nem véletlen, hogy mély kapcsolat van a számítás és a logika között” – mondta Clarkson.