ट्री कैलकुलस

 (treecalcul.us)
1 पॉइंट द्वारा GN⁺ 2024-12-11 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • यह एक ऐसी प्रणाली है जो न्यूनतम व्याकरण से computation बनाना चाहती है, और केवल एक operator △ तथा application के जरिए minimality, Turing completeness, reflectivity और modularity—इन सभी को संभालती है
  • इसका व्याकरण E::= △ | E E है, और जब △ तीन मानों पर कार्य करता है तो computation होता है; मान प्राकृतिक binary tree होते हैं जो leaf, stem और fork nodes से बने होते हैं
  • combinatory logic के K और S को Tree Calculus के भीतर व्यक्त किया जा सकता है, इसलिए इसमें Turing completeness है; और λ-calculus से अलग, यह recursive functions को normal form में व्यक्त कर सकता है
  • क्योंकि programs को भी values की तरह संभाला जाता है, self-application के जरिए introspection और reflection संभव है, और size size के 168 पर evaluate होने का उदाहरण दिया गया है
  • subterms, subtrees के रूप में दिखाई देते हैं, जिससे common functionality bootstrap करना, serialization, program analysis·optimization, और static·dynamic typing जैसे demos तक बात पहुँचती है

एक operator से बनने वाले प्राकृतिक binary tree

  • Tree Calculus की खोज Barry Jay ने की थी, और साइट पर उनकी किताब व ब्लॉग के साथ Johannes Bader द्वारा विकसित demos के लिंक दिए गए हैं
  • इसकी मुख्य विशेषताएँ चार हैं: minimal, Turing-complete, reflective, modular

  • न्यूनतमता

    • Tree Calculus में केवल एक operator △ है
    • इसका व्याकरण E ::= △ | E E के रूप में है
    • दृश्य रूप में △ एक tree node है, और E1 को E2 पर apply करने पर E2, E1 के root के दाईं ओर जुड़ जाता है
    • values प्राकृतिक binary trees हैं, और nodes को leaf, stem, fork कहा जाता है
    • व्यावहारिक demos
      • portability: कई platforms पर सरल और सुरक्षित interpreter बनाए जा सकते हैं
      • emit-json: cross-platform configuration generation के लिए उपयुक्त उदाहरण दिखाता है

ट्यूरिंग पूर्णता और reflection

  • ट्यूरिंग पूर्णता

    • combinatory logic के K और S operators को Tree Calculus में व्यक्त किया जा सकता है
    • K = △ △
    • S x = △ (△ x)
    • combinatory logic की K/S नींव complete है, इसलिए Tree Calculus भी Turing-complete है
    • λ-calculus से अलग, orange/brown जैसे fixed-point constructions के साथ recursive functions को normal form में व्यक्त किया जा सकता है

  • reflection

    • triage {l, s, f} = △ (△ l s) f leaf, stem, fork के लिए case analysis करता है
    • प्राकृतिक संख्या n को △^n △ के रूप में व्यक्त किया जा सकता है
    • 0-test को triage {true, K false, K² false} के रूप में बनाया जाता है
    • क्योंकि programs भी values हैं, intensional programs self-application के जरिए introspection और reflection कर सकते हैं
    • उदाहरण program size अपने argument के nodes की संख्या गिनता है, और size size 168 पर evaluate होता है
    • व्यावहारिक demos
      • serialize-anything: program serialization की संभावना पर चर्चा करता है
      • halting-problem: halting problem को अधिक सरल रूप में formalize करता है
      • fusion: program analysis·optimization को functions के रूप में व्यक्त करता है
      • gradual-typing: static typing और dynamic typing को function calls के रूप में संभालने का उदाहरण देता है

modularity और demos

  • subterms को subtrees के रूप में व्यक्त किया जाता है
  • पेज के शीर्ष पर दिया गया size program, triage का उपयोग कर nodes को recursively गिनता है
  • व्यावहारिक demos
    • bootstrap-basics: common functionality को आसानी से bootstrap किया जा सकता है
    • size-of-meaningful-programs: यह दिखाता है कि शक्तिशाली programs का tree अनिवार्य रूप से बड़ा होना जरूरी नहीं है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-12-11
Hacker News की राय

  • Tree Calculus एक शानदार विषय है, जिसके निहितार्थ इस वेबसाइट से कहीं आगे तक जाते हैं
    हालांकि अफसोस है कि वेबसाइट इसके प्रवर्तक और लेखक Prof. Barry Jay को स्पष्ट रूप से नहीं दिखाती। और जानना हो तो Jay की किताब देखें: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • “Specification” पेज पर उनकी किताब का संदर्भ दिया गया है
      attribution को और स्पष्ट किया जा सकता है और किया भी जाएगा, लेकिन श्रेय हड़पने का बिल्कुल इरादा नहीं है। पृष्ठभूमि इस जवाब में और लिखी है: https://news.ycombinator.com/item?id=42375914
    • इसे देखते ही मुझे सबसे पहले Barry Jay की Bondi Language / Pattern Calculus याद आई, और लगता है यह पूरी तरह गलत दिशा नहीं थी

  • देखने में तो अच्छा लगता है, लेकिन यह पेज इतनी कम guidance देता है कि समझना मुश्किल है
    “beginners” के लिए कोई explanation होता तो अच्छा रहता

    • SKI calculus या उसके cousin lambda calculus की तरह, यह एक सरल computation model है जिसमें expressions को mechanically evaluate या reduce करने के exact rules होते हैं: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      SKI calculus से फर्क यह है कि यह अपने program structure पर reflection कर सकता है; उदाहरण के लिए, दो programs समान हैं या नहीं, यह तय करना संभव है: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      साथ ही lambda calculus के विपरीत, दिए गए reduction rules लागू करने पर program एक stable normal form में converge करता है, और उन cases से बचा जा सकता है जहाँ वह infinite reduction chain में फँस सकता है: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      इसलिए programs को quote या serialize करके stable data structure के जरिए घुमाए बिना भी reflection संभव है, और यह Lisp की homoiconicity से कुछ हद तक मिलता-जुलता है
    • main landing page की बनावट काफी अजीब है
      यह किसी trendy programming language या framework website की तरह one-word title, थोड़ा buzzword जैसा phrase और animated code example इस्तेमाल करता है, लेकिन body बहुत dense और लंबी academic style में है। फिर भी, सिर्फ उस academic style से यह समझने लायक details नहीं मिलतीं कि असल में हो क्या रहा है
      मैंने काफी देर paragraphs parse करने की कोशिश की, लेकिन verbose होने के बावजूद यह आम programming language landing page की तरह बस यही बताता है कि “लेखक को इस language में क्या अच्छा लगता है”, काम करने का तरीका नहीं समझाता। लगता है आखिरकार specification ही देखना पड़ेगा
    • specification की grammar E ::= t | E E पहली नजर में यह गलतफहमी पैदा कर सकती है कि सभी expressions बस t t t t t t t जैसे दिखते हैं
      असल में parentheses structure बनाए रखना पड़ता है, इसलिए वे (t t) (t ((t t) (t t))) जैसे form में होते हैं, और top level तथा हर parenthesis के अंदर हमेशा ठीक दो sub-expressions होते हैं। यानी whitespace character एक binary operator की तरह काम करता है
      इस expression में parentheses बहुत हैं, इसलिए इस binary operator को left-associative माना जाता है। a b c को (a b) c, और a b c d को ((a b) c) d की तरह interpret किया जाता है
      इस तरह देखने पर समझ आता है कि tree कहाँ से आता है। leaf symbol सिर्फ एक t है, इसलिए unnecessary parentheses हटाने पर हर expression हमेशा t से शुरू होता है, और उसके बाद कई expressions आते हैं। पहले t को node के रूप में draw करें, और हर बाद वाले expression के लिए इसी प्रक्रिया से subtree draw करें
      specification page के semantic rules बताते हैं कि तीन या उससे अधिक subtrees वाले node को “simplify” कैसे करना है, यानी t के बाद तीन या अधिक sub-expressions लगे expression को कैसे reduce करना है
    • पेज के सबसे ऊपर “Tree Calculus [purpose summary] के लिए एक [noun phrase] है” जैसी definition sentence हो तो मदद मिलेगी
      Wikipedia articles आम तौर पर “Lambda calculus … के लिए एक formal system है”, “Matrix calculus … के लिए एक specialized notation है” जैसे शुरू होते हैं
    • संक्षेप में, यह एक programming language है जिसमें programs और values दोनों unlabeled trees हैं
      unlabeled tree एक tree-like data structure है जिसमें nodes में data नहीं होता, और children का order होता है। Tree Calculus ऐसे rules का set define करता है जो unlabeled trees को evaluate करके दूसरे unlabeled trees देता है
      rules को बार-बार apply करने पर या तो infinite loop में फँसते हैं, या ऐसे tree तक पहुँचते हैं जो आगे नहीं बदलता। rules इस तरह design किए गए हैं कि binary trees पर असर न पड़े, इसलिए binary tree को evaluate करने पर वही tree वापस मिलता है और computation finished state में होता है
      ये rules “Specification” page पर programming language theory में आम small-step semantics के रूप में लिखे गए हैं
      दावा यह है कि evaluation rules Turing-complete हैं, इसलिए कोई भी computation express किया जा सकता है, और evaluation asymptotically optimal है, यानी किसी भी language का program Tree Calculus में लगभग constant overhead के साथ चलाया जा सकता है। पहली नजर में यह दावा असंभव नहीं लगता, लेकिन असल में यह कितना महत्वपूर्ण है, स्पष्ट नहीं है
      इसका use कुछ programming language theory researchers के लिए दिलचस्प हो सकता है, और संभव है कि computation theory proofs को सरल बनाने में काम आए। अगर ऐसी चीजें आपको interesting लगती हैं, तो Tree Calculus से पहले उससे ज्यादा सरल, ज्यादा प्रसिद्ध और उपयोगी lambda calculus सीखने की सलाह दूँगा

  • homepage पर “Democratizing Functions”, “Democratizing Metatheory” लिखा है, लेकिन मतलब जो भी हो, democratizing शब्द का बहुत ज़्यादा इस्तेमाल किया जा रहा है ऐसा लगता है

    • यह usage काफ़ी आम है
      Britannica की दूसरी definition भी “किसी चीज़ को हर किसी के लिए उपलब्ध बनाना, हर किसी के लिए समझने योग्य बनाना” है: https://www.britannica.com/dictionary/democratize
    • सहमत। “What democratize really means” भी देखने लायक है: https://intage.us/articles/words/democratize/
      “भाषा संस्कृति से आकार लेती है, और आप भी उस संस्कृति का हिस्सा हैं। ज़िम्मेदारी छोड़ने की ज़रूरत नहीं है। विकल्प मौजूद हैं”

  • Tree Calculus के reduction rules के logic को “feel” से समझने के लिए मैंने खुद diagrams बनाए: https://latypoff.com/tree-calculus-visualized/
    visual सोचने वाले लोगों के लिए मददगार हो सकता है

    • बहुत मददगार। खासकर ध्यान से लिखा गया text अच्छा है
      हालांकि दूसरे diagram “Stem with a single leaf child” में error दिखता है। triangle से नीचे जाने वाली line square से जुड़ती है, लेकिन लगता है वह square की जगह circle होना चाहिए
    • वाकई अच्छा है। अगर इसे animatable form में बनाया जाए, तो website के Specification page पर बहुत फिट बैठेगा

  • मुझे जिज्ञासा है कि जिन्होंने इसे recommend किया, क्या उन्होंने सच में समझकर recommend किया था

    • मेरी नज़र में यह lambda calculus का एक और implementation जैसा दिखता है, और web page यह समझा नहीं पाता कि यह interesting क्यों है—यह भी अफ़सोस की बात है
    • मैंने recommend इसलिए किया क्योंकि लगा कि इससे interesting discussion आगे बढ़ेगा
    • मैंने recommend इसलिए किया कि उम्मीद थी कोई समझा देगा

  • क्या कोई समझा सकता है कि यह सिर्फ अलग syntax वाला Lisp या Forth क्यों नहीं है?
    मैं आलोचना करने या इसे सतही तौर पर dismiss करने की कोशिश नहीं कर रहा, सच में समझना चाहता हूँ

    • Lisp lambda calculus पर आधारित है, लेकिन lambda calculus में अपने अंदर लिखे program को modify करने का कोई tool नहीं होता
      यह feature उपयोगी है, इसलिए Lisp-family languages में macros जैसी चीज़ें जोड़ी जाती रही हैं, और इनके implementation के तरीके भी अलग-अलग हैं। Lisp family में आम eval भी lambda calculus का हिस्सा नहीं है। lambda calculus में केवल abstraction, application और variables होते हैं; environment नहीं होता
      अगर reflection की concept अच्छी तरह defined है और Tree Calculus reflective है, तो यह निश्चित रूप से सिर्फ अलग syntax वाला Lisp नहीं है, और Forth तो बिल्कुल भी नहीं
      मैं expert नहीं हूँ, इसलिए इसे काफी caution के साथ लें। Practical तौर पर यह धीमे Lisp जैसा दिख सकता है, लेकिन theoretical तौर पर यह lambda calculus से अलग है और धीमे Lisp जैसी चीज़ों को और सरलता से implement करने के आधार के रूप में इस्तेमाल हो सकता है
    • अगर mandatory parentheses और indentation sensitivity नहीं है, तो मेरी पसंद के हिसाब से यह पहले ही बड़ा advantage है
      दूसरी preferences भी बिल्कुल ठीक हैं, लेकिन homoiconicity का ज़्यादातर Lisp dialects तक सीमित रह जाना अफ़सोस की बात है

  • SKI के Z combinator को lambda calculus example से होते हुए Tree Calculus में convert करके tree के रूप में output किया
    Test नहीं किया है, लेकिन original tool से convert किया गया unoptimized code है। संबंधित background के लिए fixed-point combinator document देखें: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Z combinator को Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)) के रूप में कहीं ज़्यादा सरलता से लिखा जा सकता है, और SKI में भी इसे छोटा express किया जा सकता है

  • Johannes को Tree Calculus पर experiment करते और मेरी book GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf में जो possibilities केवल implicitly थीं, उन्हें explicitly दिखाते हुए देखना अच्छा लगा
    आखिरकार typed Tree Calculus आ गया है, और इसलिए मैंने GitHub.com/barry-jay-personal पर blog लिखना शुरू किया

    • book के लिए working link यह है: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      दाईं तरफ download button ढूँढें
    • “Typed Program Analysis Without Encodings” paper में मेरी बहुत रुचि है, लेकिन online नहीं मिला। कहाँ देखना चाहिए, जानना चाहूँगा

  • इसे काफी देर देखने के बाद मुझे कुछ बातें समझ आईं। खासकर lambda calculus या formal semantics से कुछ हद तक परिचित लोगों के लिए footing पाने में मददगार हो सकती हैं
    small-step semantics का मतलब समझने के लिए मुझे OCaml implementation तक जाना पड़ा, क्योंकि basic tree structure साफ़ नहीं दिख रहा था। definition के चार-element reduction expressions में पहले तीन terms पर parentheses लगाकर देखें तो पता चलता है कि क्या किस पर apply हो रहा है। right side पर भी parentheses कम लगते हैं
    उदाहरण के लिए (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 की तरह देखना बेहतर है
    साथ ही table में कुछ cases छूटे हैं जिन्हें शायद grammar की associativity से “obvious” माना गया है; अगर t a -> (t a), (t a) b -> (t a b) की तरह जोड़ दें, तो E E grammar के expressions पर semantic reduction को ज्यादा साफ़ तौर पर apply किया जा सकता है
    मुख्य बात यह है कि lambda calculus में lambda को बांधकर दो choices में से एक को “चुनने” जैसा बनाता है, उसी तरह यह Tree Calculus दिए गए node के leaf, stem या fork होने के आधार पर तीन choices करवाने के लिए बनाया गया है। Rules 3a, 3b, 3c का core यही है, और system की बाकी functionality इसी 3-way choice पर बनी है

    • यह explanation पहले page पर होना चाहिए था
      इसकी वजह से यह interesting calculus जैसा तो दिखता है, लेकिन यह SKI या lambda calculus की तुलना में reverse conversion, serialization, compilation के लिए ज्यादा suitable है या नहीं—यह अलग बात है। Reverse conversion मुश्किल है, serialization आसान है, और compilation ठीक-ठाक आसान है

  • Python में Leaf को खाली list, Stem को single-element list, और Fork को two-element list मानकर apply को specification के OCaml code के अनुसार implement किया जा सकता है
    false, true, not को tree के रूप में define करने पर not false -> true, not true -> false काम करता है

    • Racket या Scheme में भी यही idea इस्तेमाल किया जा सकता है
      Leaf को null, Stem को list, और Fork को cons मानें, और apply t-not t-false तथा apply t-not t-true से वही result verify किया जा सकता है