Catalog

10 Akademi 27 Eylül 2017 Çarşamba Bilgisayar felsefi bir sorunu çözmek için icat edildi Chris Stephenson Hayatımızda büyük pratik önem taşıyan bilgisayar, felsefi bir sorunu çözmek için icat edildi. Bilgisayar çok pratik bir alet olarak düşünülüyor fakat “pratik insanlar” bilgisayarın önemini kavramakta hep zorlandılar. Kapitalist dünyada teori aşağılanıyor, pratik yüceltiliyor. “Sadece bir teori” lafı hep dilimizde. Sanki teori hayatımızda anlamsız bir hobi gibi. Çözülmek istenen felsefi sorunu anlamak için azıcık matematik tarihini incelemek lazım. l Leıbnız’in rüyası 17. yüzyıl Alman matematikçisi (ve hesap makinesinin mucidi) Gottfried Leibniz’in rüyası, bütün insanlığın bilgisini sembolik hale getirmekti. Yani bugün bildiğimiz bilgisayar kayıtları ya da matematiksel bir formül gibi. Amacı her bilimsel tartışmayı, hesap makinesi kullanarak “kimin haklı olduğunu görmek için vakit kaybetmeden hesaplamak”tı. Leibniz, tartışılmaz bir mutlak doğru peşindeydi. lDavıd Hılbert’in sorunları 1900’de, Paris’te bir kongrede, Al man matematikçi David Hilbert, “yeni yüzyılda çözülecek 23 önemli matematiksel sorun” ortaya koydu. Bu 23 sorunun ikincisi “aritmetiğin çelişkisizliğini ispat etmek” idi. Yani sorulan soru şuydu: Matematiğin doğru olup olmadığını nasıl bilebiliriz? Felsefi bir sorun. Hilbert, Leibniz’in rüyasını paylaşıyordu. Matematiği tamamen sembolik hale getirmek ve bütün teoremleri belli mantık kuralları uygulayarak sonlu yöntemlerle sonlu bir aksiyom1 (prensip) setinden çıkartmak istiyordu. Bu yaklaşımın zor noktası şudur: Alıştığımız mantık yöntemlerini kullanarak bir teorem ve onun tersini ispat edebilirsek, hiçbir şeyin anlamı kalmıyor. Aritmetik için çeşitli aksiyomatik sistemler kurulmuştu. Hilbert böyle aksiyomatik sistemlerin çelişkisiz olduklarını gösteren bir ispat istedi. Alonzo Church (1903–1995) ABD’li matematikçi ve mantıkçı. Teorik bilgisayar biliminin temellerine katkısıyla bilinir. Böyle bir çelişkinin nasıl bir şey olabileceğini anlayabilmek için şöyle bir şey düşünelim: “Mahallede kendilerini tıraş etmeyen erkekler, (erkek) berber tarafından tıraş ediliyor.” Ardından “berberi kim tıraş eder” sorusuna cevap vermeye çalışalım. Eğer kendisini tıraş etmiyorsa, berber (yani kendisi) tarafından tıraş ediliyor. Yani “berber, berberi tıraş ediyor” ve “berber, berberi tıraş etmiyor” önermelerinin ikisi de doğru oluyor. Matematiksel bir sistemde böyle bir önerme ilginç bir bilmece değil, bir felaket olur. Sembolik halde ifade edilen benzer bir çelişki, Gottlob Frege’nin aksiyomatik sistemini çökertti. Frege’nin sistemindeki çelişkiyi bulan Bertrand Russell, çelişkisiz bir sistem kurmaya çalıştı. Hilbert’in sorusu böyle çözümlerin başarılı olup olmadığının ispat edilmesini istiyordu. 1928’de Hilbert, matematiğin temelleriyle ilgili bir sorun daha ortaya koydu. Aksiyomatik bir matematiksel sistemde yazılabilen bir cümlenin ispatının olup olmadığını tespit etmek için efektif bir yöntem talep etti. Bu “karar sorunu” ya da Entscheidungsproblem, “efektif yöntem”in tarifini açık bıraktı. 1930’da Kurt Gödel, bildiğimiz tamsayı aritmetiği içeren bir aksiyomatik sistemde doğru ya da yanlış olduğu ispat edilemeyen cümleler ola cağını ispat etti. İkinci bir teoremle sistemin çelişkisizliğinin sistem içinde ispat edilemeyeceğini de ispat etti. Yani Hilbert’in sorusuna “böyle bir ispat olamaz” diye cevap verdi. Entscheidungsproblem daha da önem kazandı. Bunun çözümü varsa en azından ispat edilemeyen cümleleri bilip boşu boşuna uğraşmaktan kurtulurduk. Matematiğin son çaresi bu sorunu çözmek. l Church ve Turıng Princeton’dan Alonzo Church, Cambridge’ten Alan Turing başta olmak üzere bir dizi matematikçi bu “karar” sorunuyla uğraşmaya başladı. İlk işleri “efektif yöntem” için iyi bir tanım önermekti. Church ve Turing farklı birer öneride bulundu. Church’un önerisi, modern fonksiyonel programlama dillerine benzeyen Lambda Calculus, Turing’in önerisi ise modern bir bilgisayara benzeyen kavramsal bir makine idi. Hem Turing hem de Church, kendi “efektif yöntemler”ini referans alarak, Hilbert’in sorduğu soruya olumsuz bir cevap verdi. Böyle bir karar verilemeyeceğini ispat ettiler. Church’un makalesi daha önce yayımlandı. Geç kalmak 24 yaşındaki Turing için büyük bir hayal kırıklığı oldu. Turing’in doktora tezi danışmanı hemen Church’a yazıp durumu ?KİMDİR İstanbul Bilgi Üniversitesi’nde Türkiye’nin ilk Bilgisayar Bilimleri Bölümü’nün kurucu başkanı oldu. Üniversite dışında binlerce ortaokul ve lise öğrencisinin devam ettiği bilgisayar eğitim projeleri yürüttü. Nesin Matematik Köyü’nün düzenli hocasıdır. YÖK, barış imzacısı olmasını gerekçe göstererek Nisan 2017’de çalışma iznini iptal etti. 18 senelik işine son verildi. Çevirimiçi ve gayriresmi dersler vermeye devam ediyor. Verdiği dersler şuradan takip edilebilir: http://vimeo.com/ chrisstephenson. anlattı. Church, Turing’i Princeton’a davet etti. Church ve Turing rekabet etmek yerine beraber çalıştılar. Turing, Church’un Lambda Calculus’ü için bir dizi önemli sonuç çıkarttı. Church de Turing’in makinesini Turing Machine olarak vaftiz etti. Turing, Lambda Calculus için “daha zarif ve düzgün bir çözüm” yazdı. Church de Turing’in makinesi için “daha ikna edici” dedi. Daha da önemlisi her iki “efektif yöntem”in de aynı hesaplama gücüne sahip olduğunu ispat ettiler. Yani Lambda Calculus ile yapılabilen ve yapılamayan hesapların Turing Machine’inkilerle aynı olduğunu ispat ettiler. Bu ispatlar sırasında Turing iki önemli adım atmak zorunda kaldı. İlk önerdiği makine, hesap yapmak için sonsuz bir hafıza üzerinde çalışan, bir çeşit özel tasarımlı sonlu makine idi. Entscheidungsproblem ispatını yapmak için “Evrensel Makine”yi icat etti. Evrensel Makine herhangi bir sonlu makine tarifini hafızasından okuyup o makinenin yaptığını yapabilen bir makineydi. Bu da programlanabilen bir bilgisayar oldu. Turing, Lambda Calculus ve Turing Machine’in eşitliğini ispat etmek üzere kendi makinesi için Lambda Calculus cümlelerini >>