Ağaç hesabı

 (treecalcul.us)
1 puan yazan GN⁺ 2024-12-11 | 1 yorum | WhatsApp'ta paylaş
  • Hesaplamayı asgari söz dizimiyle kurmayı amaçlayan bir sistem; tek bir operatör △ ve uygulama ile minimalite, Turing tamlığı, yansıtma ve modülerliğin tümünü ele alır
  • Söz dizimi E::= △ | E E biçimindedir; △ üç değere uygulandığında hesaplama yapılır ve değerler yaprak, gövde ve çatal düğümlerden oluşan doğal ikili ağaçlardır
  • Kombinatoryal mantığın K ve S operatörleri Tree Calculus içinde ifade edilebildiği için Turing tamdır; λ-calculus’tan farklı olarak özyinelemeli fonksiyonları normal formda ifade edebilir
  • Programlar da değer olarak ele alındığından, kendi kendine uygulama yoluyla içe bakış ve yansıtma mümkündür; size size ifadesinin 168 olarak değerlendirildiği bir örnek vardır
  • Alt terimler alt ağaçlar olarak görünür; bu da ortak işlevlerin bootstrap edilmesi, serileştirme, program analizi ve optimizasyonu, statik ve dinamik tipleme gibi demolara uzanır

Tek operatörle oluşturulan doğal ikili ağaç

  • Tree Calculus, Barry Jay tarafından keşfedildi; sitede onun kitabı ve blogunun yanı sıra Johannes Bader tarafından geliştirilen demoya bağlantılar yer alıyor
  • Temel özellikler dört başlıkta özetleniyor: minimal, Turing-complete, reflective, modular

  • Minimalite

    • Tree Calculus’ta yalnızca tek bir operatör △ vardır
    • Söz dizimi E ::= △ | E E biçimindedir
    • Görsel olarak △ bir ağaç düğümüdür; E1, E2ye uygulandığında E2, E1in kökünün sağına eklenir
    • Değerler doğal ikili ağaçlardır; düğümler leaf, stem, fork olarak adlandırılır
    • Pratik demolar
      • portability: Birden fazla platformda basit ve güvenli yorumlayıcılar oluşturulabilir
      • emit-json: Çapraz platform yapılandırma üretimine uygun bir örnek gösterir

Turing tamlığı ve yansıtma

  • Turing tamlığı

    • Kombinatoryal mantığın K ve S operatörleri Tree Calculus ile ifade edilebilir
    • K = △ △
    • S x = △ (△ x)
    • Kombinatoryal mantığın K/S temeli tam olduğundan Tree Calculus da Turing tamdır
    • λ-calculus’tan farklı olarak, orange/brown gibi sabit nokta yapılarıyla özyinelemeli fonksiyonlar normal form olarak ifade edilebilir

  • Yansıtma

    • triage {l, s, f} = △ (△ l s) f, leaf, stem ve fork için durum analizi yapar
    • Doğal sayı n, △^n △ olarak ifade edilebilir
    • 0 testi triage {true, K false, K² false} ile kurulur
    • Programlar da değer olduğundan intensional programlar, kendi kendine uygulama ile içe bakış ve yansıtma yapabilir
    • Örnek program size, argümanının düğüm sayısını hesaplar; size size ise 168 olarak değerlendirilir
    • Pratik demolar
      • serialize-anything: Program serileştirme olanağını ele alır
      • halting-problem: Durma problemini daha basit şekilde formüle eder
      • fusion: Program analizi ve optimizasyonunu fonksiyon olarak ifade eder
      • gradual-typing: Statik tipleme ve dinamik tiplemeyi fonksiyon çağrılarıyla ele alan bir örnek sunar

Modülerlik ve demolar

  • Alt terimler alt ağaçlar olarak ifade edilir
  • Sayfanın üst kısmındaki size programı, düğümleri özyinelemeli olarak saymak için triage kullanır
  • Pratik demolar

İlgili okumalar

1 yorum

 
GN⁺ 2024-12-11
Hacker News yorumları

  • Tree Calculus, bu web sitesinin ötesine uzanan sonuçları olan harika bir konu.
    Yine de sitenin kurucu ve yazar Prof. Barry Jay’i açıkça belirtmemesi üzücü. Daha fazlasını öğrenmek isterseniz Jay’in kitabına bakabilirsiniz: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • “Specification” sayfasında kitabına atıf yapılıyor.
      Atfı daha görünür kılabiliriz ve bunu yapmayı planlıyoruz, ancak emeği sahiplenme gibi bir niyet kesinlikle yok. Arka planı şu yanıtta daha ayrıntılı anlattım: https://news.ycombinator.com/item?id=42375914
    • Bunu görür görmez aklıma önce Barry Jay’in Bondi Language / Pattern Calculus çalışması geldi; meğerse tamamen alakasız değilmiş

  • İlginç görünüyor ama bu sayfa o kadar az yönlendirme sunuyor ki anlaması zor.
    “Yeni başlayanlar için” bir açıklama olsa iyi olurdu

    • SKI calculus veya onun kuzeni lambda calculus gibi, ifadeleri mekanik olarak değerlendirmek ya da indirgemek için kesin kuralları olan basit bir hesaplama modeli: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      SKI calculus’tan farkı, kendi program yapısını yansıtabilmesi; örneğin iki programın aynı olup olmadığını belirlemek mümkün: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Ayrıca lambda calculus’tan farklı olarak, verilen indirgeme kuralları uygulandığında program kararlı bir normal form’a yakınsar; böylece sonsuz indirgeme zincirlerine düşülebilen durumlar önlenebilir: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Bu yüzden programları alıntılayıp ya da serileştirip kararlı veri yapılarına dolanmak zorunda kalmadan yansıtma yapılabiliyor; bu da Lisp’in homoiconicity özelliğine benziyor
    • Ana açılış sayfasının kurgusu epey tuhaf.
      Popüler programlama dili veya framework siteleri gibi tek kelimelik bir başlık, hafif buzzword kokan ifadeler ve hareketli kod örnekleri kullanıyor; ama asıl metin gereğinden fazla yoğun ve uzun bir akademik üslupla yazılmış. Üstelik o akademik üslup, neler olup bittiğini anlamaya yetecek kadar ayrıntı da vermiyor
      Paragrafları epey çözmeye çalıştım ama uzunluğuna rağmen, tipik bir programlama dili açılış sayfası gibi yalnızca “yazarın bu dilde neyi iyi bulduğu” anlatılıyor, nasıl çalıştığı açıklanmıyor. Sonunda galiba spesifikasyona bakmak gerekiyor
    • Spesifikasyondaki E ::= t | E E grameri ilk bakışta tüm ifadelerin sadece t t t t t t t gibi göründüğü yanılgısına yol açabiliyor.
      Oysa parantez yapısını korumak gerekiyor; dolayısıyla biçim (t t) (t ((t t) (t t))) gibi oluyor ve en üst düzeyde de her parantezin içinde de her zaman tam olarak iki alt ifade bulunuyor. Yani boşluk karakteri ikili bir işleç gibi davranıyor
      Bu ifadede çok fazla parantez olduğundan, bu ikili işleç sol bağlaşımlı kabul ediliyor. a b c, (a b) c; a b c d ise ((a b) c) d diye yorumlanıyor
      Buna bu şekilde bakınca ağacın nereden geldiği görülüyor. Yaprak sembol olarak yalnızca t bulunduğu için, gereksiz parantezleri kaldırınca tüm ifadeler her zaman t ile başlıyor ve ardından bir dizi ifade geliyor. İlk t’yi düğüm olarak çizin, ardından gelen her ifade için aynı işlemi uygulayarak alt ağaçları çizin
      Spesifikasyon sayfasındaki anlam kuralları, üç veya daha fazla alt ağacı olan düğümlerin nasıl “basitleştirileceğini”, yani t sonrasına üçten fazla alt ifade eklenmiş bir ifadenin nasıl küçültüleceğini anlatıyor
    • Sayfanın en üstünde “Tree Calculus, [amaç özeti] için bir [isim tamlaması]dır” gibi bir tanım cümlesi olsa faydalı olurdu.
      Wikipedia maddeleri genelde “Lambda calculus, … için biçimsel bir sistemdir”, “Matrix calculus, … için özel bir gösterimdir” gibi başlar
    • Özetle bu, programların ve değerlerin tamamının etiketsiz ağaçlar olduğu bir programlama dili.
      Etiketsiz ağaç, düğümlerinde veri bulunmayan ve çocuklarının sırası olan ağaç biçimli bir veri yapısıdır. Tree Calculus, etiketsiz ağaçları değerlendirip başka etiketsiz ağaçlar üreten kurallar kümesini tanımlar
      Kurallar tekrar tekrar uygulandığında ya sonsuz döngüye girilir ya da artık değişmeyen bir ağaca ulaşılır. Kurallar, ikili ağaçları etkilemeyecek şekilde tasarlandığından, bir ikili ağaç değerlendirildiğinde aynı ağaç elde edilir ve hesaplama tamamlanmış olur
      Bu kurallar, “Specification” sayfasında programlama dili kuramında yaygın olan small-step semantics biçiminde yazılmış
      İddia şu: değerlendirme kuralları Turing-complete, yani her türlü hesaplamayı ifade edebiliyor; ayrıca değerlendirme asimptotik olarak optimal, yani herhangi bir dildeki bir program Tree Calculus üzerinde neredeyse sabit bir ek yükle çalıştırılabiliyor. İlk bakışta bu imkânsız bir iddia gibi görünmüyor ama pratikte ne kadar önemli olduğu da net değil
      Kullanım alanı, bazı programlama dili kuramı araştırmacıları için ilgi çekici olabilir ve hesaplama kuramı ispatlarını sadeleştirmede işe yarayabilir. Eğer bu tür şeyler ilginizi çekiyorsa, Tree Calculus’tan önce daha basit, daha bilinen ve daha kullanışlı olan lambda calculus’u öğrenmenizi öneririm

  • Ana sayfada “Democratizing Functions”, “Democratizing Metatheory” yazıyor; ne kastedilirse kastedilsin democratizing kelimesinin fazla kullanıldığı hissi güçlü

    • Bu kullanım oldukça yaygın
      Britannica’nın ikinci tanımı da “bir şeyi herkes için erişilebilir hâle getirmek, herkesin anlayabileceği hâle getirmek” şeklinde: https://www.britannica.com/dictionary/democratize
    • Katılıyorum. “What democratize really means” de bakmaya değer: https://intage.us/articles/words/democratize/
      “Dil kültür tarafından şekillendirilir ve sen de o kültürün bir parçasısın. Sorumluluktan vazgeçmek zorunda değilsin. Seçeneklerin var”

  • Tree Calculus’un indirgeme kurallarının mantığını sezgisel olarak anlamaya çalışırken kendim çizimler yaptım: https://latypoff.com/tree-calculus-visualized/
    görsel düşünen kişiler için faydalı olabilir

    • Çok yardımcı oldu. Özellikle özenle yazılmış metin çok iyi
      Yalnız ikinci şekil olan “Stem with a single leaf child” içinde bir hata var gibi görünüyor. Üçgenden inen çizgi kareye bağlanıyor, ama o karenin daire olması gerekiyor gibi
    • Gerçekten çok iyi. Bunu animasyon yapılabilir bir biçime getirirseniz sitenin Specification sayfasına çok yakışır gibi duruyor

  • Bunu öneren kişilerin gerçekten ne olduğunu anlayarak mı önerdiğini merak ediyorum

    • Bana lambda calculus’un başka bir uygulaması gibi görünüyor ve neden ilginç olduğunu açıklayamayan web sayfası da hayal kırıklığı yaratıyor
    • İlginç bir tartışma çıkacak gibi göründüğü için önerdim
    • Birinin açıklamasını umarak önerdim

  • Bunun sadece sözdizimi farklı bir Lisp ya da Forth olmamasının nedenini açıklayabilir misiniz?
    Eleştirmek ya da yüzeysel biçimde geçiştirmek istemiyorum; gerçekten anlamak istiyorum

    • Lisp, lambda calculus temellidir, ama lambda calculus’un kendisinde içine yazılmış programı değiştirecek araçlar yoktur
      Bu işlev kullanışlı olduğu için Lisp ailesi dillere makrolar gibi şeyler eklenmiştir ve bunların uygulanma biçimi de çeşitlidir. Lisp ailesinde yaygın olan eval bile lambda calculus’un bir parçası değildir. Lambda calculus’ta soyutlama, uygulama ve değişkenler vardır; ortam yoktur
      Eğer yansıtma kavramı iyi tanımlanmışsa ve Tree Calculus yansıtmalıysa, o zaman kesinlikle sadece sözdizimi farklı bir Lisp değildir; Forth ise hiç değildir
      Uzman değilim, o yüzden buna fazla güvenmeyin. Pratikte yavaş bir Lisp gibi görünebilir ama teorik olarak lambda calculus’tan farklıdır ve yavaş Lisp benzeri bir şeyi daha basit biçimde uygulamak için temel olarak kullanılabilir
    • Zorunlu parantezler ve girintiye duyarlılık yoksa, benim zevkime göre bu başlı başına büyük bir avantaj
      Başka zevkler elbette olabilir ama homoiconicity özelliğinin çoğunlukla Lisp lehçelerinin içine hapsolmuş olması üzücü

  • SKI’nin Z combinator’ünü lambda calculus örneğinden geçirip Tree Calculus’a dönüştürdüm ve ağaç olarak yazdırdım
    Test etmedim ama kaynak, bir araçla dönüştürülmüş optimize edilmemiş koddu. İlgili arka plan için fixed-point combinator maddesine bakılabilir: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Z combinator, Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)) biçiminde çok daha basit yazılabilir ve SKI ile de daha kısa ifade edilebilir

  • Johannes’in Tree Calculus ile deneyler yapıp kitabım GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf içinde yalnızca ima edilmiş olan imkânları açıkça göstermesini görmek güzel
    Sonunda typed Tree Calculus ortaya çıktı ve ben de bu yüzden GitHub.com/barry-jay-personal üzerinde blog yazmaya başladım

  • Bunu epey inceledikten sonra birkaç şey fark ettim. Özellikle lambda calculus veya biçimsel anlambilim konusunda biraz aşinalığı olan kişilerin bir başlangıç noktası bulmasına yardımcı olabilir
    Küçük adım anlambilimin ne demek olduğunu anlamak için OCaml uygulamasına kadar inmem gerekti, çünkü temel ağaç yapısı pek görünmüyordu. Tanımdaki dört öğeli indirgeme ifadelerinde ilk üç terimi parantez içine alınca neyin neye uygulandığı ortaya çıkıyor. Sağ tarafta da sanki yeterince parantez yok
    Örneğin bunu (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 şeklinde görmek daha iyi
    Ayrıca tabloda, sözdizimin birleşme özelliğinden “zaten açıkça” çıktığı varsayılan bazı durumlar eksik; t a -> (t a), (t a) b -> (t a b) gibi eklemeler yapılırsa E E dilbilgisinin ifadelerine anlamsal indirgeme daha temiz uygulanabilir
    Asıl mesele şu: lambda calculus’ta bir lambda, iki seçenekten birini “seçmeye” yarayacak şekilde bağlanırken, bu Tree Calculus verilen düğümün yaprak, gövde ya da dal olmasına göre üçlü bir seçim yapacak şekilde kurulmuş. 3a, 3b ve 3c kurallarının özü bu ve sistemin geri kalan işi bu üçlü ayrımın üzerine inşa ediliyor

    • Bu açıklama ilk sayfada olmalıydı
      Bunun ilginç bir calculus gibi görünmesini sağlıyor ama SKI ya da lambda calculus’tan daha uygun biçimde tersine dönüştürme, serileştirme ve derlemeye yarayıp yaramadığı ayrı mesele. Tersine dönüştürme zor, serileştirme kolay, derleme ise orta karar kolaylıkta görünüyor

  • Python'da Leaf boş liste, Stem tek öğeli liste, Fork ise iki öğeli liste olarak alınabilir ve apply, spesifikasyondaki OCaml koduna uygun şekilde uygulanabilir
    false, true, not ağaç olarak tanımlandığında not false -> true, not true -> false çalışır

    • Aynı fikir Racket veya Scheme'de de kullanılabilir
      Leaf için null, Stem için list, Fork için cons alınabilir; apply t-not t-false ve apply t-not t-true ile aynı sonuçlar doğrulanabilir