05 · ปรัชญาภาษา
การไต่สวนครั้งที่ 5 ในภาค I ศาลปรัชญา — ปรัชญาถามเครื่องจักรตรงๆ ว่าโค้ดของมัน และคำพูดของเราเอง แปลว่าอะไรกันแน่
โค้ดมีความหมายได้อย่างไร — แล้วเราล่ะ
ทุกการเรียกใช้ตรงกับทุกกฎเป๊ะ และไม่มีสิ่งใดที่ผู้โจมตีทำละเมิดโค้ดของสัญญาแม้แต่บรรทัดเดียว วันที่ 17 มิถุนายน 2016 ผู้โจมตีนิรนามคนหนึ่งเรียกฟังก์ชันชื่อ splitDAO ใน The DAO กองทุนลงทุนแบบกระจายศูนย์ที่ระดมอีเธอร์ได้กว่า 150 ล้านดอลลาร์จากผู้ร่วมลงทุนหลายพันคนในฤดูใบไม้ผลิปีนั้น ฟังก์ชันนี้มีไว้ให้สมาชิกถอนส่วนแบ่งของตัวเอง เสร็จแล้วจึงแก้บันทึกภายในของกองทุน แต่มันแก้บันทึก หลังจาก ส่งเงินออกไป ไม่ใช่ก่อน ผู้โจมตีจึงเรียกฟังก์ชันเดิมซ้ำจากในธุรกรรมเดียวกัน ตอนที่ยอดคงเหลือยังไม่ขยับ และเรียกซ้ำวนเป็นลูปเรียกตัวเอง (recursive loop) ถี่ยิบ กว่าลูปจะหยุด อีเธอร์ราว 3.6 ล้านหน่วย — ราว 50 ล้านดอลลาร์ตามรายงานวันนั้น — ไหลเข้าบัญชีที่ผู้โจมตีคุมอยู่ (Chainlink, "Reentrancy Attacks and The DAO Hack Explained")
ทั้งสองฝ่ายมองไบต์ชุดเดียวกันเป๊ะๆ ของซอร์สโค้ด แล้วอ่านความหมายไม่ตรงกัน ชุมชน Ethereum แตกเป็นสองฝ่ายทันทีเรื่องสิ่งที่เพิ่งเกิดขึ้น ฝ่ายแรกยกคำขวัญของขบวนการเองขึ้นมา — "โค้ดคือกฎหมาย (code is law)" — เงื่อนไขของสัญญาคือสิ่งที่ bytecode ของมันสั่งทำงาน เท่านั้น ธุรกรรมที่เดินตามโค้ดตรงตัวย่อมไม่ใช่การขโมย ต่อให้อ่านความมุ่งหมายของกองทุนเป็นภาษาอังกฤษธรรมดาแล้วได้คำตอบตรงข้ามก็ตาม ฝ่ายที่สองถือว่าสัญญามีความมุ่งหมายอยู่เหนือตัวอักษร วันที่ 20 กรกฎาคม 2016 ที่บล็อกที่ 1,920,000 เสียงข้างมากฟอร์กบล็อกเชน Ethereum ทั้งสายเพื่อพลิกการขโมยนั้นกลับ ฝ่ายข้างน้อยที่ยืนกรานอยู่กับสายเดิมกลายเป็น Ethereum Classic (The Block, "The DAO Hack at 10")
ข้อขัดแย้งนั้นคือคำถามเก่าแก่ที่สุดของปรัชญาภาษา เดินผ่านด่านศุลกากรมาพร้อมป้ายส่งของที่เขียนว่าวิทยาการคอมพิวเตอร์ (computer science) ห้าสิบห้าปีก่อนหน้านั้น Ludwig Wittgenstein ตั้งชื่อกับดักที่รอใครก็ตามที่เชื่อว่ากฎที่เขียนไว้ตัดสินการใช้งานของตัวเองได้ไว้แล้ว — "นี่คือปฏิทรรศน์ของเรา ไม่มีแนวทางปฏิบัติใดที่กฎจะกำหนดได้ เพราะแนวทางปฏิบัติใดก็ตามก็ทำให้ดูสอดคล้องกับกฎได้เสมอ" ("This was our paradox: no course of action could be determined by a rule, because any course of action can be made out to accord with the rule") (Philosophical Investigations §201, 1953) Saul Kripke อ่านข้อความนี้แล้วลับให้คมขึ้นเป็นข้อท้าทายเชิงสงสัยนิยม — ไม่มีอะไรในตัวบทของกฎ และไม่มีอะไรในการฝึกฝนที่ผ่านมาของคุณกับมัน บังคับทางตรรกะให้เลือกความต่อเนื่องแบบหนึ่งเหนืออีกแบบ จากความเป็นไปได้นับไม่ถ้วนที่ "สอดคล้อง (accord)" กับกฎเท่าๆ กัน (Kripke, Wittgenstein on Rules and Private Language, 1982) วงการคอมพิวเตอร์สร้างสาขาวิชาขึ้นมาทั้งสาขา คือความหมายเชิงรูปนัย (formal semantics) บนการพนันว่าโค้ดคือที่แห่งเดียวที่ปิดปัญหานี้ได้จริง The DAO คือวันที่การพนันนั้นถึงกำหนดจ่าย ลูปการเรียกซ้ำเข้าไปใหม่ (reentrancy) สอดคล้องกับกฎตามตัวอักษรของสัญญาอย่างสมบูรณ์ ส่วนคำถามว่ามันละเมิด กฎ หรือไม่ ขึ้นกับการตีความที่ตัวบทเปล่าๆ ให้ไม่ได้
ความหมายเชิงรูปนัย (formal semantics) ทำสำเร็จตามที่ประกาศไว้ แต่ตอบคนละคำถามกับที่ปรัชญาตั้งไว้ มันเสนอคำตอบคู่แข่งกันสองแบบต่อคำถาม "โปรแกรมนี้มีความหมายว่าอะไร" และสร้างทั้งสองแบบขึ้นมาเพื่อหนีปัญหาของ Wittgenstein โดยตรง ด้วยการตรึงความหมายแน่นจนไม่มีความกำกวมเหลือรอด ความหมายเชิงปฏิบัติการ (operational semantics) ตามประเพณีที่ Gordon Plotkin ทำให้เป็นรูปนัยในเอกสารประกอบการบรรยายที่ Aarhus ปี 1981 เรื่อง "A Structural Approach to Operational Semantics" (Plotkin, DAIMI FN-19, Aarhus University, 1981) นิยามความหมายของโปรแกรมเป็นลำดับสถานะของเครื่องที่มันสร้างขึ้น — ความหมายในฐานะร่องรอย (trace) ที่ตรวจได้ด้วยการจำลอง ความหมายเชิงนัยชี้ (denotational semantics) ที่ Christopher Strachey กับ Dana Scott สร้างที่ Programming Research Group ของ Oxford ทำอีกทาง คือจับวัตถุทางคณิตศาสตร์ใส่ให้แต่ละโปรแกรมตรงๆ โดยมากเป็นฟังก์ชันจากอินพุตไปเอาต์พุต และรับมือกรณียาก — ลูป การเรียกฟังก์ชันตัวเอง — ด้วยการหาจุดตรึงน้อยที่สุด (fixed point) ของฟังก์ชันนั้นเหนือพื้นที่มีโครงสร้างที่เรียกว่าโดเมน (domain) (Scott & Strachey, "Toward a Mathematical Semantics for Computer Languages," PRG-6, 1971) ทั้งคู่ทำให้ สิ่งที่เกิดขึ้น ชัดเจนแน่นอนเต็มที่จริง แต่ไม่มีใครแตะคำถามของ Wittgenstein เลย คำถามนั้นไม่เคยเป็นเรื่องสถานะถัดไปของเครื่อง มันเป็นเรื่องว่าสถานะที่เครื่องไปถึงคือสถานะที่กฎมี ไว้เพื่อ หรือเปล่า ช่องว่างนั้นคือจุดที่การฟอร์ก Ethereum ตกลงไปพอดี
โพรโทคอลตอบคำถามคนละข้อเรื่องความหมาย ไม่ใช่ว่าข้อความบรรยายอะไร แต่ว่ามันทำอะไร J. L. Austin ใน How to Do Things with Words — บรรยายในชุด William James Lectures ที่ Harvard ปี 1955 พิมพ์ในปี 1962 หลังเขาเสียชีวิตด้วยวัย 48 ปี — เรียกสิ่งเหล่านี้ว่าประพจน์เชิงกระทำ (performative) ถ้อยแถลงที่ตัวมันคือการกระทำ ไม่ใช่รายงานการกระทำ และใช้ได้ต่อเมื่อ "เงื่อนไขความสำเร็จของวัจนกรรม (felicity condition)" เป็นจริง คือผู้พูดถูกคน สถานการณ์ถูกจังหวะ ขั้นตอนถูกลำดับ (SEP, "Speech Acts") การ commit ไม่ได้บรรยายการเปลี่ยนแปลงในที่เก็บ (repository) มันคือการเปลี่ยนแปลงนั้น ลายเซ็นเข้ารหัส (cryptographic signature) ไม่ได้รายงานว่าคุณยินยอม การสร้างมันขึ้นมาคือการยินยอม การจับมือ TCP (TCP handshake) ไม่ได้บรรยายข้อตกลงที่จะคุยกัน การทำให้มันสำเร็จคือการเปิดช่องสัญญาณ ผู้ออกแบบโพรโทคอลบังคับใช้เงื่อนไขความสำเร็จของวัจนกรรมด้วยกลไกมาก่อนที่คำศัพท์ของ Austin จะเดินทางมาถึงวงการคอมพิวเตอร์ด้วยซ้ำ — การจับมือที่ผิดรูปแบบก็ล้มเหลวไปเฉยๆ แบบเดียวกับคำสัญญาที่ไม่จริงใจล้มเหลวในการผูกมัด
ความหมายระดับประโยคทั้งประโยคแตกเป็นสองสายโปรแกรมวิจัย และวงการคอมพิวเตอร์ทดลองทั้งสองสายมาแล้วห้าสิบปี งาน "The Proper Treatment of Quantification in Ordinary English" ของ Richard Montague (1973 ที่ทุกคนอ้างในชื่อย่อ PTQ) พยายามมอบความเข้มงวดเชิงประกอบ (compositionality) ให้ภาษาอังกฤษ แบบที่ Frege มอบให้เลขคณิต — ทุกกฎวากยสัมพันธ์จับคู่กับกฎความหมายหนึ่งข้อ ความหมายของประโยคก่อขึ้นจากส่วนประกอบอย่างเคร่งครัดผ่านตรรกะเชิงเจตนา (intensional logic) (SEP, "Montague Semantics") คู่แข่งของมันไม่ต้องใช้รูปแบบตรรกะ (logical form) เลย ประโยคของ J. R. Firth ปี 1957 ที่ว่าเรารู้จักคำหนึ่ง "จากพวกที่มันคบหา" ต่อยอดสมมติฐานเชิงการกระจาย (distributional hypothesis) ของ Zellig Harris จนตั้งเป็นความหมายเชิงการกระจาย (distributional semantics) — ความหมายของคำก็คือรูปทรงเชิงสถิติของคำข้างเคียง เท่านั้นเอง Tomáš Mikolov และคณะทำให้ไอเดียนี้คำนวณได้ในราคาถูกเมื่อปี 2013 ด้วย word2vec และโมเดลภาษาขนาดใหญ่ (large language model) ทุกตัวนับจากนั้นรับพนันก้อนนี้ไว้เต็มๆ (Mikolov et al., "Efficient Estimation of Word Representations in Vector Space," arXiv:1301.3781, 2013) สี่ทศวรรษ เงินวิจัยไหลไปทางโครงสร้างมาก่อนของ Montague ทศวรรษล่าสุดย้ายไปทางบริบทมาก่อนของ Firth เกือบทั้งหมด และการย้ายครั้งนั้นให้เครื่องจักรที่พูดคล่อง บนทฤษฎีความหมายที่ไม่เหลือที่ว่างให้ประพจน์ (proposition) เลยสักนิด
โมเดลภาษาขนาดใหญ่ (LLM) คือบททดสอบจริงที่ปรัชญาภาษาต้องเจอ และคำตัดสินแตกเป็นสองทาง มุมมองยุคหลังของ Wittgenstein — "ความหมายของคำหนึ่งคือการใช้งานของมันในภาษา" (Philosophical Investigations §43) — ดูได้รับการยืนยัน เพราะโมเดลที่ไม่เคยแตะสิ่งอ้างอิง (referent) สักครั้งยังผลิตประโยคที่ไม่มีเจ้าของภาษาคนไหนทักว่าผิด แต่ Stevan Harnad ตั้งชื่อชิ้นส่วนที่ขาดหายไปตั้งแต่ปี 1990 ก่อนของพวกนี้ถูกสร้างขึ้นด้วยซ้ำ — ระบบที่ขยับสัญลักษณ์ด้วยรูปร่างของมันและความสัมพันธ์กับสัญลักษณ์อื่นเท่านั้น ไม่เคยยึดโยงกับสิ่งที่สัญลักษณ์พูดถึง ก็เหมือนติดอยู่กับการเรียนภาษาจีนจากพจนานุกรมจีน–จีน สอดคล้องกันในตัวเองอย่างสมบูรณ์ ไม่แตะโลกจริงเลยสักนิด (Harnad, "The Symbol Grounding Problem," Physica D 42, 1990) โมเดลภาษาขนาดใหญ่จึงเป็นทั้งหลักฐานที่ดีที่สุดที่ทฤษฎีความหมายจากการใช้ (use theory of meaning) แบบบริสุทธิ์เคยได้รับ และเป็นแบบจำลองใช้งานได้ที่ชัดที่สุดของสิ่งที่นักวิจารณ์เรื่องการยึดโยง (grounding) เตือนไว้ว่าทฤษฎีความหมายจากการใช้ที่ไม่ยึดโยงจะหน้าตาเป็นอย่างไร
เชื่อมโยง
บทที่ 01 ให้กลไกเชิงตรรกะที่ทั้ง Montague และความหมายเชิงนัยชี้ (denotational semantics) พึ่งพา — ตัวบ่งปริมาณ (quantifier) ของ Frege บทที่ 02 กลับไปหาปัญหาชนิด/ตัวอย่างจริง (type/token) ที่บทนี้แตะเพียงผิวเผิน — bytecode ที่ deploy จริงของ smart contract เป็นสิ่งเดียวกับซอร์ส Solidity ของมันหรือไม่ บทที่ 04 เดินข้อโต้แย้งเรื่องการยึดโยง (grounding) ชุดเดียวกันนี้ผ่านห้องจีน (Chinese Room) บทที่ 13 เอามันไปทดสอบกับเครื่องจักรที่ฝึกจากข้อความล้วนๆ บทที่ 12 แสดงปลายทางของ "โค้ดบอกความหมายของตัวมันเอง" เมื่อถูกผลักไปจนสุด — proof assistant ที่กฎตัดสินทุกกรณีได้จริง
คำถามที่ยังเปิดอยู่
ถ้าความหมายเชิงรูปนัย (formal semantics) ระบุพฤติกรรมของโปรแกรมได้ครบถ้วน แต่ยังทิ้งคำถามค้างไว้ว่าโปรแกรมนั้นมี ไว้เพื่อ อะไร มันแก้ปัญหาของ Wittgenstein ได้จริง หรือแค่เปลี่ยนคำถามที่ตอบ ความหมายเชิงการกระจาย (distributional semantics) ชนะเพราะเป็นทฤษฎีความหมายที่ดีกว่า หรือเพราะเป็นทฤษฎีที่คอมพิวเตอร์รันไหวในสเกลใหญ่เสียที และถ้าระบบที่ไม่ยึดโยงผ่านบททดสอบเชิงพฤติกรรมของความเข้าใจได้ทุกข้อ "การยึดโยง (grounding)" ยังทำงานอะไรอยู่ นอกจากตั้งชื่อให้ความรู้สึกไม่สบายใจ
อ่านต่อ
- Ludwig Wittgenstein, Philosophical Investigations, trans. G. E. M. Anscombe, Blackwell, 1953 — §§138–242 คือข้อโต้แย้งเรื่องการทำตามกฎ (rule-following) ที่บทนี้หยิบยืมมาใช้
- Richard Montague, "The Proper Treatment of Quantification in Ordinary English," in Approaches to Natural Language, ed. Hintikka, Moravcsik & Suppes, Reidel, 1973, pp. 221–242 (PTQ), read against Tomáš Mikolov, Kai Chen, Greg Corrado & Jeffrey Dean, "Efficient Estimation of Word Representations in Vector Space," arXiv:1301.3781, 2013 — สองทฤษฎีความหมายที่วงการคอมพิวเตอร์ลองใช้จริง ห่างกันสี่สิบปี
- Stanford Encyclopedia of Philosophy, "Montague Semantics" — บันทึกหลักเรื่องจุดที่ความหมายเชิงรูปนัยกับความหมายภาษาธรรมชาติมาบรรจบกัน