कौन-सी त्रुटि मामूली गलती होती है
मुख्य बिंदु
- यदि किसी परिभाषा या प्रमाण में मौजूद त्रुटि को ठीक करना आसान हो, लेकिन उसे पहचानना कठिन हो, तो वह गलती मामूली नहीं है।
- कुछ त्रुटियाँ केवल proof assistant की मदद से ही पकड़ी जा सकती हैं।
संक्षिप्त लेख
- पिछले साल दिसंबर से इस साल 16 अप्रैल तक लगभग 170 घंटे लगाकर मैंने Lean proof assistant की standard library में मौजूद string theorem
String.splitOn_of_valid को सिद्ध किया।
- इस theorem को सिद्ध करने के दौरान मैंने
String.splitOn फ़ंक्शन की परिभाषा में एक bug खोजा।
- इस bug को ठीक करना बहुत कठिन नहीं था। उस परिभाषा में बस
i को i - j से बदलना था।
- फिर भी मैं यह नहीं मानता कि यह त्रुटि कोई मामूली गलती थी। इस परिभाषा के अनुसार
splitOn फ़ंक्शन आम तौर पर सही काम करता है, लेकिन कुछ विशेष मामलों में गलत परिणाम देता है।
- यदि मैंने Lean जैसे proof assistant का उपयोग नहीं किया होता, तो मैं ऐसी सूक्ष्म त्रुटि कभी नहीं खोज पाता।
अभी कोई टिप्पणी नहीं है.