1 puan yazan GN⁺ 2024-11-05 | 1 yorum | WhatsApp'ta paylaş
  • Alonzo Church, Alan Turing kadar kamuoyunda tanınmasa da λ-calculus ve hesaplanabilirlik kuramıyla bilişimin mantıksal temellerini atan bir mantıkçıydı
  • 1936 tarihli Church-Turing thesis, etkin biçimde hesaplanabilir bir fonksiyonun Turing machine ya da ona eşdeğer bir sistemle hesaplanabileceği çerçevesini sundu
  • Hilbert’in Entscheidungsproblem’ine, tüm matematiksel önermeleri karara bağlayan kesin bir algoritmanın bulunmadığı yanıtını vererek hesaplamanın sınırlarını netleştirdi
  • Princeton’da Stephen Kleene, J. Barkley Rosser, Alan Turing gibi isimlere danışmanlık yaptı; Turing, Church’ün danışmanlığında Ph.D.’sini tamamladı
  • Onun soyut çalışmaları, modern derleyicilerden yorumlayıcılara, fonksiyonel programlamadan akıllı telefon uygulamalarına ve yapay zekâya uzanan hesaplama soy zincirinde yaşamaya devam ediyor

Popüler şöhretinden daha büyük teorik etki

  • Alan Turing, Turing Test nedeniyle bilişim ve yapay zekânın popüler tarihinde daha sık anılsa da Church, Turing’in düşüncesi ve çalışmaları üzerinde büyük etkisi olan bir isimdi
  • Hesaplamanın ne olduğunu anlamada ve yapay zekâyı değerlendirmeye yönelik kavramları şekillendirmede Church’ün çalışmaları önemli bir temel oluşturdu
  • Church’ün katkıları olmasaydı, yapay zekâya ve onu değerlendirme biçimlerimize ilişkin bugünkü kavramlar da oldukça farklı olabilirdi

Yaşamı ve akademik eğilimi

  • Church, 14 Haziran 1903’te Washington, D.C.’de doğan, sakin ve az konuşan bir mantıkçıydı
  • Çocukken yaşadığı bir havalı tüfek kazası nedeniyle bir gözünü kaybettiğine ya da görme yetisini kısmen yitirdiğine dair kayıtlar var
  • 1920’de Connecticut’taki preparatory school’u bitirdikten sonra aynı yıl Princeton’da lisans eğitimine başladı ve 1927’de doktora programını tamamladı
  • Harvard, Göttingen ve Amsterdam’da National Research Fellow olarak zaman geçirdikten sonra Princeton’a döndü ve akademik başarılarının büyük bölümünü burada ortaya koydu
  • Düzenli tahta yazısıyla ve titiz kişiliğiyle tanınıyordu; önemli makaleleri korumak için üzerlerini Duco cement ile kapladığı bile olurdu

λ-calculus ve hesaplanabilirlik

  • Church’ün en derin katkısı, bilgisayar bilimi adı ortaya çıkmadan önce onun temelini oluşturan λ-calculus oldu
  • Church, 1936’da teorik bilgisayar biliminin temel kavramlarından Church-Turing thesis’i formüle etti
    • Etkin biçimde hesaplanabilir bir fonksiyonun Turing machine ya da ona eşdeğer bir sistemle hesaplanabileceğini söyler
    • Bir makinenin teorik olarak neler yapabileceğini anlamak için bir çerçeve sağlar
    • Algoritmik prosedürlerin ulaşabileceği sınırları da ortaya koyar
  • Bu tez temel bir kavramdır; ancak ‘effective computability’nin yorumu, fiziksel hesaplama ve insan zekâsının doğası etrafındaki tartışmalar ve sınırlamalar da varlığını sürdürür
  • Turing, mekanik prosedürleri mantıksal bir biçime aktaran Turing machine’i önerdiyse, Church bu tür makineleri teorik olarak destekleyen saf soyutlamayı sağladı

Modern programlama ve fonksiyonel düşünce

  • λ-calculus’un etkisi bugün program yazma ilkelerinde de görülür; bileşim, yüksek dereceli fonksiyonlar ve değişmezliği vurgulayan yaklaşımlarla bağlantılıdır
  • Bu biçimsel sistem, soyut matematik problemlerinin kodlanıp mekanik olarak çözülebilmesini sağladı ve modern derleyici ile yorumlayıcı mimarilerinin temeli oldu
  • Modern programcılar için λ-calculus, Lisp, Haskell, Python ya da JavaScript’in bazı paradigmalarında görülebilen iç içe fonksiyon kümeleri gibi görünebilir
  • λ-calculus’un soyutlaması, fonksiyonları first-class citizen olarak ele alan fonksiyonel programlamanın temelini oluşturdu

Entscheidungsproblem ve hesaplamanın sınırları

  • Church, mantık ve felsefenin başka alanlarına da önemli katkılar yaptı; bunun başlıca örneklerinden biri Entscheidungsproblem üzerine çalışmasıdır
  • Entscheidungsproblem, David Hilbert’in 1928’de ortaya attığı karar problemiydi; herhangi bir matematiksel önermenin doğru olup olmadığını belirleyebilecek kesin bir algoritmanın var olup olmadığını soruyordu
  • Church, böyle bir algoritmanın var olmadığı yönünde olumsuz bir yanıt verdi; bu sonuç Church's Theorem olarak bilinir
  • Bu keşif, karar kuramı üzerinde derin etki yarattı ve yalnızca hesaplamayla başarılabilecek şeylerin sınırlarını vurguladı

Princeton’ın entelektüel merkezi ve öğrencileri

  • Church, döneminin önemli mantıkçılarına ve bilgisayar bilimcilerine danışmanlık yapan bir mentordu
  • Akademik soy ağacında Stephen Kleene, J. Barkley Rosser ve Alan Turing yer alır
  • Turing, Princeton’da Church’ün danışmanlığı altında Ph.D.’sini tamamladı
  • David Kaplan’ın yeni lisansüstü öğrencilere Church’ün dersini almalarını önerdiği; ilgi alanları olmasa bile torunlarına anlatacakları bir deneyim olacağını söylediği aktarılır
  • 1930’ların Princeton’ı, John von Neumann, Kurt Gödel ve Church’ün bir arada bulunduğu, modern mantığın gelişiminde entelektüel bir merkezdi

Göze pek görünmeyen miras

  • Church, Turing, von Neumann ve Gödel gibi isimlerle aynı düzeyde popüler şöhrete ulaşamadı
  • Onun mirası, savaş dönemi şifre çözme kahramanlıkları ya da erken ölüm trajedisi gibi kamusal hayal gücünü kolayca yakalayacak bir biçimde değildi
  • Akıllı telefonlarda çalışan milyarlarca programın mantığı, λ-calculus’un soyut fonksiyonlarına kadar izlenebilir
  • Basit uygulamalardan yapay zekâya kadar, hesaplamanın görünmez DNA’sı Church’ün çalışmalarından önemli bir soy hattı devralır
  • Church’ün dehası gösterişte değil, dünyayı değiştiren titiz yapılarda ve sessiz bir zarafette yatıyordu

1 yorum

 
GN⁺ 2024-11-05
Hacker News yorumları
  • Paradigms of Artificial Intelligence Programming’de (PDF/EPUB: https://github.com/norvig/paip-lisp) anlatılan lambda adının kökeni hoşuma gitti
    Hikâyeye göre Alonzo Church, Russell ve Whitehead’in Principia Mathematica gösteriminde bağlı değişkenin üzerine yazılan şapka işaretini x̂(x + x), tek boyutlu bir dizeye dönüştürmek için ^x(x + x) gibi öne aldı; boş şapka garip göründüğü için bunu büyük lambda Λx(x + x) ile değiştirdi, sonra da karışıklığı önlemek için küçük harf λx(x + x) oldu
    John McCarthy, Princeton’da Church’ün öğrencisiydi; 1958’de Lisp’i oluştururken o dönemin keypunch makinelerinde Yunanca harf bulunmadığından (lambda (x) (+ x x)) kullandı ve bu bugüne kadar kaldı
    Bu yüzden, bu yazının konusundaki gibi Church Lisp geriye dönük anlatılarında sık sık karşımıza çıkar; ancak bilişim tarihine neredeyse hiç ilgi duymayan kişiler için “unutulmuş” biri sayılabilir

    • Bu kökenin anlaşılması zor bir sembolden fazlasını ifade etmesini umuyordum, ama gerçekte öyle değil gibi
      Dana Scott’a göre Church bizzat bu seçimi “eeny, meeny, miny, moe” tarzı rastgele bir seçim olarak nitelemiş; Barendregt tarzı açıklamayı da yakın zamanda University of Birmingham’daki bir konuşmada çürüttüğü söyleniyor
      Fransızca konuşulan bölgelerde “personne lambda” sıradan kişi/anonim kişi anlamına geldiğinden anonim fonksiyonla iyi örtüşüyor gibi görünür; lambda sıfatı da “genel/sıradan” anlamına geldiği için Yunan alfabesinin ortalarındaki bir harfin ortalama olanı temsil ettiği hissi de var
      https://math.stackexchange.com/questions/64468/why-is-lambda...
    • “Lisp genelde anlamlı isimleri tercih eder” denir ama lambda dışında car/cdr de Yunanca harf olmasalar bile hiç de şeffaf isimler değil
    • PAIP, yapay zeka konusunun kendisi epey eskimiş olsa da genel olarak harika bir kitap
      Programlamanın birçok konusunu ele alıyor ve fonksiyonel programlamaya çok maruz kalmamış kişiler için yabancı gelebilecek paradigmaları da açıyor
    • Alonzo Church’ün lambda gösteriminin kökenine dair bu tekrarlanan hikâyenin doğru olup olmadığı net değil
      Church’ün belirli bir anlamdan çok Yunan harfleri arasından rastgele bir seçime yakın olduğunu ima ettiği başka örnekler https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_... adresinde var
    • lambda calculus terimini ilk kimin ortaya attığını merak ediyorum
      Bunun McCarthy’nin Lisp’e başlamasından önce mi sonra mı olduğunu da merak ediyorum
  • “Church’ün lambda calculus’u ile Turing makinesi eşdeğer hesaplama gücüne sahiptir, ancak Turing makinesinin değiştirilebilir durum kullanması bakımından ayrılır. Bugün bile fonksiyonel diller ile imperatif diller arasında bir yarık olmasının nedeni Church ile state’in ayrılmasıdır
    Bu alıntıyı uzun zamandır biliyorum ama asıl kaynağını bulamadım
    Düzenleme: Guy Steele’in “Dilin fonksiyonel/lambda calculus kısmı ile yan etki oluşturan kısmını birbirine karıştırmak istemeyen insanlar var. Görünüşe göre Church ile state’in ayrılmasına inanıyorlar” sözünden geliyor olabilir

    • Guy’ın bu alıntısı, 2001 Lightweight Languages Workshop sonrasında MIT posta listesinde geçen bir yazışmadan
      Orijinal arşiv burada: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
    • Niklaus Wirth adıyla ilgili espri de aklıma geliyor
      Espri şu: Avrupalılar adını genelde doğru şekilde “Nick-louse Veert” diye telaffuz eder, Amerikalılar ise bunu “Nickel's Worth”e çevirip berbat eder
      Yani Avrupalılar ona adıyla, Amerikalılar ise değeriyle seslenir
      https://en.m.wikiquote.org/wiki/Niklaus_Wirth
    • Peter Norvig tarafından çıkmış gibi. Kardeş yoruma bakmak yeterli
  • Church hakkında gerçekten şaşırtıcı bir yazı okumak istiyorsanız Rota’nın anılarını öneririm
    https://www34.homepage.villanova.edu/robert.jantzen/princeto... adresindeki ilk bölüm
    İlgili bağlantılar arasında Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - Ağustos 2016 ve Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - Şubat 2015 var

    • Rota’nın anıları yalnızca Church bölümü değil; tüm web sayfası, yani “Fine Hall in its golden age: Remembrances of Princeton in the early fifties” bütünüyle onun Indiscrete Thoughts kitabından bir bölüm
      Kitabın tamamı okunmaya değer
  • Onun adını taşıyan Alonzo programlama dili neredeyse unutuldu
    https://dl.acm.org/doi/pdf/10.1145/68127.68139

  • Özellikle Frege ve Russell’ın çalışmalarını devam ettiren mantık felsefesi ile anlam/gönderim kuramı büyük ölçüde unutuldu.
    Church bu konuda çok sayıda makale yayımlamış olsa da Wikipedia gibi yerlerde neredeyse hiç ele alınmıyor.
    Yine de Stanford Encyclopedia of Philosophy maddesi biraz daha iyi: https://plato.stanford.edu/entries/church/
    Ancak onun da Church’ün başlıca çalışmalarının bir kısmını kaçırdığını duydum; muhtemelen matematikçiler için fazla felsefi, filozoflar içinse fazla teknikti.

    • Bununla bağlantılı olarak E.J. Lemmon, Beginning Logic’te önemli mantık kitaplarını sıralarken Church’ün Introduction to Mathematical Logic kitabının 0. bölümünün tüm filozoflar tarafından birkaç kez okunmaya değer olduğunu yazmıştı.
  • Asıl konu bu değil ama blog yazılarında yapay zeka üretimi illüstrasyonlar kullanma konusunda biraz daha ölçülü olunmasını isterdim.
    Church’ün gerçek fotoğrafları kamu malı olarak da mevcutken, bu illüstrasyon ona pek benzemiyor ve yazı popülerlik kazandıkça şimdiden görsel arama sonuçlarında görünmeye başladı.
    Beş dakikadan fazla üretmeye değmeyecek türden bir illüstrasyonsa, bence hiç koymamak daha iyi olabilir.
    Yine de mutlaka “AI” üretimi bir görsel kullanılacaksa, en azından buna dair bir altyazı eklenmeli.

    • Uyarı için teşekkürler, kusura bakmayın.
      İnternetten fotoğraf almak içime sinmedi; bu görsel, “sahte” bir benzerlik olmasın diye 7. denemede ürettiğim sonuçtu ve bir ölçüde benzediğini hissetmiştim.
      JvN görseli oldukça iyi çıktı, ama bundan sonra insan gibi görünen sahte benzerlikler yerine sembolik görseller kullanmak daha doğru olacak.
  • “Bilgisayar zekasının tasarımcısı” ifadesi biraz abartılı görünüyor.
    Church’ün çok iyi bir mantıkçı olduğu doğru, ama burada bilgisayar zekasıyla AI/ML kastediliyorsa katkısı fiilen yok.
    Ayrıca lambda kalkülüsünün gerçekten matematik olup olmadığından da emin değilim; daha çok zekice bir gösterime benziyor.
    Gösterimin avantajları öznel; Church’ün, fikrinin belirli programlama dili tasarımlarına ilham vermiş olmasına pek ilgi duymamış olması da ilginç.

    • “Lambda calculus” bazen basit tipli lambda kalkülüsü anlamına gelir; bu da çoğunlukla basit tipler teorisini (STT), yani “Church’ün tipler teorisi”ni ifade eder.
      STT sık sık yüksek mertebeli mantıkla da özdeşleştirilir; çünkü temel “nesneler” ve T/F doğruluk değerleri olmak üzere iki ilkel tip ve yalnızca (a --> b) fonksiyon tipiyle her türlü mantıksal nesne ifade edilebilir.
      STT açıkça Church’ün icadıdır; modern tip teorileri üzerinde büyük etkisi olmuş, Haskell gibi karmaşık tip sistemlerine sahip programlama dillerini de etkilemiştir.
  • Tam olarak kanıtlayamam ama sezgisel olarak Turing ve onun temsil ettikleri AI tarafında sonunda yüksek değer görürken, Church için bunun tersi geçerliymiş gibi geliyor.
    İlki saflıktan, mümkün olan asgari koşullardan, soyut ve “saf” hesaplamadan yola çıktı; ikincisi ise fiilen nasıl düşünebildiğimizle ilgileniyordu ve uygulamadan çok ifade ve soyutlamanın genişletilmesine önem vermiş gibiydi.

    • Bir bakış açısından Turing savaş sırasında pratik bilgisayarlar yaptı; ancak daha sonra kendi hükümeti tarafından bilgisayar yapmaya devam etmesi engellendi ve teoriye çekilmek zorunda kaldı.
      Church’ün bilgisayar pratiği deneyimi yoktu ve daha çok matematik teorisinin kendisini genişletmeye yakındı.
      İkisinin işbirliği ve Atlantik’in iki yakası arasındaki iletişimi, pratik ile teoriyi birleştirerek zorunlu/işlevsel ikiliği, Church-Turing teoremi, durma problemi ile Church teoremi arasındaki ilişki gibi temel teorileri sağlamlaştırdı.
      Bunu bir rekabet olarak görmek yanlıştır; bilgisayar biliminin “iki babası” olduğunu söylemek birçok nedenle yerindedir.
      Özellikle Turing’in ölümü düşünüldüğünde bu daha da böyledir.
      Ayrıca Turing’in uygulamayla ilgilenmediği de doğru değildir; gerçek uygulamaya dönmek istiyordu ama buna izin verilmediği gerçeği atlanmamalıdır.
      Britanya hükümetinin gizlilik sınıflandırması farklı olsaydı nelerin değişeceği büyük bir trajedi ve soru olarak kalıyor; ama öyle olsaydı, kendi zaman çizgimizde teoriyi bu kadar iyi pekiştiren Church ile işbirliğini de kaybetmiş olabilirdik.
  • 1982 Ağustos’unda CMU’da düzenlenen ACM Symposium on LISP and Functional Programming’de Alonzo Church ve Haskell Curry ile tanışabilmiş olmak büyük şanstı.
    Curry’nin sağlığının iyi olmadığı açıktı ve konferanstan yaklaşık iki hafta sonra hayatını kaybetti; ama Church sağlıklı görünüyordu ve sonrasında yaklaşık 13 yıl daha yaşadı.
    Resepsiyonda Gerry Sussman’ın odada dolaşıp ikisini tanıtırken çok heyecanlı olduğu belliydi; bizim için de onlarla tanışmak büyük bir heyecandı.

  • Church’ün büyük katkılarından biri de öğrencileriydi.
    Tek bir yerden şaşırtıcı sayıda büyük düşünür çıktı.