09 · การคำนวณได้
ภาค II เปิดการไต่สวนครั้งแรกตรงนี้ การคำนวณลุกจากเก้าอี้พยานไปนั่งเก้าอี้ผู้ซักถาม และคำถามแรกพุ่งเข้าใส่ตัวมันเอง: ขีดจำกัดที่เป็นรากฐานของมันพิสูจน์อะไรได้จริง?
ขีดจำกัดของการคำนวณ พิสูจน์อะไรเกี่ยวกับขีดจำกัดของเหตุผลได้บ้าง?
สองงานวิจัยในปี 1936 ตอบคำถามเดียวกันห่างกันหกสัปดาห์ โดยผู้เขียนทั้งสองไม่เคยอ่านบทพิสูจน์ของอีกฝ่าย บทความ "An Unsolvable Problem of Elementary Number Theory" ของ Alonzo Church ออกวันที่ 15 เมษายน ใน American Journal of Mathematics (58: 345–363) แสดงด้วย lambda-definability ว่าไม่มีอัลกอริทึมใดตัดสิน Entscheidungsproblem (ปัญหาการตัดสินใจ) ได้ — คำถามที่ David Hilbert กับ Wilhelm Ackermann ตั้งไว้ใน Grundzüge der theoretischen Logik (1928) ว่ากระบวนการเชิงกลไกจะรับรองความสมเหตุสมผลของประโยคอันดับหนึ่ง (first-order sentence) ใดๆ ได้หรือไม่ Proceedings of the London Mathematical Society รับบทความของ Alan Turing เอง "On Computable Numbers, with an Application to the Entscheidungsproblem" วันที่ 28 พฤษภาคม คำตอบเป็นลบอย่างเดียวกันเป๊ะ แต่มาคนละทางโดยสิ้นเชิง: เสมียนมนุษย์ที่ถูกลดรูปเหลือเทปกระดาษ ชุดสถานะจำกัดชุดหนึ่ง และตารางคำสั่ง Turing ผิดหวังที่รู้ว่ามีคนตีพิมพ์ตัดหน้า จึงเติมภาคผนวกพิสูจน์ว่าเครื่องของเขากับฟังก์ชัน lambda-definable ของ Church คำนวณฟังก์ชันคลาสเดียวกันพอดี นิยามของ "เชิงกลไก" สองแบบ คิดขึ้นแยกกันโดยอิสระ กลับทับกันสนิท ความบังเอิญนั้นคือหลักฐานทั้งหมดที่มีให้กับสิ่งที่วันนี้เรียกว่าข้อตั้ง Church–Turing (Church–Turing thesis) และหลักฐานไม่ใช่สิ่งเดียวกับบทพิสูจน์
มันเป็นทฤษฎีบทไม่ได้ เพราะ "คำนวณได้อย่างมีประสิทธิผล" (effectively calculable) ไม่เคยเป็นคำเชิงรูปนัยมาก่อนที่ Turing จะทำให้มันเป็นรูปนัย จะพิสูจน์ความเท่ากันระหว่างสิ่งที่แม่นยำกับสิ่งที่ถึงตอนนั้นยังเป็นแค่สัญชาตญาณย่อมทำไม่ได้ สิ่งที่ Turing ทำจริงๆ คือไล่ให้ครบทุกกรณีว่ามนุษย์ที่ทำหน้าที่ "computer" — คนที่ทำตามคำสั่งตายตัวด้วยดินสอกับกระดาษ — ทำอะไรได้บ้าง: อ่านสัญลักษณ์ เปลี่ยนสถานะภายใน เขียนสัญลักษณ์ ย้ายความสนใจ ฟอร์มัลลิสม์ (formalism) คู่แข่งทุกตัวที่เสนอมาตั้งแต่นั้น — ฟังก์ชันเวียนบังเกิดทั่วไป (general recursive functions) ของ Gödel–Herbrand, ระบบการผลิต (production systems) ของ Emil Post, เครื่องรีจิสเตอร์ (register machines) — ถูกพิสูจน์แล้วว่าเทียบเท่ากับของ Turing และ Stephen Kleene ผู้ตั้งชื่อข้อคาดการณ์นี้ว่า "Church's Thesis" ในปี 1943 อ่านการลู่เข้าหากันนั้นเป็นหลักฐานสนับสนุนเชิงอุปนัย ไม่ใช่การปิดเชิงนิรนัย ข้อตั้งนี้จึงตกอยู่ในหมวดที่โครงการของ Hilbert ไม่เคยคาดถึง: ไม่ใช่คณิตศาสตร์เต็มตัว ไม่ใช่วิทยาศาสตร์เชิงประจักษ์เต็มตัว ยืนอยู่ได้เพราะทุกคนที่พยายามหักล้างมันกลับยืนยันมันแทน
ความไม่มั่นคงนั้นเองให้ผลผลิตเชิงปรัชญา เพราะวิธีที่ Turing ใช้ไปถึงมัน — การทแยงมุม (diagonalization) การหันกลไกของระบบกลับมาโจมตีตัวมันเอง — โตเกินทฤษฎีบทที่มันสร้างไปไกล Cantor ใช้มันในปี 1891 แสดงว่าไม่มีรายการจำนวนจริงใดครบถ้วนได้ Gödel ดัดแปลงมันในปี 1931 สร้างประโยคเลขคณิตที่ยืนยันความพิสูจน์ไม่ได้ของตัวเอง Turing ดัดแปลงมันอีกครั้ง แสดงว่าไม่มีอัลกอริทึมใดตัดสินปัญหาการหยุด (halting problem) ได้ สำหรับโปรแกรมใดก็ตามจะบอกไม่ได้ว่ามันจะหยุดทำงานหรือไม่ — ป้อนตัวตัดสิน halting problem สมมติด้วยคำอธิบายของตัวมันเอง ความขัดแย้งโผล่ออกมาในบรรทัดเดียว โครงเดียวกันโผล่ซ้ำในบทพิสูจน์ของ Tarski ที่ว่าไม่มีภาษาใดที่รุ่มรวยพอจะนิยามภาคแสดงความจริง (truth predicate) ของตัวเองได้ และในปฏิทรรศน์ความรู้ได้ (paradox of knowability) ของ Frederic Fitch ปี 1963 ราวกลางศตวรรษที่ 20 diagonalization เลิกเป็นกลเม็ดของนักคณิตศาสตร์ และกลายเป็นบทพิสูจน์มาตรฐานของปรัชญาที่ว่าระบบหนึ่งส่องไฟดูตัวเองให้ทั่วไม่ได้ — รูปแบบข้อโต้แย้งที่แกนห้องพิจารณาคดีของหนังสือเล่มนี้เองพึ่งพาอยู่
ข้อกล่าวอ้างที่โด่งดังที่สุดในอาณาเขตนี้ยืนบนรูปแบบข้อโต้แย้งอันเดียวกัน J. R. Lucas พูดต่อหน้า Oxford Philosophical Society ในปี 1959 แล้วเขียนโต้แย้งเป็นลายลักษณ์อักษรใน "Minds, Machines and Gödel" (Philosophy 36, 1961: 112–127) ว่าทฤษฎีบทของ Gödel หักล้างกลไกนิยม (mechanism): สำหรับระบบรูปนัย F ที่สมเหตุสมผลใดๆ ที่แข็งแรงพอจะเข้ารหัสเลขคณิตได้ การสร้างของ Gödel ให้ประโยคจริงประโยคหนึ่งที่ F พิสูจน์ไม่ได้ แต่ผู้ให้เหตุผลที่เป็นมนุษย์ ยืนอยู่นอก F และไตร่ตรองมัน กลับเห็นได้ว่าประโยคนั้นจริง — ฉะนั้นไม่มีระบบรูปนัยเดียวใดจับทุกสิ่งที่จิตรู้ได้ครบ และจิตจึงไม่ใช่เครื่องจักร Roger Penrose รื้อฟื้นข้อโต้แย้งนี้ให้ยาวขึ้นใน The Emperor's New Mind (1989) และปกป้องเวอร์ชันที่เสริมกำลังแล้วใน Shadows of the Mind (1994) คำตอบโต้มาตรฐาน สั่งสมมาหลายทศวรรษนับจาก Paul Benacerraf เป็นต้นมา คือข้อโต้แย้งนี้แอบสอดความแน่นอนแบบเดียวกับที่ทฤษฎีบทความไม่สมบูรณ์ข้อที่*สอง*ของ Gödel ห้ามไว้เข้ามาพอดี: การจะ "เห็น" ว่าประโยค Gödel สำหรับ F เป็นจริง ผู้ให้เหตุผลต้องรู้อยู่ก่อนแล้วว่า F สมเหตุสมผล และไม่มีระบบที่สมเหตุสมผล — มนุษย์หรือเครื่องจักรก็ตาม — พิสูจน์ความสมเหตุสมผลของตัวเองจากภายในได้ ข้อโต้แย้งนี้ยังสมมติตั้งแต่แรกว่าจิตมนุษย์ถูกจำลองได้ดีในฐานะระบบรูปนัยหนึ่งเดียว ตายตัว สมเหตุสมผล ซึ่งไม่มีอะไรในที่นี้ยืนยันให้ การคำนวณ เมื่อสอบข้อกล่าวอ้างนี้จากที่นั่งพยานของตัวเอง รับรองมันไม่ได้ แต่ปรัชญาก็ตอบกลับตรงนี้เหมือนกัน เพราะข้อตั้งก่อตั้งของเครื่องจักรเองมีรูปทรงเดียวกันกับความไว้ใจตัวเองที่พิสูจน์ไม่ได้ — Church–Turing thesis รับรองอาณาเขตของตัวเองไม่ได้ถ้าไม่อาศัยสัญชาตญาณเรื่อง "เชิงกลไก" ที่ไม่มีฟอร์มัลลิสม์ใดพิสูจน์ ไม่ต่างจากที่ผู้ให้เหตุผลมนุษย์รับรองความสมเหตุสมผลของ F จากภายใน F ไม่ได้
Turing รู้ว่าข้อตั้งของตัวเองมีขอบ เพราะเขาเป็นคนขีดมันเอง วิทยานิพนธ์ปริญญาเอกที่ Princeton ปี 1939 ของเขา "Systems of Logic Based on Ordinals" เปิดตัวเครื่องออราเคิล (oracle machine): เครื่องทัวริงที่ติดออราเคิลกล่องดำไว้ ตอบคำถามที่เครื่องทัวริงตอบเองไม่ได้ B. Jack Copeland และ Diane Proudfoot ตั้งชื่อโครงการวิจัยที่งอกจากช่องนั้นในภายหลังว่าไฮเปอร์คอมพิวเตชัน (hypercomputation) และ Copeland โต้แย้งว่าโครงสร้างทางฟิสิกส์ที่แปลกประหลาด — closed timelike curve หรือการคำนวณแบบ infinite-proper-time ที่กาลอวกาศแบบ Malament–Hogarth เปิดทางให้ — อาจทำให้ออราเคิลเป็นจริงได้ในหลักการ ข้อคัดค้านที่ตรงไปตรงมาคือปัญหาการตรวจสอบยืนยัน (verification problem): ต่อให้สร้างอุปกรณ์แบบนั้นขึ้นมาได้ ก็ไม่มีอะไรจากภายนอกยืนยันได้ว่ามันคำนวณฟังก์ชันที่ non-Turing-computable แท้ๆ ไม่ใช่ฟังก์ชันที่ Turing-computable แต่ใหญ่โตมโหฬาร ตรงนี้ฟิสิกส์ ไม่ใช่ตรรกศาสตร์ เป็นผู้ลงคะแนนชี้ขาดว่าข้อตั้งนี้ล้อมการคำนวณที่เป็นไปได้ทั้งหมด หรือล้อมแค่การคำนวณเท่าที่เอกภพของเราเผอิญอนุญาต
Gödel เองอนุญาตไว้น้อยกว่าที่คนเผยแพร่งานของเขาอ้างมาก ในการบรรยาย Gibbs Lecture ปี 1951 เขาวางเงื่อนไขแบบ "หรือ" (disjunction) ไว้แล้วหยุดตรงนั้น: จิตมนุษย์ไม่เทียบเท่าเครื่องจักรจำกัดใดๆ หรือไม่ก็มีปัญหาทางคณิตศาสตร์ที่ตัดสินไม่ได้เด็ดขาดไม่ว่าด้วยวิธีใด — หรือทั้งสองอย่าง — แต่เขาปฏิเสธที่จะบอกว่าข้อไหน เขายังเป็นนักเพลโตนิยมทางคณิตศาสตร์ที่เอนไปทางข้อแรกโดยไม่เคยยืนยันว่าตนพิสูจน์มันได้ สิ่งที่ Gödel พิสูจน์คือขีดจำกัดภายในระบบรูปนัย สิ่งที่ Lucas, Penrose และวรรณกรรมรองตลอดหนึ่งศตวรรษดึงออกมาจากมัน คือข้อสรุปเรื่องจิตที่ตัวทฤษฎีบทเองไปไม่ถึง
เชื่อมโยง
บทที่ 00 เรียกปี 1936 ว่าคือช่วงที่เครื่องจักรหล่นออกมาจากบทพิสูจน์เชิงปรัชญา บทนี้ย้อนกลับไปถามว่าช่วงเวลานั้นอนุญาตอะไรไว้จริงๆ บทที่ 01 เป็นเจ้าของ Gödel และ Curry–Howard ในฐานะมรดกร่วมของตรรกศาสตร์ บทที่ 04 เป็นเจ้าของคำถามที่ข้อโต้แย้งของ Lucas–Penrose พยายามตัดสินจากภายนอก — ว่าจิตคือสิ่งที่สมองคำนวณหรือไม่ บทที่ 10 บีบ "ในหลักการ" ให้กลายเป็นทรัพยากรที่วัดได้ บทที่ 12 แสดงว่า proof assistant ทำอะไรกับความไม่สมบูรณ์ เมื่อมันถูกมองเป็นข้อจำกัดเชิงวิศวกรรมแทนคำตัดสินเชิงปรัชญา
คำถามที่ยังเปิดอยู่
Church–Turing thesis พิสูจน์เท็จได้ (falsifiable) หรือไม่ — และถ้ามี hypercomputer ที่ใช้งานได้จริง มันจะหักล้างข้อตั้งนี้ หรือแค่ย้ายเส้นขอบที่มันขีดไว้? เงื่อนไขแบบ "หรือ" ของ Gödel ในปี 1951 เคยถูกคลี่คลายไหม หรือยังเปิดค้างเหมือนที่ตัวข้อตั้งเองเปิดค้างอยู่? และถ้าจิตกลายเป็นสิ่งที่ Turing-equivalent จริง นั่นยุติข้อถกเถียงเรื่องหน้าที่นิยม (functionalism) หรือยุติแค่เรื่องการคำนวณได้ — คำถามที่บทนี้ตั้งได้แต่ตอบไม่ได้
อ่านต่อ
- B. Jack Copeland, Carl J. Posy, and Oron Shagrir, eds., Computability: Turing, Gödel, Church, and Beyond (Cambridge, MA: MIT Press, 2013).
- Alonzo Church, "An Unsolvable Problem of Elementary Number Theory," American Journal of Mathematics 58 (1936): 345–363; Alan Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem," Proceedings of the London Mathematical Society, ser. 2, 42 (1936–37): 230–265, received 28 May 1936 — doi.org/10.1112/plms/s2-42.1.230.
- Stanford Encyclopedia of Philosophy, "The Church-Turing Thesis" — plato.stanford.edu/entries/church-turing.