Deep Link การพิสูจน์คณิตศาสตร์และโปรแกรมคอมพิวเตอร์ | นิตยสารควอนต้า

การค้นพบทางวิทยาศาสตร์บางอย่างมีความสำคัญเพราะมันเผยให้เห็นสิ่งใหม่ๆ เช่น โครงสร้างเกลียวคู่ของ DNA หรือการมีอยู่ของหลุมดำ อย่างไรก็ตาม การเปิดเผยบางอย่างมีความลึกซึ้งเนื่องจากแสดงให้เห็นว่าแนวคิดเก่าสองแนวคิดซึ่งครั้งหนึ่งเคยคิดแตกต่างกัน แท้จริงแล้วคือสิ่งเดียวกัน ใช้สมการของเจมส์ เคลิร์ก แมกซ์เวลล์ที่แสดงว่าไฟฟ้าและแม่เหล็กเป็นสองลักษณะของปรากฏการณ์เดียว หรือการเชื่อมโยงของแรงโน้มถ่วงกับกาล-อวกาศที่เป็นเส้นโค้งของทฤษฎีสัมพัทธภาพทั่วไป

การติดต่อทางจดหมายของ Curry-Howard ทำเช่นเดียวกัน แต่ในขนาดที่ใหญ่ขึ้น ไม่เพียงเชื่อมโยงแนวคิดที่แยกจากกันภายในสาขาเดียว แต่ยังเชื่อมโยงสาขาวิชาทั้งหมด: วิทยาการคอมพิวเตอร์ และ ตรรกะทางคณิตศาสตร์. หรือที่รู้จักในชื่อ Curry-Howard isomorphism (คำที่มีความหมายว่ามีการติดต่อกันแบบหนึ่งต่อหนึ่งระหว่างสองสิ่ง) มันสร้างความเชื่อมโยงระหว่างการพิสูจน์ทางคณิตศาสตร์และโปรแกรมคอมพิวเตอร์

กล่าวง่ายๆ ก็คือ การติดต่อทางจดหมายของ Curry-Howard ระบุว่าแนวคิดสองประการจากวิทยาการคอมพิวเตอร์ (ประเภทและโปรแกรม) เทียบเท่ากับข้อเสนอและการพิสูจน์ตามลำดับ - แนวคิดจากตรรกะ

การขยายสาขาประการหนึ่งของการติดต่อสื่อสารนี้คือการเขียนโปรแกรมซึ่งมักถูกมองว่าเป็นงานฝีมือส่วนบุคคล ได้รับการยกระดับไปสู่ระดับทางคณิตศาสตร์ในอุดมคติ การเขียนโปรแกรมไม่ใช่แค่ "การเขียนโค้ด" เท่านั้น แต่ยังเป็นการพิสูจน์ทฤษฎีบทด้วย สิ่งนี้ทำให้การเขียนโปรแกรมเป็นระเบียบและมีวิธีให้เหตุผลทางคณิตศาสตร์เกี่ยวกับความถูกต้องของโปรแกรม

จดหมายโต้ตอบนี้ตั้งชื่อตามนักวิจัยสองคนที่ค้นพบมันโดยอิสระ ในปี 1934 นักคณิตศาสตร์และนักตรรกวิทยา Haskell Curry สังเกตเห็นความคล้ายคลึงกันระหว่างฟังก์ชันในคณิตศาสตร์และความสัมพันธ์โดยนัยในตรรกะ ซึ่งอยู่ในรูปแบบของประโยค "if-then" ระหว่างสองข้อเสนอ

แรงบันดาลใจจากการสังเกตของ Curry นักตรรกวิทยาทางคณิตศาสตร์ William Alvin Howard ค้นพบความเชื่อมโยงที่ลึกซึ้งยิ่งขึ้นระหว่างการคำนวณและตรรกะในปี 1969 โดยแสดงให้เห็นว่าการใช้โปรแกรมคอมพิวเตอร์นั้นเหมือนกับการทำให้การพิสูจน์เชิงตรรกะง่ายขึ้น เมื่อโปรแกรมคอมพิวเตอร์ทำงาน แต่ละบรรทัดจะถูก "ประเมิน" เพื่อให้ได้เอาต์พุตเดียว ในทำนองเดียวกัน ในการพิสูจน์ คุณเริ่มต้นด้วยข้อความที่ซับซ้อนซึ่งคุณสามารถลดความซับซ้อนได้ (เช่น โดยกำจัดขั้นตอนที่ซ้ำซ้อน หรือแทนที่นิพจน์ที่ซับซ้อนด้วยขั้นตอนที่ง่ายกว่า) จนกว่าคุณจะได้ข้อสรุป — ข้อความที่กระชับและกระชับมากขึ้นที่ได้มาจากข้อความชั่วคราวจำนวนมาก .

แม้ว่าคำอธิบายนี้จะสื่อความหมายทั่วไปของการโต้ตอบกัน แต่เพื่อให้เข้าใจอย่างถ่องแท้ เราจำเป็นต้องเรียนรู้เพิ่มเติมอีกเล็กน้อยเกี่ยวกับสิ่งที่นักวิทยาศาสตร์คอมพิวเตอร์เรียกว่า "ทฤษฎีประเภท"

เริ่มต้นด้วยความขัดแย้งที่มีชื่อเสียง: ในหมู่บ้านแห่งหนึ่งมีช่างตัดผมคนหนึ่งที่โกนผู้ชายทุกคนที่ไม่โกนตัวเองและมีเพียงพวกเขาเท่านั้น ช่างตัดผมโกนตัวเองหรือเปล่า? ถ้าคำตอบคือใช่ เขาต้องไม่โกนตัวเอง (เพราะเขาโกนเฉพาะผู้ชายที่ไม่โกนตัวเองเท่านั้น) ถ้าคำตอบคือไม่ เขาก็ต้องโกนตัวเอง (เพราะเขาโกนผู้ชายทุกคนที่ไม่โกนตัวเอง) นี่เป็นเวอร์ชันที่ไม่เป็นทางการของความขัดแย้งที่ Bertrand Russell ค้นพบขณะพยายามสร้างรากฐานของคณิตศาสตร์โดยใช้แนวคิดที่เรียกว่าเซต นั่นคือ เป็นไปไม่ได้ที่จะกำหนดชุดที่มีชุดทั้งหมดที่ไม่มีตัวเองอยู่โดยปราศจากความขัดแย้ง

เพื่อหลีกเลี่ยงความขัดแย้งนี้ รัสเซลแสดงให้เห็นว่า เราสามารถใช้ "ประเภท" ได้ โดยคร่าวแล้ว สิ่งเหล่านี้คือหมวดหมู่ที่มีค่าเฉพาะเรียกว่าอ็อบเจ็กต์ ตัวอย่างเช่น หากมีประเภทที่เรียกว่า “Nat” ซึ่งหมายถึงจำนวนธรรมชาติ วัตถุของประเภทนั้นจะเป็น 1, 2, 3 และอื่นๆ โดยทั่วไปนักวิจัยจะใช้เครื่องหมายทวิภาคเพื่อระบุประเภทของวัตถุ เลข 7 ที่เป็นประเภทจำนวนเต็มสามารถเขียนได้เป็น “7: Integer” คุณสามารถมีฟังก์ชันที่นำวัตถุประเภท A และแยกวัตถุประเภท B ออกมา หรือฟังก์ชันที่รวมวัตถุคู่หนึ่งที่เป็นประเภท A และประเภท B ให้เป็นประเภทใหม่ที่เรียกว่า “A × B”

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

ในโลกของทฤษฎีประเภท การพิสูจน์ว่าข้อความนั้นเป็นจริงอาจดูแตกต่างจากสิ่งที่เราคุ้นเคย หากเราต้องการพิสูจน์ว่าจำนวนเต็ม 8 เป็นเลขคู่ ก็ต้องแสดงว่า 8 เป็นวัตถุประเภทเฉพาะที่เรียกว่า "คู่" โดยที่กฎการเป็นสมาชิกจะหารด้วย 2 ลงตัว หลังจากตรวจสอบแล้วว่า 8 หารลงตัว เมื่อ 2 เราสามารถสรุปได้ว่า 8 นั้นเป็น "ผู้อยู่อาศัย" ประเภทคู่อย่างแน่นอน

Curry และ Howard แสดงให้เห็นว่าประเภทต่างๆ มีพื้นฐานเทียบเท่ากับข้อเสนอเชิงตรรกะ เมื่อฟังก์ชัน “อยู่ใน” ประเภทหนึ่ง — นั่นคือเมื่อคุณสามารถกำหนดฟังก์ชันที่เป็นวัตถุประเภทนั้นได้สำเร็จ — คุณกำลังแสดงให้เห็นอย่างมีประสิทธิภาพว่าประพจน์ที่เกี่ยวข้องนั้นเป็นจริง ดังนั้นฟังก์ชันที่รับอินพุตประเภท A และให้เอาต์พุตประเภท B ซึ่งแสดงเป็นประเภท A → B จะต้องสอดคล้องกับความหมายโดยนัย: “ถ้า A แล้ว B” ตัวอย่างเช่น ลองสมมุติฐานว่า “ถ้าฝนตก พื้นดินก็จะเปียก” ในทฤษฎีประเภท ข้อเสนอนี้จะถูกจำลองโดยฟังก์ชันที่มีประเภท “Raining → GroundIsWet” สูตรที่ดูแตกต่างในความเป็นจริงแล้วมีความเหมือนกันทางคณิตศาสตร์

แม้ว่าความเชื่อมโยงดังกล่าวอาจดูเป็นนามธรรม แต่การเชื่อมโยงดังกล่าวไม่เพียงแต่เปลี่ยนวิธีที่ผู้ปฏิบัติงานด้านคณิตศาสตร์และวิทยาการคอมพิวเตอร์คิดเกี่ยวกับงานของพวกเขาเท่านั้น แต่ยังนำไปสู่การประยุกต์ใช้ในทางปฏิบัติหลายอย่างในทั้งสองสาขาอีกด้วย สำหรับวิทยาการคอมพิวเตอร์ เป็นรากฐานทางทฤษฎีสำหรับการตรวจสอบซอฟต์แวร์ ซึ่งเป็นกระบวนการรับรองความถูกต้องของซอฟต์แวร์ ด้วยการวางกรอบพฤติกรรมที่ต้องการในแง่ของข้อเสนอเชิงตรรกะ โปรแกรมเมอร์สามารถพิสูจน์ทางคณิตศาสตร์ได้ว่าโปรแกรมมีพฤติกรรมตามที่คาดไว้ นอกจากนี้ยังเป็นรากฐานทางทฤษฎีที่แข็งแกร่งสำหรับการออกแบบภาษาโปรแกรมเชิงฟังก์ชันที่มีประสิทธิภาพยิ่งขึ้น

และสำหรับวิชาคณิตศาสตร์นั้นการติดต่อสื่อสารได้นำไปสู่การกำเนิดของ ผู้ช่วยพิสูจน์หรือเรียกอีกอย่างว่าผู้พิสูจน์ทฤษฎีบทเชิงโต้ตอบ เหล่านี้คือเครื่องมือซอฟต์แวร์ที่ช่วยในการสร้างการพิสูจน์ที่เป็นทางการ เช่น Coq และ Lean ใน Coq แต่ละขั้นตอนของการพิสูจน์โดยพื้นฐานแล้วคือโปรแกรม และความถูกต้องของหลักฐานจะถูกตรวจสอบด้วยอัลกอริธึมการตรวจสอบประเภท นักคณิตศาสตร์ยังใช้เครื่องช่วยพิสูจน์ด้วย โดยเฉพาะอย่างยิ่ง ผู้พิสูจน์ทฤษฎีบทแบบลีน — เพื่อทำให้คณิตศาสตร์เป็นระเบียบ ซึ่งเกี่ยวข้องกับการนำเสนอแนวคิดทางคณิตศาสตร์ ทฤษฎีบท และการพิสูจน์ในรูปแบบที่เข้มงวดและสามารถตรวจสอบได้ด้วยคอมพิวเตอร์ ซึ่งช่วยให้คอมพิวเตอร์สามารถตรวจสอบภาษาที่ไม่เป็นทางการของคณิตศาสตร์ได้

นักวิจัยยังคงสำรวจผลที่ตามมาจากความเชื่อมโยงระหว่างคณิตศาสตร์และการเขียนโปรแกรม การติดต่อโต้ตอบแบบฉบับของเคอร์รี-ฮาวเวิร์ดผสมผสานการเขียนโปรแกรมด้วยตรรกะประเภทหนึ่งที่เรียกว่าตรรกะสัญชาตญาณ แต่กลับกลายเป็นว่ามีตรรกะประเภทอื่นๆ มากขึ้นที่สามารถคล้อยตามการรวมเข้าด้วยกันดังกล่าวได้เช่นกัน

“สิ่งที่เกิดขึ้นในศตวรรษนับตั้งแต่ความเข้าใจอย่างลึกซึ้งของ Curry ก็คือเราค้นพบกรณีต่างๆ มากขึ้นเรื่อยๆ ที่ 'ระบบลอจิคัล X สอดคล้องกับระบบคำนวณ Y'” กล่าว ไมเคิลคลาร์กสันนักวิทยาศาสตร์คอมพิวเตอร์ที่ Cornell University นักวิจัยได้เชื่อมโยงการเขียนโปรแกรมเข้ากับตรรกะประเภทอื่นๆ เช่น ตรรกะเชิงเส้น ซึ่งรวมถึงแนวคิดเรื่อง "ทรัพยากร" และตรรกะโมดอล ซึ่งเกี่ยวข้องกับแนวคิดเกี่ยวกับความเป็นไปได้และความจำเป็น

และแม้ว่าจดหมายฉบับนี้จะมีชื่อของ Curry และ Howard แต่พวกเขาไม่ได้เป็นเพียงคนเดียวที่ค้นพบมัน สิ่งนี้พิสูจน์ถึงลักษณะพื้นฐานของการติดต่อสื่อสาร: ผู้คนสังเกตเห็นมันครั้งแล้วครั้งเล่า “ดูเหมือนจะไม่ใช่เรื่องบังเอิญที่มีการเชื่อมโยงอย่างลึกซึ้งระหว่างการคำนวณและตรรกะ” คลาร์กสันกล่าว