- Bağımlı tipler (type theory) ispat nesnelerini içerir, ancak yazar bunu gereksiz ve verimsiz bir yapı olarak değerlendiriyor
- Geçmişte AUTOMATH ve Martin-Löf biçimsel sistemi gibi bağımlı tiplere dayalı sistemleri doğrudan incelemiş olsa da, Isabelle zamanla genel amaçlı (generic) bir mantık çerçevesi olarak gelişti
- Basit tip kuramı (higher-order logic) temelli Isabelle/HOL, otomasyon, büyük ölçekli kütüphaneler ve okunabilirlik açısından güçlü yanlara sahip
- ALEXANDRIA projesi aracılığıyla yalnızca yüksek dereceli mantıkla bile ileri düzey matematiksel teoremlerin biçimselleştirilebildiği gösterildi
- Lean gibi bağımlı tip sistemleri olgunlaşmış olsa da, yazar performans sorunları ve karmaşıklık nedeniyle hâlâ yüksek dereceli mantık yaklaşımının pratikliğini tercih ediyor
Bağımlı tipler ve ispat nesneleri
- Bağımlı tip kuramında ispat nesneleri (proof objects) zorunludur, ancak yazar bunu alan israfı olarak görüyor
- LCF yapısında, yalnızca mantığın içinde değil, uygulama dilinin tür denetimi düzeyinde de geçerli ispat adımlarının çalıştırılması mümkün
- Robin Milner'in içgörüsüyle proof kernel kavramı ortaya çıktı ve bu Isabelle'in temelini oluşturdu
- Yazar, “bağımlı tipleri neden kullanmadınız?” sorusuna “uzun süre kullandım” diye yanıt veriyor
AUTOMATH deneyimi
- 1977'de Caltech'te N. G. de Bruijn'in AUTOMATH derslerini dinledi, ancak sistemi doğrudan kullanamadı
- Bunun nedeni o dönemde Eindhoven Üniversitesi sisteminin ARPAnet'e bağlı olmaması ve ALGOL 60 tabanlı bir bilgisayar gerektirmesiydi
- AUTOMATH bir bağımlı tip sistemi olsa da Curry–Howard eşlemesini gerçekleştirmiyordu
- Kullanıcının istediği mantığın sembollerini ve çıkarım kurallarını aksiyom olarak eklemesi gerekiyordu
- de Bruijn bunu “her türlü yemeği sunan büyük bir restoran”a benzetiyordu
- Isabelle bu fikri devralarak mantık çerçevesi olarak genellik arayışını sürdürdü
- Ancak de Bruijn küme kuramından nefret ediyor ve matematiği özünde tip temelli görüyordu
- Yazar, AUTOMATH'ın doğruluk denetimini sorduğunda de Bruijn ona dil kuramı üzerine 300 sayfalık bir kitap gönderdi, ancak bu tatmin edici olmadı
Martin-Löf tip kuramı
- Göteborg'daki Chalmers Üniversitesi'nde Martin-Löf tip kuramı üzerine çalışırken program sentezi olasılığına büyük ilgi duydu
- Heyting'in sezgici mantığı ilkelerini doğrudan gerçekleştirmesi nedeniyle bunu açık biçimde “doğru” buldu
- Yıllarca bu alanda çalıştı ve Isabelle'in ilk sürümünü Martin-Löf kuramı ile gerçekleştirdi
- Bu sürüm bugün hâlâ Isabelle/CTT olarak dağıtıma dâhil
- Ancak Per Martin-Löf merkezli dogmatik atmosfer ve zorla dayatılan içkin eşitlik (intensional equality) yönelimi nedeniyle bu araştırma çizgisi çöktü
- Daha sonra ortaya çıkan Calculus of Constructions (CoC), Rocq, Lean gibi sistemler de aynı soruları geride bıraktı
- CoC onlarca yıl boyunca çeşitli varyantlar ve isteğe bağlı aksiyomlarla şekillendi
Araştırma tercihleri ve Isabelle'in yönü
- Araştırmacılar, yeni bir biçimsel sistem geliştirmek ile mevcut sistemi genişleterek kullanmak arasında seçim yapmak zorunda
- Isabelle, çeşitli mantıkları kabul edebilen genelleştirilmiş bir çerçeve olarak tasarlandı
- 1985'te Mike Gordon, Church'ün basit tip kuramı ile donanım doğrulaması yaptı
- Ardından John Harrison, vektör boyutlarını kodlama yöntemini geliştirdi
- Isabelle/HOL, Church kuramına aksiyomatik type class'lar ve locale modül sistemi ekledi
- Lean topluluğu, CoC temeli üzerinde geniş kapsamlı matematik biçimselleştirmesi (mathlib) gerçekleştirdi
ALEXANDRIA projesi ve yüksek dereceli mantığın sınır testi
- ERC destekli ALEXANDRIA projesi, Isabelle'in otomasyon, kütüphane ve okunabilirlik yönlerini öne çıkardı
- Başta yüksek dereceli mantığın sınırlarına çarpılacağı düşünülüyordu, ancak pratikte Grothendieck şemaları gibi ileri matematik de başarıyla biçimselleştirildi
- Paulo Emílio de Vilhena ve Martin Baillon, her cismin cebirsel olarak kapalı bir genişlemeye sahip olduğunu kanıtladı
- Proje, Balog–Szemerédi–Gowers teoremi gibi ileri sonuçlara kadar genişledi
- “Bağımlı tipler olmadan matematik biçimselleştirmesi yapılamaz” iddiası ortadan kalktı; geriye yalnızca “bağımlı tipler daha temizdir” iddiası kaldı
Lean ve bağımlı tiplere dair güncel görüş
- Lean'in topluluk büyüklüğü ve Blueprint aracı kıskandırıcı olsa da, performans sorunları ve karmaşıklık sürüyor
- intensional equality ile yaşanan çatışmalar ve bağımlı tiplerin ne zaman kullanılacağına karar vermenin zorluğu tekrar tekrar bildiriliyor
- Yazar, bağımlı tipleri Tesla'nın Full Self-Driving sistemine benzeterek abartılı beklentilere ve pratikteki rahatsızlıklara dikkat çekiyor
Ek: yüksek dereceli mantığın kuramsal sınırları
- Bazıları yüksek dereceli mantığın ispat kuramı açısından zayıf olduğunu savunuyor, ancak bu yalnızca ZF küme kuramına kıyasla daha zayıf olduğu anlamına geliyor
- ALEXANDRIA sonuçlarına göre yüksek dereceli mantıkla da Grothendieck şemaları gibi karmaşık matematiksel yapılar ele alınabiliyor
- Yalnızca iki ispatta ZF aksiyomlarının eklenmesi gerekti; bunlar da ZF nesnelerine doğrudan atıfta bulunan teoremlerdi
Dipnot
- Sezgicilik, dili yalnızca bir kayıt aracı olarak gören bir felsefedir; bu, günümüzdeki yapıcı matematik (constructive mathematics) ile aynı şey değildir
1 yorum
Hacker News görüşü
Bağımlı tipler (dependent types) belirli durumlarda çok faydalıdır
Örneğin Python’ın “10×5 boyutunda float32 matris”i bir tip olarak ifade edip tip denetimi yapabilmesinin iyi olacağını düşünüyorum
Ancak Curry–Howard yazışması gibi, ispat ile tipi özdeşleştiren kavramlar insan açısından kafa karıştırıcıdır
Tip hataları yalnızca düzeltilebilir basit yanlışlar gibi gelirken, ispat hataları çok daha karmaşık ve düşünme gerektiren sorunlardır
Bu yüzden Lean’in asıl gücünün tip sisteminde değil, toplulukta ve mathlib’in açık kaynak yapısında olduğunu düşünüyorum
Isabelle’in AFP’si bir akademik dergi gibi işletilirken, Lean’de pull request tabanlı işbirliği daha aktiftir
Şu anda yeni bir teorem ispatlayıcısı olan Acorn’u(acornprover.org) geliştiriyorum ve Lean ile Isabelle’in güçlü yanlarını birleştirmeye çalışıyorum
Lean’in basit bağımlı tip ifade gücü iyi, ancak fazla derine inildiğinde debug etmek zorlaşıyor
Ancak yalnızca çalışma anında bilinen indeks aralığını derleme zamanında garanti etmek mümkün değildir
Gerçek bir bağımlı tip dili, çalışma zamanı hatalarını tip düzeyinde önleyebilir
Aslında bağımlı tip dillerinde bile çalışma zamanı hatalarını önlemek için bağımlı tiplerin kullanıldığı durumlar nadirdir,
daha çok veri yapısı değişmezleri veya program tanımından sonraki doğrulama için kullanılır
İlgili kaynaklar: division-by-zero in type theory FAQ, Xavier Leroy sunum slaytları
Örneğin bu kodun 38. satırındaki gibi matris boyutu tip olarak ifade edilebilir
Vektör tip tanımı ya da
matris çarpımı sonuç tipi de uygulanmış
Ancak bunlar kişisel proje düzeyinde denemeler; büyük ölçekli veri projeleri için uygun olmayabilir
Bu, Propositions as Types kavramıyla ilişkilidir
Bağımlı tiplerin çalışma anında nasıl davrandığını, hem derleme hem de çalışma zamanı tip denetiminin gerekip gerekmediğini merak ediyorum
Uygulamada dolaylı başvuruların artmasıyla gelen karmaşıklık oluşmaz mı diye düşünüyorum
Dr. Paulson’ın iddiası bağımlı tiplerin kötü olduğu değil, zorunlu olmadıklarıdır
Lean’in performans sorunları ya da intensional equality ile ilgili tartışmaların daha fazla ele alınması iyi olurdu
Isabelle’in HEq(bağlantı) benzeri, tanımsal eşitlik olmayan durumlar sorun çıkarır
Bu yüzden bağımlı tipleri mümkün olduğunca az kullanmanın daha iyi olduğunu düşünüyorum
ACL2 gibi statik tip içermeyen sistemlerde de yeterli doğrulama yapılabilir
Sonuçta önemli olan, pratiklik ile doğrulanabilirlik arasındaki dengedir
Lean veya Agda ise henüz endüstriyel ölçekte doğrulamada daha az kullanılmaktadır
Concrete Semantics(bağlantı) ile Logical Verification 2025(bağlantı) karşılaştırması da ilginç olabilir
Gerçekçi olarak bakıldığında refinement types daha pratik olabilir
Örnek: Rust Creusot, Dafny, LiquidHaskell’in leftpad ispat örneği
Ancak program doğrulamada “iki ispat aynıdır” gibi karmaşık yardımcı lemmalar gerekir ve bunlar çoğu zaman ispatlanamaz
Asıl önemli olan bir özelliğin ne kadar faydalı olduğudur; varlığının zorunlu olup olmaması değil
Sonuçta araç seçimi geliştirici tercihi ve verimlilik meselesidir
Modern mantık tartışmalarının önemli bir kısmının sonunda estetik tercihlere dayanması ilginç
Eğer pratik faydaları ezici ölçüde baskın olsaydı bu tartışmalar olmazdı
Bu arada Paulson ile Lamport’un 1999 tarihli “Typing in Specification Languages” makalesi iyi bir okuma olabilir
Sonrasında Lamport’un TLA+ örneğinde olduğu gibi gayriresmî formalizm de gelişti
Derleme zamanı güvenceleri gibi avantajlar elde edilirken, bunun bedeli karmaşıklık ve daha uzun build süreleridir
Sonuçta temel soru, “bu değiş tokuş buna değer mi”dir
HOL’ün (basit tip teorisi) sorunu bağımlılık değil, mantıksal gücünün yetersizliğidir
Bu, Zermelo küme teorisinin sınırlı bir sürümüne denktir ve modern matematiği bütünüyle formelleştirmek için zayıf kalır
Özellikle kategori teorisi (category theory) gibi alanlardaki boyut sorunlarını ele almak zordur
Bunun gerçek matematikçilerin çalışma tarzından ne kadar farklı olduğunu merak ediyorum
Örneğin ‘inaccessible cardinal’ eklemek, tip teorisindeki ‘universe’ kavramına benzer bir yapı sağlar
Ben formal methods alanında uzmanlaştım ve bağımlı tipleri havalı buluyordum, ama gerçek kullanım her zaman zorlu bir mücadele oldu
F# kullanırken F*’ı devreye almaya çalıştım, ancak ekip arkadaşlarım matematiksel öğrenme eğrisini göz korkutucu buldu
Sonunda matematik içeren araçları mühendislerin iyi öğrenmediği gibi alaycı bir sonuca vardım
SMT tabanlı constraint solving kullanarak hafif bağımlı tip kullanımı sağlar
Ama “bu gerçekten doğru mu” gibi felsefi sorulara cevap vermez
Matematiksel ispat ile yazılım doğrulama dünyaları oldukça farklıdır
Sonuçta zaman sınırlıdır
Şirketimiz Phosphor’da bağımlı tipleri veritabanı/graf sorgularıyla birleştirerek denemeler yapıyoruz
RDF’nin sınırlamalarını telafi ettik ve mantık tabanlı bir sorgu sistemi kurabildik
Pratikte ise TypeDB(typedb.com) kullanıyoruz; MongoDB’den daha hızlı ve karmaşık veri modelleme için faydalı
Bu, Palantir’in ontology kavramına da benziyor
Sonuçta bağımlı tiplerin sırrı, ne zaman kullanılmaması gerektiğini bilmekte yatıyor gibi görünüyor
Lean ya da Rocq’yu eleştirmekten çok, duruma göre Isabelle tarzı bir yaklaşımın da seçilebileceğini düşünüyorum
Paulson ekibinin Alexandria adlı formelleştirme projesi(bağlantı) etkileyici görünüyor
Özellikle kuantum hesaplama algoritmalarının formelleştirilmesi çalışması(makale bağlantısı) ilginç
Eskiden bağımlı tiplerin gelecek olduğuna inanıyordum, ancak gerçek projelerde üretkenlik kaybı büyüktü
Şimdi daha açık ve bakımı kolay çözümleri tercih ediyorum
Eğer ekip tarafından anlaşılabilen ve genişletilebilen bir araçsa, iyi araç odur
Ben tam bağımlı tiplerden ziyade, onların sınırındaki tip sistemlerini seviyorum
Örneğin Purescript, Haskell’den daha güçlü row-type desteğini yerleşik olarak sunuyor ve
tip düzeyinde listeler, string’ler ve regex’leri de destekliyor
Bunlar typeclass tabanlı mantık programlama yaklaşımı içinde kullanılabiliyor