2 puan yazan GN⁺ 2024-08-05 | 1 yorum | WhatsApp'ta paylaş
  • “Turing-complete değilse güvenlidir” türü tartışmalar matematiksel anlamla uyuşmaz; Turing-tam olmama, sonlanma, determinizm ve sandboxing gibi pratik özelliklerden büyük ölçüde bağımsızdır
  • Çalışma süresi girdiye bağlı bir ilkel özyinelemeli fonksiyon ile sınırlanan Turing Machine hesaplamaları, ilkel özyinelemeli fonksiyon olarak da yeniden yazılabilir
  • İlkel özyinelemeli fonksiyonlar her zaman sonlanır; ancak 2^(2^N) gibi hızla büyüyen fonksiyonlar da oluşturabildiğinden, sonlanma garantisi pratik çalışma süresi anlamına gelmez
  • Pratikte hiç durmayan programlarla milyarlarca yıl sonra biten programlar benzer sorunlar yaratır; Turing-complete diller de bir adım sayacı ile zorla durdurulabilir
  • Bir yapılandırma dilinin kalitesi, Turing-complete olup olmamasından çok determinizm, net semantik, saflık, güvenlik/sandboxing, çalışma süresi kontrolü ve basitliğe bağlıdır

Turing-completeness tartışmalarındaki temel yanlış anlama

  • İnternetteki programcılar, belirli alanlarda “Turing-complete olmamayı” sık sık bir avantaj ya da gereksinim gibi dile getirir
  • Ancak Turing completeness matematikten gelen belirli bir terimdir; pratikçilerin istediği çeşitli özelliklerin yerine kullanıldığında anlamı bulanıklaşır
  • Asıl gereken özellikler sonlanma garantisi, hızlı çalışma, deterministik davranış, sandboxing ve basit bir yapılandırma dili gibi şeylerdir; bunlar Turing completeness ile büyük ölçüde diktir
  • Bu farkı anlamak için ilkel özyinelemeli fonksiyonlar (Primitive Recursive Functions, PRF) hakkında basit bir teorik sonuca ihtiyaç vardır

Yeterince hızlı bir Turing Machine PRF’ye dönüştürülebilir

  • Turing-complete bir dilde yazılmış bir programın çalışma süresinin O(2^(2^N)) değerinden hızlı olduğu bilinebiliyorsa, aynı algoritma Turing-tam olmayan bir dilde de uygulanabilir
  • Pratik problemlerin çoğu 2^(2^N) değerinden hızlı biten alana girer
  • Dolayısıyla Turing-tam olmayan diller, pratik hesaplama gücünü anlamlı biçimde sınırlamaz ve hesaplamayı kontrol etmeye yönelik özel bir yeteneği de otomatik olarak sağlamaz
  • Pratik açıdan şu iki program fiilen aynı sorunu yaratır
    • Sonlanmayan program
    • Ancak 1 milyarın 1 milyar katı gibi bir adım sayısından sonra sonlanan program
  • Turing-complete dillerde de uygulama düzeyinde adım sayısını sayıp belirli bir sınırdan sonra hata ile durdurursanız sonlanmama sorununun kendisi basitçe engellenebilir

FSM: Her zaman sonlanır ama ifade gücü sınırlıdır

  • Finite State Machine (FSM), bir dizgeyi girdi olarak alıp “yes” veya “no” döndüren bir tanıyıcıdır
  • FSM, sonlu bir durum kümesi, başlangıç durumu, yes durumları kümesi ve geçiş fonksiyonundan oluşur
  • Girdideki her sembole geçiş fonksiyonu tekrar tekrar uygulandıktan sonra, sonuç son durumun yes durumu olup olmamasına göre belirlenir
  • FSM’nin ifade gücü regular expression ile eşdeğerdir
  • FSM, girdi uzunluğuna doğrusal zamanda çalışır ve her zaman sonlanır; ancak her dizge kümesini tanıyamaz
    • Örneğin 1, 010, 00100, 0001000 gibi 1 sembolünün iki yanında eşit sayıda 0 bulunan dizgeler kümesi FSM ile tanınamaz
    • Yeterince uzun girdilerde durumlar tekrar eder ve bir döngü oluşur; bu döngü aralığı çoğaltıldığında FSM hâlâ yes durumuna ulaşır, ancak dizge koşulu bozulur

Turing Machine: FSM’ye değişken bir bant eklenmiş model

  • Turing Machine (TM), FSM gibi durumlara ve geçiş fonksiyonuna sahiptir; ancak değişmez girdi yerine değişken bir bant üzerinde çalışır
  • Her adımda TM mevcut bant sembolünü okur ve şu işlemleri yapar
    • Mevcut sembolü yeni bir sembolle değiştirir
    • İç durumunu değiştirir
    • Kafayı sola veya sağa bir hücre hareket ettirir
  • TM halt durumuna ulaştığında durur ve o andaki bant içeriği sonuç olur
  • FSM ikili bir tanıyıcıyken, TM fonksiyon hesaplayan bir aygıttır
  • TM mutlaka durmak zorunda değildir; bant üzerinde gidip gelip durum değiştirirken son duruma hiç ulaşmayabilir

Universal Turing Machine ve hesaplama gücü

  • Bir TM’nin programı, kullanıcı girdisi olarak verilen kod değil, geçiş fonksiyonunun kendisine hardcode edilmiş halidir
  • Ancak herhangi bir TM ve girdisi bir metin dosyası olarak kodlanabilir ve bunu yorumlayan bir “interpreter” TM oluşturulabilir
  • Böyle bir TM, Universal Turing Machine’dir ve girdi olarak verilen başka bir TM’yi simüle eder
  • Python ile bir TM interpreter’ı yazılabilir; tersine Python interpreter’ı da TM ile uygulanabilir, bu yüzden ikisi hesaplama gücü açısından eşdeğer görülebilir
  • FSM, TM’den daha zayıftır
    • TM, FSM’yi simüle edebilir
    • TM, iki yanında eşit sayıda 0 bulunan ve ortasında 1 olan dizgeleri bant manipülasyonuyla karara bağlayabilir
    • FSM aynı problemi çözemez

Bant iki stack olarak görülebilir

  • TM’nin bandı, genel programlama dillerinde doğrudan uygulaması zor bir soyutlamadır
  • Bant ve kafa konumu iki stack ile temsil edilebilir
    • Kafanın solundaki içerik sol stack’tir
    • Kafanın sağındaki içerik, sırası ters çevrilerek sağ stack’tir
  • Kafayı sola veya sağa taşıma işlemi, bir stack’ten pop edip diğerine push etmeye dönüşür
  • Bu nedenle TM, “iki stack’e sahip bir FSM” ile eşdeğer hesaplama gücüne sahiptir
  • Stack sembolleri yalnızca 0 ve 1 ise stack’in kendisi tek bir doğal sayı ile de temsil edilebilir
    • top kontrolü: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Turing Machine’in sınırları: Halting Problem ve Rice türü sonuçlar

  • Tüm TM’ler metin olarak kodlanabildiğinden, olası TM’ler sonsuz bir liste halinde sıralanabilir
  • Köşegenleştirme argümanı kullanılarak TM ile hesaplanamayan fonksiyonların var olduğu gösterilebilir
  • Daha somut bir örnek Halting Problem’dir
    • Bir TM’nin kaynak kodu ve girdisi verildiğinde, o TM’nin bir gün durup durmayacağını belirleme problemidir
  • halts(program, input) fonksiyonunun her zaman doğru şekilde sonlandığını varsayarsak, kendi kaynak kodunu girdi olarak alan weird programında çelişki ortaya çıkar
    • Duracağına karar verirse sonsuz döngüye girer ve durmaz
    • Durmayacağına karar verirse hemen sonlanır
  • Bu yüzden halts bazı durumlarda yanlış olmalı ya da bazı durumlarda sonlanmamalıdır
  • Daha genel olarak, herhangi bir TM için davranışı koruyan önemsiz olmayan bir özellik algoritmik olarak karara bağlanamaz
    • Sözdizimsel özellikler kontrol edilebilir; ancak refactoring sonrasında da korunan davranış özellikleri genel olarak karara bağlanamaz

İlkel özyinelemeli fonksiyonlar: Her zaman sonlanan hesaplama aygıtı

  • İlkel özyinelemeli fonksiyonlar (PRF), doğal sayı demetlerini alıp tek bir doğal sayı döndüren fonksiyonlar olarak tanımlanır
  • Temel fonksiyonlar zero ve succ’tır
    • zero = 0
    • succ(x) = x + 1
  • Fonksiyon bileşimiyle sabitler oluşturulabilir
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • Genel özyinelemeye izin verilmez; ancak yineleme sayısı önceden sabitlenmiş sınırlı bir döngü olan LOOP(init, f, n) izinlidir
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • Temel kısıt, yineleme sayısı n değerinin döngü başlamadan önce sabitlenmesi ve döngü gövdesinde döngü sayacının değiştirilememesidir

PRF ile temel programlama yapıları oluşturmak

  • Toplama add(x, y) = LOOP(x, succ, y) olarak tanımlanabilir
  • Çarpma mul(x, y) = LOOP(0, add x, y) olarak tanımlanabilir
  • Üs alma pow(x, y) = LOOP(1, mul x, y) olarak tanımlanabilir
  • Bunlarla hızlı büyüyen fonksiyonlar da oluşturulabilir
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • pred temel fonksiyonlara eklenirse saturating subtraction ve Boole işlemleri oluşturulabilir
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) de aritmetik ifadeyle temsil edilebilir
  • Karşılaştırma işlemleri, kalan ve bölme de üst sınırlı yineleme ve koşullu ifadeler kullanılarak uygulanabilir

PRF’nin veri yapıları ve TM simülasyonu

  • PRF birden fazla argüman alabilir ama sonuç tek bir doğal sayı olduğundan, veri yapılarının doğal sayı olarak kodlanması gerekir
  • (a, b) çifti 2^a * 3^b olarak temsil edilebilir
  • Bileşenleri çıkarmak için belirli bir asalın en büyük üssünü bulmak yeterlidir
    • fst(p), p’yi bölen 2’nin en büyük kuvvetinin üssüdür
    • snd(p), p’yi bölen 3’ün en büyük kuvvetinin üssüdür
  • Aynı şekilde üç değer (S, stack1, stack2) de tek bir doğal sayı içinde paketlenebilir
  • Bir TM konfigürasyonu şu üç öğeyle temsil edilebilir
    • Mevcut durum S
    • Bandın sol stack’i
    • Bandın sağ stack’i
  • Stack işlemleri kalan, çarpma ve bölme ile uygulanabildiğinden, TM’nin tek bir adımı PRF olarak kodlanabilir
  • LOOP(initial_config, single_step, n) kullanılarak TM tam olarak n adım boyunca simüle edilebilir
  • Sorun, yeterli n değerinin bilinmemesidir; ancak çalışma süresi bir PRF ile sınırlıysa, o kadar tekrar edecek şekilde yapılabilir
  • Sonuçta çalışma süresi ilkel özyinelemeli fonksiyonla sınırlı olan TM hesaplamaları PRF ile değiştirilebilir

PRF’nin sınırları: Her zaman sonlansa da TM kadar güçlü değildir

  • PRF her zaman sonlanır, ancak sonlanan tüm fonksiyonları ifade edemez
  • TM ile hesaplanabilen fakat PRF ile hesaplanamayan fonksiyonlar vardır
  • Bunu göstermek için PRF sözdizim ağacının derinliği üzerinden büyüme hızına üst sınır konur
  • Derinliği d veya daha az olan PRF’lerin, belirli tek değişkenli A_d fonksiyonundan daha hızlı büyüyemeyeceği şekilde bir üst sınır belirlenebilir
  • A(d, x) şöyle tanımlanır
    • A(1, x) = x + 1
    • A(d + 1, 0) = A(d, A(d, 0))
    • A(d + 1, x) = A(d, A(d + 1, x - 1))
  • Bu tanımda her özyinelemeli çağrıda (d, x) sözlüksel olarak küçüldüğü için TM’de hesaplanırsa sonlanır
  • a(x) = A(x, x) herhangi bir PRF’den daha hızlı büyür ve TM ile hesaplanabilir, ancak PRF ile hesaplanamaz

Pratiğe dönersek: Turing-tam olmamak tek başına yeterli değildir

  • Turing Machine durmayabilir
  • FSM ve PRF gibi her zaman sonlanan aygıtların da hızlı biteceği garanti değildir
  • PRF, 2^(2^N) gibi büyük fonksiyonları hesaplayabildiğinden, sonlanma garantisi tek başına pratik çalışma süresini garanti etmez
  • Gerçek dünyadaki birçok algoritmanın çalışma süresi PRF ile sınırlıdır; bu yüzden Turing-tam olmayan aygıtlarla da ifade edilebilir
  • Turing-complete hesaplamayı PRF gibi yapmak için genel yöntem, bir yineleme sayacı eklemek ve sayaç fazla büyürse zorla durdurmaktır

Yapılandırma dilinde gerçekten gereken özellikler

  • Yapılandırma dilleri çoğu zaman “Turing-tam olmamayı” tasarım hedefi olarak öne çıkarır; ancak gerçekte gerekenler daha güçlü birkaç özelliktir
  • Determinizm

    • Yapılandırma dili deterministik olmalıdır
    • Python’daki id([]) gibi her çalıştırmada farklı değer üreten davranışlar genel programlamada kabul edilebilir olsa da yapılandırma için uygun değildir
    • Yapılandırmalar çoğu zaman incremental build veya caching sistemlerinde anahtar olarak kullanılır; determinizm dışı davranış girerse cache davranışı sarsılır
  • Net semantik

    • Dil davranışı, başvurulabilir bir ölçüte göre net biçimde sabitlenmiş olmalıdır
    • ASLR’yi kapatıp belirli bir allocator kullanarak Python’daki id([]) değerini deterministik yapmak mümkün olsa da, sonucun öngörülebilir veya uygulamalar arasında aynı olacağı garanti edilmez
    • Farklı uygulamalarda veya Python sürümü değişikliklerinde de aynı davranışı garanti etmek için semantiğin açık olması gerekir
  • Saflık

    • Yapılandırma ortam değişkenlerini veya disk dosyalarını okuyabiliyorsa, yapılandırmanın anlamı değerlendirme ortamına bağlı olur
    • Caching’in doğru çalışması için yapılandırma dili saflık özelliğine sahip olmalıdır
  • Güvenlik ve sandboxing

    • Saflık ve güvenlik, ikisi de genel IO’yu dışa açmayan bir yaklaşımla sağlanabilir
    • İki özelliğin amacı farklıdır
    • Saflık, sonucun deterministik olmaktan çıkmasını engellemek içindir
    • Güvenlik, saldırgana erişim token’ları gibi kaynakları açmamak içindir
  • Çalışma süresi kontrolü

    • IO kontrol edilse bile kötü niyetli bir yapılandırma CPU yakarak hizmet engelleme saldırısı yapabilir
    • Çalışma süresi garantisi için iki yaklaşım kullanılabilir
    • İşlemeyi, girdi boyutuyla doğrudan orantılı bariz doğrusal bir yapı olacak şekilde sınırlamak
    • Her atomik adımda bir sayacı azaltıp sayaç 0 olduğunda durduran ölçümlü yürütme (metered execution) kullanmak
  • Basitlik

    • Yapılandırma dili, kullanıcıları basit programlar yazmaya yönlendirmelidir
    • Özyinelemeyi ve sonsuz döngüleri yasaklamak, basitliği teşvik eden bir hız kesici olabilir
    • Ancak PRF örneğinde olduğu gibi bu tür yasaklar, keyfi özyinelemeli programlar yazmayı tamamen engellemez; yalnızca dolambaçlı kod gerektirir
    • İlgili bir örnek olarak some roundabout code görülebilir

Son özet

  • Girdiye bağlı çalışma süresi bir ilkel özyinelemeli fonksiyonla sınırlanan Turing Machine algoritmaları, ilkel özyinelemeli fonksiyon olarak da uygulanabilir
  • Turing-tam olmamak sonlanma garantisi gibi bir özellik sağlayabilir; ancak pratikte gereken çalışma süresi üst sınırını veya yapılandırma dili kalitesini otomatik olarak garanti etmez
  • Yapılandırma dili tasarımında önemli olan konu Turing completeness’in kendisinden çok determinizm, net semantik, saflık, sandboxing, çalışma süresi ölçümü ve basitliktir

1 yorum

 
GN⁺ 2024-08-05
Hacker News yorumları
  • Kendini tanıtma: https://www.nayuki.io/page/primitive-recursive-functions

    • Orijinal yazıdan çok daha iyi, ama bugünlerde herkes ELI5 tarzı kolay açıklamaları daha çok tercih ediyor gibi
  • Yazının sonuç bölümünde konfigürasyon dilleri ile ilgili oldukça iyi ölçütler var; mevcut diller arasında bu ölçütlerin hepsini ya da çoğunu karşılayan bir şey var mı merak ediyorum

    • Bu ölçütleri karşılayan örnekler olarak Dhall [1] ve Cue [2] var, ama bir bakıma ilginç örnekler değiller
      Dhall, bilinçli olarak total fonksiyonel bir dil olduğu için “Turing-complete olmama” yönüne gidiyor; Cue’da ise fonksiyon yok, dolayısıyla özyineleme yapılacak bir şey de yok
      RCL [3] ölçütleri karşılıyor diye düşünüyorum. Deterministik ve saf; ölçümlü yürütme sunuyor ve dosya sistemi erişimini sandbox’a alıyor. Sandbox politikası izin verirse dosya okuyabiliyor, ama bu tür dosyalar kaynak kodun bir parçası sayılıyor ve import ile aynı şekilde davranıyor
      RCL’de, yazarın söylediği nedenlerden dolayı “Turing-complete olmama” yoluna gitmek istemedik. Bir programın eninde sonunda biteceği gerçeği pratikte pek yararlı bir özellik değil; tersine, Agda gibi total fonksiyonel dillerde bile çok karmaşık programlar yazılabiliyor, yani Turing-complete olmamak basit programları/konfigürasyonları garanti etmiyor
      RCL’deki tüm döngüler sınırlı, ama fonksiyonlar olduğu için özyineleme de mümkün. Tail call yok; bu yüzden başta yerel stack taşmasını önlemek için özyineleme derinliği sınırı koymuştuk, fakat fuzzer sabit stack alanıyla çalışıp yine de durmayan bir fonksiyon buldu ve bunu hâlâ tam olarak anlamış değilim: let f = g => g(g(h => k => g(g(h)))); f(f)
      Sonuçta bu tür patolojik fonksiyonları ifade edebilmek pratikte sorun olmuyor. Yürütme adımı sayısına bir sınır, yani “gas limiti” ya da yazarın dediği “ölçümlü yürütme” koymak yeterli. Kodu basit tutmak için yerleşik döngü yapılarının sınırlı olması ve özyinelemenin zahmetli olması iyi bir yönlendirici etken, ama nihayetinde en değerli araçlar kod incelemesi ve sağduyu
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • Emredici ve “saf” da değil, ama C bile her döngüye girmeden önce yineleme sayısının üst sınırının bilinebilmesini hedefleyen bir yönde tasarlandı; bu yüzden ilkel özyinelemeli
      Dennis Ritchie’nin MIT’deki araştırması, onun loop programming adını verdiği konuya odaklanıyordu
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      Neredeyse tüm modern programcıların varsayılan olarak izlediği yapısal programlama, fiilen ilkel özyinelemeli fonksiyonlara doğru iten bir paradigma. Yapısal programlama, pop ve fonksiyonel gibi diğer iki türe kıyasla neredeyse evrensel kabul gördüğü için Dijkstra’nın “goto zararlıdır” makalesi konusunda kafa karışıklığı yaşanıyor gibi
      İlkel özyinelemeli fonksiyonlar hesaplanabilir fonksiyonların tamamını kapsamaz, ama sonlanması garanti olan sezgisel fonksiyonların neredeyse tamamını kapsar. Elbette döngüye girerken yineleme sayısının bilinmediği döngülere gerçekten ihtiyaç duyulan durumlar da var; ama yalnızca gerçekten gerektiğinde kullanılırsa kaçınılabilir bir ayak silahıdır
      COBOL bile sınırsız goto’yu ALTER komutuna taşıyarak modernize edildi. Modern ve yararlı diller arasında PR fonksiyonlarına izin vermeyen bir dil aklıma gelmiyor
      C’de de while kullanmaktan kaçınarak ve fall through’dan açıkça kaçınacak şekilde yazarak neredeyse her zaman mutlaka sonlanan total fonksiyon kodu oluşturabilirsiniz
      ML’in tip çıkarımı gibi patolojik durumlar da var. Karmaşıklık sınıfına kıyasla gerçek maliyeti çok daha düşük olduğu için, total fonksiyon olmasa ve dilin bu tür kullanımı sınırlaması zor olsa bile buna katlanmaya değer
      Pratik açıdan bakıldığında tüm diller genelde bu ölçütlerin çoğunu destekleyen varsayılanlar sunar; ancak bunları zorunlu kılan kısıtlar dilin kullanışlılığını ciddi biçimde sınırlar. Hatta çok eleştirilen SOLID ve Clean framework’lerin bile bu modele doğru ittiğini düşünüyorum
      Yapısal programlama o kadar yaygınlaştı ki bu noktayı unutmak, hatta öğretmemek kolay. Yaşlı sakallı biri olarak WHILE vb. şeylerin tehlikelerini öğrendiğimi hatırlıyorum
    • Dhall’ı seçip hangi ölçütte başarısız olduğuna bakmak yeterli olabilir. En yakını o gibi görünüyor
  • O(2^(2^N)) ifadesinden daha hızlı çalıştığı sözü muhtemelen basitleştirme amaçlıydı, ama “çok büyük sayı” kısmı güveni biraz zedeliyor
    Daha doğrusu “çok hızlı büyüyen fonksiyon” denmeli gibi. Ya da programın O(2^(2^N)) adımdan daha az sürede bittiği anlamına geliyor gibi görünüyor

  • Sınırlı bir dilin bazı uygulamalar için daha iyi olduğu ilk kısma bakınca, avantajın gerekli adım sayısının üst sınırını statik olarak hesaplayabilmek olduğu düşünülebilir
    Böylece herhangi bir girdi için sınırı ihlal eden hesaplamalar reddedilip anlamlı bir hata döndürülebilir
    Buna karşılık Turing-tam bir dile çalışma zamanı sınırı koyma yaklaşımında, ilgilenilen bazı girdiler için sınır fazla düşük belirlenmiş olabilir. Çalıştırıp sınıra takılana kadar bilemezsiniz. C++ şablon özyinelemesinde bunu ara sıra görüyorum
    Tamamen kafam karışmış da olabilir; daha iyi bilen biri açıklarsa iyi olur

    • Eski bir iş arkadaşım 3 kata yakın bir değer koymuştu; birkaç yıl sonra gerçek iş yükü o sınıra takılınca, ben makul hesaplama miktarının 10 katı sınır kullanmaya başladım
      Kötü bir iş akışının başarısız olması birkaç kat daha uzun sürse bile hâlâ milisaniye mertebesinde olacağı için büyük bir zarar görmüyorum
      Bu sorun genelde birisi problem alanını yönlü döngüsüz grafik olarak ele alıp “döngüsüz” olmayı zorlayamadığında karşınıza çıkar. Bir problemi yönlü döngüsüz grafik olarak modellemek, Frodo’dan yüzüğü alıp almamayı düşünen Dark Galadriel gibidir. “Herkes beni sevecek ve umutsuzluğa kapılacak.” Böyle şeyler yapan insanlar her zaman gurur duymaları gerekenden çok daha fazla gurur duyar
      Sonunda pahalı ve karmaşık çözümlere çekilen müşterilerin parası biter ve kendi problemleri de çok daha küçük görünmeye başlar. O zaman kelimenin tam anlamıyla geriye, iş başına maliyeti müşterinin işini sürdürecek kadar düşüremeyen uygulamalar kalır
    • Blokzincir hesaplamalarının yakıt kullanımını doğru tahmin etmek başkaları için ilginç olabilir ama benim için değil
      Ben daha çok bunu, statik tip denetimi, null olmaması, değişmezlik gibi önceki çekiçleri atlatan hataları yakalamaya yarayan araç kutusundaki bir başka çekiç olarak kullanmayı ilginç buluyorum
      Sonlu zamanda sona erdiğini bilmek doğruluğu kanıtlamaz; ama ben kodun sonlu zamanda sona erdiğini beyan ettiğimde derleyici buna katılmıyorsa, o kodun yanlış olduğuna inanırım
    • Statik olarak belirlenen üst sınır, yaygın durumdaki gerçek çalışma süresi karmaşıklığını ciddi biçimde olduğundan büyük gösterebilir. Çünkü özyinelemede erken çıkışa yol açan koşullu ifadelerin nasıl değerlendirileceği genel olarak öngörülemez
      Erken çıkışın çalışma süresini etkilemesi için tembel değerlendirme veya kısa devre koşullu ifadeler varsaymak gerekir; pratik bir dilde ise genelde bunlar zaten bulunur
    • Peki ya o üst sınır aşırı gevşekse? Örneğin deterministik hızlı sıralama genelde n log n’dir ama girdi boyutuna göre ikinci dereceden bir üst sınıra sahiptir
      O zaman hızlı sıralama hesaplamasını reddedecek misiniz? Daha uç bir örnek olarak Hindley–Milner algoritmasının üstel zaman üst sınırı vardır ama pratikte çoğu zaman doğrusal zamanda çalışır
    • “Statik olarak hesaplanıyor” mu bilmiyorum ama dilin yeteneklerini ciddi biçimde sınırlamanın tek avantajının, veriye bağlı olmayan türde bir hesaplama sınırı koyabilmek olduğunu düşünüyorum
      Yine de bunun gerçekten güçlü bir gereksinim olduğu tek bir durum bile aklıma gelmiyor. “Sorgu çok uzun sürdü” hatası veremeyen kaç sistem var ki?
  • Sona ermeme/sınırlı olma ilkesine dayalı bir backend web programlama dili denemek istemiştim
    Fikir şu: Derleyici, her fonksiyonun verilen durum ve argümanlar için yürütmesinin sınırlar içinde olduğunu kanıtlayacak; X’in alt sınır, Y’nin üst sınır olduğunu gösterebilecek. Bu bilgi giriş noktalarına kadar yayılacak
    Yazarın daha güçlü semantiklere ihtiyaç olduğu görüşüne katılıyorum; bu dili de bu yüzden düşündüm. Programların çalışma süresi hakkında garanti istemek sık rastlanan bir durum
    Temelinde ilkel özyinelemeli fonksiyonlar olurdu ama pratikte Turing-tam olabilir. Rust’ın hatalı borrow’ları reddederken ham işaretçiler için unsafe sunması gibi, bu dil de basit yineleme ilkellerini temel alarak üst sınırı hesaplar ya da unsafe operatörü kullanıp sınırlar için alternatif bir formül sunmayı gerektirirdi

  • Yazıdaki kısa yakınma/motivasyon kısmını pek anlayamadım
    “Genellikle belirli alanlarda Turing-tam olmamak bir avantaj ya da gereksinim olarak övülür. Bence bu tartışmaların çoğu konuyu yanlış anlıyor — Turing-tam olmamak insanların beklediği anlama gelmez” denen kısım
    Bu tartışmalar neden yanlış? Çoğu biçimsel analiz aracı, örneğin Coq, Isabelle, Agda, genelde fonksiyonun sona erdiğine dair kanıt ister. Bu, o fonksiyonun total bir fonksiyon olduğunu kanıtlamakla aynı şey değil mi; dolayısıyla ilkel özyinelemeli olduğu anlamına gelmez mi?

    • Tamamını okumadım ama bu yazı, bazı yapılandırma dillerinin “Turing-tam değil” olmasını bir özellik olarak öne çıkarmasından doğmuş gibi görünüyor. Oysa asıl pazarlamak istedikleri özellik muhtemelen makul ölçüde sınırlı çalışma süresi
      Yakın zamandaki CEL tartışmasında da gündeme gelmişti:
      https://news.ycombinator.com/item?id=40954652
    • Biçimsel kanıttan söz ediyorsanız, modern programlamada kullanılan bilimsel karşı örneklerden değil; genel durumda bir fonksiyonun total olduğunu kanıtlamak NP-tam bir arama problemidir
      Yanlış hatırlamıyorsam bu, co-NP oracle’ı olan NP’ye ya da polinom hiyerarşinin ikinci seviyesine denktir. Küçük problemlerde mümkün olsa bile pahalıdır
      Bu araçlar, programları total fonksiyon olacak şekilde yapılandırdığınızda en iyi çalışır. Bunun en yaygın yolu da yapısal programlamada yalnızca FOR kullanmak veya yineleme sayısı sınırlı WHILE/özyineleme kullanmaktır
      Yalnızca SAT ile ilgili olsa da, Schaefer’in ikilem teoreminde ele alınan kolay işlenebilir biçimler, aklıma gelen en erişilebilir mercek
    • Yazının gösterdiği gibi sona eren ama ilkel özyinelemeli olmayan fonksiyonlar vardır; bu yüzden total fonksiyon kanıtı, ilkel özyinelemeli olduğu anlamına gelmez
      Agda ve muhtemelen başka araçlar da sona eren ama ilkel özyinelemeli olmayan bazı fonksiyonlar için sonlanmayı kanıtlayabilir. Elbette hepsi için bu mümkün değildir
      Yazının şikâyet ettiği yanlış anlama kabaca şöyle görünüyor: “Turing-tamlık hesaplama yapabilmek demektir; Turing-tam olmamak ise hesaplama yapamamak ve iyi yapılandırma dili özelliklerine sahip olmak demektir.”
      Yazının ana fikri, Turing-tam olmasa bile hesaplama maliyeti yüksek veya zor pek çok işin yapılabileceği; bir yapılandırma dili için yalnızca Turing-tam olmamaktan çok daha katı sınırlara ihtiyaç olduğudur
    • Turing-tam olmamanın, düzgün biçimde sona eren total fonksiyonlar olmaktan başka yolları da olabilir. Örneğin sonsuz döngü ne evrensel hesaplama yapabilir ne de sona erer
  • Ben bir CUE geliştiricisiyim. CUE ilkel özyinelemelidir ve “iyi” bir yapılandırma dilinden beklenen ölçütleri de karşılar