„=“ не е просто знак: Кевин Бъзърд преосмисля основите на математиката

Математик обяснява разликите в разбирането на равенството в програмирането и математиката.

В нова публикация, която прилича повече на редакционна статия или набор от наблюдения, отколкото на теория или изследване, математикът Кевин Бъзърд разглежда една проста идея от програмирането, която става „по-сложна“, когато се преведе на езика на математиката: какво всъщност означава знакът за равенство? И какво не означава?

Бъзърд стана известен с усилията си да преведе класическите математически доказателства в код, който може да бъде проверен с компютър, включително доказателството на великата теорема на Ферма. За него, като класически математик, светът на компютърния код крие много изненади.

„Преди шест години си мислех, че напълно разбирам същността на математическото равенство“, пише Бъзърд в своята научна работа. – Бях убеден, че това е добре дефиниран термин, който не представлява интерес за практикуващия математик, който има необходимите знания, но не се задълбочава в основните принципи на своята дисциплина. Когато обаче започнах да изучавам математиката на магистърско ниво с помощта на компютъризирана система за проверка на различните теореми, открих, че понятието за равенство е много по-сложно и многостранно, отколкото бях предполагал преди“.

Бъзърд констатира, че всеки студент в курса по програмиране бързо научава: в кодирането, че има няколко вида равенство и че за да се програмира правилно, трябва изцяло да се премине през някои стъпки, които човешкият ум лесно прескача при извършване на математическите операции.

„Низът „2 + 2“, въведен в една компютърна алгебрична система, не е равен на низа „4“, изведен от системата; извършва се някаква сложна обработка“,

обяснява Бъзърд.

Той подчертава, че програмирането трябва да отчита различните нюанси, свързани с представянето на данните и операциите върху тях. Това, което може да изглежда очевидно за хората при работа с математическите изрази, при компютърните изчисления изисква внимателно обмисляне и стриктно спазване на правилата. Компютърът не разполага с интуитивното разбиране, присъщо на човешкия ум, така че всяка стъпка трябва да бъде ясно дефинирана и изпълнена според съответния алгоритъм.

Важно е да се помни, че дори нещо да изглежда незначително, това не означава, че то не е важно и не си струва да се обсъжда. Има много нюанси, свързани с този въпрос: трябва ли един и същ знак за равенство да се отчита за изрази, закръглени нагоре или надолу? Дали знакът за равенство означава същото, ако между двете страни мине време (малко странен пример от страна на маттематика – когато две пилета станат три)?

Този въпрос не е свързан с предефиниране на каквото и да било в математиката – той е свързан с точността и намерението.

Според Бъзърд значението на знака за равенство оставя много какво да се желае в аспекта „прецизност и намерение“. В статията си той описва сегашното състояние на символа като „нестрого“.

„На практика ние използваме понятието за равенство доста небрежно, разчитайки на някакво дълбоко интуитивно разбиране, а не на логическата рамка, в която считаме, че работим“,

пише той.

В избраната от него програма за доказване на концепцията, известна като Lean system, стъпките трябва да бъдат дефинирани много по-точно.

Зад кулисите на уравненията в нашите умове и в „умовете“ на компютрите, които програмираме, има повече стъпки, отколкото се вижда на пръв поглед – всичко зависи от това как ги организираме. Някои езици за програмиране, известни като „силно типизирани“ езици, изискват да се посочи типът на променливата. Например, „x“ може да бъде цяло число, дълго десетично число или низ от символи като за парола. Всеки от тези типове се съхранява заедно със стойността на променливата. Ако се опитате да извършите математическа операция или да приравните променливи от различни типове, езикът за програмиране няма да го позволи.

В други езици (известни като „слабо типизирани“), както и в повечето математически практики, „типът“ е по-контекстуално понятие. Вместо да проверява присвоения тип, програмният език проверява дали съдържанието на променливата позволява извършването на необходимата операция. Например при изчисляване на „2+2=4“ низът „2+2“ се преобразува в цяло число 4 и едва след това се сравняват целите числа от двете страни на знака за равенство. Това е просто за човешкото интуитивно мислене, но компютрите се нуждаят от ясни инструкции.

Проектът Lean има за цел да преведе математическите доказателства в алгоритмични стъпки за компютъра. Бъзърд дава за пример математика Александър Гротендик, който използва „слабо типизирана“ математика, като комбинира различни дисциплини. Гротендиек въведе новия термин „канонично изоморфен“ като нов вид равенство, което би довело до грешка в Lean, тъй като той използва = и ≅ ( знак за конгруентност ) с различни цели.

За да се формализира математиката за компютърна обработка, е необходимо да се отстранят този вид „дупки“, като доказателството се разбие на елементарни стъпки. Това ще помогне на създателите на библиотеки за Lean. В дългосрочен план Lean може да подобри математиката, като улесни проверката на все по-дълги и сложни доказателства.

Бъзърд признава, че „неправилната употреба“ на символа за равенство може да заблуди читателя. Но тъй като доказателствата стават все по-сложни, е важно колкото се може по-ясно да се кодират значенията за всеобщо разбиране. Основната цел е да се положат основите на формализирането на математиката в компютърните системи.