Fungsi Rekursif Primitif untuk Programmer Praktis

 (matklad.github.io)
2 poin oleh GN⁺ 2024-08-05 | 1 komentar | Bagikan ke WhatsApp
  • Diskusi seperti “aman jika tidak Turing-complete” tidak sejalan dengan makna matematisnya, dan non-Turing completeness sebagian besar terpisah dari sifat praktis seperti terminasi, determinisme, dan sandboxing
  • Komputasi Turing Machine yang waktu eksekusinya dibatasi oleh fungsi rekursif primitif terhadap input dapat ditulis ulang sebagai fungsi rekursif primitif
  • Fungsi rekursif primitif selalu berhenti, tetapi juga bisa membentuk fungsi yang tumbuh sangat cepat seperti 2^(2^N), sehingga jaminan terminasi tidak serta-merta berarti waktu eksekusi yang praktis
  • Dalam praktik, program yang tidak pernah berhenti dan program yang baru selesai setelah miliaran tahun menimbulkan masalah yang mirip; bahasa Turing-complete pun dapat dihentikan paksa dengan penghitung langkah
  • Kualitas bahasa konfigurasi lebih banyak ditentukan oleh determinisme, semantik yang jelas, kemurnian, keamanan dan sandboxing, kontrol waktu eksekusi, serta kesederhanaan daripada oleh apakah ia Turing-complete atau tidak

Inti kesalahpahaman dalam diskusi Turing-completeness

  • Para programmer di internet sering menyebut “bukan Turing-complete” sebagai keunggulan atau persyaratan di domain tertentu
  • Namun Turing completeness adalah istilah spesifik dari matematika, sehingga maknanya menjadi kabur jika dipakai sebagai pengganti berbagai sifat yang diinginkan praktisi
  • Sifat yang sebenarnya dibutuhkan adalah jaminan terminasi, eksekusi cepat, perilaku deterministik, sandboxing, dan bahasa konfigurasi yang sederhana; semua ini sebagian besar ortogonal terhadap Turing completeness
  • Untuk memahami perbedaan ini, diperlukan hasil teori sederhana tentang fungsi rekursif primitif (Primitive Recursive Functions, PRF)

Turing Machine yang cukup cepat dapat diubah menjadi PRF

  • Sekalipun sebuah program ditulis dalam bahasa Turing-complete, jika diketahui waktu eksekusinya lebih cepat daripada O(2^(2^N)), algoritme yang sama dapat diimplementasikan juga dalam bahasa non-Turing-complete
  • Sebagian besar masalah praktis berada di wilayah yang selesai lebih cepat daripada 2^(2^N)
  • Karena itu, bahasa non-Turing-complete tidak membatasi kemampuan komputasi praktis secara bermakna, dan juga tidak otomatis memberikan kemampuan khusus untuk mengendalikan komputasi
  • Dari sudut pandang praktik, dua program berikut pada dasarnya menimbulkan masalah yang sama
    • Program yang tidak pernah berhenti
    • Program yang baru berhenti setelah jumlah langkah sebesar satu miliar kali satu miliar
  • Bahasa Turing-complete pun dapat dengan sederhana mencegah masalah non-terminasi itu sendiri jika pada tahap implementasi jumlah langkah dihitung dan eksekusi dihentikan dengan error setelah batas tertentu

FSM: selalu berhenti, tetapi daya ekspresinya terbatas

  • Finite State Machine (FSM) adalah recognizer yang menerima string sebagai input dan mengembalikan “yes” atau “no”
  • FSM terdiri dari himpunan state terbatas, state awal, himpunan state yes, dan fungsi transisi
  • Setelah fungsi transisi diterapkan berulang untuk setiap simbol input, hasil ditentukan berdasarkan apakah state akhir termasuk state yes
  • Daya ekspresi FSM setara dengan regular expression
  • FSM berjalan linear terhadap panjang input dan selalu berhenti, tetapi tidak dapat mengenali semua himpunan string
    • Misalnya, himpunan string yang memiliki jumlah 0 yang sama di kedua sisi 1, seperti 1, 010, 00100, 0001000, tidak dapat dikenali oleh FSM
    • Pada input yang cukup panjang, state akan berulang sehingga terbentuk siklus; jika bagian siklus itu diduplikasi, FSM tetap mencapai state yes, tetapi syarat string menjadi rusak

Turing Machine: model yang menambahkan tape variabel ke FSM

  • Turing Machine (TM) memiliki state dan fungsi transisi seperti FSM, tetapi bekerja di atas tape yang dapat berubah, bukan input yang tidak berubah
  • Pada setiap langkah, TM membaca simbol tape saat ini dan melakukan operasi berikut
    • Mengganti simbol saat ini dengan simbol baru
    • Mengubah state internal
    • Menggerakkan head satu kotak ke kiri atau ke kanan
  • Ketika TM mencapai state halt, ia berhenti, dan isi tape pada saat itu menjadi hasilnya
  • FSM adalah recognizer biner, sedangkan TM adalah perangkat untuk menghitung fungsi
  • TM tidak harus berhenti; ia dapat bolak-balik di tape dan mengubah state tanpa pernah mencapai state akhir

Universal Turing Machine dan kemampuan komputasi

  • Program TM tidak diberikan sebagai kode lewat input pengguna, melainkan di-hardcode pada fungsi transisi itu sendiri
  • Namun TM dan input apa pun dapat dienkode sebagai file teks, lalu dibuat TM “interpreter” yang menafsirkannya
  • TM semacam ini adalah Universal Turing Machine, yang menyimulasikan TM lain yang diberikan sebagai input
  • Karena interpreter TM dapat dibuat dengan Python, dan sebaliknya interpreter Python juga dapat diimplementasikan sebagai TM, keduanya dapat dianggap setara dari sisi kemampuan komputasi
  • FSM lebih lemah daripada TM
    • TM dapat menyimulasikan FSM
    • TM dapat menentukan string yang memiliki jumlah 0 yang sama di kedua sisi dan 1 di tengah melalui manipulasi tape
    • FSM tidak dapat memecahkan masalah yang sama

Tape dapat dilihat sebagai dua stack

  • Tape TM adalah abstraksi yang tidak nyaman untuk diimplementasikan langsung dalam bahasa pemrograman umum
  • Isi tape dan posisi head dapat direpresentasikan sebagai dua stack
    • Isi di kiri head adalah stack kiri
    • Isi di kanan head, dengan urutan dibalik, adalah stack kanan
  • Operasi menggerakkan head ke kiri atau ke kanan berubah menjadi operasi pop dari satu stack dan push ke stack lain
  • Karena itu, TM memiliki kemampuan komputasi yang setara dengan “FSM dengan dua stack”
  • Jika simbol stack hanya 0 dan 1, stack itu sendiri juga dapat direpresentasikan sebagai satu bilangan natural
    • melihat top: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Batasan Turing Machine: Halting Problem dan hasil sejenis Rice

  • Karena setiap TM dapat dienkode sebagai teks, TM yang mungkin dapat disusun dalam daftar tak hingga
  • Dengan argumen diagonalisasi, dapat ditunjukkan bahwa ada fungsi yang tidak dapat dihitung oleh TM
  • Contoh yang lebih konkret adalah Halting Problem
    • Ini adalah masalah menentukan, ketika diberikan source code dan input sebuah TM, apakah TM tersebut akan berhenti suatu saat
  • Jika diasumsikan halts(program, input) selalu berhenti dengan benar, muncul kontradiksi pada program weird yang menerima source code dirinya sendiri sebagai input
    • Jika diputuskan akan berhenti, ia masuk infinite loop dan tidak berhenti
    • Jika diputuskan tidak akan berhenti, ia langsung berhenti
  • Karena itu, halts harus salah pada sebagian kasus, atau tidak berhenti pada sebagian kasus
  • Secara lebih umum, sifat nontrivial yang mempertahankan perilaku untuk TM arbitrer tidak dapat diputuskan oleh algoritme
    • Sifat sintaksis dapat diperiksa, tetapi sifat perilaku yang tetap terjaga setelah refactoring umumnya tidak dapat diputuskan

Fungsi rekursif primitif: perangkat komputasi yang selalu berhenti

  • Fungsi rekursif primitif (PRF) didefinisikan sebagai fungsi yang menerima tuple bilangan natural dan mengembalikan satu bilangan natural
  • Fungsi dasar adalah zero dan succ
    • zero = 0
    • succ(x) = x + 1
  • Konstanta dapat dibuat melalui komposisi fungsi
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • Rekursi umum tidak diizinkan, tetapi loop terbatas LOOP(init, f, n) dengan jumlah iterasi yang telah ditentukan sebelumnya diizinkan
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • Batasan utamanya adalah jumlah iterasi n ditetapkan sebelum loop dimulai, dan penghitung loop tidak dapat diubah di dalam body loop

Membuat konstruksi pemrograman dasar dengan PRF

  • Penjumlahan dapat didefinisikan sebagai add(x, y) = LOOP(x, succ, y)
  • Perkalian dapat didefinisikan sebagai mul(x, y) = LOOP(0, add x, y)
  • Perpangkatan dapat didefinisikan sebagai pow(x, y) = LOOP(1, mul x, y)
  • Dengan ini, fungsi yang tumbuh cepat juga dapat dibuat
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • Jika pred ditambahkan ke fungsi dasar, saturated subtraction dan operasi boolean dapat dibuat
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) juga dapat direpresentasikan sebagai ekspresi aritmetika
  • Operasi perbandingan, modulo, dan pembagian juga dapat diimplementasikan menggunakan iterasi berbatas dan ekspresi kondisional

Struktur data PRF dan simulasi TM

  • PRF dapat menerima beberapa argumen, tetapi hasilnya satu bilangan natural, sehingga struktur data harus dienkode sebagai bilangan natural
  • Pasangan (a, b) dapat direpresentasikan sebagai 2^a * 3^b
  • Untuk mengambil komponennya, cari eksponen maksimum dari bilangan prima tertentu
    • fst(p) adalah eksponen pangkat terbesar dari 2 yang membagi p
    • snd(p) adalah eksponen pangkat terbesar dari 3 yang membagi p
  • Dengan cara yang sama, tiga nilai (S, stack1, stack2) juga dapat dikemas menjadi satu bilangan natural
  • Konfigurasi TM dapat direpresentasikan dengan tiga elemen berikut
    • State saat ini S
    • Stack kiri tape
    • Stack kanan tape
  • Karena manipulasi stack dapat diimplementasikan dengan modulo, perkalian, dan pembagian, satu langkah TM dapat dienkode sebagai PRF
  • Dengan LOOP(initial_config, single_step, n), TM dapat disimulasikan secara tepat selama n langkah
  • Masalahnya adalah kita tidak dapat mengetahui n yang cukup, tetapi jika waktu eksekusi dibatasi oleh suatu PRF, maka simulasi dapat dibuat berulang sebanyak itu
  • Pada akhirnya, komputasi TM yang waktu eksekusinya dibatasi oleh fungsi rekursif primitif dapat digantikan oleh PRF

Batasan PRF: meski selalu berhenti, tidak sekuat TM

  • PRF selalu berhenti, tetapi tidak dapat merepresentasikan semua fungsi yang berhenti
  • Ada fungsi yang dapat dihitung oleh TM namun tidak dapat dihitung oleh PRF
  • Untuk menunjukkannya, batas atas laju pertumbuhan ditentukan berdasarkan kedalaman syntax tree PRF
  • PRF dengan kedalaman d atau kurang dapat diberi batas atas agar tidak tumbuh lebih cepat daripada fungsi unary tertentu A_d
  • A(d, x) didefinisikan sebagai berikut
    • 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))
  • Definisi ini berhenti jika dihitung dengan TM karena setiap pemanggilan rekursif membuat (d, x) lebih kecil secara leksikografis
  • a(x) = A(x, x) tumbuh lebih cepat daripada PRF mana pun, dan dapat dihitung oleh TM tetapi tidak oleh PRF

Kembali ke praktik: non-Turing completeness saja tidak cukup

  • Turing Machine dapat tidak berhenti
  • Perangkat yang selalu berhenti seperti FSM dan PRF pun tidak menjamin selesai dengan cepat
  • Karena PRF dapat menghitung fungsi besar seperti 2^(2^N), jaminan terminasi saja tidak menjamin waktu eksekusi yang praktis
  • Banyak algoritme nyata memiliki waktu eksekusi yang dibatasi oleh PRF, sehingga dapat diekspresikan juga dengan perangkat non-Turing-complete
  • Cara umum untuk membuat komputasi Turing-complete menjadi seperti PRF adalah menambahkan penghitung iterasi, lalu menghentikan paksa jika penghitung menjadi terlalu besar

Sifat yang sebenarnya dibutuhkan bahasa konfigurasi

  • Bahasa konfigurasi sering menjadikan “non-Turing-complete” sebagai tujuan desain, tetapi yang sebenarnya dibutuhkan adalah beberapa sifat yang lebih kuat

  • Determinisme

    • Bahasa konfigurasi harus deterministik
    • Perilaku seperti id([]) di Python, yang menghasilkan nilai berbeda pada setiap eksekusi, mungkin dapat diterima dalam pemrograman umum tetapi tidak cocok untuk konfigurasi
    • Konfigurasi sering digunakan sebagai kunci untuk incremental build atau sistem caching, sehingga jika nondeterminisme masuk, perilaku cache menjadi goyah

  • Semantik yang jelas

    • Perilaku bahasa harus ditetapkan dengan jelas sebagai acuan yang dapat dirujuk
    • Sekalipun id([]) di Python dapat dibuat deterministik dengan mematikan ASLR dan memakai allocator tertentu, hasilnya tidak dijamin dapat diprediksi atau sama antarimplementasi
    • Agar perilaku yang sama terjamin pada implementasi lain atau perubahan versi Python, semantiknya harus jelas

  • Kemurnian

    • Jika konfigurasi dapat membaca environment variable atau file disk, makna konfigurasi bergantung pada lingkungan evaluasi
    • Agar caching bekerja dengan benar, bahasa konfigurasi harus memiliki kemurnian

  • Keamanan dan sandboxing

    • Kemurnian dan keamanan sama-sama dapat dicapai dengan tidak mengekspos IO umum
    • Tujuan kedua sifat ini berbeda
    • Kemurnian bertujuan mencegah hasil menjadi nondeterministik
    • Keamanan bertujuan mencegah sumber daya seperti token akses terekspos kepada penyerang

  • Kontrol waktu eksekusi

    • Meski IO dikendalikan, konfigurasi berbahaya tetap dapat melakukan serangan denial of service dengan membakar CPU
    • Untuk menjamin waktu eksekusi, dua pendekatan dapat digunakan
    • Membatasi pemrosesan agar menjadi struktur linear yang jelas dan langsung sebanding dengan ukuran input
    • Menggunakan eksekusi terukur (metered execution), yaitu mengurangi counter pada setiap langkah atomik dan menghentikan eksekusi saat counter mencapai 0

  • Kesederhanaan

    • Bahasa konfigurasi harus mendorong pengguna menulis program yang sederhana
    • Melarang rekursi dan infinite loop dapat menjadi speed bump yang mendorong kesederhanaan
    • Namun seperti pada contoh PRF, larangan ini tidak sepenuhnya mencegah penulisan program rekursif arbitrer; hanya membuatnya memerlukan kode yang berputar-putar
    • Contoh terkait dapat dilihat di some roundabout code

Ringkasan akhir

  • Algoritme Turing Machine yang waktu eksekusinya terhadap input dibatasi oleh suatu fungsi rekursif primitif juga dapat diimplementasikan sebagai fungsi rekursif primitif
  • Non-Turing completeness dapat memberi satu sifat berupa jaminan terminasi, tetapi tidak otomatis menjamin batas waktu eksekusi atau kualitas bahasa konfigurasi yang dibutuhkan dalam praktik
  • Dalam desain bahasa konfigurasi, isu yang lebih penting daripada Turing completeness itu sendiri adalah determinisme, semantik yang jelas, kemurnian, sandboxing, pengukuran waktu eksekusi, dan kesederhanaan

Bacaan terkait

1 komentar

 
GN⁺ 2024-08-05
Komentar Hacker News

  • Promosi diri: https://www.nayuki.io/page/primitive-recursive-functions

    • Jauh lebih baik daripada artikel aslinya, tetapi belakangan sepertinya semua orang lebih menyukai penjelasan mudah gaya ELI5

  • Di bagian kesimpulan artikel ada beberapa kriteria yang cukup bagus terkait bahasa konfigurasi, dan saya penasaran apakah ada bahasa saat ini yang memenuhi semua atau sebagian besar kriteria itu

    • Contoh yang memenuhi kriteria ini adalah Dhall [1] dan Cue [2], tetapi dalam arti tertentu keduanya bukan contoh yang menarik
      Dhall sengaja merupakan bahasa fungsi total, jadi arahnya adalah “tidak Turing-complete”, sementara Cue tidak memiliki fungsi sehingga tidak ada yang bisa direkursikan
      Menurut saya RCL [3] memenuhi kriterianya. Deterministik dan murni, menyediakan eksekusi terukur, serta melakukan sandboxing terhadap akses filesystem. Jika kebijakan sandbox mengizinkan, ia bisa membaca file, tetapi file semacam itu dianggap sebagai bagian dari kode sumber dan berperilaku sama seperti import
      Di RCL, saya tidak ingin menuju “tidak Turing-complete” karena alasan yang disebutkan penulis. Fakta bahwa sebuah program pada akhirnya berhenti bukanlah properti yang terlalu berguna dalam praktik, dan sebaliknya bahkan dalam bahasa fungsi total seperti Agda pun kita bisa menulis program yang sangat kompleks, sehingga ketidaklengkapan Turing tidak menjamin program/konfigurasi yang sederhana
      Semua loop di RCL memiliki batas, tetapi karena ada fungsi, rekursi juga dimungkinkan. Tidak ada tail call, jadi awalnya saya menambahkan batas kedalaman rekursi untuk mencegah stack overflow native, tetapi fuzzer menemukan fungsi yang berhenti meskipun dijalankan dengan ruang stack konstan, dan saya masih belum sepenuhnya memahaminya: let f = g => g(g(h => k => g(g(h)))); f(f)
      Pada akhirnya, kemampuan mengekspresikan fungsi patologis semacam ini bukan masalah dalam praktik. Cukup berikan batas jumlah langkah eksekusi, yaitu “batas gas” atau “eksekusi terukur” seperti yang disebut penulis. Untuk menjaga kode tetap sederhana, fakta bahwa struktur iterasi bawaan memiliki batas dan rekursi dibuat tidak nyaman adalah pendorong yang baik, tetapi pada akhirnya alat yang paling berharga adalah code review dan penilaian yang baik
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • Meski imperatif dan juga tidak “murni”, bahkan C dirancang ke arah agar batas atas jumlah iterasi bisa diketahui sebelum memasuki setiap loop, sehingga bersifat rekursif primitif
      Penelitian Dennis Ritchie di MIT berfokus pada topik yang ia sebut pemrograman loop
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      Pemrograman terstruktur, yang diikuti secara default oleh hampir semua programmer modern, pada dasarnya adalah paradigma yang mendorong ke arah fungsi rekursif primitif. Karena pemrograman terstruktur diterima hampir secara universal dibanding dua jenis lain seperti pop dan fungsional, orang tampaknya jadi bingung tentang makalah Dijkstra “goto dianggap berbahaya”
      Fungsi rekursif primitif memang tidak mencakup semua fungsi yang dapat dihitung, tetapi mencakup hampir semua fungsi intuitif yang dijamin berhenti. Tentu saja ada kasus ketika loop yang jumlah iterasinya belum diketahui saat masuk loop memang benar-benar diperlukan, tetapi itu adalah jebakan yang bisa dihindari jika hanya digunakan saat benar-benar perlu
      Bahkan COBOL pun dimodernisasi dengan memindahkan goto tak terbatas ke perintah ALTER. Saya tidak terpikir ada bahasa modern dan berguna yang tidak mengizinkan fungsi PR
      Bahkan di C, jika menulis dengan menghindari while dan secara eksplisit menghindari fall through, hampir selalu kita bisa membuat kode fungsi total yang pasti berhenti
      Ada juga kasus patologis seperti inferensi tipe ML. Biaya aktualnya jauh lebih murah dibanding kelas kompleksitasnya, sehingga meskipun bukan fungsi total dan sulit bagi bahasa untuk membatasi penggunaan seperti ini, tetap layak diterima
      Secara praktis, semua bahasa umumnya menyediakan default yang mendukung sebagian besar kriteria semacam ini, tetapi pembatasan yang memaksanya akan sangat membatasi kegunaan bahasa. Bahkan SOLID dan framework Clean yang sering dicela pun menurut saya mendorong ke arah model ini
      Pemrograman terstruktur sudah begitu umum sehingga poin ini mudah dilupakan, bahkan kadang gagal diajarkan. Dari sudut pandang orang tua berjanggut, saya ingat pernah belajar tentang bahaya WHILE dan semacamnya
    • Sepertinya tinggal pilih Dhall lalu lihat di kriteria mana ia gagal. Itu tampak paling mendekati

  • Pernyataan bahwa ia berjalan lebih cepat daripada O(2^(2^N)) mungkin dimaksudkan sebagai penyederhanaan, tetapi bagian “bilangan yang sangat besar” sedikit mengurangi kredibilitas
    Lebih tepatnya seharusnya “fungsi yang tumbuh sangat cepat”. Atau maksudnya mungkin program selesai dalam kurang dari O(2^(2^N)) langkah

  • Jika hanya melihat bagian awal bahwa bahasa yang terbatas lebih baik untuk sebagian aplikasi, rasanya keunggulannya adalah kita bisa menghitung batas atas jumlah langkah yang diperlukan secara statis
    Dengan begitu, perhitungan yang melanggar batas untuk input apa pun bisa ditolak dan mengembalikan error yang bermakna
    Sebaliknya, pendekatan memberi batas runtime pada bahasa Turing-complete bisa saja menetapkan batas terlalu rendah untuk sebagian input yang kita pedulikan. Kita tidak tahu sampai menjalankannya dan terkena batas. Kadang saya melihat hal seperti ini pada rekursi template C++
    Bisa saja saya benar-benar salah paham, jadi akan bagus kalau ada yang lebih paham bisa menjelaskan

    • Setelah mantan rekan kerja dulu menetapkan angka hampir 3 kali lipat, lalu beberapa tahun kemudian beban kerja nyata terkena batas itu, saya memakai batas 10 kali dari jumlah komputasi yang masuk akal
      Meski alur kerja yang buruk butuh beberapa kali lebih lama sebelum gagal, tetap saja masih dalam orde milidetik, jadi menurut saya tidak banyak merugikan
      Biasanya masalah ini muncul ketika seseorang memperlakukan domain masalah sebagai graf berarah asiklik, tetapi tidak berhasil memaksakan sifat “asiklik”-nya. Memodelkan masalah sebagai graf berarah asiklik itu seperti Dark Galadriel yang mempertimbangkan apakah akan menerima cincin dari Frodo. “Semua akan mencintaiku dan putus asa.” Orang-orang yang membuat hal seperti ini selalu jauh lebih bangga daripada hal yang sebenarnya pantas mereka banggakan
      Pada akhirnya, pelanggan yang terseret ke solusi mahal dan kompleks akan kehabisan uang, dan masalah mereka sendiri juga mulai terlihat jauh lebih kecil. Lalu, secara harfiah, yang tersisa hanyalah aplikasi yang biaya per tugasnya tidak bisa dibuat cukup rendah untuk mempertahankan bisnis pelanggan
    • Memprediksi pemakaian bahan bakar komputasi blockchain secara tepat mungkin menarik bagi orang lain, tetapi tidak bagi saya
      Saya lebih tertarik memakainya sebagai palu lain di kotak perkakas untuk menangkap bug yang lolos dari palu-palu sebelumnya seperti pemeriksaan tipe statis, tidak ada null, dan tidak ada mutasi
      Fakta bahwa program berakhir dalam waktu hingga memang tidak membuktikan kebenaran, tetapi jika saya menyatakan bahwa kode saya berakhir dalam waktu hingga dan compiler tidak setuju, saya akan percaya bahwa kode itu salah
    • Batas atas yang ditentukan secara statis bisa sangat melebih-lebihkan kompleksitas waktu eksekusi aktual pada kasus umum. Sebab, secara umum kita tidak bisa memprediksi bagaimana percabangan kondisi yang menyebabkan early termination dalam rekursi akan dievaluasi
      Agar early termination memengaruhi waktu eksekusi, kita harus mengasumsikan lazy evaluation atau short-circuit conditional, tetapi bahasa praktis biasanya memang memilikinya
    • Bagaimana jika batas atas itu sangat longgar? Misalnya quicksort deterministik biasanya n log n, tetapi memiliki batas atas kuadratik terhadap ukuran input
      Apakah perhitungan quicksort lalu akan ditolak? Lebih ekstrem lagi, algoritma Hindley–Milner punya batas atas waktu eksponensial, tetapi dalam praktiknya sering berjalan dalam waktu linear
    • Saya tidak tahu apakah itu “dihitung secara statis”, tetapi menurut saya satu-satunya keunggulan dari membatasi kemampuan bahasa secara besar-besaran adalah kita bisa memasang batas komputasi yang tidak bergantung pada data
      Namun sulit bagi saya membayangkan situasi ketika itu benar-benar merupakan persyaratan kuat. Berapa banyak sistem yang tidak bisa mengeluarkan error “query berjalan terlalu lama”?

  • Saya pernah ingin mencoba bahasa pemrograman web backend yang berbasis prinsip tidak tidak-berakhir/berbatas
    Idenya, compiler membuktikan bahwa setiap fungsi, untuk state dan argumen yang diberikan, dieksekusi dalam batas tertentu, serta bisa menunjukkan bahwa X adalah batas bawah dan Y adalah batas atas. Informasi ini dipropagasikan sampai ke entry point
    Saya setuju dengan penulis bahwa kita membutuhkan semantik yang lebih kuat, dan karena itulah saya memikirkan bahasa ini. Sering kali kita menginginkan jaminan atas waktu eksekusi program
    Intinya akan berbasis fungsi rekursif primitif, tetapi dalam praktiknya bisa saja Turing-complete. Seperti Rust menolak borrow yang salah tetapi tetap menyediakan unsafe untuk pointer primitif, bahasa ini juga akan menghitung batas atas berdasarkan primitive sederhana untuk iterasi, atau memungkinkan operator unsafe dan meminta kita menyediakan rumus pengganti untuk batasnya

  • Saya tidak begitu memahami bagian keluhan/motivasi singkat di tulisan itu
    Maksud saya bagian: “Biasanya, di area tertentu, sifat tidak Turing-complete dipuji sebagai keunggulan atau persyaratan. Saya pikir kebanyakan diskusi seperti itu salah paham — tidak Turing-complete tidak berarti seperti yang orang harapkan”
    Mengapa diskusi seperti itu dianggap salah? Kebanyakan alat analisis formal, misalnya Coq, Isabelle, dan Agda, biasanya mensyaratkan bukti bahwa sebuah fungsi berakhir. Itu sama saja dengan membuktikan bahwa fungsi tersebut adalah fungsi total, dan dengan demikian berarti fungsi itu rekursif primitif, bukan?

    • Saya belum membacanya sampai akhir, tetapi tulisan ini tampaknya berangkat dari beberapa bahasa konfigurasi yang mengiklankan “tidak Turing-complete” sebagai fitur. Padahal fitur yang sebenarnya ingin dipromosikan kemungkinan adalah waktu eksekusi yang dibatasi secara wajar
      Ini juga muncul dalam diskusi terbaru tentang CEL:
      https://news.ycombinator.com/item?id=40954652
    • Kalau yang dibahas adalah pembuktian formal, maka dalam kasus umum membuktikan bahwa sebuah fungsi adalah fungsi total adalah masalah pencarian NP-complete, bukan contoh tandingan ilmiah yang dipakai dalam pemrograman modern
      Kalau ingatan saya benar, ini setara dengan NP dengan oracle co-NP, atau tingkat kedua dari hierarki polinomial. Bahkan untuk masalah kecil pun, ini bisa dilakukan tetapi mahal
      Alat-alat seperti ini bekerja paling baik ketika program distrukturkan agar menjadi fungsi total. Dalam pemrograman terstruktur, cara yang paling umum adalah hanya memakai FOR, atau memakai WHILE/rekursi dengan jumlah iterasi terbatas
      Meski hanya terkait SAT, bentuk-bentuk yang mudah ditangani dalam teorema dikotomi Schaefer adalah lensa paling mudah diakses yang bisa saya pikirkan
    • Seperti ditunjukkan tulisan itu, ada fungsi yang berakhir tetapi tidak rekursif primitif, jadi pembuktian fungsi total tidak berarti fungsi itu rekursif primitif
      Agda, dan mungkin alat lain juga, dapat membuktikan termination untuk sebagian fungsi rekursif non-primitif yang memang berakhir. Tentu tidak semuanya mungkin
      Kesalahpahaman yang dikeluhkan tulisan itu kira-kira terlihat seperti ini: “Turing-completeness berarti bisa melakukan komputasi, sedangkan non-Turing-completeness berarti tidak bisa melakukan komputasi dan memiliki sifat bahasa konfigurasi yang baik.”
      Inti tulisan itu adalah bahwa meski tidak Turing-complete, kita tetap bisa melakukan banyak hal yang biaya komputasinya besar atau rumit, dan untuk bahasa konfigurasi, dibutuhkan batasan yang jauh lebih ketat daripada sekadar tidak Turing-complete
    • Ada cara lain untuk menjadi tidak Turing-complete selain menjadi fungsi total yang berakhir dengan rapi. Misalnya, infinite loop tidak bisa melakukan komputasi universal dan juga tidak berakhir

  • Saya adalah pengembang CUE. CUE bersifat rekursif primitif, dan juga memenuhi kriteria yang diharapkan dari bahasa konfigurasi yang “baik”