Hàm đệ quy nguyên thủy cho lập trình viên thực hành

 (matklad.github.io)
2 điểm bởi GN⁺ 2024-08-05 | 1 bình luận | Chia sẻ qua WhatsApp
  • Những thảo luận kiểu “không Turing-complete thì an toàn” lệch khỏi ý nghĩa toán học; tính không Turing-complete hầu như độc lập với các thuộc tính thực dụng như tính dừng, tính quyết định và sandboxing
  • Các phép tính của Turing Machine có thời gian chạy bị giới hạn bởi một hàm đệ quy nguyên thủy theo đầu vào cũng có thể được viết lại thành hàm đệ quy nguyên thủy
  • Hàm đệ quy nguyên thủy luôn dừng, nhưng vẫn có thể tạo ra các hàm tăng rất nhanh như 2^(2^N), nên đảm bảo dừng không đồng nghĩa với thời gian chạy thực tế
  • Trong thực tế, chương trình không dừng và chương trình kết thúc sau hàng tỷ năm gây ra vấn đề gần như giống nhau; ngay cả ngôn ngữ Turing-complete cũng có thể bị buộc dừng bằng bộ đếm bước
  • Chất lượng của ngôn ngữ cấu hình phụ thuộc nhiều hơn vào tính quyết định, ngữ nghĩa rõ ràng, tính thuần, bảo mật/sandboxing, kiểm soát thời gian chạy và sự đơn giản, hơn là việc có Turing-complete hay không

Hiểu lầm cốt lõi trong thảo luận về Turing-completeness

  • Trên Internet, các lập trình viên thường nói “không Turing-complete” trong một miền cụ thể như một ưu điểm hoặc yêu cầu
  • Tuy nhiên Turing completeness là một thuật ngữ cụ thể đến từ toán học; nếu dùng nó để thay thế cho nhiều thuộc tính mà người làm thực tế mong muốn, ý nghĩa sẽ trở nên mơ hồ
  • Những thuộc tính thực sự cần là đảm bảo dừng, chạy nhanh, hành vi quyết định, sandboxing, ngôn ngữ cấu hình đơn giản, v.v.; chúng phần lớn trực giao với Turing completeness
  • Để hiểu khác biệt này, cần một kết quả lý thuyết đơn giản về hàm đệ quy nguyên thủy (Primitive Recursive Functions, PRF)

Turing Machine đủ nhanh có thể chuyển thành PRF

  • Ngay cả một chương trình viết bằng ngôn ngữ Turing-complete, nếu biết thời gian chạy nhanh hơn O(2^(2^N)), thì cùng thuật toán đó cũng có thể được triển khai trong một ngôn ngữ không Turing-complete
  • Phần lớn bài toán thực dụng nằm trong phạm vi kết thúc nhanh hơn 2^(2^N)
  • Vì vậy, ngôn ngữ không Turing-complete không hạn chế năng lực tính toán thực tế một cách có ý nghĩa, và cũng không tự động trao cho ta một năng lực đặc biệt để kiểm soát tính toán
  • Từ góc nhìn thực tế, hai chương trình sau về cơ bản tạo ra cùng một vấn đề
    • Chương trình không kết thúc
    • Chương trình chỉ kết thúc sau số bước kiểu một tỷ nhân một tỷ
  • Ngay cả ngôn ngữ Turing-complete, nếu ở tầng triển khai đếm số bước và dừng bằng lỗi sau một ngưỡng nhất định, thì có thể đơn giản chặn vấn đề không dừng

FSM: luôn dừng nhưng khả năng biểu đạt bị giới hạn

  • Finite State Machine(FSM) là bộ nhận dạng nhận chuỗi làm đầu vào và trả về “yes” hoặc “no”
  • FSM gồm một tập trạng thái hữu hạn, trạng thái bắt đầu, tập trạng thái yes và hàm chuyển trạng thái
  • Sau khi áp dụng lặp lại hàm chuyển trạng thái cho từng ký hiệu của đầu vào, kết quả được xác định dựa trên việc trạng thái cuối cùng có thuộc trạng thái yes hay không
  • Khả năng biểu đạt của FSM tương đương với biểu thức chính quy (regular expression)
  • FSM chạy tuyến tính theo độ dài đầu vào và luôn dừng, nhưng không thể nhận dạng mọi tập chuỗi
    • Ví dụ, tập chuỗi như 1, 010, 00100, 0001000, nơi có cùng số lượng 0 ở hai bên 1, không thể được FSM nhận dạng
    • Với đầu vào đủ dài, trạng thái sẽ lặp lại và tạo thành chu kỳ; nếu sao chép đoạn chu kỳ đó, FSM vẫn đi tới trạng thái yes, nhưng điều kiện của chuỗi bị phá vỡ

Turing Machine: mô hình thêm băng có thể thay đổi vào FSM

  • Turing Machine(TM) có trạng thái và hàm chuyển trạng thái như FSM, nhưng hoạt động trên một băng có thể thay đổi thay vì đầu vào bất biến
  • Ở mỗi bước, TM đọc ký hiệu hiện tại trên băng và thực hiện các thao tác sau
    • Thay ký hiệu hiện tại bằng ký hiệu mới
    • Thay đổi trạng thái nội bộ
    • Di chuyển đầu đọc sang trái hoặc phải một ô
  • Khi TM đạt trạng thái halt thì dừng, và nội dung băng ở thời điểm đó trở thành kết quả
  • Trong khi FSM là bộ nhận dạng nhị phân, TM là thiết bị tính toán hàm
  • TM không nhất thiết phải dừng; nó có thể đi qua lại trên băng và đổi trạng thái mà vẫn không bao giờ đạt trạng thái cuối

Universal Turing Machine và năng lực tính toán

  • Chương trình của TM không phải là mã được cung cấp dưới dạng đầu vào người dùng, mà được hard-code trong chính hàm chuyển trạng thái
  • Tuy nhiên, có thể mã hóa một TM bất kỳ cùng đầu vào thành tệp văn bản, rồi tạo một TM “interpreter” để diễn giải nó
  • TM như vậy là Universal Turing Machine, mô phỏng một TM khác được đưa vào làm đầu vào
  • Có thể viết interpreter TM bằng Python, và ngược lại cũng có thể triển khai interpreter Python bằng TM, nên có thể xem hai bên tương đương về năng lực tính toán
  • FSM yếu hơn TM
    • TM có thể mô phỏng FSM
    • TM có thể dùng thao tác trên băng để quyết định chuỗi có cùng số lượng 0 ở hai bên và 1 ở giữa hay không
    • FSM không thể giải bài toán đó

Băng có thể được xem như hai stack

  • Băng của TM là một trừu tượng khó triển khai trực tiếp trong ngôn ngữ lập trình thông thường
  • Nội dung băng và vị trí đầu đọc có thể được biểu diễn bằng hai stack
    • Nội dung bên trái đầu đọc là stack trái
    • Nội dung bên phải đầu đọc được đảo thứ tự thành stack phải
  • Thao tác di chuyển đầu đọc sang trái hoặc phải trở thành thao tác pop từ một stack và push sang stack kia
  • Vì vậy, TM có năng lực tính toán tương đương “FSM với hai stack”
  • Nếu ký hiệu trong stack chỉ là 0 và 1, bản thân stack cũng có thể được biểu diễn bằng một số tự nhiên
    • xem top: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Giới hạn của Turing Machine: Halting Problem và các kết quả kiểu Rice

  • Vì mọi TM đều có thể được mã hóa thành văn bản, ta có thể liệt kê các TM khả dĩ thành một danh sách vô hạn
  • Dùng lập luận đường chéo, có thể chứng minh tồn tại hàm không thể được TM tính toán
  • Ví dụ cụ thể hơn là Halting Problem
    • Đây là bài toán quyết định, khi được cho mã nguồn và đầu vào của một TM, liệu TM đó có dừng vào lúc nào đó hay không
  • Nếu giả sử halts(program, input) luôn kết thúc đúng, sẽ phát sinh mâu thuẫn trong chương trình weird nhận chính mã nguồn của nó làm đầu vào
    • Nếu phán đoán là sẽ dừng, nó đi vào vòng lặp vô hạn và không dừng
    • Nếu phán đoán là không dừng, nó kết thúc ngay
  • Vì vậy halts phải sai trong một số trường hợp, hoặc không kết thúc trong một số trường hợp
  • Tổng quát hơn, với một TM bất kỳ, không thể quyết định bằng thuật toán các thuộc tính không tầm thường bảo toàn hành vi
    • Thuộc tính cú pháp có thể kiểm tra được, nhưng các thuộc tính hành vi vẫn giữ sau refactoring nhìn chung không thể quyết định được

Hàm đệ quy nguyên thủy: thiết bị tính toán luôn dừng

  • Hàm đệ quy nguyên thủy(PRF) được định nghĩa là hàm nhận một tuple số tự nhiên và trả về một số tự nhiên
  • Các hàm cơ bản là zero và succ
    • zero = 0
    • succ(x) = x + 1
  • Có thể tạo hằng số thông qua hợp thành hàm
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • Đệ quy tổng quát không được phép, nhưng được phép vòng lặp giới hạn LOOP(init, f, n) với số lần lặp cố định trước
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • Ràng buộc cốt lõi là số lần lặp n được cố định trước khi vòng lặp bắt đầu, và thân vòng lặp không thể thay đổi bộ đếm vòng lặp

Tạo các cấu trúc lập trình cơ bản bằng PRF

  • Phép cộng có thể được định nghĩa là add(x, y) = LOOP(x, succ, y)
  • Phép nhân có thể được định nghĩa là mul(x, y) = LOOP(0, add x, y)
  • Lũy thừa có thể được định nghĩa là pow(x, y) = LOOP(1, mul x, y)
  • Từ đó có thể tạo các hàm tăng rất nhanh
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • Nếu thêm pred vào các hàm cơ bản, có thể tạo phép trừ bão hòa và các phép toán Boolean
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) cũng có thể được biểu diễn bằng biểu thức số học
  • Các phép so sánh, phần dư và phép chia cũng có thể được triển khai bằng lặp có cận trên và biểu thức điều kiện

Cấu trúc dữ liệu của PRF và mô phỏng TM

  • PRF có thể nhận nhiều đối số, nhưng kết quả chỉ là một số tự nhiên, nên cần mã hóa cấu trúc dữ liệu thành số tự nhiên
  • Cặp (a, b) có thể được biểu diễn bằng 2^a * 3^b
  • Để lấy các thành phần, chỉ cần tìm số mũ lớn nhất của một số nguyên tố cụ thể
    • fst(p) là số mũ lớn nhất của lũy thừa 2 chia hết p
    • snd(p) là số mũ lớn nhất của lũy thừa 3 chia hết p
  • Theo cách tương tự, ba giá trị (S, stack1, stack2) cũng có thể được đóng gói thành một số tự nhiên
  • Cấu hình TM có thể được biểu diễn bằng ba yếu tố sau
    • Trạng thái hiện tại S
    • Stack bên trái của băng
    • Stack bên phải của băng
  • Thao tác stack có thể được triển khai bằng phần dư, phép nhân và phép chia, nên một bước đơn lẻ của TM có thể được mã hóa bằng PRF
  • Dùng LOOP(initial_config, single_step, n) có thể mô phỏng TM trong đúng n bước
  • Vấn đề là không biết n đủ lớn là bao nhiêu, nhưng nếu thời gian chạy bị giới hạn bởi một PRF nào đó, có thể cho lặp đúng bấy nhiêu
  • Sau cùng, tính toán TM có thời gian chạy bị giới hạn bởi hàm đệ quy nguyên thủy có thể được thay bằng PRF

Giới hạn của PRF: dù luôn dừng, nó không mạnh bằng TM

  • PRF luôn dừng, nhưng không biểu diễn được mọi hàm có dừng
  • Có những hàm TM tính được nhưng PRF không tính được
  • Để chứng minh điều này, đặt cận trên tốc độ tăng trưởng dựa trên độ sâu của cây cú pháp PRF
  • PRF có độ sâu không quá d có thể được đặt cận sao cho không tăng nhanh hơn một hàm một ngôi cụ thể A_d
  • A(d, x) được định nghĩa như sau
    • A(1, x) = x + 1
    • A(d + 1, 0) = A(d, A(d, 0))
    • A(d + 1, x) = A(d, A(d + 1, x - 1))
  • Định nghĩa này sẽ kết thúc nếu tính trên TM, vì mỗi lần gọi đệ quy thì (d, x) nhỏ hơn theo thứ tự từ điển
  • a(x) = A(x, x) tăng nhanh hơn mọi PRF, và TM có thể tính được nhưng PRF thì không

Trở lại thực tế: chỉ không Turing-complete là chưa đủ

  • Turing Machine có thể không dừng
  • Các thiết bị luôn dừng như FSM và PRF cũng không đảm bảo kết thúc nhanh
  • PRF có thể tính các hàm lớn như 2^(2^N), nên chỉ đảm bảo dừng không đảm bảo thời gian chạy thực dụng
  • Nhiều thuật toán trong thực tế có thời gian chạy bị giới hạn bởi PRF, nên cũng có thể biểu diễn bằng thiết bị không Turing-complete
  • Cách tổng quát để biến tính toán Turing-complete thành giống PRF là thêm bộ đếm vòng lặp, và buộc dừng nếu bộ đếm trở nên quá lớn

Những thuộc tính thực sự cần cho ngôn ngữ cấu hình

  • Ngôn ngữ cấu hình thường đặt “không Turing-complete” làm mục tiêu thiết kế, nhưng thứ thực sự cần là nhiều thuộc tính mạnh hơn

  • Tính quyết định

    • Ngôn ngữ cấu hình phải có tính quyết định
    • Hành vi trả ra giá trị khác nhau mỗi lần chạy như id([]) của Python có thể được chấp nhận trong lập trình thông thường, nhưng không phù hợp với cấu hình
    • Cấu hình thường được dùng làm khóa cho incremental build hoặc hệ thống cache, nên nếu có tính không quyết định, hành vi cache sẽ dao động

  • Ngữ nghĩa rõ ràng

    • Hành vi của ngôn ngữ phải được cố định rõ ràng theo một chuẩn có thể tham chiếu
    • Dù có thể tắt ASLR và dùng một allocator cụ thể để làm cho id([]) của Python trở nên quyết định, kết quả đó không được đảm bảo là dự đoán được hoặc giống nhau giữa các implementation
    • Muốn đảm bảo cùng hành vi ở implementation khác hoặc khi đổi phiên bản Python, ngữ nghĩa phải rõ ràng

  • Tính thuần

    • Nếu cấu hình có thể đọc biến môi trường hoặc tệp trên đĩa, ý nghĩa của cấu hình sẽ phụ thuộc vào môi trường đánh giá
    • Để caching hoạt động đúng, ngôn ngữ cấu hình cần có tính thuần

  • Bảo mật và sandboxing

    • Tính thuần và bảo mật đều có thể đạt được bằng cách không phơi bày IO thông thường
    • Mục đích của hai thuộc tính này khác nhau
    • Tính thuần nhằm ngăn kết quả trở nên không quyết định
    • Bảo mật nhằm tránh phơi bày các tài nguyên như access token cho kẻ tấn công

  • Kiểm soát thời gian chạy

    • Ngay cả khi kiểm soát IO, cấu hình độc hại vẫn có thể thực hiện tấn công từ chối dịch vụ bằng cách đốt CPU
    • Có thể dùng hai cách để đảm bảo thời gian chạy
    • Giới hạn để xử lý có cấu trúc tuyến tính rõ ràng, tỷ lệ trực tiếp với kích thước đầu vào
    • Dùng thực thi có đo đếm (metered execution), giảm bộ đếm ở mỗi bước nguyên tử và dừng khi bộ đếm về 0

  • Sự đơn giản

    • Ngôn ngữ cấu hình nên dẫn dắt người dùng viết chương trình đơn giản
    • Cấm đệ quy và vòng lặp vô hạn có thể đóng vai trò như gờ giảm tốc để khuyến khích sự đơn giản
    • Tuy nhiên, như ví dụ PRF cho thấy, các lệnh cấm như vậy không hoàn toàn ngăn được việc viết chương trình đệ quy tùy ý; chúng chỉ khiến cần dùng mã vòng vèo hơn
    • Ví dụ liên quan có thể xem some roundabout code

Tổng kết cuối cùng

  • Thuật toán Turing Machine có thời gian chạy theo đầu vào bị giới hạn bởi một hàm đệ quy nguyên thủy nào đó cũng có thể được triển khai bằng hàm đệ quy nguyên thủy
  • Tính không Turing-complete có thể đem lại một thuộc tính là đảm bảo dừng, nhưng không tự động đảm bảo cận trên thời gian chạy hay chất lượng ngôn ngữ cấu hình cần trong thực tế
  • Trong thiết kế ngôn ngữ cấu hình, vấn đề quan trọng hơn bản thân Turing completeness là tính quyết định, ngữ nghĩa rõ ràng, tính thuần, sandboxing, đo đếm thời gian chạy và sự đơn giản

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-08-05
Các ý kiến trên Hacker News

  • Tự quảng bá: https://www.nayuki.io/page/primitive-recursive-functions

    • Hay hơn bài gốc nhiều, nhưng dạo này có vẻ ai cũng thích kiểu giải thích dễ hiểu theo phong cách ELI5 hơn

  • Ở phần kết của bài có vài tiêu chí khá hay liên quan đến ngôn ngữ cấu hình, nên tôi tò mò liệu trong các ngôn ngữ hiện nay có ngôn ngữ nào thỏa mãn tất cả hoặc phần lớn các tiêu chí đó không

    • Có Dhall [1] và Cue [2] là ví dụ đáp ứng các tiêu chí này, nhưng theo một nghĩa nào đó thì chúng không phải là ví dụ thú vị
      Dhall chủ ý là một ngôn ngữ total functional nên đi theo hướng “không Turing-complete”, còn Cue không có hàm nên cũng chẳng có gì để đệ quy
      Tôi cho rằng RCL [3] đáp ứng các tiêu chí. Nó quyết định được, thuần, cung cấp thực thi có đo lường, và sandbox hóa truy cập hệ thống tệp. Nếu chính sách sandbox cho phép thì có thể đọc tệp, nhưng những tệp đó được xem là một phần của mã nguồn và hoạt động giống như import
      Trong RCL, vì những lý do tác giả đã nêu, tôi không muốn đi theo hướng “không Turing-complete”. Việc chương trình cuối cùng sẽ kết thúc không phải là một thuộc tính hữu ích lắm trong thực tế; ngược lại, ngay cả trong các ngôn ngữ total functional như Agda, người ta vẫn có thể viết các chương trình rất phức tạp, nên tính không Turing-complete không bảo đảm chương trình/cấu hình sẽ đơn giản
      Trong RCL, mọi vòng lặp đều có giới hạn, nhưng vì có hàm nên cũng có thể đệ quy. Không có tail call, nên ban đầu tôi đặt giới hạn độ sâu đệ quy để tránh tràn native stack, nhưng fuzzer đã tìm ra một hàm vừa chạy với không gian stack hằng số vừa không dừng, và đến giờ tôi vẫn chưa hiểu hoàn toàn: let f = g => g(g(h => k => g(g(h)))); f(f)
      Rốt cuộc, việc có thể biểu diễn những hàm bệnh hoạn như vậy không phải là vấn đề trong thực tế. Chỉ cần đặt giới hạn số bước thực thi, tức “giới hạn gas” hay “thực thi có đo lường” như tác giả nói. Việc các cấu trúc lặp dựng sẵn có giới hạn và đệ quy bất tiện là một cơ chế dẫn dắt tốt để giữ mã đơn giản, nhưng cuối cùng công cụ giá trị nhất vẫn là review code và phán đoán tốt
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • Dù là mệnh lệnh và cũng không “thuần”, ngay cả C cũng được thiết kế theo hướng cho phép biết cận trên của số lần lặp trước khi đi vào mọi vòng lặp, nên nó là nguyên thủy đệ quy
      Nghiên cứu của Dennis Ritchie tại MIT tập trung vào chủ đề mà ông gọi là lập trình vòng lặp
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      Lập trình có cấu trúc, thứ gần như mọi lập trình viên hiện đại mặc định tuân theo, thực chất là một mô hình đẩy ta về phía các hàm nguyên thủy đệ quy. Có lẽ vì lập trình có cấu trúc đã được chấp nhận gần như phổ quát so với hai kiểu khác như pop và functional, nên mọi người dễ hiểu nhầm bài “goto is harmful” của Dijkstra
      Hàm nguyên thủy đệ quy không bao gồm toàn bộ các hàm tính được, nhưng nó bao gồm gần như mọi hàm trực quan có bảo đảm kết thúc. Tất nhiên vẫn có trường hợp thực sự cần vòng lặp mà khi bước vào chưa biết số lần lặp, nhưng nếu chỉ dùng khi thật sự cần thì đó là khẩu súng có thể tránh tự bắn vào chân
      Ngay cả COBOL cũng đã được hiện đại hóa bằng cách chuyển goto không giới hạn sang lệnh ALTER. Tôi không nghĩ ra ngôn ngữ hiện đại và hữu ích nào lại không cho phép các hàm PR
      Trong C, nếu tránh while và chủ động tránh fall through, gần như lúc nào cũng có thể viết mã hàm total chắc chắn kết thúc
      Cũng có những trường hợp bệnh hoạn như suy luận kiểu của ML. Chi phí thực tế rẻ hơn nhiều so với lớp độ phức tạp, nên dù ngôn ngữ khó hạn chế kiểu sử dụng này khi không phải là total function, nó vẫn đáng để chấp nhận
      Nhìn thực dụng thì hầu hết mọi ngôn ngữ đều cung cấp các mặc định hỗ trợ phần lớn những tiêu chí này, nhưng các ràng buộc để cưỡng chế chúng sẽ hạn chế nghiêm trọng tính hữu dụng của ngôn ngữ. Tôi nghĩ ngay cả SOLID và framework Clean vốn hay bị chê cũng đẩy theo mô hình này
      Lập trình có cấu trúc đã trở nên quá phổ biến nên ta dễ quên điểm này, thậm chí không dạy được nữa. Với tư cách một ông già râu ria, tôi còn nhớ mình từng được học về sự nguy hiểm của WHILE và những thứ tương tự
    • Có lẽ nên chọn Dhall rồi xem nó thất bại ở tiêu chí nào. Trông nó là gần nhất

  • Câu nói chạy nhanh hơn O(2^(2^N)) có lẽ chỉ là cách diễn đạt đơn giản hóa, nhưng phần “số rất lớn” làm giảm độ tin cậy một chút
    Chính xác hơn có lẽ nên nói là “hàm tăng rất nhanh”. Hoặc có vẻ ý là chương trình kết thúc trong ít hơn O(2^(2^N)) bước

  • Nếu chỉ nhìn vào phần đầu rằng ngôn ngữ bị giới hạn tốt hơn cho một số ứng dụng, tôi nghĩ ưu điểm là có thể tính tĩnh cận trên của số bước cần thiết
    Khi đó, với bất kỳ đầu vào nào, các phép tính vi phạm giới hạn đều có thể bị từ chối và trả về lỗi có ý nghĩa
    Ngược lại, cách đặt giới hạn runtime cho một ngôn ngữ Turing-complete có thể đặt giới hạn quá thấp đối với một số đầu vào mà ta quan tâm. Chỉ khi chạy đến lúc chạm giới hạn mới biết được. Thỉnh thoảng tôi thấy chuyện này trong đệ quy template của C++
    Cũng có thể tôi đang hiểu sai hoàn toàn, nên mong ai biết rõ hơn giải thích

    • Một đồng nghiệp cũ từng đặt một con số gần gấp 3 lần, rồi vài năm sau tải công việc thực tế chạm đúng giới hạn đó; từ đó tôi dùng giới hạn gấp 10 lần lượng tính toán hợp lý
      Dù workflow tệ phải mất thêm vài lần thời gian mới thất bại thì vẫn chỉ ở mức mili giây, nên tôi nghĩ không gây thiệt hại lớn
      Thường ta gặp vấn đề này khi ai đó xử lý miền bài toán như một đồ thị có hướng không chu trình, nhưng lại không thể cưỡng chế tính “không chu trình”. Mô hình hóa bài toán thành đồ thị có hướng không chu trình giống như Dark Galadriel đang cân nhắc có nhận chiếc nhẫn từ Frodo hay không. “Tất cả sẽ yêu mến ta và tuyệt vọng.” Những người tạo ra kiểu này luôn tự hào về nó hơn rất nhiều so với mức đáng tự hào
      Cuối cùng, những khách hàng bị kéo vào các giải pháp đắt đỏ và phức tạp sẽ cạn tiền, và vấn đề của họ cũng bắt đầu trông nhỏ hơn nhiều. Khi đó, theo đúng nghĩa đen, chỉ còn lại một ứng dụng không thể hạ chi phí mỗi tác vụ đủ thấp để duy trì việc kinh doanh của khách hàng
    • Việc dự đoán chính xác mức dùng nhiên liệu của tính toán blockchain có thể thú vị với người khác, nhưng không thú vị với tôi
      Tôi hứng thú hơn với việc dùng nó như một chiếc búa khác trong hộp công cụ để bắt các lỗi đã lọt qua những chiếc búa trước đó như kiểm tra kiểu tĩnh, không có null, không có thay đổi
      Việc biết chắc nó kết thúc trong thời gian hữu hạn không chứng minh được tính đúng đắn, nhưng nếu tôi tuyên bố mã kết thúc trong thời gian hữu hạn mà compiler không đồng ý, thì tôi sẽ tin rằng mã đó sai
    • Cận trên được xác định tĩnh có thể đánh giá quá cao đáng kể độ phức tạp thời gian chạy thực tế trong trường hợp phổ biến. Lý do là nói chung không thể dự đoán các điều kiện gây kết thúc sớm trong đệ quy sẽ được đánh giá như thế nào
      Để kết thúc sớm ảnh hưởng đến thời gian chạy, phải giả định có lazy evaluation hoặc điều kiện short-circuit, nhưng ngôn ngữ thực dụng thì thường sẽ có những thứ đó
    • Nếu cận trên đó cực kỳ lỏng thì sao? Ví dụ quicksort xác định thường là n log n, nhưng có cận trên bậc hai theo kích thước đầu vào
      Vậy có từ chối phép tính quicksort không? Cực đoan hơn, thuật toán Hindley–Milner có cận trên thời gian lũy thừa, nhưng trên thực tế nhiều khi chạy trong thời gian tuyến tính
    • Tôi không biết liệu nó có được “tính tĩnh” hay không, nhưng tôi cho rằng lợi ích duy nhất của việc hạn chế mạnh năng lực ngôn ngữ là có thể đặt giới hạn tính toán theo cách không phụ thuộc vào dữ liệu
      Tuy nhiên, khó mà nghĩ ra tình huống nào mà đó thật sự là yêu cầu mạnh. Có bao nhiêu hệ thống không thể trả lỗi “truy vấn chạy quá lâu”?

  • Tôi từng muốn dùng một ngôn ngữ lập trình web backend dựa trên nguyên tắc không kết thúc/có biên
    Ý tưởng là compiler chứng minh rằng mọi hàm, với trạng thái và đối số đã cho, đều chạy trong biên, và có thể chỉ ra X là cận dưới còn Y là cận trên. Thông tin này được truyền tiếp đến tận entry point
    Tôi đồng ý với tác giả rằng cần ngữ nghĩa mạnh hơn, và vì vậy tôi đã nghĩ đến ngôn ngữ này. Có nhiều trường hợp ta muốn có bảo đảm về thời gian chạy của chương trình
    Cốt lõi có lẽ sẽ dựa trên hàm đệ quy nguyên thủy, nhưng trên thực tế vẫn có thể Turing-complete. Giống như Rust từ chối borrow sai nhưng vẫn cung cấp unsafe cho con trỏ nguyên thủy, ngôn ngữ này cũng sẽ tính cận trên dựa trên các primitive lặp đơn giản, hoặc cho phép dùng toán tử unsafe và cung cấp công thức thay thế cho biên

  • Tôi không hiểu rõ phần than phiền/động cơ ngắn trong bài
    Đó là đoạn: “Thông thường, trong một miền cụ thể, việc không Turing-complete được ca ngợi là ưu điểm hoặc yêu cầu. Tôi cho rằng phần lớn các thảo luận như vậy đang hiểu sai — không Turing-complete không có nghĩa như mọi người kỳ vọng”
    Vì sao các thảo luận đó lại sai? Phần lớn công cụ phân tích hình thức, chẳng hạn Coq, Isabelle, Agda, thường yêu cầu chứng minh rằng hàm sẽ kết thúc. Điều này tương đương với chứng minh hàm đó là hàm toàn phần, và vì thế chẳng phải có nghĩa là nó đệ quy nguyên thủy sao?

    • Tôi chưa đọc hết, nhưng có vẻ bài này xuất phát từ việc một số ngôn ngữ cấu hình quảng bá “không Turing-complete” như một tính năng. Trong khi tính năng họ thực sự muốn quảng bá có lẽ là thời gian chạy được giới hạn hợp lý
      Điều này cũng xuất hiện trong thảo luận gần đây về CEL:
      https://news.ycombinator.com/item?id=40954652
    • Nếu đang nói về chứng minh hình thức, thì trong trường hợp tổng quát, việc chứng minh một hàm là hàm toàn phần là một bài toán tìm kiếm NP-complete, chứ không phải phản ví dụ mang tính khoa học dùng trong lập trình hiện đại
      Nếu tôi nhớ đúng, nó tương đương với NP có oracle co-NP, hoặc tầng thứ hai của hệ phân cấp đa thức. Dù làm được với các bài toán nhỏ, nó vẫn đắt
      Các công cụ này hoạt động tốt nhất khi chương trình được cấu trúc sao cho trở thành hàm toàn phần. Trong đó, cách phổ biến nhất là trong lập trình có cấu trúc chỉ dùng FOR, hoặc chỉ dùng WHILE/đệ quy có giới hạn số lần lặp
      Dù chỉ liên quan đến SAT, các dạng dễ xử lý được đề cập trong định lý lưỡng phân của Schaefer là lăng kính dễ tiếp cận nhất mà tôi có thể nghĩ đến
    • Như bài viết cho thấy, có những hàm kết thúc nhưng không đệ quy nguyên thủy, nên chứng minh hàm toàn phần không có nghĩa là đệ quy nguyên thủy
      Agda, và có lẽ cả các công cụ khác, có thể chứng minh tính kết thúc cho một số hàm đệ quy phi nguyên thủy có kết thúc. Tất nhiên không thể chứng minh tất cả
      Hiểu lầm mà bài viết phàn nàn có vẻ đại khái là: “Turing-completeness nghĩa là có thể tính toán, còn không Turing-complete nghĩa là không thể tính toán và có các thuộc tính tốt cho ngôn ngữ cấu hình.”
      Ý chính của bài là ngay cả khi không Turing-complete, vẫn có thể làm rất nhiều việc tốn kém hoặc rắc rối về chi phí tính toán, và nếu là ngôn ngữ cấu hình thì cần những giới hạn nghiêm ngặt hơn nhiều so với việc chỉ không Turing-complete
    • Có thể có nhiều cách để trở thành không Turing-complete ngoài việc trở thành một hàm toàn phần kết thúc gọn gàng. Ví dụ, vòng lặp vô hạn vừa không tính toán phổ dụng được, vừa không kết thúc

  • Tôi là nhà phát triển CUE. CUE có tính đệ quy nguyên thủy, và cũng đáp ứng các tiêu chí mà người ta mong đợi ở một ngôn ngữ cấu hình “tốt”