แคลคูลัสต้นไม้

 (treecalcul.us)
1 คะแนน โดย GN⁺ 2024-12-11 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • เป็นระบบที่มุ่งสร้างการคำนวณด้วยไวยากรณ์ขั้นต่ำ โดยครอบคลุมทั้งความเป็นขั้นต่ำ ความสมบูรณ์แบบทัวริง การสะท้อน และความเป็นโมดูลาร์ ด้วยโอเปอเรเตอร์เพียงตัวเดียว △ และการนำไปใช้
  • ไวยากรณ์คือ E::= △ | E E และเมื่อ △ กระทำกับค่าสามค่า การคำนวณจะเกิดขึ้น โดยค่าคือต้นไม้ไบนารีตามธรรมชาติที่ประกอบด้วยโหนดใบ ลำต้น และกิ่งแยก
  • สามารถแสดง K และ S ของ combinatory logic ภายใน Tree Calculus ได้ จึงมีความสมบูรณ์แบบทัวริง และต่างจาก λ-calculus ตรงที่สามารถแสดงฟังก์ชันเวียนเกิดเป็นรูปแบบปกติได้
  • โปรแกรมก็ถูกจัดการเป็นค่าได้ จึงรองรับ introspection และการสะท้อนผ่านการนำไปใช้กับตัวเอง โดยมีตัวอย่างที่ size size ประเมินได้เป็น 168
  • พจน์ย่อยปรากฏเป็นต้นไม้ย่อย นำไปสู่เดโมอย่างการบูตสแตรปฟังก์ชันพื้นฐานร่วมกัน การทำ serialization การวิเคราะห์และปรับให้เหมาะสมของโปรแกรม รวมถึงการกำหนดชนิดแบบสแตติกและไดนามิก

ต้นไม้ไบนารีตามธรรมชาติที่สร้างด้วยโอเปอเรเตอร์เดียว

  • Tree Calculus ถูกค้นพบโดย Barry Jay และบนเว็บไซต์มีลิงก์ไปยังหนังสือและบล็อกของเขา รวมถึงเดโมที่พัฒนาโดย Johannes Bader
  • คุณสมบัติหลักสรุปได้เป็นสี่ข้อคือ minimal, Turing-complete, reflective, modular

  • ความเป็นขั้นต่ำ

    • ใน Tree Calculus มีโอเปอเรเตอร์เพียงตัวเดียวคือ △
    • ไวยากรณ์อยู่ในรูป E ::= △ | E E
    • ในเชิงภาพ △ คือโหนดของต้นไม้ และเมื่อนำ E1 ไปใช้กับ E2 จะทำให้ E2 ไปติดที่ด้านขวาของรากของ E1
    • ค่าคือต้นไม้ไบนารีตามธรรมชาติ และโหนดเรียกว่า leaf, stem, fork
    • เดโมเชิงใช้งานจริง
      • portability: สามารถสร้างอินเทอร์พรีเตอร์ที่เรียบง่ายและปลอดภัยบนหลายแพลตฟอร์มได้
      • emit-json: แสดงตัวอย่างที่เหมาะกับการสร้างการตั้งค่าข้ามแพลตฟอร์ม

ความสมบูรณ์แบบทัวริงและการสะท้อน

  • ความสมบูรณ์แบบทัวริง

    • สามารถแสดงโอเปอเรเตอร์ K และ S ของ combinatory logic ด้วย Tree Calculus ได้
    • K = △ △
    • S x = △ (△ x)
    • เนื่องจากฐาน K/S ของ combinatory logic มีความสมบูรณ์ Tree Calculus จึง Turing-complete เช่นกัน
    • ต่างจาก λ-calculus ตรงที่สามารถแสดงฟังก์ชันเวียนเกิดเป็น รูปแบบปกติ ได้ด้วยโครงสร้างจุดตรึงอย่าง orange/brown

  • การสะท้อน

    • triage {l, s, f} = △ (△ l s) f ทำการวิเคราะห์กรณีสำหรับ leaf, stem, fork
    • จำนวนธรรมชาติ n สามารถแสดงได้เป็น △^n △
    • การทดสอบว่าเป็น 0 สร้างได้ด้วย triage {true, K false, K² false}
    • เนื่องจากโปรแกรมก็เป็นค่า โปรแกรมแบบ intensional จึงสามารถทำ introspection และการสะท้อนผ่านการนำไปใช้กับตัวเองได้
    • โปรแกรมตัวอย่าง size คำนวณจำนวนโหนดของอาร์กิวเมนต์ และ size size ประเมินได้เป็น 168
    • เดโมเชิงใช้งานจริง
      • serialize-anything: กล่าวถึงความเป็นไปได้ในการทำ serialization ของโปรแกรม
      • halting-problem: ทำให้การนิยามปัญหาการหยุดง่ายขึ้น
      • fusion: แสดงการวิเคราะห์และปรับให้เหมาะสมของโปรแกรมเป็นฟังก์ชัน
      • gradual-typing: ให้ตัวอย่างการจัดการ static typing และ dynamic typing ผ่านการเรียกฟังก์ชัน

ความเป็นโมดูลาร์และเดโม

  • พจน์ย่อยแสดงเป็น ต้นไม้ย่อย
  • โปรแกรม size ที่ด้านบนของหน้าใช้ triage เพื่อนับโหนดแบบเวียนเกิด
  • เดโมเชิงใช้งานจริง
    • bootstrap-basics: สามารถบูตสแตรปฟังก์ชันพื้นฐานร่วมกันได้ง่าย
    • size-of-meaningful-programs: แสดงให้เห็นว่าโปรแกรมทรงพลังไม่จำเป็นต้องเป็นต้นไม้ขนาดใหญ่เสมอไป

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-12-11
ความคิดเห็นบน Hacker News

  • Tree Calculus เป็นหัวข้อที่ยอดเยี่ยมซึ่งมีนัยสำคัญเกินกว่าเว็บไซต์นี้
    แต่น่าเสียดายที่เว็บไซต์ไม่ได้ระบุชื่อ Prof. Barry Jay ผู้ริเริ่มและผู้เขียนไว้อย่างชัดเจน หากอยากรู้เพิ่มเติม สามารถดูหนังสือของ Jay ได้: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • ในหน้า “Specification” มีการอ้างอิงถึงหนังสือของเขาอยู่
      สามารถทำให้การให้เครดิตชัดเจนขึ้นได้ และเราก็ตั้งใจจะทำเช่นนั้น แต่ไม่มีเจตนาจะฉวยเครดิตเลยแม้แต่น้อย ผมเขียนเบื้องหลังเพิ่มเติมไว้ในคำตอบนี้: https://news.ycombinator.com/item?id=42375914
    • ทันทีที่เห็นสิ่งนี้ ผมนึกถึง Bondi Language / Pattern Calculus ของ Barry Jay ก่อนเลย ซึ่งดูเหมือนจะไม่ได้เดาผิดไปเสียทีเดียว

  • ดูน่าสนใจดี แต่หน้านี้ให้คำแนะนำน้อยเกินไปจนเข้าใจยาก
    อยากให้มีคำอธิบายแบบ “สำหรับผู้เริ่มต้น”

    • เหมือนกับ SKI calculus หรือญาติของมันอย่าง lambda calculus นี่เป็นโมเดลการคำนวณแบบเรียบง่ายที่มีกฎแน่นอนสำหรับประเมินหรือลดรูปนิพจน์อย่างเป็นกลไก: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      สิ่งที่ต่างจาก SKI calculus คือสามารถสะท้อนตรวจดูโครงสร้างของโปรแกรมตัวเองได้ เช่น สามารถตัดสินได้ว่าโปรแกรมสองโปรแกรมเหมือนกันหรือไม่: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      อีกทั้งต่างจาก lambda calculus ตรงที่เมื่อใช้กฎการลดรูปที่กำหนดไว้ โปรแกรมจะลู่เข้าสู่ normal form ที่เสถียร และหลีกเลี่ยงกรณีที่อาจตกไปอยู่ในสายโซ่การลดรูปไม่สิ้นสุดได้: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      ดังนั้นจึงสะท้อนตรวจดูได้โดยไม่ต้องอ้อมไป quote หรือ serialize โปรแกรมให้เป็นโครงสร้างข้อมูลที่เสถียร และมีแง่มุมคล้ายกับ homoiconicity ของ Lisp
    • โครงสร้างของหน้า landing page หลักค่อนข้างแปลก
      มันใช้ชื่อเรื่องคำเดียว วลีที่ออกแนว buzzword นิด ๆ และตัวอย่างโค้ดแบบเคลื่อนไหวเหมือนเว็บไซต์ภาษาโปรแกรมหรือเฟรมเวิร์กยอดนิยม แต่เนื้อหากลับแน่นและยาวในสำนวนวิชาการมากเกินไป อย่างไรก็ตาม แม้ใช้สำนวนวิชาการนั้น ก็ยังไม่มีรายละเอียดมากพอให้เข้าใจว่าเกิดอะไรขึ้นจริง ๆ
      ผมลองไล่อ่านและแยกความหมายของย่อหน้าอยู่นาน แต่ถึงจะยืดยาว ก็พูดแค่ “ผู้เขียนคิดว่าภาษานี้ดีตรงไหน” เหมือน landing page ของภาษาโปรแกรมทั่วไป ไม่ได้อธิบายว่ามันทำงานอย่างไร สุดท้ายคงต้องไปดูสเปก
    • ไวยากรณ์ในสเปก E ::= t | E E มองครั้งแรกอาจทำให้เข้าใจผิดได้ว่านิพจน์ทั้งหมดดูเหมือนแค่ t t t t t t t
      จริง ๆ แล้วต้องรักษาโครงสร้างวงเล็บไว้ จึงจะเป็นรูปอย่าง (t t) (t ((t t) (t t))) และที่ระดับบนสุดกับภายในวงเล็บแต่ละคู่จะมีนิพจน์ย่อยพอดีสองตัวเสมอ กล่าวคืออักขระช่องว่างทำหน้าที่เหมือนตัวดำเนินการทวิภาค
      เนื่องจากนิพจน์นี้มีวงเล็บมาก จึงมองตัวดำเนินการทวิภาคนี้เป็นแบบ จับกลุ่มซ้าย a b c จะตีความเป็น (a b) c และ a b c d จะตีความเป็น ((a b) c) d
      เมื่อมองแบบนี้จะเห็นว่าต้นไม้มาจากไหน เพราะมีสัญลักษณ์ปลายใบเพียงตัวเดียวคือ t หากเอาวงเล็บที่ไม่จำเป็นออก นิพจน์ทั้งหมดจะขึ้นต้นด้วย t เสมอ แล้วตามด้วยนิพจน์หลายตัว ให้วาด t ตัวแรกเป็นโหนด แล้วสำหรับนิพจน์ที่ตามมาแต่ละตัวก็ทำขั้นตอนเดียวกันเพื่อวาดทรีย่อย
      กฎความหมายในหน้าสเปกบอกวิธี “ทำให้เรียบง่าย” สำหรับโหนดที่มีทรีย่อยตั้งแต่สามตัวขึ้นไป หรือก็คือวิธีลดรูปนิพจน์ที่มีนิพจน์ย่อยตั้งแต่สามตัวขึ้นไปต่อท้าย t
    • ถ้าด้านบนสุดของหน้ามี ประโยคนิยาม อย่าง “Tree Calculus คือ [นามวลี] สำหรับ [สรุปจุดประสงค์]” ก็น่าจะช่วยได้
      เป็นรูปแบบเดียวกับที่บทความวิกิพีเดียมักเริ่มว่า “Lambda calculus เป็นระบบเชิงรูปแบบสำหรับ …”, “Matrix calculus เป็นสัญกรณ์พิเศษสำหรับ …”
    • สรุปคือ มันเป็นภาษาโปรแกรมที่ โปรแกรมและค่าล้วนเป็นต้นไม้ไร้ป้ายกำกับ
      ต้นไม้ไร้ป้ายกำกับคือโครงสร้างข้อมูลแบบต้นไม้ที่โหนดไม่มีข้อมูล แต่ลำดับของลูกมีความหมาย Tree Calculus นิยามชุดกฎสำหรับประเมินต้นไม้ไร้ป้ายกำกับให้ได้ต้นไม้ไร้ป้ายกำกับอีกต้น
      เมื่อใช้กฎซ้ำ ๆ อาจเข้าสู่ลูปไม่สิ้นสุด หรือไปถึงต้นไม้ที่ไม่เปลี่ยนแปลงอีกแล้ว กฎถูกออกแบบไม่ให้กระทบต้นไม้ทวิภาค ดังนั้นเมื่อประเมินต้นไม้ทวิภาคจะได้ต้นไม้เดิมกลับมา และถือว่าการคำนวณสิ้นสุดแล้ว
      กฎเหล่านี้เขียนไว้ในหน้า “Specification” ในรูปแบบ small-step semantics ซึ่งพบได้บ่อยในทฤษฎีภาษาโปรแกรม
      ข้ออ้างคือกฎการประเมินมีความ Turing complete จึงแสดงการคำนวณใด ๆ ได้ และการประเมินมีประสิทธิภาพเชิงกำกับแบบเหมาะที่สุด ทำให้โปรแกรมจากภาษาใด ๆ สามารถรันใน Tree Calculus ได้ด้วยโอเวอร์เฮดเกือบคงที่ ฟังครั้งแรกก็ไม่ใช่ข้ออ้างที่ไร้เหตุผล แต่ยังไม่ชัดเจนว่ามันสำคัญจริงแค่ไหน
      การใช้งานน่าจะน่าสนใจสำหรับนักวิจัยทฤษฎีภาษาโปรแกรมบางส่วน และอาจใช้เพื่อทำให้บทพิสูจน์ในทฤษฎีการคำนวณเรียบง่ายขึ้นได้ หากคุณสนใจเรื่องแบบนี้ ผมแนะนำให้เริ่มเรียน lambda calculus ก่อน เพราะเรียบง่ายกว่า เป็นที่รู้จักมากกว่า และมีประโยชน์มากกว่า Tree Calculus

  • ในหน้าเว็บเขียนว่า “Democratizing Functions”, “Democratizing Metatheory” แต่ไม่ว่าจะหมายถึงอะไรก็ตาม รู้สึกชัดเจนว่าใช้คำว่า democratizing กันพร่ำเพรื่อ

    • การใช้แบบนี้พบได้ค่อนข้างบ่อย
      ความหมายที่สองของ Britannica ก็ระบุว่า “ทำให้บางสิ่งพร้อมให้ทุกคนใช้งานได้, ทำให้ทุกคนเข้าใจได้”: https://www.britannica.com/dictionary/democratize
    • เห็นด้วย “What democratize really means” ก็น่าอ่านประกอบ: https://intage.us/articles/words/democratize/
      “ภาษาเกิดจากการหล่อหลอมของวัฒนธรรม และคุณก็เป็นส่วนหนึ่งของวัฒนธรรมนั้น ไม่จำเป็นต้องสละความรับผิดชอบ คุณมีทางเลือก”

  • ผมลองทำภาพขึ้นมาเองเพื่อทำความเข้าใจตรรกะของกฎการย่อรูปใน Tree Calculus แบบใช้ “สัญชาตญาณ”: https://latypoff.com/tree-calculus-visualized/
    อาจช่วยได้สำหรับ คนที่คิดเป็นภาพ

    • ช่วยได้มาก โดยเฉพาะข้อความที่เขียนอย่างละเอียดนั้นดีมาก
      แต่ภาพที่สอง “Stem with a single leaf child” ดูเหมือนจะมีข้อผิดพลาด เส้นที่ลงมาจากสามเหลี่ยมต่อไปยังสี่เหลี่ยม แต่สี่เหลี่ยมนั้นน่าจะควรเป็นวงกลม
    • ดีจริง ๆ ถ้าทำให้อยู่ในรูปแบบที่ทำแอนิเมชันได้ น่าจะเข้ากับหน้า Specification ของเว็บไซต์มาก

  • สงสัยว่าคนที่แนะนำสิ่งนี้เข้าใจจริง ๆ ไหมว่ามันคืออะไร แล้วถึงแนะนำ

    • ในสายตาผม มันดูเหมือน การนำ lambda calculus ไปใช้อีกแบบหนึ่ง และก็น่าเสียดายที่หน้าเว็บอธิบายไม่ได้ว่ามันน่าสนใจตรงไหน
    • แนะนำเพราะคิดว่าน่าจะมีการถกเถียงที่น่าสนใจตามมา
    • แนะนำเพราะหวังว่าจะมีใครสักคนมาอธิบายให้ฟัง

  • ใครช่วยอธิบายได้ไหมว่าทำไมสิ่งนี้ถึงไม่ใช่แค่ Lisp หรือ Forth ที่ไวยากรณ์ต่างกัน?
    ไม่ได้จะวิจารณ์หรือมองแบบผิวเผิน แต่อยากเข้าใจจริง ๆ

    • Lisp มีพื้นฐานจาก lambda calculus แต่ตัว lambda calculus เองไม่มีเครื่องมือสำหรับแก้ไขโปรแกรมที่เขียนอยู่ภายในตัวมันเอง
      เพราะความสามารถนี้มีประโยชน์ ภาษาในตระกูล Lisp จึงมีการเพิ่มสิ่งอย่าง macro เข้ามา และวิธี implement ก็หลากหลาย แม้แต่ eval ที่พบได้ทั่วไปในตระกูล Lisp ก็ไม่ใช่ส่วนหนึ่งของ lambda calculus ใน lambda calculus มีแค่นามธรรม การประยุกต์ใช้ และตัวแปร ไม่มี environment
      ถ้าแนวคิดเรื่อง reflection ถูกนิยามไว้อย่างดี และ Tree Calculus เป็น reflective จริง ๆ มันก็ไม่ใช่ Lisp ที่แค่ไวยากรณ์ต่างกันแน่นอน และยิ่งไม่ใช่ Forth เข้าไปใหญ่
      ผมไม่ใช่ผู้เชี่ยวชาญ จึงควรฟังแบบเผื่อไว้มาก ๆ ในเชิงปฏิบัติอาจดูเหมือน Lisp ที่ช้า แต่ในเชิงทฤษฎีมันต่างจาก lambda calculus และสามารถใช้เป็นฐานที่ง่ายกว่าในการ implement สิ่งที่คล้าย Lisp แบบช้า ๆ ได้
    • ถ้าไม่มีวงเล็บบังคับและไม่ไวต่อ indentation สำหรับรสนิยมของผมก็ถือเป็นข้อดีใหญ่แล้ว
      รสนิยมแบบอื่นก็แน่นอนว่าไม่เป็นไร แต่ก็น่าเสียดายที่ homoiconicity ส่วนใหญ่ถูกขังอยู่ใน dialect ของ Lisp

  • ผมลองแปลง Z combinator ของ SKI ผ่านตัวอย่าง lambda calculus ไปเป็น Tree Calculus แล้วพิมพ์ออกมาเป็นต้นไม้
    ยังไม่ได้ทดสอบ แต่ต้นฉบับเป็นโค้ดที่ยังไม่ optimize ซึ่งแปลงด้วยเครื่องมือ ดูพื้นฐานที่เกี่ยวข้องได้ในเอกสาร fixed-point combinator: 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 ได้สั้นกว่านี้ด้วย

  • ดีใจที่เห็น Johannes ทดลองกับ Tree Calculus และแสดงความเป็นไปได้ที่เคยมีอยู่เพียงโดยนัยในหนังสือของผม GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf ออกมาอย่างชัดเจน
    ในที่สุดก็มี Tree Calculus แบบมีชนิดข้อมูลแล้ว ผมจึงเริ่มเขียนบล็อกที่ GitHub.com/barry-jay-personal

    • ลิงก์ที่ใช้งานได้ไปยังหนังสืออยู่ที่นี่: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      มองหาปุ่มดาวน์โหลดทางด้านขวาก็พอ
    • ผมสนใจเปเปอร์ “Typed Program Analysis Without Encodings” มาก แต่หาออนไลน์ไม่เจอ อยากรู้ว่าควรไปดูที่ไหน

  • ผมนั่งดูสิ่งนี้อยู่พักใหญ่แล้วได้ข้อสรุปบางอย่าง โดยเฉพาะอาจช่วยให้คนที่คุ้นกับ lambda calculus หรือ formal semantics อยู่บ้างตั้งหลักได้
    ผมต้องลงไปดู implementation ใน OCaml เพื่อทำความเข้าใจว่า small-step semantics หมายถึงอะไร เพราะมองไม่ค่อยเห็นโครงสร้างต้นไม้พื้นฐาน ในสูตรย่อรูปสี่รายการของนิยาม ถ้าใส่วงเล็บให้สามพจน์แรก จะเห็นว่าอะไรถูกนำไปประยุกต์กับอะไร ด้านขวาก็ดูเหมือนจะขาดวงเล็บเช่นกัน
    เช่น ควรมองเป็น (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 จะดีกว่า
    อีกอย่าง ในตารางยังขาดกรณีที่ดูเหมือนผู้เขียนถือว่า “แน่นอนอยู่แล้ว” จาก associativity ของไวยากรณ์ ถ้าเพิ่มไว้เป็น t a -> (t a), (t a) b -> (t a b) ก็จะทำให้นำการย่อความหมายไปใช้กับนิพจน์ในไวยากรณ์ E E ได้สะอาดขึ้น
    แก่นสำคัญคือ เหมือนกับที่ใน lambda calculus มัด lambda ไว้เพื่อทำให้ “เลือก” หนึ่งในสองทางได้ Tree Calculus นี้ถูกสร้างให้ทำ สามทางเลือก ตามว่าโหนดที่ให้มาเป็นใบ ลำต้น หรือกิ่ง นี่คือหัวใจของกฎ 3a, 3b, 3c และความสามารถที่เหลือของระบบก็สร้างขึ้นบนการเลือกแบบสามแขนงนี้

    • คำอธิบายนี้ควรอยู่ในหน้าแรก
      ต้องขอบคุณมันที่ทำให้ดูเหมือน calculus ที่น่าสนใจ แต่การจะแปลงกลับ serialize หรือ compile ได้เหมาะกว่า SKI หรือ lambda calculus หรือไม่นั้นเป็นอีกเรื่องหนึ่ง การแปลงกลับยาก, serialization ง่าย, ส่วนการ compile ก็พอทำได้ค่อนข้างง่าย

  • ใน Python สามารถกำหนดให้ Leaf เป็นลิสต์ว่าง, Stem เป็นลิสต์ที่มีสมาชิกตัวเดียว และ Fork เป็นลิสต์ที่มีสมาชิกสองตัว แล้ว implement apply ให้ตรงกับโค้ด OCaml ในสเปกได้
    เมื่อกำหนด false, true, not เป็น tree แล้ว not false -> true และ not true -> false จะทำงานได้

    • ใน Racket หรือ Scheme ก็ใช้ไอเดียเดียวกันได้
      กำหนดให้ Leaf เป็น null, Stem เป็น list, และ Fork เป็น cons จากนั้นตรวจสอบผลลัพธ์เดียวกันได้ด้วย apply t-not t-false และ apply t-not t-true