Кореспонденцията Къри-Хауърд за начинаещи
Какво е общото между програмирането и философията? Много повече, отколкото си мислите. Тази статия ще обясни с лесни за начинаещи термини как точно изглежда тази връзка и как е била открита. Ще разделя тази концепция на четири раздела:
· Логика: ключът към философията и програмирането
· Предложенията като типове
· Доказателствата като програми
· Какво означава това за програмистите
Логика: Ключът към философията и програмирането
Ключовото звено в свързването на философията и програмирането е логиката. През четвърти век пр. н. е. Аристотел създава вид логика, която ще формира основата за следване на всяка логика, изградена върху предложения и заключения.
Твърдение: Всички хора са смъртни.
Предложение: Всички гърци са мъже.
Извод: Всички гърци са смъртни.
Предложенията са факти, които предлагаме, са верни, и заключенията, които можем да заключим, че са верни, след като разгледаме всички предложения заедно.
През следващите векове тези идеи ще бъдат надградени и ще се развият в нови видове логика, позволявайки да се правят по-сложни предложения и заключения и в крайна сметка да се създаде модерна математика, каквато я познаваме днес.
През 30-те години на миналия век логиката продължава да се развива, но сега се изследва нова област на науката: компютърните науки. През следващите 30 години двама учени ще стигнат до заключение, което ще промени завинаги математиката и компютърните науки:
Математическата логика и компютърните програми са равни!
Тези двама души са математикът Хаскел Къри и логикът Уилям Алвин Хауърд и тяхното откритие е наречено Кореспонденция Къри-Хауърд.
И така, какво точно представлява кореспонденцията Къри-Хауърд и как ни казва, че логиката и програмите са равни? За да отговорим на този въпрос, ще разгледаме две връзки: предложения и типове и доказателства и програми.
Предложенията като видове
Логическите предложения ни позволяват да изразим знания за света около нас, а доказателствата ни казват дали това знание е точно или не. Кореспонденцията Къри-Хауърд ни казва, че можем също да заявим това знание с „компютърни типове“ и да го докажем с помощта на компютърни програми. За да демонстрирате това в действие, разгледайте този прост математически проблем:
Здравей + 5 =?
Ако мислите, че това е глупав въпрос, прав сте! Но защо няма смисъл? Е, когато използваме символа +, очакваме да съберем две числа, а думата „здравей“ не е число. Можем да заявим това с логично предложение, което казва:
За всеки две неща, които се събират заедно, тези две неща са числа.
Кореспонденцията Къри-Хауърд ни казва, че можем да кажем едно и също нещо, използвайки типове. В този случай ние даваме типа на функцията за добавяне.
Добавянето е функция, която приема две числа като вход и връща ново число като изход.
Function Plus Input : Number, Number Output : Number
Това се нарича сигнатура на типа на функцията — тя идентифицира функцията, точно както вашият подпис би ви идентифицирал.
И така, сега, когато имаме нашето логическо предложение и нашия тип компютър, можем да използваме кореспонденцията Къри-Хауърд, за да покажем, че hello + 5 няма смисъл с логическо доказателство и компютърна програма.
Доказателствата като програми
Да започнем с логическата страна:
За всеки две неща, които се събират заедно, тези две неща са числа.
В нашия пример за hello + 5 имаме две неща, които се добавят заедно:
- "Здравейте"
- 5
Нашето предложение ни казва, че и двете неща, които се събират заедно, са числа, а нашето твърдение ни казва нещо различно: че само едно от тях е число - което е логически непоследователно.
И така, използвахме логика, за да покажем защо твърдението ни няма смисъл - сега можем да използваме компютърна програма, за да направим същото.
Не забравяйте, че нашата функция има този тип подпис:
Function Plus Input : Number, Number Output : Number
И така, какво се случва, когато опитаме нашата функция с нашите входове от hello и 5?
> Hello + 5 Type Error: Expected type "Number", recieved type "String"
Програмата ни не успява да се стартира, което ни дава типова грешка. Преди да се опита да събере нашите входове, компютърът провери типовете на входовете. Наричаме това проверка на типа и се натъкна на проблем: не успя да извърши проверка на типа.
И така, както логиката, така и компютърът ни казаха, че hello + 5 няма смисъл с логическа несъответствие и грешка в типа. С кореспонденцията Къри-Хауърд знаем, че това не е съвпадение и че всъщност логиката и програмата правят едно и също нещо.
Какво означава това за програмистите
Въпреки че показването, че hello + 5 няма смисъл, не е точно революционен резултат. Кореспонденцията Къри-Хауърд е от решаващо значение за изследванията в областта на програмирането и философията.
Кореспонденцията Къри-Хауърд позволява на компютърни учени, математици и философи да използват един и същи език и да работят заедно, за да създават нов софтуер, теории и рамки.
Когато типовете, логическите теории и програмите станат по-сложни, последиците от кореспонденцията Къри-Хауърд могат да се използват за създаване на сложни модели и доказване на свойствата на програмите.
Изучаването на основите на компютърните науки е важно, за да станете по-добър програмист. Ако искате да научите повече за тези фундаментални концепции за компютърни науки по лесен за начинаещи начин, очаквайте бъдещите ми статии, обхващащи теория на типовете и функционално програмиране.
Референции
- Хауърд, Уилям А. „Понятието за конструиране на формули като типове.“ До HB Curry: есета върху комбинаторната логика, ламбда смятане и формализъм 44 (1980): 479–490.
- „Педро, Пиер-Мари. „Изоморфизмът на Къри-Хауърд за манекени.“ (2015)»
