Matematik Kanıtlarını ve Bilgisayar Programlarını Eşitleyen Deep Link | Quanta Dergisi

Bazı bilimsel keşifler önemlidir çünkü yeni bir şeyi ortaya çıkarırlar; örneğin DNA'nın çift sarmal yapısı veya kara deliklerin varlığı. Ancak bazı açıklamalar derindir çünkü bir zamanlar farklı sanılan iki eski kavramın aslında aynı olduğunu gösterirler. James Clerk Maxwell'in elektrik ve manyetizmanın tek bir olgunun iki yönü olduğunu veya genel göreliliğin yerçekimini eğri bir uzay-zamanla ilişkilendirdiğini gösteren denklemlerini ele alalım.

Curry-Howard yazışmaları da aynı şeyi yapıyor, ancak daha büyük ölçekte, yalnızca bir alandaki ayrı kavramları değil, tüm disiplinleri birbirine bağlıyor: Bilgisayar Bilimleri ve matematiksel mantık. Curry-Howard izomorfizmi (iki şey arasında bire bir benzerlik olduğu anlamına gelen bir terim) olarak da bilinen bu terim, matematiksel kanıtlarla bilgisayar programları arasında bir bağlantı kurar.

Basitçe ifade etmek gerekirse, Curry-Howard yazışmaları, bilgisayar bilimindeki iki kavramın (türler ve programlar) sırasıyla önermelere ve kanıtlara, yani mantıktaki kavramlara eşdeğer olduğunu öne sürmektedir.

Bu yazışmanın bir sonucu da, genellikle kişisel bir zanaat olarak görülen programlamanın idealleştirilmiş matematik düzeyine yükseltilmesidir. Bir program yazmak sadece “kodlama” değildir, bir teoremi kanıtlama eylemi haline gelir. Bu, programlama eylemini resmileştirir ve programların doğruluğu hakkında matematiksel olarak akıl yürütmenin yollarını sağlar.

Yazışma, onu bağımsız olarak keşfeden iki araştırmacının adını almıştır. 1934 yılında matematikçi ve mantıkçı Haskell Curry, matematikteki fonksiyonlar ile mantıktaki iki önerme arasındaki "eğer-o halde" ifadeleri şeklini alan çıkarım ilişkisi arasında bir benzerlik fark etti.

Curry'nin gözleminden ilham alan matematik mantıkçısı William Alvin Howard, 1969'da hesaplama ile mantık arasında daha derin bir bağlantı keşfetti; bu, bir bilgisayar programını çalıştırmanın mantıksal bir kanıtı basitleştirmeye çok benzediğini gösterdi. Bir bilgisayar programı çalıştığında, her satır tek bir çıktı elde etmek için "değerlendirilir". Benzer şekilde, bir ispatta, basitleştirebileceğiniz karmaşık ifadelerle başlarsınız (örneğin gereksiz adımları ortadan kaldırarak veya karmaşık ifadeleri daha basit ifadelerle değiştirerek) bir sonuca varıncaya kadar - birçok ara ifadeden türetilen daha yoğun ve özlü bir ifade. .

Bu açıklama, yazışmanın genel bir anlamını aktarsa ​​da, bunu tam olarak anlamak için bilgisayar bilimcilerinin "tip teorisi" dediği şey hakkında biraz daha fazla şey öğrenmemiz gerekiyor.

Ünlü bir paradoksla başlayalım: Bir köyde, kendisini tıraş etmeyen tüm erkekleri ve sadece onları tıraş eden bir berber yaşar. Berber kendini tıraş eder mi? Cevap evet ise, kendisini tıraş etmemelidir (çünkü yalnızca kendisi tıraş olmayan erkekleri tıraş eder). Cevap hayırsa, kendini tıraş etmesi gerekir (çünkü kendisi tıraş olmayan tüm erkekleri tıraş eder). Bu, Bertrand Russell'ın kümeler adı verilen bir kavramı kullanarak matematiğin temellerini oluşturmaya çalışırken keşfettiği paradoksun gayri resmi bir versiyonudur. Yani, kendisini içermeyen tüm kümeleri içeren bir kümeyi çelişkilerle karşılaşmadan tanımlamak imkansızdır.

Russell, bu paradoksu önlemek için "tipleri" kullanabileceğimizi gösterdi. Kabaca söylemek gerekirse bunlar, belirli değerlerine nesne adı verilen kategorilerdir. Örneğin, doğal sayılar anlamına gelen "Nat" adında bir tür varsa, nesneleri 1, 2, 3 vb.'dir. Araştırmacılar genellikle bir nesnenin türünü belirtmek için iki nokta üst üste kullanırlar. Tam sayı türünden 7 sayısı “7: Tamsayı” şeklinde yazılabilir. A tipi bir nesneyi alıp B tipi bir nesneyi ortaya çıkaran veya A tipi ve B tipi bir nesne çiftini "A × B" adı verilen yeni bir türde birleştiren bir fonksiyona sahip olabilirsiniz.

Bu nedenle paradoksu çözmenin bir yolu bu türleri bir hiyerarşiye yerleştirmektir, böylece yalnızca kendilerinden "düşük seviyedeki" unsurları içerebilirler. O zaman bir tür kendisini içeremez, bu da paradoksu yaratan kendine referans verme durumunu ortadan kaldırır.

Tip teorisi dünyasında, bir ifadenin doğru olduğunu kanıtlamak alışık olduğumuzdan farklı görünebilir. 8 tam sayısının çift olduğunu kanıtlamak istiyorsak, o zaman mesele 8'in gerçekten de "Çift" adı verilen belirli bir türde nesne olduğunu göstermektir; burada üyelik kuralı 2'ye bölünebilirdir. 8'in bölünebilir olduğunu doğruladıktan sonra 2'ye göre 8'in gerçekten de Even türünden bir "sakin" olduğu sonucuna varabiliriz.

Curry ve Howard, türlerin temelde mantıksal önermelere eşdeğer olduğunu gösterdi. Bir fonksiyon bir tipte "yerleştiğinde", yani o tipte bir nesne olan bir fonksiyonu başarılı bir şekilde tanımlayabildiğinizde, karşılık gelen önermenin doğru olduğunu etkili bir şekilde göstermiş olursunuz. Dolayısıyla, A tipi bir girdi alan ve A → B tipi olarak gösterilen B tipi bir çıktı veren işlevler şu sonuca karşılık gelmelidir: "Eğer A ise, o zaman B." Örneğin, "Yağmur yağıyorsa yer ıslaktır" önermesini ele alalım. Tip teorisinde bu önerme, "Raining → GroundIsWet" tipindeki bir fonksiyonla modellenecektir. Farklı görünen formülasyonlar aslında matematiksel olarak aynıdır.

Bu bağlantı kulağa ne kadar soyut gelse de, yalnızca matematik ve bilgisayar bilimi uygulayıcılarının çalışmaları hakkındaki düşüncelerini değiştirmekle kalmamış, aynı zamanda her iki alanda da çeşitli pratik uygulamalara yol açmıştır. Bilgisayar bilimi için, yazılımın doğruluğunu sağlama süreci olan yazılım doğrulaması için teorik bir temel sağlar. Programcılar, istenen davranışları mantıksal önermeler çerçevesinde çerçeveleyerek, bir programın beklendiği gibi davrandığını matematiksel olarak kanıtlayabilirler. Ayrıca daha güçlü işlevsel programlama dilleri tasarlamak için güçlü bir teorik temel sağlar.

Ve matematik için yazışmalar şunun doğuşuna yol açmıştır: ispat yardımcılarıetkileşimli teorem kanıtlayıcıları olarak da adlandırılır. Bunlar, Coq ve Lean gibi resmi kanıtların oluşturulmasına yardımcı olan yazılım araçlarıdır. Coq'da ispatın her adımı aslında bir programdır ve ispatın geçerliliği tip kontrol algoritmaları ile kontrol edilir. Matematikçiler aynı zamanda ispat yardımcılarından da faydalanıyor; özellikle de Yalın teoremi kanıtlayıcı - matematiksel kavramların, teoremlerin ve kanıtların kesin, bilgisayarla doğrulanabilir bir formatta temsil edilmesini içeren matematiği resmileştirmek. Bu, bazen resmi olmayan matematik dilinin bilgisayarlar tarafından kontrol edilmesine olanak tanır.

Araştırmacılar hâlâ matematik ve programlama arasındaki bu bağlantının sonuçlarını araştırıyorlar. Orijinal Curry-Howard yazışması, programlamayı sezgisel mantık adı verilen bir tür mantıkla birleştiriyor, ancak daha fazla mantık türünün de bu tür birleştirmelere uygun olabileceği ortaya çıktı.

"Curry'nin öngörüsünden bu yana geçen yüzyılda yaşanan şey, 'mantıksal sistem X'in hesaplamalı sistem Y'ye karşılık geldiği' giderek daha fazla örneği keşfetmeye devam etmemizdir" dedi. Michael ClarksonCornell Üniversitesi'nde bilgisayar bilimcisi. Araştırmacılar programlamayı halihazırda "kaynaklar" kavramını içeren doğrusal mantık ve olasılık ve zorunluluk kavramlarını ele alan modal mantık gibi diğer mantık türleriyle ilişkilendirdiler.

Ve bu yazışmalar Curry ve Howard'ın isimlerini taşısa da, bunu keşfedenlerin yalnızca onlar olmadığı kesindir. Bu, yazışmaların temel niteliğini kanıtlıyor: İnsanlar bunu tekrar tekrar fark etmeye devam ediyor. Clarkson, "Hesaplama ve mantık arasında derin bir bağlantı olması tesadüf değil gibi görünüyor" dedi.