อลอนโซ เชิร์ช: สถาปนิกผู้ถูกลืมของปัญญาคอมพิวเตอร์
(onepercentrule.substack.com)- Alonzo Church อาจไม่เป็นที่รู้จักในวงกว้างเท่า Alan Turing แต่เขาคือนักตรรกศาสตร์ผู้วางรากฐานเชิงตรรกะของการคอมพิวติ้งด้วย λ-calculus และทฤษฎีความสามารถในการคำนวณ
- Church-Turing thesis ในปี 1936 ได้เสนอกรอบคิดว่าฟังก์ชันใดก็ตามที่คำนวณได้อย่างมีประสิทธิผล สามารถคำนวณได้ด้วย Turing machine หรือระบบที่สมมูลกัน
- จาก Entscheidungsproblem ของ Hilbert เขาได้ให้คำตอบว่าไม่มีอัลกอริทึมแบบตัดสินได้แน่ชัดที่ใช้ตัดสินข้อความทางคณิตศาสตร์ทุกข้อได้ ซึ่งทำให้ขอบเขตของการคำนวณชัดเจนขึ้น
- ที่ Princeton เขาเป็นอาจารย์ให้กับ Stephen Kleene, J. Barkley Rosser, Alan Turing และคนอื่น ๆ โดย Turing สำเร็จ Ph.D. ภายใต้การดูแลของ Church
- งานเชิงนามธรรมของเขายังคงอยู่ในสายธารวิวัฒนาการของการคำนวณที่ทอดยาวมาถึงคอมไพเลอร์ อินเทอร์พรีเตอร์ การเขียนโปรแกรมเชิงฟังก์ชัน แอปสมาร์ตโฟน และ AI
อิทธิพลทางทฤษฎีที่ยิ่งใหญ่กว่าชื่อเสียงในหมู่คนทั่วไป
- Alan Turing มักถูกกล่าวถึงบ่อยกว่าในประวัติศาสตร์สาธารณะของการคอมพิวติ้งและปัญญาประดิษฐ์จากแนวคิด Turing Test แต่ Church คือบุคคลที่มีอิทธิพลอย่างมากต่อแนวคิดและงานของ Turing
- งานของ Church เป็นรากฐานสำคัญต่อการทำความเข้าใจว่าการคำนวณคืออะไร และต่อการสร้างกรอบแนวคิดสำหรับประเมิน AI
- หากไม่มีผลงานของ Church แนวคิดปัจจุบันเกี่ยวกับปัญญาประดิษฐ์และวิธีประเมินมันก็อาจแตกต่างไปอย่างมาก
ชีวิตและแนวโน้มทางวิชาการ
- Church เป็น นักตรรกศาสตร์ ที่เงียบขรึมและพูดน้อย เกิดเมื่อวันที่ 14 มิถุนายน 1903 ที่ Washington, D.C.
- มีบันทึกว่าในวัยเด็กเขาตาบอดหรือสูญเสียการมองเห็นบางส่วนที่ตาข้างหนึ่งจากอุบัติเหตุปืนลม
- หลังจบ preparatory school ใน Connecticut ในปี 1920 เขาเริ่มเรียนมหาวิทยาลัยที่ Princeton ในปีเดียวกัน และสำเร็จการศึกษาระดับปริญญาเอกในปี 1927
- หลังใช้เวลาเป็น National Research Fellow ที่ Harvard, Göttingen และ Amsterdam เขากลับมาที่ Princeton และสร้างผลงานทางวิชาการส่วนใหญ่ของตนที่นั่น
- เขาเป็นที่รู้จักจากลายมือบนกระดานที่เป็นระเบียบและนิสัยที่พิถีพิถัน ถึงขั้นเคลือบบทความสำคัญด้วย Duco cement เพื่อเก็บรักษาไว้
λ-calculus และความสามารถในการคำนวณ
- ผลงานที่ลึกซึ้งที่สุดของ Church คือ λ-calculus ซึ่งเป็นรากฐานก่อนที่สาขานี้จะมีชื่อว่า computer science
- ในปี 1936 Church ได้วางรูปแบบอย่างเป็นทางการของ Church-Turing thesis ซึ่งเป็นแนวคิดหลักของวิทยาการคอมพิวเตอร์เชิงทฤษฎี
- เนื้อหาคือฟังก์ชันที่คำนวณได้อย่างมีประสิทธิผล สามารถคำนวณได้ด้วย Turing machine หรือระบบที่สมมูลกัน
- มันให้กรอบสำหรับทำความเข้าใจว่าในทางทฤษฎีแล้วเครื่องจักรทำอะไรได้บ้าง
- พร้อมกันนั้นก็เผยให้เห็นขอบเขตที่กระบวนการเชิงอัลกอริทึมไม่อาจก้าวข้ามได้
- แม้แนวคิดนี้จะเป็นรากฐานสำคัญ แต่ก็ยังมีการถกเถียงและข้อจำกัดเกี่ยวกับการตีความคำว่า ‘effective computability’ การคำนวณทางกายภาพ และธรรมชาติของสติปัญญามนุษย์
- หาก Turing เสนอ Turing machine เพื่อแปลงกระบวนการเชิงกลให้เป็นรูปแบบตรรกะ Church ก็เป็นผู้มอบ นามธรรมบริสุทธิ์ ที่ค้ำจุนเครื่องจักรแบบนั้นในทางทฤษฎี
การเขียนโปรแกรมสมัยใหม่และแนวคิดเชิงฟังก์ชัน
- อิทธิพลของ λ-calculus ยังปรากฏในหลักการเขียนโปรแกรมปัจจุบัน โดยเชื่อมโยงกับแนวทางที่เน้น composition, higher-order functions และ immutability
- ระบบเชิงรูปแบบนี้ทำให้สามารถเข้ารหัสปัญหาคณิตศาสตร์เชิงนามธรรมเป็นโค้ดและแก้ด้วยเครื่องจักรได้อย่างเป็นระบบ อีกทั้งยังเป็นพื้นฐานของสถาปัตยกรรมคอมไพเลอร์และอินเทอร์พรีเตอร์สมัยใหม่
- สำหรับโปรแกรมเมอร์ยุคปัจจุบัน λ-calculus อาจดูคล้ายชุดของฟังก์ชันซ้อนกันที่พบได้ในบางพาราไดม์ของ Lisp, Haskell, Python หรือ JavaScript
- นามธรรมของ λ-calculus เป็นรากฐานของ การเขียนโปรแกรมเชิงฟังก์ชัน ที่ปฏิบัติต่อฟังก์ชันในฐานะ first-class citizen
Entscheidungsproblem และขีดจำกัดของการคำนวณ
- Church ยังมีผลงานสำคัญในด้านอื่นของตรรกศาสตร์และปรัชญา โดยตัวอย่างเด่นคือผลงานเกี่ยวกับ Entscheidungsproblem
- Entscheidungsproblem คือปัญหาการตัดสินใจที่ David Hilbert ตั้งขึ้นในปี 1928 โดยถามว่ามีอัลกอริทึมแบบตัดสินได้แน่ชัดที่สามารถระบุความจริงหรือเท็จของข้อความทางคณิตศาสตร์ใด ๆ ได้หรือไม่
- Church ให้คำตอบเชิงปฏิเสธว่าอัลกอริทึมเช่นนั้นไม่มีอยู่ และผลลัพธ์นี้เป็นที่รู้จักในชื่อ Church's Theorem
- การค้นพบนี้ส่งอิทธิพลอย่างลึกซึ้งต่อทฤษฎีการตัดสินใจ และย้ำถึงขีดจำกัดของสิ่งที่การคำนวณเพียงอย่างเดียวจะทำได้
ศูนย์กลางทางปัญญาที่ Princeton และลูกศิษย์ของเขา
- Church เป็น เมนเทอร์ ที่ให้คำแนะนำแก่นักตรรกศาสตร์และนักวิทยาการคอมพิวเตอร์คนสำคัญหลายคนในยุคนั้น
- สายธารทางวิชาการของเขาครอบคลุม Stephen Kleene, J. Barkley Rosser และ Alan Turing
- Turing สำเร็จ Ph.D. ที่ Princeton ภายใต้การดูแลของ Church
- มีเรื่องเล่าว่า David Kaplan เคยแนะนำให้นักศึกษาบัณฑิตใหม่ไปนั่งเรียนคลาสของ Church โดยบอกว่าแม้จะไม่ใช่สาขาที่สนใจ ก็จะเป็นประสบการณ์ที่ได้เล่าให้หลานฟัง
- Princeton ในทศวรรษ 1930 เป็นศูนย์กลางทางปัญญาของพัฒนาการด้านตรรกะสมัยใหม่ โดยมี John von Neumann, Kurt Gödel และ Church อยู่ร่วมกัน
มรดกที่มองไม่ค่อยเห็น
- Church ไม่ได้มีชื่อเสียงในหมู่สาธารณชนระดับเดียวกับ Turing, von Neumann หรือ Gödel
- มรดกของเขาไม่ได้มาในรูปเรื่องเล่าฮีโร่การถอดรหัสช่วงสงครามหรือโศกนาฏกรรมจากการจากไปก่อนวัยอันควร ซึ่งมักดึงดูดจินตนาการของผู้คนได้ง่ายกว่า
- โปรแกรมหลายพันล้านตัวที่รันอยู่บนสมาร์ตโฟนสามารถสืบย้อนตรรกะของมันกลับไปถึง ฟังก์ชันเชิงนามธรรม ใน λ-calculus ได้
- ตั้งแต่แอปธรรมดาไปจนถึงปัญญาประดิษฐ์ DNA ที่มองไม่เห็นของการคำนวณต่างสืบทอดสายธารสำคัญมาจากงานของ Church
- ความอัจฉริยะของ Church ไม่ได้อยู่ที่ความหวือหวา แต่อยู่ในโครงสร้างอันเข้มงวดและความสง่างามอันเงียบงันที่เปลี่ยนโลก
1 ความคิดเห็น
ความคิดเห็นจาก Hacker News
ชอบเรื่อง ที่มาของชื่อ lambda ใน Paradigms of Artificial Intelligence Programming(PDF/EPUB: https://github.com/norvig/paip-lisp)
เรื่องเล่าว่า Alonzo Church นำเครื่องหมายคาเร็ตที่ Russell และ Whitehead ใช้เขียนไว้เหนือ bound variable ในสัญกรณ์ของ Principia Mathematica อย่าง
x̂(x + x)ย้ายมาไว้ข้างหน้าเป็น^x(x + x)เพื่อทำให้เป็นสตริงหนึ่งมิติ แล้วเพราะคาเร็ตว่าง ๆ ดูประหลาด จึงเปลี่ยนเป็นแลมบ์ดาตัวใหญ่Λx(x + x)ก่อนจะกลายเป็นตัวเล็กλx(x + x)เพื่อหลีกเลี่ยงความสับสนเนื้อหาบอกว่า John McCarthy เป็นลูกศิษย์ของ Church ที่ Princeton และตอนสร้าง Lisp ในปี 1958 เครื่อง keypunch สมัยนั้นไม่มีอักษรกรีก จึงใช้
(lambda (x) (+ x x))และมันก็อยู่มาจนถึงทุกวันนี้ดังนั้นอย่างที่เป็นหัวข้อของบทความนี้ Church จึงมักถูกกล่าวถึงบ่อยในบทความย้อนรำลึกถึง Lisp และอาจเป็นบุคคลที่ “ถูกลืม” เฉพาะสำหรับคนที่แทบไม่สนใจประวัติศาสตร์คอมพิวติงเท่านั้น
ตามที่ Dana Scott เล่า Church เองบอกว่าการเลือกนั้นเป็น การเลือกแบบสุ่ม ทำนอง “eeny, meeny, miny, moe” และยังว่าคำอธิบายแบบ Barendregt ก็ถูกโต้แย้งในบรรยายล่าสุดที่ University of Birmingham
ในโลกภาษาฝรั่งเศส “personne lambda” หมายถึงคนธรรมดาหรือคนนิรนาม จึงดูเข้ากับ anonymous function ได้ดี และคำคุณศัพท์ lambda ก็มีความหมายว่า “ทั่วไป/ธรรมดา” ด้วย จึงให้ความรู้สึกว่าอักษรที่อยู่แถวกลาง ๆ ของอักษรกรีกสื่อถึงสิ่งที่เป็นค่าเฉลี่ย
https://math.stackexchange.com/questions/64468/why-is-lambda...
ครอบคลุมหัวข้อการเขียนโปรแกรมหลายเรื่อง และยังเปิดให้เห็น paradigm ที่อาจไม่คุ้นสำหรับคนที่ไม่ค่อยได้สัมผัส functional programming
มีกรณีอื่นที่บ่งชี้ว่า Church เลือกจากอักษรกรีกแบบใกล้เคียงกับ การเลือกแบบสุ่ม มากกว่าจะมีความหมายเฉพาะ อยู่ที่ https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...
และอยากรู้ด้วยว่าเป็นก่อนหรือหลัง McCarthy เริ่มทำ Lisp
“lambda calculus ของ Church และ Turing machine มีพลังในการคำนวณเทียบเท่ากัน แต่ Turing machine ต่างตรงที่ใช้สถานะที่เปลี่ยนแปลงได้ จนถึงทุกวันนี้ ที่ยังมีรอยแยกระหว่างภาษา functional กับภาษา imperative ก็เพราะ การแยก Church ออกจาก state”
ผมรู้จักคำพูดนี้มานานแล้ว แต่หาแหล่งที่มาต้นฉบับไม่เจอ
แก้ไข: อาจมาจากคำพูดของ Guy Steele ที่ว่า “มีคนที่ไม่ต้องการผสมส่วนของภาษาที่เป็น functional/lambda calculus เข้ากับส่วนที่ก่อให้เกิด side effect พวกเขาดูเหมือนจะเชื่อใน separation of Church and state”
อาร์ไคฟ์ต้นฉบับอยู่ที่นี่: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
เป็นมุกที่ว่า ชาวยุโรปโดยมากออกเสียงชื่อเขาอย่างถูกต้องว่า “Nick-louse Veert” แต่ชาวอเมริกันทำเสียเป็น “Nickel's Worth”
กล่าวคือ ชาวยุโรปเรียกเขาด้วยชื่อ ส่วนชาวอเมริกันเรียกเขาด้วยมูลค่า
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
ถ้าอยากอ่านบทความที่น่าทึ่งจริง ๆ เกี่ยวกับ Church ขอแนะนำบันทึกความทรงจำของ Rota
เป็นส่วนแรกของ https://www34.homepage.villanova.edu/robert.jantzen/princeto...
ลิงก์ที่เกี่ยวข้องมี Alonzo Church, 92, Theorist of the Limits of Mathematics(1995) - https://news.ycombinator.com/item?id=12240815 - สิงหาคม 2016, Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - กุมภาพันธ์ 2015
ทั้งเล่มก็ควรค่าแก่การอ่าน
ภาษาโปรแกรม Alonzo ที่ตั้งชื่อตามเขาแทบจะถูกลืมไปแล้ว
https://dl.acm.org/doi/pdf/10.1145/68127.68139
โดยเฉพาะ ปรัชญาตรรกะ ที่สืบต่อจากงานของ Frege และ Russell รวมถึงทฤษฎีความหมาย/การอ้างอิง แทบถูกลืมไปเกือบหมด
Church ตีพิมพ์บทความเกี่ยวกับหัวข้อนี้ไว้มาก แต่ในที่อย่าง Wikipedia แทบไม่กล่าวถึงเลย
ถึงอย่างนั้น รายการใน Stanford Encyclopedia of Philosophy ก็ยังดีกว่าเล็กน้อย: https://plato.stanford.edu/entries/church/
เพียงแต่ได้ยินมาว่ามันก็ยังพลาดงานสำคัญบางส่วนของเขา และดูเหมือนจะเป็นปรัชญาเกินไปสำหรับนักคณิตศาสตร์ และเป็นเทคนิคเกินไปสำหรับนักปรัชญา
แม้จะไม่ใช่ประเด็นหลัก แต่ก็อยากให้ยับยั้งการใช้ ภาพประกอบที่สร้างโดย AI ในบล็อกโพสต์สักหน่อย
ภาพถ่ายจริงของ Church ก็มีอยู่ในสาธารณสมบัติด้วย แต่ภาพประกอบนี้ไม่ได้เหมือนเขาเป็นพิเศษ และเมื่อบทความเริ่มได้รับความนิยม มันก็ปรากฏในผลการค้นหารูปภาพแล้ว
ถ้าเป็นภาพประกอบที่แทบไม่คุ้มแม้แต่จะใช้เวลาสร้างเกิน 5 นาที ผมว่าตัดออกไปเลยน่าจะดีกว่า
แต่ถ้าจำเป็นต้องใช้ภาพที่สร้างด้วย “AI” จริง ๆ อย่างน้อยก็ควรใส่คำบรรยายกำกับไว้แบบนั้น
ผมไม่ค่อยสบายใจที่จะดึงรูปออนไลน์มาใช้ และภาพนี้เป็นผลลัพธ์ครั้งที่ 7 ที่ทำขึ้นเพื่อไม่ให้กลายเป็นหน้าตาคล้ายแบบ ‘ปลอม’ และผมก็รู้สึกว่ามันคล้ายอยู่พอสมควร
ภาพ JvN ทำออกมาได้ค่อนข้างดี แต่ต่อไปน่าจะเหมาะกว่าหากใช้ ภาพเชิงสัญลักษณ์ แทนหน้าตาคล้ายบุคคลแบบปลอม ๆ
คำว่า “สถาปนิกแห่งปัญญาคอมพิวเตอร์” ดูจะเกินไปหน่อย
Church เป็นนักตรรกศาสตร์ที่ยอดเยี่ยมก็จริง แต่ถ้าปัญญาคอมพิวเตอร์ในที่นี้หมายถึง AI/ML ผลงานของเขาแทบไม่มีเลย
อีกเรื่องคือผมก็ไม่แน่ใจว่า แลมบ์ดาแคลคูลัส เป็นคณิตศาสตร์จริง ๆ หรือไม่ มันดูใกล้เคียงกับสัญกรณ์อันชาญฉลาดมากกว่า
ข้อดีของสัญกรณ์เป็นเรื่องเชิงอัตวิสัย และก็น่าสนใจด้วยว่า Church เองไม่ได้สนใจนักที่ไอเดียของเขาไปเป็นแรงบันดาลใจให้การออกแบบภาษาโปรแกรมบางภาษา
STT มักถูกมองว่าเทียบเท่ากับตรรกะลำดับสูงด้วย เพราะสามารถแสดงวัตถุเชิงตรรกะใด ๆ ได้ด้วยชนิดตั้งต้นเพียงสองชนิด คือ “ปัจเจก” และค่าความจริง T/F รวมถึงชนิดฟังก์ชัน
(a --> b)STT เป็นสิ่งประดิษฐ์ของ Church อย่างชัดเจน และมีอิทธิพลอย่างมากต่อทฤษฎีชนิดสมัยใหม่ รวมถึงภาษาโปรแกรมที่มีระบบชนิดซับซ้อนอย่าง Haskell
แม้จะพิสูจน์ได้ไม่ครบถ้วน แต่ตามสัญชาตญาณแล้ว Turing และสิ่งที่เขาเป็นตัวแทน ดูเหมือนจะได้รับการยกย่องสูงในฝั่ง AI ในท้ายที่สุด ขณะที่ Church ดูเหมือนจะตรงกันข้าม
ฝ่ายแรกเริ่มจากความบริสุทธิ์ เงื่อนไขขั้นต่ำที่สุดที่เป็นไปได้ และการคำนวณเชิงนามธรรมที่ “บริสุทธิ์” ส่วนฝ่ายหลังดูเหมือนสนใจว่าเราคิดได้จริงอย่างไร และให้ความสำคัญกับ การขยายการแสดงออกและนามธรรม มากกว่าการนำไปใช้งานจริง
Church ไม่มีประสบการณ์ทำงานกับคอมพิวเตอร์จริง และใกล้เคียงกับฝ่ายที่ต้องการขยายตัวทฤษฎีคณิตศาสตร์เองมากกว่า
ความร่วมมือของทั้งสองและการสื่อสารข้ามมหาสมุทรแอตแลนติกช่วยผสานภาคปฏิบัติกับทฤษฎี ทำให้ทฤษฎีแกนกลางอย่างความเป็นคู่ระหว่าง imperative/functional, ทฤษฎีบท Church-Turing, ความสัมพันธ์ระหว่างปัญหาการหยุดกับทฤษฎีบทของ Church แข็งแรงขึ้น
การมองว่าเป็นการแข่งขันกันนั้นผิด และคำกล่าวว่าวิทยาการคอมพิวเตอร์มี “บิดาสองคน” ก็เหมาะสมด้วยหลายเหตุผล
โดยเฉพาะเมื่อคำนึงถึงการเสียชีวิตของ Turing ด้วย
อีกทั้งไม่ใช่ว่า Turing ไม่สนใจการนำไปใช้งานจริง และไม่ควรมองข้ามว่าเขาอยากกลับไปทำการใช้งานจริง แต่ไม่ได้รับอนุญาต
ยังเหลือโศกนาฏกรรมและคำถามใหญ่ไว้ว่าหากการจัดชั้นความลับของรัฐบาลอังกฤษต่างออกไป อะไรจะเปลี่ยนไปบ้าง แต่ถ้าเป็นเช่นนั้น เราก็อาจสูญเสียความร่วมมือกับ Church ที่ช่วยทำให้ทฤษฎีในเส้นเวลาของเรามั่นคงได้ดีขนาดนั้น
เป็นโชคดีที่ได้พบ Alonzo Church และ Haskell Curry ในงาน ACM Symposium on LISP and Functional Programming ที่ CMU เมื่อเดือนสิงหาคม 1982
Curry สุขภาพไม่ดีอย่างชัดเจน และเสียชีวิตราว 2 สัปดาห์หลังงานประชุม แต่ Church ดูแข็งแรง และมีชีวิตต่อมาอีกประมาณ 13 ปี
ตอนงานเลี้ยงรับรอง Gerry Sussman เดินไปรอบห้องเพื่อแนะนำทั้งสองคนด้วยความตื่นเต้นอย่างมาก และสำหรับพวกเรา การได้พบพวกเขาก็เป็นเรื่องน่าปลื้มใจอย่างยิ่ง
หนึ่งในผลงานสำคัญของ Church คือ ลูกศิษย์ ของเขา
มีนักคิดที่น่าทึ่งหลั่งไหลออกมาจากที่เดียวกัน