Curry-Howard Bağıntısı: Bir Matematik İspatı Aslında Bir Bilgisayar Programı mı?

İki Ayrı Dünya mı?

Bir tarafta matematiksel ispatlar var: bir teoremin doğru olduğunu, mantık adımlarıyla, su sızdırmaz biçimde göstermek. Diğer tarafta bilgisayar programları var: bir görevi yerine getiren, adım adım talimatlar. Bu ikisi, ilk bakışta birbiriyle alakasız iki dünya gibi görünür. Biri soyut hakikatle, diğeri pratik hesapla ilgilidir.

Ama $20.$ yüzyılın ortasında, mantıkçı Haskell Curry ve William Howard'ın (ve başkalarının) keşfettiği şaşırtıcı bir gerçek, bu iki dünyanın aslında aynı yapının iki farklı dili olduğunu gösterdi. Bu derin bağlantıya Curry-Howard bağıntısı denir ve bazen "ispatlar programlardır, önermeler tiplerdir" diye özetlenir.

Sözlük: İki Dünya Arasındaki Çeviri

Curry-Howard bağıntısının özü, mantık ile programlama arasında kusursuz bir sözlük kurmasıdır. Bir taraftaki her kavram, diğer tarafta tam bir karşılığa sahiptir:

• Bir önerme (kanıtlanacak matematiksel ifade), bir programlama dilindeki bir tipe (veri türüne) karşılık gelir.
• O önermenin bir ispatı, o tipte bir programa (ya da değere) karşılık gelir.
• Bir önermeyi kanıtlamak, o tipte çalışan bir program yazmakla aynı şeydir.

Bunu somut bir benzetmeyle düşünelim. "Eğer A doğruysa, B de doğrudur" şeklindeki bir mantıksal ifadeyi (A'dan B çıkarımı) ele alın. Programlama dilinde bunun karşılığı, "A tipinde bir girdi alıp B tipinde bir çıktı veren bir fonksiyon"dur. Bu çıkarımı kanıtlamak — yani "A verildiğinde B'ye nasıl ulaşırız?" sorusunu yanıtlamak — tam olarak böyle bir fonksiyon inşa etmek demektir. Mantıktaki "çıkarım", programlamadaki "fonksiyon"un ta kendisidir.

Benzer şekilde, mantıktaki "ve" bağlacı, programlamadaki "bir veri çiftine" (iki şeyi bir arada tutan yapıya) karşılık gelir; "veya" bağlacı, "iki seçenekten biri" türüne karşılık gelir. Mantığın her parçası, hesaplamanın bir parçasıyla eşleşir.

İspat = Hesaplama

Bu bağıntının en güzel yanı, sadece bir benzetme olmamasıdır; birebir, yapısal bir eşdeğerliktir. Bir ispatı "sadeleştirmek" (gereksiz adımları temizlemek), tam olarak bir programı çalıştırmaya (hesaplamayı yapmaya) karşılık gelir. Yani bir matematiksel ispatı adım adım işlettiğinizde, aslında bir bilgisayar programını yürütüyorsunuzdur. İspatlamak ve hesaplamak, derinlemesine aynı eylemdir.

Bu, hem matematik hem bilgisayar bilimi için baş döndürücü bir içgörüdür. "Doğruluk" (bir teoremin geçerliliği) ile "hesaplama" (bir programın çalışması), aynı madalyonun iki yüzü çıkar.

Pratik Güç: İspat Asistanları

Bu soyut bağıntı, bugün son derece pratik bir teknolojinin temelidir: ispat asistanları (proof assistants). Bunlar, Coq, Lean ve Agda gibi yazılımlardır ve şu olağanüstü işi yaparlar: bir matematiksel teoremi, bir bilgisayar programı yazar gibi bilgisayara yazdırırsınız ve bilgisayar, ispatın her adımının doğru olup olmadığını mekanik olarak kontrol eder.

Curry-Howard sayesinde bu mümkündür: madem ispat bir programdır, bilgisayar bir programı denetler gibi ispatı da denetleyebilir. Bunun sonuçları devrim niteliğindedir:

• Mutlak kesinlik: İnsan matematikçiler bazen ispatlarında gözden kaçan hatalar yapar. Bir ispat asistanı, mantığın tek bir adımının bile eksik ya da yanlış olmasına izin vermez. Bu sayede, son derece karmaşık teoremler (ünlü Dört Renk Teoremi ve bazı dev modern ispatlar gibi) bilgisayarla kusursuz biçimde doğrulanmıştır.
• Güvenilir yazılım: Aynı fikir tersine de çalışır — kritik yazılımların (örneğin uçak ya da tıbbi cihaz kontrol sistemleri) "doğru çalıştığını" matematiksel bir teorem gibi kanıtlamak için kullanılır. Program ile ispat aynı şey olduğundan, programın doğruluğunu kanıtlamak doğal hâle gelir.

Daha Derin Bir Birlik

Curry-Howard bağıntısı, matematiğin en sevilen temalarından birinin çarpıcı bir örneğidir: görünüşte ayrı alanların altında yatan gizli birlik. Mantık, hesaplama ve hatta belirli geometrik yapılar (kategori teorisi aracılığıyla), aslında aynı derin gerçekliğin farklı görünümleri olarak ortaya çıkar. Bu üçlü bağa bazen "Curry-Howard-Lambek" yazışması denir ve modern teorik bilgisayar biliminin felsefi kalbinde durur.

Curry-Howard bağıntısı, matematik ile bilgisayar biliminin sandığımızdan çok daha derin bir akrabalık taşıdığını gösterir. Bir teoremi kanıtlamak ile bir program yazmak — biri kâğıt üstünde soyut hakikat, diğeri makinede pratik hesap gibi görünen bu iki eylem — aslında tek ve aynı şeydir. Bu içgörü, sadece felsefi bir güzellik değil; bugün matematiğin en zorlu ispatlarını doğrulayan ve en kritik yazılımları güvenli kılan teknolojinin temelidir. Bazen iki ayrı dünya sandığımız şeyler, tek bir dilin iki lehçesi çıkar.