ข้อผิดพลาดแบบไหนที่ถือว่าเป็นความผิดพลาดเล็กน้อย
ประเด็นสำคัญ
- หากข้อผิดพลาดในนิยามหรือบทพิสูจน์แก้ไขได้ง่าย แต่สังเกตเห็นได้ยาก ความผิดพลาดนั้นก็ไม่ใช่เรื่องเล็กน้อย
- ข้อผิดพลาดบางอย่างต้องอาศัยตัวช่วยพิสูจน์จึงจะค้นพบได้
เนื้อหาโดยย่อ
- ตั้งแต่เดือนธันวาคมปีที่แล้วถึงวันที่ 16 เมษายนปีนี้ ผู้เขียนใช้เวลาราว 170 ชั่วโมงเพื่อพิสูจน์ทฤษฎีบทสตริง
String.splitOn_of_valid ในไลบรารีมาตรฐานของ Lean proof assistant
- ระหว่างการพิสูจน์ทฤษฎีบทนี้ ได้ค้นพบบั๊กในนิยามของฟังก์ชัน
String.splitOn
- การแก้บั๊กนี้ไม่ยากนัก เพียงแค่เปลี่ยน
i เป็น i - j ในนิยามดังกล่าว
- แต่ถึงอย่างนั้น ก็ไม่ได้หมายความว่าข้อผิดพลาดนี้เป็นความผิดพลาดเล็กน้อย เพราะตามนิยามนี้ ฟังก์ชัน
splitOn มักทำงานได้ถูกต้องก็จริง แต่ในกรณีพิเศษบางอย่างจะให้ผลลัพธ์ที่ผิด
- หากไม่ได้ใช้ตัวช่วยพิสูจน์อย่าง Lean ผู้เขียนก็คงไม่มีทางค้นพบข้อผิดพลาดที่ละเอียดอ่อนเช่นนี้ได้เลย
ยังไม่มีความคิดเห็น