„=“ не е просто знак: Кевин Бъзърд преосмисля основите на математиката
Математик изяснява разликите в разбирането на равенството в програмирането и математиката.
В нова обява, която наподобява повече на публицистична публикация или набор от наблюдения, в сравнение с доктрина или проучване, математикът Кевин Бъзърд преглежда една елементарна концепция от програмирането, която става „ по-сложна “, когато се преведе на езика на математиката: какво в действителност значи знакът за тъждество? И какво не значи?
Бъзърд стана прочут с напъните си да преведе класическите математически доказателства в код, който може да бъде тестван с компютър, в това число доказателството на великата теорема на Ферма. За него, като типичен математик, светът на компютърния код крие доста изненади.
„ Преди шест години си мислех, че изцяло разбирам същността на математическото тъждество “, написа Бъзърд в своята научна работа. – Бях уверен, че това е добре дефиниран термин, който не съставлява интерес за практикуващия математик, който има нужните познания, само че не се задълбочава в главните правила на своята дисциплинираност. Когато обаче започнах да уча математиката на магистърско равнище благодарение на компютъризирана система за инспекция на другите теореми, открих, че понятието за тъждество е доста по-сложно и многостранно, в сравнение с бях предполагал преди “.
Бъзърд установи, че всеки студент в курса по програмиране бързо научава: в кодирането, че има няколко типа тъждество и че с цел да се програмира вярно, би трябвало напълно да се премине през някои стъпки, които човешкият разум елементарно прескача при осъществяване на математическите интервенции.
„ Низът „ 2 + 2 “, въведен в една компютърна алгебрична система, не е еднакъв на низа „ 4 “, изведен от системата; прави се някаква комплицирана обработка “,
обяснява Бъзърд.
Той акцентира, че програмирането би трябвало да регистрира другите нюанси, свързани с представянето на данните и интервенциите върху тях. Това, което може да наподобява явно за хората при работа с математическите изрази, при компютърните калкулации изисква деликатно обсъждане и прецизно съблюдаване на разпоредбите. Компютърът не разполага с интуитивното схващане, присъщо на човешкия разум, тъй че всяка стъпка би трябвало да бъде ясно дефинирана и изпълнена съгласно съответния логаритъм.
Важно е да се помни, че даже нещо да наподобява нищожно, това не значи, че то не е значимо и не си коства да се разисква. Има доста нюанси, свързани с този въпрос: би трябвало ли еднакъв знак за тъждество да се регистрира за изрази, закръглени нагоре или надолу? Дали знакът за тъждество значи същото, в случай че сред двете страни мине време (малко чудноват образец от страна на маттематика – когато две пилета станат три)?
Този въпрос не е обвързван с предефиниране на каквото и да било в математиката – той е обвързван с точността и желанието.
Според Бъзърд смисъла на знака за тъждество оставя доста какво да се желае в аспекта „ точност и желание “. В публикацията си той разказва настоящето положение на признака като „ нестрого “.
„ На процедура ние използваме понятието за тъждество много повърхностно, разчитайки на някакво надълбоко интуитивно схващане, а не на логическата рамка, в която считаме, че работим “,
написа той.
В определената от него стратегия за доказване на концепцията, известна като Lean system, стъпките би трябвало да бъдат дефинирани доста по-точно.
Зад кулисите на уравненията в нашите мозъци и в „ мозъците “ на компютрите, които програмираме, има повече стъпки, в сравнение с се вижда на пръв взор – всичко зависи от това по какъв начин ги организираме. Някои езици за програмиране, известни като „ мощно типизирани “ езици, изискват да се уточни видът на променливата. Например, „ x “ може да бъде цяло число, дълго десетично число или низ от знаци като за ключова дума. Всеки от тези видове се съхранява дружно със цената на променливата. Ако се опитате да извършите математическа интервенция или да приравните променливи от разнообразни видове, езикът за програмиране няма да го разреши.
В други езици (известни като „ едва типизирани “), както и в множеството математически практики, „ видът “ е по-контекстуално разбиране. Вместо да ревизира присвоения вид, програмният език ревизира дали наличието на променливата разрешава осъществяването на нужната интервенция. Например при пресмятане на „ 2+2=4 “ низът „ 2+2 “ се преобразува в цяло число 4 и едвам по-късно се съпоставят задачите цифри от двете страни на знака за тъждество. Това е просто за човешкото интуитивно мислене, само че компютрите се нуждаят от ясни указания.
Проектът Lean има за цел да преведе математическите доказателства в алгоритмични стъпки за компютъра. Бъзърд дава за образец математика Александър Гротендик, който употребява „ едва типизирана “ математика, като комбинира разнообразни дисциплини. Гротендиек вкара новия термин „ канонично изоморфен “ като нов тип тъждество, което би довело до неточност в Lean, защото той употребява = и ≅ ( знак за конгруентност ) с разнообразни цели.
За да се формализира математиката за компютърна обработка, е належащо да се отстранят този тип „ дупки “, като доказателството се разбие на обикновени стъпки. Това ще помогне на основателите на библиотеки за Lean. В дълготраен проект Lean може да усъвършенства математиката, като улесни инспекцията на все по-дълги и комплицирани доказателства.
Бъзърд признава, че „ неправилната приложимост “ на признака за тъждество може да заблуди читателя. Но защото доказателствата стават все по-сложни, е значимо колкото се може по-ясно да се кодират смислите за всеобщо схващане. Основната цел е да се положат основите на формализирането на математиката в компютърните системи.
