12 · Types and Proofs
12 · ชนิดกับบทพิสูจน์
Fourth hearing of Part II. The last three chapters asked what computation can do, how long it takes, and what it moves; this one asks what happens to the oldest philosophical prize — certainty — once proof itself becomes a checkable artifact.
บทนี้ถามว่าเกิดอะไรขึ้นกับรางวัลเชิงปรัชญาที่เก่าแก่ที่สุด — ความแน่นอน — เมื่อบทพิสูจน์เองกลายเป็นสิ่งประดิษฐ์ที่ตรวจสอบได้ นี่คือการไต่สวนครั้งที่สี่ของภาค II สามบทก่อนหน้าถามว่าการคำนวณทำอะไรได้ ใช้เวลานานแค่ไหน และเคลื่อนอะไร
What happens to certainty when proof becomes an artifact?
ความแน่นอนจะเหลืออะไร เมื่อบทพิสูจน์กลายเป็นสิ่งประดิษฐ์
In 1976 Kenneth Appel and Wolfgang Haken proved the four-color theorem with the help of a computer program that checked close to fifteen hundred map configurations no human being would ever survey by hand — chapter 03 already sat with the shock that verdict caused: a proof too long for any mathematician to read start to finish. Nearly thirty years later Georges Gonthier closed a different case about the same theorem. His formalization, completed in the Coq proof assistant and published as "Formal Proof — The Four-Color Theorem" (Notices of the American Mathematical Society 55, 2008: 1382–1393), did not merely rerun Appel and Haken's argument; it re-derived the whole proof, combinatorics and case-checking alike, as a sequence of steps validated by a small trusted kernel that a single person can, in principle, audit line by line. The theorem that once symbolized proof outrunning human comprehension became, in Gonthier's hands, the theorem that showed comprehension could be replaced by something more exacting than any human reader: a machine that does not skim.
ปี 1976 ทฤษฎีบทสี่สี (four-color theorem) ถูกพิสูจน์ด้วยโปรแกรมคอมพิวเตอร์ที่ไล่ตรวจการจัดวางแผนที่เกือบหนึ่งพันห้าร้อยแบบ จำนวนที่ไม่มีมนุษย์คนไหนไล่ด้วยมือไหว คนพิสูจน์คือ Kenneth Appel และ Wolfgang Haken บทที่ 03 นั่งอยู่กับแรงสั่นสะเทือนของคำตัดสินนั้นมาแล้ว: บทพิสูจน์ที่ยาวเกินกว่านักคณิตศาสตร์คนใดจะอ่านจบตั้งแต่ต้นจนจบ เกือบสามสิบปีต่อมา Georges Gonthier ปิดอีกคดีหนึ่งของทฤษฎีบทเดียวกัน การทำให้เป็นรูปนัย (formalization) ของเขา เสร็จใน proof assistant ชื่อ Coq และตีพิมพ์เป็น "Formal Proof — The Four-Color Theorem" (Notices of the American Mathematical Society 55, 2008: 1382–1393) ไม่ได้รันข้อโต้แย้งของ Appel กับ Haken ซ้ำเฉยๆ มันสร้างบทพิสูจน์ทั้งชิ้นขึ้นใหม่ ทั้ง combinatorics และการไล่ตรวจกรณี ให้เป็นลำดับขั้นตอนที่ kernel (แกนตรวจสอบ) เล็กๆ ที่ไว้ใจได้รับรองความถูกต้อง และคนคนเดียวตรวจได้ทีละบรรทัดในหลักการ ทฤษฎีบทที่เคยเป็นสัญลักษณ์ของบทพิสูจน์ที่วิ่งพ้นความเข้าใจของมนุษย์ กลายมาเป็นทฤษฎีบท ในมือของ Gonthier ที่แสดงว่าความเข้าใจถูกแทนที่ได้ด้วยบางอย่างที่เข้มงวดกว่าผู้อ่านมนุษย์คนใด: เครื่องจักรที่ไม่อ่านผ่านๆ
What makes Gonthier's kernel trustworthy is a correspondence discovered, not designed, twice over. Haskell Curry noticed in 1934 that the types assigned to combinators in combinatory logic could be read as axiom schemes of intuitionistic implicational logic, and in 1958 that a fragment of Hilbert-style proof systems coincided with a fragment of typed combinatory logic. William Howard made the analogy exact three decades later without knowing Curry's full history, circulating a manuscript in 1969 that was finally published as "The Formulae-as-Types Notion of Construction" in a 1980 festschrift for Curry edited by Jonathan Seldin and J. Roger Hindley. Howard showed that a proof, written in the natural-deduction style Gerhard Gentzen had introduced in 1935, and a program, written in the simply typed lambda calculus, are the same object viewed from two directions: a proposition is a type, a proof of it is a program of that type, and simplifying a proof — removing a detour — is executing the program. N. G. de Bruijn arrived at a version of the same idea independently at almost the same time, building it into his Automath system before either he or Howard knew of the other's work. Three researchers, working from logic, from combinators, and from an automated proof-checker, kept finding the identical seam — the strongest kind of evidence this book has for its own claim that philosophy and computing are one project rediscovered rather than two projects borrowed from each other.
สิ่งที่ทำให้ kernel ของ Gonthier ไว้ใจได้คือความสอดคล้อง (correspondence) ที่ถูกค้นพบ ไม่ใช่ถูกออกแบบ และค้นพบซ้ำถึงสองรอบ Haskell Curry สังเกตในปี 1934 ว่าชนิด (type) ที่กำกับ combinator ในตรรกะเชิงการจัด (combinatory logic) อ่านได้ในฐานะ axiom scheme ของตรรกะเชิงเงื่อนไขแบบสัญชานนิยม (intuitionistic) และในปี 1958 ว่าส่วนหนึ่งของระบบพิสูจน์แบบ Hilbert ตรงกับส่วนหนึ่งของตรรกะเชิงการจัดที่มีชนิดกำกับ สามทศวรรษถัดมา William Howard ทำการเทียบเคียงนั้นให้แม่นยำ โดยไม่รู้ประวัติทั้งหมดของ Curry เขาส่งต้นฉบับเวียนอ่านในปี 1969 และมันได้ตีพิมพ์ในที่สุดเป็น "The Formulae-as-Types Notion of Construction" ใน festschrift ปี 1980 ที่ทำขึ้นให้ Curry โดยมี Jonathan Seldin และ J. Roger Hindley เป็นบรรณาธิการ Howard แสดงว่าบทพิสูจน์ที่เขียนในสไตล์การนิรนัยธรรมชาติ (natural deduction) ที่ Gerhard Gentzen เสนอไว้ในปี 1935 กับโปรแกรมที่เขียนในแคลคูลัสแลมบ์ดาที่มีชนิดอย่างง่าย (simply typed lambda calculus) คือวัตถุชิ้นเดียวกันที่มองจากคนละด้าน: ประพจน์คือชนิด บทพิสูจน์ของประพจน์คือโปรแกรมของชนิดนั้น และการลดรูปบทพิสูจน์ — ตัดทางอ้อมทิ้ง — คือการรันโปรแกรม N. G. de Bruijn คิดไอเดียรุ่นเดียวกันนี้ขึ้นเองในเวลาไล่เลี่ยกันแทบพอดี และวางมันลงในระบบ Automath ของเขา ก่อนที่เขากับ Howard จะรู้ว่าอีกฝ่ายทำเรื่องเดียวกันอยู่ นักวิจัยสามคน คนหนึ่งมาจากตรรกศาสตร์ คนหนึ่งมาจาก combinator คนหนึ่งมาจากตัวตรวจสอบบทพิสูจน์อัตโนมัติ ต่างเจอรอยต่อเดียวกันครั้งแล้วครั้งเล่า — หลักฐานที่หนักที่สุดที่หนังสือเล่มนี้มี สำหรับข้อกล่าวอ้างของมันเองว่าปรัชญากับการคำนวณคือโครงการเดียวที่ถูกค้นพบซ้ำ ไม่ใช่สองโครงการที่ยืมของกัน
The correspondence gave a century-old heresy its revenge. L. E. J. Brouwer's 1908 paper "The Unreliability of the Logical Principles" rejected the law of excluded middle — the claim that every statement is either true or false — for mathematics whose objects are mental constructions rather than mind-independent facts, building on the intuitionistic program he had opened in his 1907 dissertation. For most of the twentieth century this looked like a minority taste, a scruple most working mathematicians could safely ignore. Curry–Howard explains why it stopped being optional inside a proof assistant: a constructive proof that something exists must, under the correspondence, be a program that builds the thing, while a classical proof by contradiction — assume no such object exists, derive a contradiction, conclude one does — corresponds to no program at all, because it never says how to build anything. Coq, Agda, and Lean are, at their foundations, implementations of intuitionistic type theory not out of philosophical loyalty to Brouwer but because only the constructive fragment hands back code you can run. Intuitionism became load-bearing engineering exactly at the point where it stopped being asked to defend itself philosophically.
ความสอดคล้องนี้คือการแก้แค้นของความนอกรีตที่มีอายุนับศตวรรษ บทความปี 1908 ของ L. E. J. Brouwer เรื่อง "The Unreliability of the Logical Principles" ปฏิเสธกฎแห่งไตรวินิจฉัย (law of excluded middle) — ข้อกล่าวอ้างที่ว่าทุกประพจน์เป็นจริงหรือเท็จอย่างใดอย่างหนึ่งเสมอ — สำหรับคณิตศาสตร์ที่วัตถุของมันเป็นสิ่งสร้างทางจิต ไม่ใช่ข้อเท็จจริงที่เป็นอิสระจากจิต ต่อยอดจากโครงการสัญชานนิยม (intuitionism) ที่เขาเปิดไว้ในวิทยานิพนธ์ปี 1907 ตลอดศตวรรษที่ 20 เกือบทั้งศตวรรษ ข้อปฏิเสธนี้ดูเหมือนรสนิยมของคนกลุ่มน้อย เป็นความลังเลใจที่นักคณิตศาสตร์ผู้ทำงานจริงมองข้ามได้อย่างปลอดภัย Curry–Howard อธิบายว่าทำไมมันเลิกเป็นทางเลือกในโลกของ proof assistant: บทพิสูจน์เชิงสร้าง (constructive proof) ที่ว่าบางสิ่งมีอยู่ ภายใต้ความสอดคล้องนี้ ต้องเป็นโปรแกรมที่สร้างสิ่งนั้นออกมา ส่วนบทพิสูจน์เชิงคลาสสิก (classical proof) แบบพิสูจน์โดยข้อขัดแย้ง — สมมติว่าไม่มีวัตถุนั้นอยู่ อนุมานความขัดแย้ง สรุปว่ามันมีอยู่ — ไม่ตรงกับโปรแกรมใดเลย เพราะมันไม่บอกวิธีสร้างอะไรสักอย่าง Coq, Agda และ Lean ที่รากฐานคือการสร้าง (implementation) ของทฤษฎีชนิดสัญชานนิยม (intuitionistic type theory) ไม่ใช่เพราะภักดีทางปรัชญาต่อ Brouwer แต่เพราะมีแต่ส่วนเชิงสร้างเท่านั้นที่คืนโค้ดที่รันได้กลับมาให้ สัญชานนิยมกลายเป็นวิศวกรรมที่แบกน้ำหนักจริง พอดีตรงจุดที่มันเลิกถูกขอให้ปกป้องตัวเองเชิงปรัชญา
Once that machinery existed, mathematics started handing it its hardest, longest proofs. Thomas Hales completed a proof of the Kepler conjecture — that no packing of equal spheres is denser than the familiar grocer's stack — in 1998, but the 250-page argument, part conventional and part computer-assisted, took twelve referees four years and left them only 99 percent confident it was correct. Hales responded in 2003 by launching the Flyspeck project to re-derive every step inside HOL Light and Isabelle; the formalization was completed in 2014, checked and independently rechecked that year, and published as "A Formal Proof of the Kepler Conjecture" (Forum of Mathematics, Pi, 2017). Flyspeck's tens of thousands of lemmas rest on a kernel small enough for a handful of people to inspect completely, in place of twelve referees who could only sample a proof too long to read whole. Lean's mathlib, a continuously growing, community-verified library built on the same foundations, now formalizes results across the whole of mathematics as they are proved, turning "has this been checked" into a question with a machine-checkable answer rather than a matter of reputation.
พอกลไกนั้นมีอยู่ คณิตศาสตร์ก็ยื่นบทพิสูจน์ที่ยากที่สุดและยาวที่สุดของตัวเองให้มันตรวจ Thomas Hales พิสูจน์ข้อคาดการณ์ของ Kepler (Kepler conjecture) สำเร็จในปี 1998 ว่าไม่มีวิธีอัดทรงกลมขนาดเท่ากันแบบใดแน่นไปกว่ากองผลไม้ที่พ่อค้าเรียงไว้ แต่ข้อโต้แย้ง 250 หน้านั้นเป็นแบบดั้งเดิมครึ่งหนึ่ง ใช้คอมพิวเตอร์ช่วยอีกครึ่งหนึ่ง กินเวลาผู้ตรวจทานสิบสองคนไปสี่ปี และจบลงที่ความมั่นใจเพียง 99 เปอร์เซ็นต์ว่าถูกต้อง Hales ตอบด้วยการเปิดโครงการ Flyspeck ในปี 2003 เพื่อสร้างทุกขั้นตอนขึ้นใหม่ภายใน HOL Light และ Isabelle งานรูปนัยเสร็จในปี 2014 ตรวจสอบและตรวจซ้ำโดยอิสระในปีเดียวกัน ตีพิมพ์เป็น "A Formal Proof of the Kepler Conjecture" (Forum of Mathematics, Pi, 2017) บทตั้ง (lemma) หลายหมื่นข้อของ Flyspeck วางอยู่บน kernel ที่เล็กพอให้คนหยิบมือเดียวตรวจได้ครบทุกบรรทัด แทนผู้ตรวจทานสิบสองคนที่สุ่มอ่านได้เพียงบางส่วนของบทพิสูจน์ที่ยาวเกินกว่าจะอ่านจบ mathlib ของ Lean คลังที่โตขึ้นทุกวันและชุมชนช่วยกันตรวจ ยืนบนรากฐานเดียวกัน วันนี้มันทำผลลัพธ์ทั่วทั้งคณิตศาสตร์ให้เป็นรูปนัยไปพร้อมกับที่ผลลัพธ์เหล่านั้นถูกพิสูจน์ "เรื่องนี้ถูกตรวจสอบแล้วหรือยัง" จึงเลิกเป็นเรื่องของชื่อเสียง และกลายเป็นคำถามที่เครื่องจักรตอบได้
Vladimir Voevodsky pushed the foundations themselves one step further. Homotopy Type Theory: Univalent Foundations of Mathematics — the collective volume written by the Institute for Advanced Study program he led, published in 2013 — proposed reading types not as bare sets but as spaces, and proofs of equality between elements as paths between points — under Voevodsky's univalence axiom, structures that are isomorphic can be treated as identical, which gives mathematics's oldest and most abused word, "equal," a precise, checkable meaning it had never quite had before.
Vladimir Voevodsky ดันตัวรากฐานเองไปอีกขั้น Homotopy Type Theory: Univalent Foundations of Mathematics เล่มรวมที่เขียนโดยโปรแกรมของ Institute for Advanced Study ที่เขาเป็นผู้นำ ตีพิมพ์ปี 2013 เสนอให้อ่านชนิด (type) ไม่ใช่เซตเปล่าๆ แต่เป็นปริภูมิ (space) และอ่านบทพิสูจน์ความเท่ากันระหว่างสมาชิกเป็นเส้นทางระหว่างจุด ภายใต้สัจพจน์เอกค่า (univalence axiom) ของ Voevodsky โครงสร้างที่ isomorphic กันถือเป็นสิ่งเดียวกันได้ คำว่า "เท่ากัน" คำที่เก่าแก่ที่สุดและถูกใช้ผิดหนักที่สุดในคณิตศาสตร์ จึงได้ความหมายที่แม่นยำและตรวจสอบได้ ความหมายที่มันไม่เคยมีจริงๆ มาก่อน
None of this delivers the certainty Hilbert wanted in 1930. A proof assistant's guarantee is only as strong as its kernel, and the kernel rests on a compiler, which rests on hardware, which can fail — the same regress Wittgenstein pressed against any rule that claims to interpret itself, and the same one chapter 03 raised as a Gettier problem for sensors and pipelines. What Curry–Howard delivers instead is certainty re-engineered as a budget: instead of trusting a 250-page argument and twelve tired referees, trust a kernel of a few thousand lines, state exactly what would have to fail for the proof to be wrong, and let that be the whole of the remaining doubt. Philosophy wanted proof to end an argument once and for all; computation's counteroffer is a proof that tells you precisely how small the argument left over actually is.
ไม่มีอะไรในนี้ส่งมอบความแน่นอนแบบที่ Hilbert ต้องการในปี 1930 การรับประกันของ proof assistant แข็งแรงเท่า kernel ของมันเท่านั้น kernel วางอยู่บนคอมไพเลอร์ คอมไพเลอร์วางอยู่บนฮาร์ดแวร์ และฮาร์ดแวร์พังได้ — การถอยกลับไม่รู้จบ (regress) อันเดียวกับที่ Wittgenstein กดดันกฎใดๆ ที่อ้างว่าตีความตัวเองได้ และอันเดียวกับที่บทที่ 03 ยกขึ้นมาเป็นปัญหาเก็ตติเยร์ (Gettier problem) ของเซนเซอร์และไปป์ไลน์ สิ่งที่ Curry–Howard ส่งมอบให้แทนคือความแน่นอนที่ถูกออกแบบใหม่เป็นงบประมาณ: แทนที่จะไว้ใจข้อโต้แย้ง 250 หน้ากับผู้ตรวจทานที่เหนื่อยล้าสิบสองคน ให้ไว้ใจ kernel ไม่กี่พันบรรทัด ระบุให้ชัดว่าอะไรต้องพังบทพิสูจน์จึงจะผิด แล้วให้เท่านั้นเป็นความสงสัยที่เหลืออยู่ทั้งหมด ปรัชญาอยากให้บทพิสูจน์ปิดข้อโต้แย้งเด็ดขาดครั้งเดียวจบ ข้อเสนอโต้กลับของการคำนวณคือบทพิสูจน์ที่บอกได้แม่นยำว่าข้อโต้แย้งที่เหลือนั้นเล็กแค่ไหน
Connections
เชื่อมโยง
Chapter 01 introduces Curry–Howard as the logic chapter's treaty between the two disciplines; this chapter completes it. Chapter 03 is where the four-color theorem first caused its epistemological shock — this chapter is its answer. Chapter 09 supplies the incompleteness results that proof assistants must live inside rather than escape. Chapter 11's Kolmogorov complexity measures the length of a proof the way this chapter measures its trustworthiness.
บทที่ 01 แนะนำความสอดคล้อง Curry–Howard (Curry–Howard correspondence) ในฐานะสนธิสัญญาระหว่างสองสาขาวิชาของบทตรรกศาสตร์ บทนี้ทำให้มันครบ บทที่ 03 คือจุดที่ทฤษฎีบทสี่สีก่อแรงสั่นสะเทือนเชิงญาณวิทยาครั้งแรก บทนี้คือคำตอบ บทที่ 09 ให้ผลลัพธ์เรื่องความไม่สมบูรณ์ที่ proof assistant ต้องอยู่ข้างใน ไม่ใช่หนีพ้น Kolmogorov complexity ในบทที่ 11 วัดความยาวของบทพิสูจน์ แบบเดียวกับที่บทนี้วัดความน่าเชื่อถือของมัน
Open questions
คำถามที่ยังเปิดอยู่
If a kernel can be made small enough for one person to audit, has the regress of trusting the verifier actually been stopped, or only shortened to a link short enough to overlook? Does univalence settle what "the same structure" means in mathematics generally, or only inside type theory's own house? And now that Lean's mathlib checks new results as they are proved, does mathematical knowledge still need the human community of referees at all, or only the community that decides which theorems are worth proving in the first place?
ถ้า kernel เล็กพอให้คนคนเดียวตรวจได้ การถอยกลับไม่รู้จบของการไว้ใจตัวตรวจสอบหยุดลงจริงหรือ หรือแค่ถูกย่อจนเหลือจุดเชื่อมที่สั้นพอจะมองข้าม สัจพจน์เอกค่า (univalence) ยุติความหมายของ "โครงสร้างเดียวกัน" ให้คณิตศาสตร์ทั้งวงการ หรือยุติได้แค่ในบ้านของทฤษฎีชนิดเอง และตอนนี้ที่ mathlib ของ Lean ตรวจผลลัพธ์ใหม่ไปพร้อมกับที่มันถูกพิสูจน์ ความรู้ทางคณิตศาสตร์ยังต้องการชุมชนมนุษย์ของผู้ตรวจทานอยู่หรือไม่ หรือต้องการแค่ชุมชนที่ตัดสินว่าทฤษฎีบทไหนคุ้มค่าแก่การพิสูจน์ตั้งแต่แรก
Go deeper
อ่านต่อ
- Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7 (Cambridge: Cambridge University Press, 1989) — free edition at paultaylor.eu/stable/prot.pdf.
- William Howard, "The Formulae-as-Types Notion of Construction," in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, ed. J. P. Seldin and J. R. Hindley (New York: Academic Press, 1980), 479–490; Georges Gonthier, "Formal Proof — The Four-Color Theorem," Notices of the American Mathematical Society 55 (2008): 1382–1393 — ams.org/notices/200811/tx081101382p.pdf.
- Stanford Encyclopedia of Philosophy, "Intuitionism in the Philosophy of Mathematics" — plato.stanford.edu/entries/intuitionism.
- Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7 (Cambridge: Cambridge University Press, 1989) — free edition at paultaylor.eu/stable/prot.pdf.
- William Howard, "The Formulae-as-Types Notion of Construction," in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, ed. J. P. Seldin and J. R. Hindley (New York: Academic Press, 1980), 479–490; Georges Gonthier, "Formal Proof — The Four-Color Theorem," Notices of the American Mathematical Society 55 (2008): 1382–1393 — ams.org/notices/200811/tx081101382p.pdf.
- Stanford Encyclopedia of Philosophy, "Intuitionism in the Philosophy of Mathematics" — plato.stanford.edu/entries/intuitionism.