ฟังก์ชันรีเคอร์ชันพื้นฐานสำหรับโปรแกรมเมอร์สายปฏิบัติ

 (matklad.github.io)
2 คะแนน โดย GN⁺ 2024-08-05 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • การถกเถียงในทำนองว่า “ถ้าไม่เป็น Turing-complete ก็ปลอดภัย” นั้นคลาดเคลื่อนจากความหมายทางคณิตศาสตร์ และ ความไม่เป็น Turing-complete ก็แทบไม่เกี่ยวกับคุณสมบัติที่ใช้งานจริงอย่างการจบการทำงาน ความกำหนดแน่นอน หรือ sandboxing
  • การคำนวณของ Turing Machine ที่เวลารันถูกจำกัดด้วย ฟังก์ชันรีเคอร์ชันพื้นฐาน ของอินพุต ก็สามารถเขียนใหม่ด้วยฟังก์ชันรีเคอร์ชันพื้นฐานได้เช่นกัน
  • ฟังก์ชันรีเคอร์ชันพื้นฐานจบการทำงานเสมอ แต่ก็สามารถสร้างฟังก์ชันที่โตเร็วมากอย่าง 2^(2^N) ได้ ดังนั้น การรับประกันว่าจะจบ ไม่ได้หมายความว่าจะใช้เวลารันในทางปฏิบัติได้เสมอ
  • ในงานจริง โปรแกรมที่ไม่หยุดกับโปรแกรมที่กว่าจะจบต้องรออีกหลายพันล้านปีสร้างปัญหาแทบไม่ต่างกัน และภาษาที่เป็น Turing-complete ก็สามารถบังคับหยุดได้ด้วย ตัวนับสเต็ป
  • คุณภาพของภาษา config ขึ้นอยู่กับ ความกำหนดแน่นอน, ความหมายเชิงนิยามที่ชัดเจน, ความบริสุทธิ์, ความปลอดภัยและ sandboxing, การควบคุมเวลารัน, และความเรียบง่าย มากกว่าจะขึ้นกับการเป็น Turing-complete หรือไม่

ความเข้าใจผิดหลักในการถกเถียงเรื่อง Turing-completeness

  • โปรแกรมเมอร์บนอินเทอร์เน็ตมักพูดถึงการ “ไม่เป็น Turing-complete” ว่าเป็นข้อดีหรือเป็นข้อกำหนดในบางโดเมน
  • แต่ Turing completeness เป็นคำเฉพาะจากคณิตศาสตร์ ดังนั้นถ้านำมาใช้แทนคุณสมบัติหลายอย่างที่ผู้ปฏิบัติงานต้องการ ความหมายก็จะพร่าเลือน
  • คุณสมบัติที่ต้องการจริง ๆ คือการรับประกันว่าจะจบ การรันที่เร็ว พฤติกรรมแบบกำหนดแน่นอน sandboxing หรือภาษา config ที่เรียบง่าย ซึ่งส่วนใหญ่แล้วเป็นคนละแกนกับ Turing completeness
  • เพื่อเข้าใจความต่างนี้ ต้องอาศัยผลทางทฤษฎีแบบง่าย ๆ ของ ฟังก์ชันรีเคอร์ชันพื้นฐาน (Primitive Recursive Functions, PRF)

Turing Machine ที่เร็วพอสามารถแปลงเป็น PRF ได้

  • แม้โปรแกรมจะเขียนด้วยภาษาที่เป็น Turing-complete ถ้ารู้ว่าเวลารันเร็วกว่า O(2^(2^N)) ก็สามารถนำอัลกอริทึมเดียวกันไปทำใน ภาษาที่ไม่เป็น Turing-complete ได้
  • ปัญหาเชิงปฏิบัติส่วนใหญ่อยู่ในขอบเขตที่จบเร็วกว่านั้น
  • ดังนั้นภาษาที่ไม่เป็น Turing-complete จึงไม่ได้จำกัดความสามารถในการคำนวณสำหรับงานจริงอย่างมีนัยสำคัญ และก็ไม่ได้มอบพลังพิเศษในการควบคุมการคำนวณให้อัตโนมัติ
  • ในมุมมองงานจริง โปรแกรมสองแบบต่อไปนี้แทบสร้างปัญหาเหมือนกัน
    • โปรแกรมที่ไม่จบการทำงาน
    • โปรแกรมที่กว่าจะจบต้องรอหลังผ่านไป 10^9 คูณ 10^9 สเต็ป
  • แม้แต่ภาษาที่เป็น Turing-complete ก็สามารถ นับจำนวนสเต็ป ในระดับ implementation แล้วหยุดด้วย error เมื่อเกินเพดานที่กำหนด เพื่อกันปัญหาไม่จบการทำงานได้ตรง ๆ

FSM: จบเสมอ แต่พลังการแสดงออกจำกัด

  • Finite State Machine (FSM) เป็น recognizer ที่รับสตริงเป็นอินพุตแล้วคืนค่า “yes” หรือ “no”
  • FSM ประกอบด้วยเซตสถานะจำกัด สถานะเริ่มต้น เซตของสถานะ yes และฟังก์ชันการเปลี่ยนสถานะ
  • หลังจากใช้ฟังก์ชันการเปลี่ยนสถานะซ้ำกับแต่ละสัญลักษณ์ของอินพุตแล้ว ผลลัพธ์จะถูกกำหนดจากว่าสถานะสุดท้ายอยู่ในเซต yes หรือไม่
  • พลังการแสดงออกของ FSM เทียบเท่ากับ regular expression
  • FSM ทำงานเป็นเชิงเส้นตามความยาวอินพุตและจบเสมอ แต่ไม่สามารถรู้จำเซตของสตริงได้ทุกแบบ
    • ตัวอย่างเช่น เซตของสตริงอย่าง 1, 010, 00100, 0001000 ที่มี 0 อยู่สองข้างของ 1 เท่ากันนั้น FSM ไม่สามารถรู้จำได้
    • เมื่ออินพุตยาวพอ สถานะจะเริ่มวนซ้ำเป็นวัฏจักร และถ้าคัดลอกช่วงวัฏจักรนั้น FSM ก็ยังไปถึงสถานะ yes ได้ แต่เงื่อนไขของสตริงจะพัง

Turing Machine: โมเดลที่เพิ่มเทปแบบเปลี่ยนค่าได้ให้ FSM

  • Turing Machine (TM) มีสถานะและฟังก์ชันการเปลี่ยนสถานะเหมือน FSM แต่ทำงานบนเทปที่แก้ไขได้แทนอินพุตคงที่
  • ในแต่ละสเต็ป TM จะอ่านสัญลักษณ์ปัจจุบันบนเทปแล้วทำงานดังนี้
    • แทนที่สัญลักษณ์ปัจจุบันด้วยสัญลักษณ์ใหม่
    • เปลี่ยนสถานะภายใน
    • เลื่อนหัวอ่านไปทางซ้ายหรือขวาหนึ่งช่อง
  • เมื่อ TM ไปถึงสถานะ halt ก็จะหยุด และเนื้อหาบนเทป ณ ตอนนั้นคือผลลัพธ์
  • FSM เป็นตัวรู้จำแบบไบนารี ขณะที่ TM เป็นอุปกรณ์สำหรับคำนวณฟังก์ชัน
  • TM ไม่จำเป็นต้องหยุดเสมอ และอาจเลื่อนไปมาบนเทปพร้อมเปลี่ยนสถานะโดยไม่เคยไปถึงสถานะสุดท้ายเลย

Universal Turing Machine และพลังการคำนวณ

  • โปรแกรมของ TM ไม่ได้มาในรูปโค้ดที่ผู้ใช้ป้อนเข้าไป แต่ถูก hardcode อยู่ใน ฟังก์ชันการเปลี่ยนสถานะ เอง
  • อย่างไรก็ตาม เราสามารถเข้ารหัส TM ใด ๆ และอินพุตของมันเป็นไฟล์ข้อความ แล้วสร้าง TM แบบ “interpreter” ที่แปลความมันได้
  • TM แบบนี้เรียกว่า Universal Turing Machine และมันจะจำลอง TM ตัวอื่นที่ได้รับมาเป็นอินพุต
  • เราสามารถสร้าง TM interpreter ด้วย Python ได้ และในทางกลับกันก็สร้าง Python interpreter ด้วย TM ได้ ดังนั้นทั้งสองจึงถือว่าเทียบเท่ากันในแง่พลังการคำนวณ
  • FSM อ่อนกว่า TM
    • TM สามารถจำลอง FSM ได้
    • TM สามารถตัดสินสตริงที่มี 0 จำนวนเท่ากันสองข้างและมี 1 อยู่ตรงกลางได้ด้วยการจัดการเทป
    • FSM แก้ปัญหาเดียวกันนี้ไม่ได้

มองเทปเป็นสแตกสองกองได้

  • เทปของ TM เป็น abstraction ที่ไม่สะดวกจะ implement โดยตรงในภาษาทั่วไป
  • เทปและตำแหน่งของหัวอ่านสามารถแทนด้วย สแตกสองกอง
    • เนื้อหาทางซ้ายของหัวอ่านคือสแตกซ้าย
    • เนื้อหาทางขวาของหัวอ่านคือสแตกขวาโดยกลับลำดับไว้
  • การเลื่อนหัวอ่านไปซ้ายหรือขวาจึงกลายเป็นการ pop จากสแตกหนึ่งแล้ว push ไปอีกสแตกหนึ่ง
  • ดังนั้น TM จึงมีพลังการคำนวณเทียบเท่ากับ “FSM ที่มีสแตกสองกอง”
  • ถ้าสัญลักษณ์ในสแตกมีแค่ 0 และ 1 ก็สามารถแทนสแตกทั้งกองด้วยจำนวนธรรมชาติหนึ่งจำนวนได้
    • ตรวจ top: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

ข้อจำกัดของ Turing Machine: Halting Problem และผลลัพธ์ตระกูล Rice

  • TM ทุกตัวสามารถเข้ารหัสเป็นข้อความได้ จึงสามารถลิสต์ TM ที่เป็นไปได้ทั้งหมดเป็นรายการอนันต์ได้
  • ด้วยวิธีพิสูจน์แบบ diagonalization เราสามารถแสดงได้ว่ามีฟังก์ชันที่ TM คำนวณไม่ได้อยู่จริง
  • ตัวอย่างที่เฉพาะเจาะจงกว่าคือ Halting Problem
    • เมื่อให้ซอร์สโค้ดของ TM และอินพุตมาแล้ว ต้องตัดสินว่า TM นั้นจะหยุดในสักวันหรือไม่
  • ถ้าสมมติว่า halts(program, input) จบเสมอและถูกต้องเสมอ จะเกิดความขัดแย้งกับโปรแกรม weird ที่รับซอร์สโค้ดของตัวเองเป็นอินพุต
    • ถ้าตัดสินว่าจะหยุด มันจะเข้าลูปอนันต์และไม่หยุด
    • ถ้าตัดสินว่าจะไม่หยุด มันจะจบทันที
  • ดังนั้น halts ต้องมีบางกรณีที่ตอบผิด หรือบางกรณีที่ไม่จบการทำงาน
  • โดยทั่วไปกว่านั้น เราไม่สามารถตัดสินเชิงอัลกอริทึมเกี่ยวกับคุณสมบัติที่ไม่เป็น trivial และคงพฤติกรรมเดิมของ TM ใด ๆ ได้
    • คุณสมบัติทางไวยากรณ์ตรวจได้ แต่คุณสมบัติด้านพฤติกรรมที่ยังคงอยู่หลัง refactor โดยทั่วไปตัดสินไม่ได้

ฟังก์ชันรีเคอร์ชันพื้นฐาน: อุปกรณ์คำนวณที่จบเสมอ

  • ฟังก์ชันรีเคอร์ชันพื้นฐาน (PRF) นิยามเป็นฟังก์ชันที่รับทูเพิลของจำนวนธรรมชาติและคืนค่าจำนวนธรรมชาติหนึ่งจำนวน
  • ฟังก์ชันพื้นฐานคือ zero และ succ
    • zero = 0
    • succ(x) = x + 1
  • เราสามารถสร้างค่าคงที่ผ่านการประกอบฟังก์ชันได้
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • ไม่อนุญาตให้ใช้ recursion ทั่วไป แต่อนุญาตลูปแบบจำกัด LOOP(init, f, n) ที่จำนวนรอบถูกกำหนดล่วงหน้า
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • ข้อจำกัดสำคัญคือจำนวนรอบ n ต้องถูกตรึงไว้ก่อนเริ่มลูป และตัวนับลูปเปลี่ยนจากใน body ของลูปไม่ได้

สร้างองค์ประกอบการเขียนโปรแกรมพื้นฐานด้วย PRF

  • การบวกนิยามได้เป็น add(x, y) = LOOP(x, succ, y)
  • การคูณนิยามได้เป็น mul(x, y) = LOOP(0, add x, y)
  • การยกกำลังนิยามได้เป็น pow(x, y) = LOOP(1, mul x, y)
  • จากนั้นก็สร้างฟังก์ชันที่โตเร็วได้
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • ถ้าเพิ่ม pred เข้าไปในฟังก์ชันพื้นฐาน ก็จะสร้างการลบแบบอิ่มตัวและ boolean operation ได้
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) ก็เขียนเป็นนิพจน์เชิงคณิตศาสตร์ได้
  • การเปรียบเทียบ ค่าเศษ และการหาร ก็ implement ได้ด้วยลูปที่มีเพดานและนิพจน์เงื่อนไข

โครงสร้างข้อมูลของ PRF และการจำลอง TM

  • PRF รับอาร์กิวเมนต์ได้หลายตัว แต่ผลลัพธ์มีได้เพียงจำนวนธรรมชาติเดียว ดังนั้นต้องเข้ารหัสโครงสร้างข้อมูลเป็นจำนวนธรรมชาติ
  • คู่ (a, b) สามารถแทนด้วย 2^a * 3^b
  • หากต้องการดึงองค์ประกอบออกมา ก็หาเลขชี้กำลังสูงสุดของจำนวนเฉพาะที่หารลงตัว
    • fst(p) คือเลขชี้กำลังสูงสุดของ 2 ที่หาร p ลงตัว
    • snd(p) คือเลขชี้กำลังสูงสุดของ 3 ที่หาร p ลงตัว
  • แบบเดียวกันนี้ ค่าสามตัว (S, stack1, stack2) ก็แพ็กเป็นจำนวนธรรมชาติเดียวได้
  • สถานะการตั้งค่าของ TM แสดงได้ด้วยองค์ประกอบสามตัวดังนี้
    • สถานะปัจจุบัน S
    • สแตกด้านซ้ายของเทป
    • สแตกด้านขวาของเทป
  • การจัดการสแตก implement ได้ด้วย modulo การคูณ และการหาร ดังนั้นจึงเข้ารหัส หนึ่งสเต็ป ของ TM เป็น PRF ได้
  • เมื่อใช้ LOOP(initial_config, single_step, n) ก็สามารถจำลอง TM ได้ตรงตามจริงเป็นเวลา n สเต็ป
  • ปัญหาคือเราไม่รู้ n ที่มากพอ แต่ถ้ารู้ว่าเวลารันถูกจำกัดด้วย PRF ตัวใด ก็แค่ให้ลูปซ้ำตามนั้น
  • สรุปคือ การคำนวณของ TM ที่เวลารันถูกจำกัดด้วยฟังก์ชันรีเคอร์ชันพื้นฐาน สามารถแทนด้วย PRF ได้

ข้อจำกัดของ PRF: จบเสมอแต่ไม่ได้ทรงพลังเท่า TM

  • PRF จบเสมอ แต่ไม่ได้แสดงฟังก์ชันที่จบการทำงานทั้งหมดได้
  • มีฟังก์ชันที่ TM คำนวณได้แต่ PRF คำนวณไม่ได้
  • วิธีแสดงคือกำหนดเพดานอัตราการเติบโตโดยอิงจาก ความลึก ของ syntax tree ของ PRF
  • PRF ที่มีความลึกไม่เกิน d จะถูกครอบบนไว้ไม่ให้โตเร็วเกินฟังก์ชันเอกภาคบางตัว A_d
  • นิยามของ A(d, x) เป็นดังนี้
    • 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))
  • นิยามนี้เมื่อคำนวณบน TM จะจบ เพราะทุกครั้งที่เรียก recursion ค่า (d, x) จะเล็กลงตามลำดับพจนานุกรม
  • ฟังก์ชัน a(x) = A(x, x) โตเร็วกว่าทุก PRF และแม้ TM จะคำนวณได้ แต่ PRF คำนวณไม่ได้

กลับมาที่งานจริง: แค่ไม่เป็น Turing-complete ยังไม่พอ

  • Turing Machine อาจไม่หยุดได้
  • อุปกรณ์ที่จบเสมออย่าง FSM และ PRF ก็ไม่ได้รับประกันว่าจะจบเร็ว
  • PRF คำนวณฟังก์ชันใหญ่มากอย่าง 2^(2^N) ได้ ดังนั้นการรับประกันว่าจะจบเพียงอย่างเดียวจึงไม่พอจะรับประกันเวลารันที่ใช้งานได้จริง
  • อัลกอริทึมจริงจำนวนมากมีเวลารันที่ถูกจำกัดด้วย PRF จึงสามารถแสดงได้แม้ด้วยอุปกรณ์ที่ไม่เป็น Turing-complete
  • วิธีทั่วไปในการทำให้การคำนวณแบบ Turing-complete มีพฤติกรรมคล้าย PRF คือเพิ่มตัวนับรอบ แล้วบังคับหยุดเมื่อค่าตัวนับใหญ่เกินไป

คุณสมบัติที่ภาษา config ต้องการจริง ๆ

  • หลายครั้งภาษา config ตั้งเป้าออกแบบว่า “ไม่เป็น Turing-complete” แต่ของที่ต้องการจริง ๆ คือคุณสมบัติที่แรงกว่านั้นหลายอย่าง

  • ความกำหนดแน่นอน

    • ภาษา config ควรเป็นแบบ deterministic
    • พฤติกรรมอย่าง id([]) ของ Python ที่ให้ค่าต่างกันในแต่ละครั้ง อาจยอมรับได้ในงานเขียนโปรแกรมทั่วไป แต่ไม่เหมาะกับ config
    • config มักถูกใช้เป็นคีย์ของระบบ incremental build หรือ caching ดังนั้นถ้ามีความไม่กำหนดแน่นอนเข้ามา พฤติกรรมของ cache จะสั่นคลอน

  • ความหมายเชิงนิยามที่ชัดเจน

    • พฤติกรรมของภาษาควรถูกตรึงไว้อย่างชัดเจนด้วยเกณฑ์อ้างอิงที่ตรวจสอบได้
    • แม้จะปิด ASLR และใช้ allocator เฉพาะเพื่อทำให้ id([]) ของ Python เป็น deterministic ได้ แต่ก็ไม่ได้แปลว่าผลนั้นจะคาดเดาได้หรือเหมือนกันทุก implementation
    • ถ้าต้องการรับประกันพฤติกรรมเดียวกันข้าม implementation หรือข้ามเวอร์ชันของ Python ก็ต้องมี semantics ที่ชัดเจน

  • ความบริสุทธิ์

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

  • ความปลอดภัยและ sandboxing

    • ทั้งความบริสุทธิ์และความปลอดภัยทำได้โดยไม่เปิดเผย IO ทั่วไป
    • แต่จุดประสงค์ของสองคุณสมบัตินี้ต่างกัน
    • ความบริสุทธิ์มีไว้เพื่อกันไม่ให้ผลลัพธ์กลายเป็นแบบไม่กำหนดแน่นอน
    • ความปลอดภัยมีไว้เพื่อไม่ให้ทรัพยากรอย่าง access token รั่วไปถึงผู้โจมตี

  • การควบคุมเวลารัน

    • ต่อให้ควบคุม IO ได้ ก็ยังโจมตีแบบ ปฏิเสธการให้บริการ ด้วยการเผา CPU ผ่าน config อันตรายได้
    • หากต้องการรับประกันเวลารัน สามารถใช้ได้สองแนวทาง
    • จำกัดให้การประมวลผลมีโครงสร้างเชิงเส้นที่ชัดเจน ซึ่งแปรผันตรงกับขนาดอินพุต
    • ใช้การรันแบบมีมิเตอร์ (metered execution) โดยลดค่าตัวนับทุก atomic step และหยุดเมื่อค่าตัวนับเป็น 0

  • ความเรียบง่าย

    • ภาษา config ควรชี้นำให้ผู้ใช้เขียนโปรแกรมที่เรียบง่าย
    • การห้าม recursion และลูปอนันต์อาจเป็น speed bump ที่ช่วยชี้นำไปสู่ความเรียบง่าย
    • แต่ดังตัวอย่าง PRF การห้ามเช่นนี้ไม่ได้กันการเขียนโปรแกรมแบบ recursive โดยอ้อมอย่างสมบูรณ์ เพียงแค่ทำให้ต้องเขียนโค้ดอ้อมมากขึ้น
    • ดูตัวอย่างที่เกี่ยวข้องได้ที่ some roundabout code

สรุปท้ายบท

  • อัลกอริทึมของ Turing Machine ที่เวลารันบนอินพุตถูกจำกัดด้วยฟังก์ชันรีเคอร์ชันพื้นฐานบางตัว สามารถ implement ได้ด้วยฟังก์ชันรีเคอร์ชันพื้นฐานเช่นกัน
  • ความไม่เป็น Turing-complete อาจมอบคุณสมบัติเดียวคือการรับประกันว่าจะจบ แต่ไม่ได้รับประกันเพดานเวลารันหรือคุณภาพของภาษา config ที่งานจริงต้องการโดยอัตโนมัติ
  • ในการออกแบบภาษา config ประเด็นสำคัญกว่าการเป็น Turing complete คือความกำหนดแน่นอน ความหมายเชิงนิยามที่ชัดเจน ความบริสุทธิ์ sandboxing การวัดควบคุมเวลารัน และความเรียบง่าย

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

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

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

  • โปรโมตตัวเอง: https://www.nayuki.io/page/primitive-recursive-functions

    • ดีกว่าบทความต้นฉบับมาก แต่ดูเหมือนว่าช่วงนี้ทุกคนจะชอบ คำอธิบายง่าย ๆ แบบ ELI5 มากกว่า

  • ในส่วนสรุปของบทความมีเกณฑ์ที่ค่อนข้างดีเกี่ยวกับ ภาษา configuration เลยสงสัยว่ามีภาษาในปัจจุบันที่ตรงตามเกณฑ์ทั้งหมดหรือส่วนใหญ่หรือไม่

    • ตัวอย่างที่ตรงตามเกณฑ์นี้มี Dhall [1] และ Cue [2] แต่ในแง่หนึ่งก็ไม่ใช่ตัวอย่างที่น่าสนใจนัก
      Dhall เป็นภาษาฟังก์ชันแบบ total โดยเจตนา จึงไปในทาง “ไม่ให้เป็น Turing-complete” ส่วน Cue ไม่มีฟังก์ชัน จึงไม่มีอะไรให้ recurse
      ผมคิดว่า RCL [3] ตรงตามเกณฑ์ เป็นแบบ deterministic และ pure มีการรันแบบมีการวัดปริมาณ และ sandbox การเข้าถึงไฟล์ซิสเต็ม ถ้า policy ของ sandbox อนุญาต ก็อ่านไฟล์ได้ แต่ไฟล์แบบนั้นถือเป็นส่วนหนึ่งของซอร์สโค้ดและทำงานเหมือน import
      ใน RCL เราไม่อยากไปทาง “ไม่ให้เป็น Turing-complete” ด้วยเหตุผลที่ผู้เขียนพูดถึง การที่โปรแกรมจะจบลงในท้ายที่สุดไม่ใช่คุณสมบัติที่มีประโยชน์นักในงานจริง และในทางกลับกัน แม้แต่ภาษา total function อย่าง Agda ก็ยังเขียนโปรแกรมที่ซับซ้อนมากได้ ดังนั้นการไม่เป็น Turing-complete จึงไม่ได้รับประกันโปรแกรม/การตั้งค่าที่เรียบง่าย
      loop ทุกตัวใน RCL มีขอบเขต แต่มีฟังก์ชันจึง recurse ได้ด้วย ไม่มี tail call ดังนั้นตอนแรกจึงใส่ข้อจำกัดความลึกของ recursion เพื่อกัน native stack overflow แต่ fuzzer ไปเจอฟังก์ชันที่หยุดได้ทั้งที่รันด้วยพื้นที่ stack คงที่ และจนถึงตอนนี้ก็ยังไม่เข้าใจทั้งหมด: let f = g => g(g(h => k => g(g(h)))); f(f)
      สุดท้ายแล้ว การที่สามารถแสดงฟังก์ชันพยาธิแบบนี้ได้ไม่ใช่ปัญหาในงานจริง แค่มีข้อจำกัดจำนวนขั้นตอนการรัน หรือ “gas limit” หรือที่ผู้เขียนเรียกว่า “การรันแบบมีการวัดปริมาณ” ก็พอ การที่โครงสร้าง loop ในตัวมีขอบเขตและ recursion ไม่สะดวกเป็นตัวชักนำที่ดีให้รักษาโค้ดให้เรียบง่าย แต่สุดท้ายเครื่องมือที่มีค่าที่สุดคือ code review และวิจารณญาณที่ดี
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • แม้จะเป็นแบบ imperative และไม่ “pure” แต่แม้แต่ C ก็ถูกสร้างไปในทิศทางที่พยายามให้รู้ขอบเขตบนของจำนวนรอบก่อนเข้า loop ทุกตัว จึงเป็นแบบ primitive recursive
      งานวิจัยของ Dennis Ritchie ที่ MIT โฟกัสหัวข้อที่เขาเรียกว่า loop programming
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      Structured programming ที่โปรแกรมเมอร์สมัยใหม่แทบทุกคนยึดเป็นพื้นฐาน โดยแท้จริงแล้วเป็นพาราไดม์ที่ผลักไปทางฟังก์ชัน primitive recursive เนื่องจาก structured programming ได้รับการยอมรับแทบทั่วไปเมื่อเทียบกับอีกสองแนวทางอย่าง pop และ functional จึงดูเหมือนผู้คนจะสับสนกับบทความ “goto ถือว่าเป็นอันตราย” ของ Dijkstra
      ฟังก์ชัน primitive recursive ไม่ได้ครอบคลุมฟังก์ชันที่คำนวณได้ทั้งหมด แต่ครอบคลุมฟังก์ชันเชิงสัญชาตญาณที่รับประกันว่าจะจบแทบทั้งหมด แน่นอนว่ามีบางกรณีที่จำเป็นต้องใช้ loop ซึ่งไม่รู้จำนวนรอบตอนเริ่มเข้า loop จริง ๆ แต่ถ้าใช้เฉพาะตอนจำเป็นจริง ๆ ก็เป็นปืนที่ยิงเท้าตัวเองซึ่งหลีกเลี่ยงได้
      แม้แต่ COBOL ก็ถูกทำให้ทันสมัยขึ้นโดยย้าย goto แบบไม่จำกัดไปไว้ในคำสั่ง ALTER นึกไม่ออกว่ามีภาษาสมัยใหม่ที่มีประโยชน์ภาษาไหนที่ไม่อนุญาตฟังก์ชัน PR
      ใน C เอง หากเขียนโดยหลีกเลี่ยง while และหลีกเลี่ยง fall through อย่างชัดเจน ก็แทบจะสร้างโค้ด total function ที่ต้องจบเสมอได้เกือบตลอด
      ก็มีกรณีพยาธิอย่าง type inference ของ ML อยู่บ้าง ต้นทุนจริงถูกกว่ามากเมื่อเทียบกับ complexity class ดังนั้นแม้ภาษาจะจำกัดการใช้งานแบบนี้ได้ยากหากไม่ทำให้เป็น total function ก็ยังคุ้มที่จะยอมรับ
      ในเชิงปฏิบัติ ภาษาทุกภาษามักให้ค่าเริ่มต้นที่รองรับเกณฑ์เหล่านี้ส่วนใหญ่ แต่ข้อจำกัดที่บังคับใช้สิ่งนี้จะจำกัดประโยชน์ของภาษาอย่างรุนแรง ผมมองว่าแม้แต่ SOLID กับ Clean framework ที่มักถูกด่าก็ยังผลักไปทางโมเดลนี้
      Structured programming กลายเป็นเรื่องแพร่หลายมากจนลืมประเด็นนี้ได้ง่าย และถึงขั้นสอนกันไม่เป็นด้วยซ้ำ จากมุมของคนแก่มีเครา ผมจำได้ว่าเคยเรียนรู้ถึงอันตรายของ WHILE และอื่น ๆ
    • น่าจะเลือกดู Dhall แล้วดูว่ามันพลาดเกณฑ์ไหน ใกล้เคียงที่สุดแล้ว

  • คำกล่าวที่ว่ามันรันเร็วกว่า O(2^(2^N)) คงเป็นคำพูดที่พยายามทำให้เรียบง่าย แต่ส่วนที่ว่า “จำนวนที่ใหญ่มาก” ทำให้ความน่าเชื่อลดลงเล็กน้อย
    พูดให้ถูกน่าจะเป็น “ฟังก์ชันที่เติบโตเร็วมาก” หรือไม่ก็เหมือนจะหมายความว่าโปรแกรมจบในจำนวนน้อยกว่า O(2^(2^N)) ขั้นตอน

  • ถ้าดูเฉพาะส่วนแรกที่บอกว่าภาษาที่ถูกจำกัดเหมาะกับบางแอปพลิเคชันมากกว่า ผมคิดว่าข้อดีคือสามารถ คำนวณขอบเขตบน ของจำนวนขั้นตอนที่ต้องใช้แบบสแตติกได้หรือเปล่า
    ถ้าอย่างนั้น การคำนวณที่ละเมิดข้อจำกัดสำหรับอินพุตใด ๆ ก็จะถูกปฏิเสธและส่งคืนข้อผิดพลาดที่มีความหมายได้
    ในทางกลับกัน วิธีที่กำหนดข้อจำกัดตอนรันไทม์ให้กับภาษาที่ Turing-complete อาจตั้งข้อจำกัดต่ำเกินไปสำหรับอินพุตบางตัวที่เราสนใจได้ จะไม่รู้จนกว่าจะรันแล้วชนข้อจำกัด บางครั้งเห็นเรื่องแบบนี้ใน recursion ของ template ใน C++
    ผมอาจจะเข้าใจผิดไปหมดก็ได้ ถ้ามีคนที่รู้ดีกว่าช่วยอธิบายจะดีมาก

    • หลังจากอดีตเพื่อนร่วมงานคนหนึ่งตั้งตัวเลขไว้เกือบ 3 เท่า แล้วไม่กี่ปีต่อมา workload จริงไปชนข้อจำกัดนั้น ผมจึงใช้ ข้อจำกัด 10 เท่า ของปริมาณการคำนวณที่สมเหตุสมผล
      แม้ workflow แย่ ๆ จะใช้เวลานานขึ้นอีกหลายเท่ากว่าจะล้มเหลว ก็ยังอยู่ในระดับมิลลิวินาที จึงไม่น่าก่อความเสียหายมาก
      โดยทั่วไปจะเจอปัญหานี้เมื่อมีคนจัดการโดเมนปัญหาเป็นกราฟมีทิศทางแบบไม่มีวงจร แต่บังคับความ “ไม่มีวงจร” ไม่ได้ การโมเดลปัญหาเป็นกราฟมีทิศทางแบบไม่มีวงจรเหมือน Dark Galadriel ที่กำลังลังเลว่าจะรับแหวนจาก Frodo หรือไม่ “ทุกคนจะรักข้าและสิ้นหวัง” คนที่สร้างของแบบนี้มักภูมิใจกับมันมากกว่าที่ควรจะภูมิใจเสมอ
      สุดท้ายลูกค้าที่ถูกดึงเข้ามาด้วยวิธีแก้ปัญหาที่แพงและซับซ้อนก็เงินหมด และปัญหาของตัวเองก็เริ่มดูเล็กลงมาก แล้วในความหมายตามตัวอักษร ก็จะเหลือเพียงแอปที่ไม่สามารถลดต้นทุนต่อ task ให้ต่ำพอจะรักษาธุรกิจของลูกค้าไว้ได้
    • การทำนาย ปริมาณการใช้เชื้อเพลิง ของการคำนวณบนบล็อกเชนอย่างแม่นยำอาจน่าสนใจสำหรับคนอื่น แต่ไม่ใช่สำหรับผม
      ผมสนใจมากกว่ากับการใช้มันเป็นค้อนอีกอันในกล่องเครื่องมือ เพื่อจับบั๊กที่หลุดผ่านค้อนก่อนหน้าอย่างการตรวจสอบชนิดแบบสแตติก, ไม่มี null, ไม่มีการเปลี่ยนแปลงค่า
      การที่รู้ว่าจะจบภายในเวลาจำกัดไม่ได้พิสูจน์ความถูกต้องสอดคล้อง แต่ถ้าผมประกาศว่าโค้ดจะจบภายในเวลาจำกัด แล้วคอมไพเลอร์ไม่เห็นด้วย ผมก็จะเชื่อว่าโค้ดนั้นผิด
    • ขอบเขตบนที่กำหนดแบบสแตติกอาจประเมินความซับซ้อนของเวลารันจริงในกรณีทั่วไปสูงเกินไปมาก เพราะโดยทั่วไปไม่สามารถทำนายได้ว่าเงื่อนไขที่ทำให้เกิด การจบก่อนกำหนด ใน recursion จะถูกประเมินอย่างไร
      ถ้าการจบก่อนกำหนดจะมีผลต่อเวลารัน ก็ต้องสมมติว่ามี lazy evaluation หรือเงื่อนไขแบบ short-circuit แต่ภาษาเชิงปฏิบัติโดยมากก็มักมีสิ่งเหล่านั้น
    • แล้วถ้าขอบเขตบนนั้นหลวมสุด ๆ ล่ะ? เช่น deterministic quicksort โดยปกติเป็น n log n แต่มี ขอบเขตบนกำลังสอง ตามขนาดอินพุต
      ถ้าอย่างนั้นจะปฏิเสธการคำนวณ quicksort ไหม? ยิ่งสุดโต่งกว่านั้น อัลกอริทึม Hindley–Milner มีขอบเขตบนแบบเอกซ์โพเนนเชียล แต่ในทางปฏิบัติมักรันเป็นเวลาเชิงเส้น
    • ไม่รู้ว่ามัน “คำนวณแบบสแตติก” หรือเปล่า แต่ผมเห็นว่าข้อดีเพียงอย่างเดียวของการจำกัดความสามารถของภาษาอย่างมาก คือการตั้ง ข้อจำกัดการคำนวณ แบบที่ไม่ขึ้นกับข้อมูลได้
      แต่ก็คิดไม่ออกเลยว่ามีสถานการณ์ไหนที่นี่เป็นข้อกำหนดที่แข็งมากจริง ๆ มีระบบสักกี่ระบบที่ไม่สามารถส่งข้อผิดพลาดว่า “คิวรีใช้เวลานานเกินไป” ได้?

  • ผมเคยอยากลองใช้ภาษาโปรแกรมมิงเว็บฝั่งแบ็กเอนด์ที่ตั้งอยู่บนหลักการ ไม่จบ/มีขอบเขต
    แนวคิดคือคอมไพเลอร์พิสูจน์ได้ว่าทุกฟังก์ชันมีการรันอยู่ภายในขอบเขตสำหรับสถานะและอาร์กิวเมนต์ที่ให้มา และแสดงได้ว่า X เป็นขอบเขตล่าง ส่วน Y เป็นขอบเขตบน ข้อมูลนี้จะถูกส่งต่อไปถึง entry point
    ผมเห็นด้วยกับผู้เขียนที่บอกว่าต้องการ semantics ที่แข็งแรงกว่า และนั่นคือเหตุผลที่คิดถึงภาษานี้ขึ้นมา หลายครั้งเราต้องการการรับประกันเกี่ยวกับเวลารันของโปรแกรม
    แก่นหลักน่าจะอิงกับฟังก์ชัน primitive recursive แต่ในทางปฏิบัติอาจเป็น Turing-complete ได้ เหมือนที่ Rust ปฏิเสธ borrow ที่ผิด แต่ก็มี unsafe สำหรับ raw pointer ภาษานี้ก็จะคำนวณขอบเขตจาก primitive แบบวนซ้ำง่าย ๆ หรือให้ใช้ตัวดำเนินการ unsafe แล้วระบุสูตรทดแทนสำหรับขอบเขตได้

  • ผมไม่ค่อยเข้าใจส่วนบ่น/แรงจูงใจสั้น ๆ ของบทความ
    คือส่วนที่ว่า “โดยทั่วไปในบางโดเมน การไม่เป็น Turing-complete มักถูกยกย่องว่าเป็นข้อดีหรือข้อกำหนด ผมคิดว่าการถกเถียงส่วนใหญ่ในเรื่องนี้เข้าใจผิด — การบอกว่าไม่เป็น Turing-complete ไม่ได้หมายความอย่างที่ผู้คนคาดหวัง”
    ทำไมการถกเถียงพวกนั้นถึงผิด? เครื่องมือวิเคราะห์เชิงรูปแบบส่วนใหญ่ เช่น Coq, Isabelle, Agda มักกำหนดให้ต้องมีหลักฐานว่าฟังก์ชันจบการทำงาน นี่เท่ากับการพิสูจน์ว่าฟังก์ชันนั้นเป็นฟังก์ชันทั้งหมด และดังนั้นก็หมายความว่าเป็น primitive recursive ไม่ใช่หรือ?

    • ยังอ่านไม่จบ แต่บทความนี้ดูเหมือนจะมาจากการที่ภาษา configuration บางตัวชู “ไม่เป็น Turing-complete” เป็นฟีเจอร์ ทั้งที่ฟีเจอร์ที่น่าจะอยากโปรโมตจริง ๆ คือ เวลารันที่ถูกจำกัดอย่างสมเหตุสมผล
      ประเด็นนี้ก็เพิ่งถูกพูดถึงในการอภิปรายเกี่ยวกับ CEL เมื่อไม่นานนี้:
      https://news.ycombinator.com/item?id=40954652
    • ถ้ากำลังพูดถึงการพิสูจน์เชิงรูปแบบ ในกรณีทั่วไป การพิสูจน์ว่าฟังก์ชันเป็นฟังก์ชันทั้งหมดนั้นเป็น ปัญหาค้นหาแบบ NP-complete ไม่ใช่ตัวอย่างโต้แย้งเชิงวิทยาศาสตร์ที่ใช้กันในการเขียนโปรแกรมสมัยใหม่
      ถ้าจำไม่ผิด สิ่งนี้เทียบเท่ากับ NP ที่มี oracle แบบ co-NP หรือระดับที่สองของ polynomial hierarchy แม้จะทำได้ในปัญหาเล็ก ๆ แต่ก็แพง
      เครื่องมือเหล่านี้ทำงานได้ดีที่สุดเมื่อจัดโครงสร้างโปรแกรมให้เป็นฟังก์ชันทั้งหมด ในบรรดาวิธีเหล่านั้น วิธีที่พบบ่อยที่สุดคือใช้เฉพาะ FOR ใน structured programming หรือใช้ WHILE/recursion ที่มีจำนวนรอบจำกัด
      แม้จะเกี่ยวข้องเฉพาะกับ SAT แต่รูปแบบที่จัดการได้ในทฤษฎีบท dichotomy ของ Schaefer เป็นเลนส์ที่เข้าถึงง่ายที่สุดเท่าที่ผมนึกออก
    • อย่างที่บทความแสดงให้เห็น มีฟังก์ชันที่จบการทำงานแต่ไม่ใช่ primitive recursive ดังนั้น การพิสูจน์ว่าเป็นฟังก์ชันทั้งหมด จึงไม่ได้หมายความว่าเป็น primitive recursive
      Agda และอาจรวมถึงเครื่องมืออื่น ๆ สามารถพิสูจน์การจบการทำงานของฟังก์ชัน recursive ที่ไม่ใช่ primitive recursive บางส่วนได้ แน่นอนว่าเป็นไปไม่ได้ที่จะทำได้ทั้งหมด
      ความเข้าใจผิดที่บทความบ่นถึงน่าจะประมาณนี้: “Turing-completeness หมายถึงคำนวณได้ ส่วน non-Turing-completeness หมายถึงคำนวณไม่ได้และมีคุณสมบัติที่ดีสำหรับภาษา configuration”
      ใจความของบทความคือ แม้ไม่เป็น Turing-complete ก็ยังทำงานที่มีต้นทุนการคำนวณสูงหรือยุ่งยากได้มากมาย และถ้าเป็นภาษา configuration ก็ต้องมีข้อจำกัดที่เข้มงวดกว่าการแค่ไม่เป็น Turing-complete มาก
    • วิธีที่จะไม่เป็น Turing-complete อาจมีมากกว่าการเป็นฟังก์ชันทั้งหมดที่จบการทำงานอย่างเรียบร้อย เช่น ลูปไม่รู้จบ ก็ทั้งไม่สามารถคำนวณแบบสากลได้ และไม่จบการทำงาน

  • ผมเป็นนักพัฒนา CUE CUE เป็นแบบ primitive recursive และยังเป็นไปตามเกณฑ์ที่คาดหวังจากภาษา configuration ที่ “ดี” ด้วย