Phép tính cây

 (treecalcul.us)
1 điểm bởi GN⁺ 2024-12-11 | 1 bình luận | Chia sẻ qua WhatsApp
  • Một hệ thống nhằm cấu thành phép tính với cú pháp tối thiểu, dùng chỉ một toán tử △ và phép áp dụng để đồng thời xử lý tính tối giản, tính đầy đủ Turing, tính phản chiếu và tính mô-đun
  • Cú pháp là E::= △ | E E, và khi △ tác động lên ba giá trị thì phép tính được thực hiện; các giá trị là cây nhị phân tự nhiên gồm các nút lá, thân và nhánh chạc
  • Có thể biểu diễn K và S của logic tổ hợp trong Tree Calculus nên nó có tính đầy đủ Turing; khác với λ-calculus, có thể biểu diễn hàm đệ quy ở dạng chuẩn tắc
  • Vì chương trình cũng được xử lý như giá trị nên có thể introspection và phản chiếu thông qua tự áp dụng; có ví dụ size size được đánh giá thành 168
  • Các hạng con lộ ra thành các cây con, dẫn tới các demo như bootstrap chức năng dùng chung, tuần tự hóa, phân tích/tối ưu hóa chương trình và gõ kiểu tĩnh/động

Cây nhị phân tự nhiên được tạo bằng một toán tử

  • Tree Calculus do Barry Jay phát hiện, và trang web liên kết tới sách và blog của ông cùng các demo do Johannes Bader phát triển
  • Các đặc tính cốt lõi được tóm gọn thành bốn điểm: minimal, Turing-complete, reflective, modular

  • Tính tối giản

    • Tree Calculus chỉ có một toán tử △
    • Cú pháp có dạng E ::= △ | E E
    • Về trực quan, △ là một nút cây, và khi áp dụng E1 vào E2 thì E2 được gắn vào bên phải nút gốc của E1
    • Giá trị là cây nhị phân tự nhiên, các nút được gọi là leaf, stem, fork
    • Demo thực tế
      • portability: có thể tạo trình thông dịch đơn giản và an toàn trên nhiều nền tảng
      • emit-json: cho thấy một ví dụ phù hợp để tạo cấu hình đa nền tảng

Tính đầy đủ Turing và tính phản chiếu

  • Tính đầy đủ Turing

    • Có thể biểu diễn các toán tử K và S của logic tổ hợp bằng Tree Calculus
    • K = △ △
    • S x = △ (△ x)
    • Vì nền tảng K/S của logic tổ hợp là đầy đủ nên Tree Calculus cũng đầy đủ Turing
    • Không giống λ-calculus, có thể biểu diễn các hàm đệ quy ở dạng chuẩn tắc bằng các cấu trúc điểm bất động như orange/brown

  • Tính phản chiếu

    • triage {l, s, f} = △ (△ l s) f thực hiện phân tích theo trường hợp đối với leaf, stem, fork
    • Số tự nhiên n có thể được biểu diễn dưới dạng △^n △
    • Kiểm tra 0 được cấu thành bằng triage {true, K false, K² false}
    • Vì chương trình cũng là giá trị nên các chương trình intensional có thể thực hiện introspection và phản chiếu bằng cách tự áp dụng
    • Chương trình ví dụ size tính số nút của đối số, và size size được đánh giá thành 168
    • Demo thực tế
      • serialize-anything: nói về khả năng tuần tự hóa chương trình
      • halting-problem: mô hình hóa bài toán dừng theo cách đơn giản hơn
      • fusion: biểu diễn phân tích/tối ưu hóa chương trình dưới dạng hàm
      • gradual-typing: cung cấp ví dụ xử lý gõ kiểu tĩnh và động như các lời gọi hàm

Tính mô-đun và demo

  • Các hạng con được biểu diễn thành cây con
  • Chương trình size ở đầu trang sử dụng triage để đếm đệ quy các nút
  • Demo thực tế

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-12-11
Ý kiến trên Hacker News

  • Tree Calculus là một chủ đề thú vị với những hàm ý vượt ra ngoài website này
    Tuy nhiên hơi tiếc là website không ghi rõ GS. Barry Jay, người sáng lập kiêm tác giả. Nếu muốn tìm hiểu thêm thì có thể xem sách của Jay: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • Trang “Specification” có tham chiếu đến sách của ông
      Việc ghi nguồn có thể và sẽ được làm rõ hơn, nhưng hoàn toàn không có ý định nhận vơ công lao. Tôi đã viết thêm bối cảnh trong phản hồi này: https://news.ycombinator.com/item?id=42375914
    • Vừa nhìn thấy cái này tôi đã nghĩ ngay đến Bondi Language / Pattern Calculus của Barry Jay, có vẻ cũng không hoàn toàn lệch hướng

  • Trông có vẻ hay, nhưng trang này hướng dẫn quá ít nên khó hiểu
    Giá mà có phần giải thích kiểu “dành cho người mới bắt đầu” thì tốt

    • Giống như SKI calculus hoặc họ hàng của nó là lambda calculus, đây là một mô hình tính toán đơn giản có các quy tắc chính xác để đánh giá hoặc rút gọn biểu thức một cách máy móc: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      Khác với SKI calculus ở chỗ nó có thể phản tư về cấu trúc chương trình của chính mình, chẳng hạn có thể xác định hai chương trình có giống nhau hay không: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Ngoài ra, không giống lambda calculus, khi áp dụng các quy tắc rút gọn đã cho, chương trình sẽ hội tụ về một dạng chuẩn ổn định, tránh được các trường hợp có thể rơi vào chuỗi rút gọn vô hạn: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Vì vậy nó có thể phản tư mà không cần trích dẫn hoặc tuần tự hóa chương trình để đi vòng qua một cấu trúc dữ liệu ổn định, và có điểm tương tự homoiconicity của Lisp
    • Cấu trúc trang đích chính khá lạ
      Nó dùng tiêu đề một từ, câu chữ hơi kiểu buzzword, và ví dụ mã động như website của một ngôn ngữ lập trình hay framework đang thịnh hành, nhưng phần nội dung lại quá dày đặc và dài theo văn phong học thuật. Thế nhưng chỉ riêng văn phong học thuật đó cũng không cung cấp đủ chi tiết để hiểu chuyện gì đang diễn ra
      Tôi đã cố phân tích các đoạn văn một hồi lâu, nhưng dù dài dòng, nó vẫn chỉ nói “tác giả nghĩ ngôn ngữ này hay ở điểm nào” giống một trang đích ngôn ngữ lập trình thông thường, chứ không giải thích cách nó hoạt động. Cuối cùng có lẽ phải xem phần đặc tả
    • Ngữ pháp E ::= t | E E trong đặc tả thoạt nhìn dễ khiến người ta hiểu nhầm rằng mọi biểu thức chỉ trông như t t t t t t t
      Thực ra phải giữ cấu trúc ngoặc, nên nó có dạng như (t t) (t ((t t) (t t))), và ở cấp cao nhất cũng như bên trong mỗi cặp ngoặc luôn có đúng hai biểu thức con. Nói cách khác, ký tự khoảng trắng hoạt động như một toán tử nhị phân
      Vì biểu thức này có nhiều ngoặc, toán tử nhị phân này được xem là kết hợp trái. a b c được hiểu là (a b) c, còn a b c d được hiểu là ((a b) c) d
      Nhìn theo cách này sẽ thấy cây xuất hiện từ đâu. Vì ký hiệu lá chỉ có một t, nếu bỏ các ngoặc không cần thiết thì mọi biểu thức luôn bắt đầu bằng t, sau đó là nhiều biểu thức đi kèm. Vẽ t đầu tiên làm nút, rồi với mỗi biểu thức theo sau, lặp lại cùng quy trình để vẽ cây con
      Các quy tắc ngữ nghĩa trên trang đặc tả nói về cách “đơn giản hóa” một nút có từ ba cây con trở lên, tức cách rút gọn một biểu thức trong đó sau t có từ ba biểu thức con trở lên
    • Sẽ hữu ích nếu ngay đầu trang có một câu định nghĩa kiểu “Tree Calculus là [cụm danh từ] dành cho [tóm tắt mục đích]”
      Kiểu như các bài Wikipedia thường bắt đầu bằng “Lambda calculus là một hệ hình thức dùng để …”, “Matrix calculus là một ký pháp chuyên biệt dùng để …”
    • Tóm lại, đây là một ngôn ngữ lập trình trong đó chương trình và giá trị đều là cây không nhãn
      Cây không nhãn là cấu trúc dữ liệu dạng cây mà các nút không có dữ liệu, và thứ tự các nút con là có ý nghĩa. Tree Calculus định nghĩa một tập quy tắc để đánh giá cây không nhãn và thu được một cây không nhãn khác
      Nếu áp dụng lặp lại các quy tắc, hoặc sẽ rơi vào vòng lặp vô hạn, hoặc sẽ đạt đến một cây không còn thay đổi nữa. Các quy tắc được thiết kế để không ảnh hưởng đến cây nhị phân, nên nếu đánh giá một cây nhị phân thì kết quả vẫn là cây đó và phép tính ở trạng thái đã kết thúc
      Các quy tắc này được viết trên trang “Specification” dưới dạng ngữ nghĩa bước nhỏ, vốn phổ biến trong lý thuyết ngôn ngữ lập trình
      Điều được tuyên bố là các quy tắc đánh giá này Turing-complete, nên có thể biểu diễn mọi phép tính, và việc đánh giá là tối ưu về tiệm cận, nên chương trình của bất kỳ ngôn ngữ nào cũng có thể chạy trong Tree Calculus với overhead gần như hằng số. Thoạt nhìn đây không phải tuyên bố vô lý, nhưng thực sự quan trọng đến mức nào thì chưa rõ
      Ứng dụng của nó có thể hấp dẫn với một số nhà nghiên cứu lý thuyết ngôn ngữ lập trình, và có thể dùng để đơn giản hóa các chứng minh trong lý thuyết tính toán. Nếu bạn thấy những thứ này thú vị, tôi khuyên nên học lambda calculus trước, vì nó đơn giản hơn Tree Calculus, nổi tiếng hơn và hữu dụng hơn

  • Trên trang chủ có ghi “Democratizing Functions”, “Democratizing Metatheory”, nhưng dù nghĩa là gì thì vẫn có cảm giác từ democratizing đang bị lạm dụng khá nặng

    • Cách dùng này khá phổ biến
      Định nghĩa thứ hai của Britannica cũng là “làm cho mọi người đều có thể sử dụng một thứ gì đó, làm cho mọi người đều có thể hiểu một thứ gì đó”: https://www.britannica.com/dictionary/democratize
    • Đồng ý. “What democratize really means” cũng đáng tham khảo: https://intage.us/articles/words/democratize/
      “Ngôn ngữ được định hình bởi văn hóa, và bạn cũng là một phần của văn hóa đó. Không cần từ bỏ trách nhiệm. Bạn có lựa chọn”

  • Tôi đã tự làm hình minh họa để hiểu “bằng cảm giác” logic của các quy tắc rút gọn trong Tree Calculus: https://latypoff.com/tree-calculus-visualized/
    Có thể hữu ích cho những người suy nghĩ bằng hình ảnh

    • Rất hữu ích. Đặc biệt phần văn bản viết rất cẩn thận
      Tuy nhiên có vẻ có lỗi ở hình thứ hai “Stem with a single leaf child”. Đường đi xuống từ tam giác nối tới một hình vuông, nhưng hình vuông đó có lẽ phải là hình tròn
    • Thật sự rất hay. Nếu làm nó thành dạng có thể tạo hoạt ảnh thì có vẻ sẽ rất hợp với trang Specification của website

  • Tôi tò mò không biết những người đề xuất cái này có thật sự hiểu nó là gì rồi mới đề xuất không

    • Trong mắt tôi, nó trông như một cách triển khai khác của phép tính lambda, và trang web cũng đáng tiếc vì không giải thích được vì sao nó thú vị
    • Tôi đề xuất vì nghĩ rằng sẽ có một cuộc thảo luận thú vị tiếp nối
    • Tôi đề xuất vì hy vọng ai đó sẽ giải thích

  • Có ai giải thích được vì sao đây không chỉ là Lisp hay Forth với cú pháp khác không?
    Tôi không có ý chỉ trích hay xem nhẹ, mà thật sự muốn hiểu

    • Lisp dựa trên phép tính lambda, nhưng bản thân phép tính lambda không có công cụ để sửa đổi chương trình được viết bên trong chính nó
      Vì tính năng này hữu ích nên các ngôn ngữ họ Lisp đã được bổ sung những thứ như macro, và cách triển khai cũng đa dạng. Ngay cả eval thường gặp trong họ Lisp cũng không phải là một phần của phép tính lambda. Phép tính lambda chỉ có trừu tượng hóa, áp dụng và biến, không có môi trường
      Nếu khái niệm phản tỉnh được định nghĩa rõ và Tree Calculus có tính phản tỉnh, thì chắc chắn nó không chỉ là Lisp với cú pháp khác, và càng không phải là Forth
      Tôi không phải chuyên gia nên hãy cân nhắc kỹ. Về thực tiễn nó có thể trông giống một Lisp chậm, nhưng về lý thuyết thì nó khác với phép tính lambda và có thể dùng làm nền tảng để triển khai những thứ giống Lisp chậm theo cách đơn giản hơn
    • Nếu không có ngoặc bắt buộc và không nhạy với thụt lề, thì theo gu của tôi đó đã là một lợi thế lớn rồi
      Tất nhiên các gu khác cũng hoàn toàn ổn, nhưng thật đáng tiếc khi tính đồng hình giữa mã và dữ liệu phần lớn bị nhốt trong các phương ngữ Lisp

  • Tôi đã thử chuyển Z combinator của SKI sang Tree Calculus qua ví dụ phép tính lambda, rồi xuất ra dạng cây
    Chưa kiểm thử, nhưng bản gốc là mã chưa tối ưu được chuyển đổi bằng công cụ. Tham khảo tài liệu về fixed-point combinator để biết nền tảng liên quan: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Z combinator có thể viết đơn giản hơn nhiều dưới dạng Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)), và cũng có thể biểu diễn ngắn hơn bằng SKI

  • Thật vui khi thấy Johannes thử nghiệm Tree Calculus và thể hiện rõ ràng những khả năng vốn chỉ được ngụ ý trong cuốn sách của tôi tại GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf
    Cuối cùng đã có Tree Calculus có kiểu, nên tôi đã bắt đầu viết blog tại GitHub.com/barry-jay-personal

    • Liên kết hoạt động tới cuốn sách là ở đây: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Chỉ cần tìm nút tải xuống ở bên phải
    • Tôi rất quan tâm tới bài báo “Typed Program Analysis Without Encodings” nhưng không tìm thấy trên mạng. Không biết nên xem ở đâu

  • Sau khi nhìn kỹ cái này một lúc, tôi nhận ra vài điều. Đặc biệt có thể giúp những người đã khá quen với phép tính lambda hoặc ngữ nghĩa hình thức có chỗ bám ban đầu
    Tôi đã phải đi xuống tới triển khai OCaml để hiểu ngữ nghĩa bước nhỏ nghĩa là gì, vì cấu trúc cây cơ bản không hiện rõ. Trong bốn công thức rút gọn của phần định nghĩa, nếu thêm ngoặc vào ba hạng đầu thì sẽ thấy cái gì được áp dụng vào cái gì. Vế phải cũng có vẻ thiếu ngoặc
    Ví dụ nên nhìn theo kiểu (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 thì tốt hơn
    Ngoài ra trong bảng còn thiếu những trường hợp có lẽ được xem là “hiển nhiên” từ tính kết hợp của cú pháp; nếu thêm như t a -> (t a), (t a) b -> (t a b) thì có thể áp dụng rút gọn ngữ nghĩa cho các biểu thức trong ngữ pháp E E gọn gàng hơn
    Điểm cốt lõi là, giống như trong phép tính lambda, lambda được dùng để gói lại và khiến một trong hai lựa chọn được “chọn”, Tree Calculus này được thiết kế để thực hiện ba lựa chọn tùy theo node đã cho là lá, thân hay nhánh. Đây là trọng tâm của các quy tắc 3a, 3b, 3c, và phần chức năng còn lại của hệ thống được xây dựng trên lựa chọn ba nhánh này

    • Lẽ ra phần giải thích này nên nằm ngay ở trang đầu
      Nhờ vậy nó trông như một phép tính thú vị, nhưng việc nó có phù hợp hơn SKI hay phép tính lambda cho giải chuyển đổi, tuần tự hóa và biên dịch hay không lại là chuyện khác. Giải chuyển đổi thì khó, tuần tự hóa thì dễ, còn biên dịch thì tương đối dễ

  • Trong Python, có thể biểu diễn Leaf bằng danh sách rỗng, Stem bằng danh sách một phần tử, Fork bằng danh sách hai phần tử, rồi triển khai apply theo mã OCaml trong đặc tả
    Khi định nghĩa false, true, not dưới dạng cây thì not false -> true, not true -> false hoạt động

    • Cũng có thể dùng cùng ý tưởng trong Racket hoặc Scheme
      Leaf là null, Stem là list, Fork là cons, và có thể kiểm tra cùng kết quả với apply t-not t-false và apply t-not t-true