Kalkulus Pohon

 (treecalcul.us)
1 poin oleh GN⁺ 2024-12-11 | 1 komentar | Bagikan ke WhatsApp
  • Sebuah sistem yang berupaya menyusun komputasi dengan sintaks minimal, membahas minimalitas, kelengkapan Turing, reflektivitas, dan modularitas hanya dengan satu operator △ serta aplikasi
  • Sintaksnya adalah E::= △ | E E, dan ketika △ bekerja pada tiga nilai, komputasi dilakukan; nilainya adalah pohon biner alami yang terdiri dari node daun, batang, dan percabangan
  • K dan S dari logika kombinator dapat diekspresikan di dalam Tree Calculus, sehingga bersifat Turing-complete; berbeda dari λ-calculus, fungsi rekursif dapat diekspresikan dalam bentuk normal
  • Karena program juga diperlakukan sebagai nilai, introspection dan refleksi melalui self-application dimungkinkan; ada contoh size size yang dievaluasi menjadi 168
  • Subterm tampak sebagai subtree, yang berlanjut ke demo seperti bootstrap fungsi umum, serialisasi, analisis dan optimisasi program, serta static/dynamic typing

Pohon biner alami yang dibuat dengan satu operator

  • Tree Calculus ditemukan oleh Barry Jay, dan situsnya menautkan ke buku serta blognya, juga demo yang dikembangkan oleh Johannes Bader
  • Karakteristik intinya dirangkum menjadi empat: minimal, Turing-complete, reflective, dan modular

  • Minimalitas

    • Tree Calculus hanya memiliki satu operator, △
    • Sintaksnya berbentuk E ::= △ | E E
    • Secara visual, △ adalah node pohon, dan ketika E1 diterapkan pada E2, E2 ditempelkan di sisi kanan root E1
    • Nilainya adalah pohon biner alami, dan node disebut leaf, stem, dan fork
    • Demo praktis
      • portability: memungkinkan pembuatan interpreter yang sederhana dan aman di berbagai platform
      • emit-json: menunjukkan contoh yang cocok untuk menghasilkan konfigurasi lintas platform

Kelengkapan Turing dan refleksi

  • Kelengkapan Turing

    • Operator K dan S dari logika kombinator dapat diekspresikan dengan Tree Calculus
    • K = △ △
    • S x = △ (△ x)
    • Karena basis K/S dalam logika kombinator bersifat lengkap, Tree Calculus juga Turing-complete
    • Berbeda dari λ-calculus, fungsi rekursif dapat diekspresikan dalam bentuk normal dengan konstruksi fixed point seperti orange/brown

  • Reflektivitas

    • triage {l, s, f} = △ (△ l s) f melakukan analisis kasus untuk leaf, stem, dan fork
    • Bilangan natural n dapat direpresentasikan sebagai △^n △
    • Uji 0 disusun sebagai triage {true, K false, K² false}
    • Karena program juga merupakan nilai, program intensional dapat melakukan introspection dan refleksi melalui self-application
    • Contoh program size menghitung jumlah node pada argumennya, dan size size dievaluasi menjadi 168
    • Demo praktis
      • serialize-anything: membahas kemungkinan serialisasi program
      • halting-problem: memformulasikan masalah halting dengan lebih sederhana
      • fusion: mengekspresikan analisis dan optimisasi program sebagai fungsi
      • gradual-typing: menyediakan contoh yang menangani static typing dan dynamic typing sebagai pemanggilan fungsi

Modularitas dan demo

  • Subterm direpresentasikan sebagai subtree
  • Program size di bagian atas halaman menggunakan triage untuk menghitung node secara rekursif
  • Demo praktis

Bacaan terkait

1 komentar

 
GN⁺ 2024-12-11
Opini Hacker News

  • Tree Calculus adalah topik keren dengan implikasi yang melampaui situs web ini
    Namun sayang situs webnya tidak secara eksplisit mencantumkan Prof. Barry Jay sebagai pencetus sekaligus penulisnya. Jika ingin tahu lebih lanjut, lihat buku Jay: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • Halaman “Specification” memang merujuk ke bukunya
      Atribusi bisa dibuat lebih jelas, dan kami memang berniat melakukannya, tetapi sama sekali tidak ada niat untuk mengambil kredit. Latar belakangnya saya tulis lebih lanjut di balasan ini: https://news.ycombinator.com/item?id=42375914
    • Begitu melihat ini, yang pertama terlintas di benak saya adalah Bondi Language / Pattern Calculus milik Barry Jay, dan sepertinya itu tidak sepenuhnya meleset

  • Memang terlihat keren, tetapi halaman ini memberi terlalu sedikit panduan sehingga sulit dipahami
    Akan bagus kalau ada penjelasan “untuk pemula”

    • Seperti SKI calculus atau kerabatnya, lambda calculus, ini adalah model komputasi sederhana dengan aturan persis untuk mengevaluasi atau mereduksi ekspresi secara mekanis: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      Bedanya dari SKI calculus adalah ia dapat merefleksikan struktur programnya sendiri, misalnya memungkinkan untuk menentukan apakah dua program sama: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Selain itu, berbeda dari lambda calculus, jika aturan reduksi yang diberikan diterapkan, program akan konvergen ke normal form yang stabil, sehingga menghindari kasus yang bisa masuk ke rantai reduksi tak hingga: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Jadi refleksi dimungkinkan tanpa harus mengutip atau menserialisasi program lalu memutar lewat struktur data yang stabil, dan ada kemiripan dengan homoiconicity pada Lisp
    • Susunan halaman landing utamanya cukup aneh
      Ia memakai judul satu kata, frasa yang agak seperti buzzword, dan contoh kode bergerak seperti situs web bahasa pemrograman atau framework yang sedang tren, tetapi isi teksnya justru bergaya akademis yang terlalu padat dan panjang. Namun gaya akademis itu sendiri pun tidak menyediakan detail yang cukup untuk memahami apa yang sebenarnya terjadi
      Saya mencoba mem-parsing paragraf-paragrafnya cukup lama, tetapi meski bertele-tele, seperti halaman landing bahasa pemrograman pada umumnya ia hanya mengatakan “apa yang menurut penulis bagus dari bahasa ini”, bukan menjelaskan cara kerjanya. Pada akhirnya sepertinya harus melihat spesifikasinya
    • Tata bahasa pada spesifikasi, E ::= t | E E, saat pertama dilihat mudah membuat orang keliru mengira semua ekspresi hanyalah seperti t t t t t t t
      Kenyataannya struktur tanda kurung harus dipertahankan, sehingga bentuknya menjadi seperti (t t) (t ((t t) (t t))), dan pada tingkat teratas maupun di dalam setiap tanda kurung selalu ada tepat dua subekspresi. Dengan kata lain, karakter spasi bertindak seperti operator biner
      Karena ekspresi ini memiliki banyak tanda kurung, operator biner ini dipandang sebagai left-associative. a b c ditafsirkan sebagai (a b) c, dan a b c d sebagai ((a b) c) d
      Dengan cara pandang ini, terlihat dari mana pohonnya berasal. Karena satu-satunya simbol terminal adalah t, jika tanda kurung yang tidak perlu dihapus, semua ekspresi selalu diawali t dan diikuti beberapa ekspresi. Gambar t pertama sebagai node, lalu untuk setiap ekspresi yang mengikutinya, gambar subtree dengan prosedur yang sama
      Aturan semantik di halaman spesifikasi menjelaskan cara “menyederhanakan” node yang memiliki tiga subtree atau lebih, yaitu cara mereduksi ekspresi yang memiliki tiga atau lebih subekspresi setelah t
    • Akan membantu jika di bagian paling atas halaman ada kalimat definisi seperti “Tree Calculus adalah [frasa nomina] untuk [ringkasan tujuan]”
      Artikel Wikipedia biasanya dimulai seperti “Lambda calculus adalah sistem formal untuk …”, “Matrix calculus adalah notasi khusus untuk …”, dan semacamnya
    • Singkatnya, ini adalah bahasa pemrograman yang program dan nilainya sama-sama berupa pohon tanpa label
      Pohon tanpa label adalah struktur data berbentuk pohon yang node-nya tidak memiliki data, tetapi urutan anak-anaknya ada. Tree Calculus mendefinisikan sekumpulan aturan untuk mengevaluasi pohon tanpa label menjadi pohon tanpa label lain
      Jika aturan diterapkan berulang-ulang, hasilnya bisa masuk loop tak hingga, atau mencapai pohon yang tidak berubah lagi. Aturan dirancang agar tidak memengaruhi pohon biner, sehingga jika pohon biner dievaluasi, hasilnya adalah pohon yang sama dan komputasinya berada dalam keadaan selesai
      Aturan-aturan ini ditulis di halaman “Specification” dalam bentuk small-step semantics yang umum dalam teori bahasa pemrograman
      Klaimnya adalah aturan evaluasi ini Turing complete sehingga dapat mengekspresikan komputasi apa pun, dan evaluasinya secara asimtotik optimal sehingga program dari bahasa apa pun dapat dijalankan di Tree Calculus dengan overhead yang hampir konstan. Sekilas klaim ini tidak terdengar mustahil, tetapi seberapa penting dalam praktiknya belum jelas
      Kegunaannya mungkin menarik bagi sebagian peneliti teori bahasa pemrograman, dan mungkin bisa dipakai untuk menyederhanakan pembuktian dalam teori komputasi. Jika hal semacam ini menarik bagi Anda, saya menyarankan mempelajari lambda calculus terlebih dahulu, karena lebih sederhana, lebih dikenal, dan lebih berguna daripada Tree Calculus

  • Di beranda tertulis “Democratizing Functions” dan “Democratizing Metatheory”; apa pun maksudnya, terasa sekali kata democratizing dipakai berlebihan

  • Saya membuat sendiri gambar untuk memahami logika aturan reduksi Tree Calculus dengan “intuisi”: https://latypoff.com/tree-calculus-visualized/
    Ini mungkin membantu orang yang berpikir secara visual

    • Sangat membantu. Terutama teksnya yang ditulis dengan cermat terasa bagus
      Namun pada gambar kedua, “Stem with a single leaf child”, tampaknya ada kesalahan. Garis yang turun dari segitiga tersambung ke persegi, padahal sepertinya persegi itu seharusnya lingkaran
    • Bagus sekali. Kalau dibuat dalam bentuk yang bisa dianimasikan, rasanya akan sangat cocok untuk halaman Specification di situs webnya

  • Saya penasaran apakah orang-orang yang merekomendasikan ini benar-benar memahami apa ini lalu merekomendasikannya

    • Di mata saya, ini tampak seperti implementasi lain dari kalkulus lambda, dan sayang sekali halaman webnya juga tidak menjelaskan mengapa ini menarik
    • Saya merekomendasikannya karena tampaknya akan memicu diskusi yang menarik
    • Saya merekomendasikannya sambil berharap ada seseorang yang menjelaskan

  • Bisakah seseorang menjelaskan mengapa ini bukan sekadar Lisp atau Forth dengan sintaks berbeda?
    Saya bukan bermaksud mengkritik atau meremehkan secara dangkal; saya benar-benar ingin memahami

    • Lisp berbasis kalkulus lambda, sedangkan kalkulus lambda sendiri tidak memiliki alat untuk memodifikasi program yang tertulis di dalam dirinya
      Karena kemampuan ini berguna, bahasa-bahasa keluarga Lisp menambahkan hal seperti makro, dan cara implementasinya pun beragam. Bahkan eval yang umum di keluarga Lisp bukan bagian dari kalkulus lambda. Kalkulus lambda hanya memiliki abstraksi, aplikasi, dan variabel; tidak ada environment
      Jika konsep refleksi terdefinisi dengan baik dan Tree Calculus bersifat reflektif, maka ini jelas bukan sekadar Lisp dengan sintaks berbeda, apalagi Forth
      Saya bukan pakar, jadi anggap dengan banyak catatan. Secara praktis ini mungkin terlihat seperti Lisp yang lambat, tetapi secara teoretis berbeda dari kalkulus lambda dan bisa dipakai sebagai dasar yang lebih sederhana untuk mengimplementasikan sesuatu seperti Lisp yang lambat
    • Jika tidak ada tanda kurung wajib dan sensitivitas terhadap indentasi, bagi selera saya itu sudah menjadi keunggulan besar
      Selera lain tentu saja tidak masalah, tetapi sayang homoikonisitas sebagian besar terkurung di dalam dialek-dialek Lisp

  • Saya mencoba mengubah kombinator Z dari SKI ke Tree Calculus melalui contoh kalkulus lambda, lalu mencetaknya sebagai pohon
    Belum saya uji, tetapi aslinya adalah kode belum dioptimalkan yang dikonversi dengan alat. Untuk latar belakang terkait, lihat dokumen kombinator titik tetap: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Kombinator Z dapat ditulis jauh lebih sederhana dalam bentuk Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)), dan juga bisa diekspresikan lebih pendek dalam SKI

  • Senang melihat Johannes bereksperimen dengan Tree Calculus dan secara eksplisit menunjukkan kemungkinan yang hanya tersirat dalam buku saya di GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf
    Akhirnya ada Tree Calculus bertipe, sehingga saya mulai menulis blog di GitHub.com/barry-jay-personal

    • Tautan yang berfungsi ke bukunya ada di sini: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Cari saja tombol unduh di sisi kanan
    • Saya sangat tertarik dengan makalah “Typed Program Analysis Without Encodings”, tetapi tidak bisa menemukannya secara online. Saya penasaran sebaiknya mencarinya di mana

  • Setelah cukup lama menelaah ini, ada beberapa hal yang saya sadari. Ini terutama bisa membantu orang yang sudah cukup akrab dengan kalkulus lambda atau semantik formal untuk mulai memahami
    Saya sampai harus turun ke implementasi OCaml untuk memahami apa arti semantik langkah kecil, karena struktur pohon dasarnya tidak terlihat jelas. Dalam empat rumus reduksi elemen pada definisi, jika tiga suku pertama diberi tanda kurung, terlihat apa yang diaplikasikan ke apa. Sisi kanan juga tampak kurang tanda kurung
    Misalnya, lebih baik membacanya sebagai (t (t) a) b -> a, (t (t a) b) c -> (a c) (b c), (t (t a b) c) t -> a, (t (t a b) c) (t u) -> b u, (t (t a b) c) (t u v) -> (c u) v
    Selain itu, tabelnya melewatkan beberapa kasus yang tampaknya dianggap “jelas” dari asosiativitas sintaks. Jika ditambahkan seperti t a -> (t a), (t a) b -> (t a b), reduksi makna dapat diterapkan dengan lebih rapi pada ekspresi dalam tata bahasa E E
    Intinya, seperti dalam kalkulus lambda kita membungkus lambda agar “memilih” salah satu dari dua opsi, Tree Calculus ini dibuat agar melakukan tiga pilihan bergantung pada apakah node yang diberikan adalah daun, batang, atau cabang. Inilah inti aturan 3a, 3b, 3c, dan sisa fungsi sistem dibangun di atas pilihan tiga-cabang ini

    • Penjelasan ini seharusnya ada di halaman pertama
      Berkat penjelasan ini, memang terlihat seperti kalkulus yang menarik, tetapi apakah ini lebih cocok untuk inversi, serialisasi, dan kompilasi dibanding SKI atau kalkulus lambda adalah soal lain. Inversi sulit, serialisasi mudah, dan kompilasi lumayan mudah

  • Di Python, Leaf dapat direpresentasikan sebagai daftar kosong, Stem sebagai daftar berisi satu elemen, dan Fork sebagai daftar berisi dua elemen, lalu apply dapat diimplementasikan sesuai kode OCaml dalam spesifikasi
    Jika false, true, dan not didefinisikan sebagai pohon, maka not false -> true dan not true -> false akan berfungsi

    • Ide yang sama juga bisa digunakan di Racket atau Scheme
      Leaf cukup dibuat sebagai null, Stem sebagai list, dan Fork sebagai cons; hasil yang sama dapat diperiksa dengan apply t-not t-false dan apply t-not t-true