Интензионалност и појам алгоритма

Abstract

Екстензионални приступ проблему значења заснован је на претпоставци да се значење речи или већих језичких целина састоји искључиво у томе шта означавају. Са друге стране, интензионалним семантичким приступом можемо назвати онај у којем се значење не своди искључиво на његове референцијалне аспекте, већ се узима у обзир и семантички садржај. Иако на изглед наивно, екстензионално схватање значења је оно које превладава у логици, док је интензионално у великој мери занемарено. Разлика између интензионалног и екстензионалног у филозофији није нова. Међутим, често није била довољно јасно и прецизно дефинисана. Један од циљева овог рада је да одговоримо на питање шта би то значило дати интензионалну анализу појма у логици и математици. Такође ћемо показати да интензионално схватање значења има предности у односу на екстензионално у решавању неких појмовних проблема који се у логици јављају. Један од њих је проблем одређења појма алгоритма и њиме ћемо се у овом раду бавити. Прво поглавље је уводно и служи да пружи историјски и филозофски оквир за питања којима ћемо се бавити у каснијим поглављима. У првом делу тог поглавља указаћемо на неке од разлога који су довели до тога да у логици и математици екстензионално схватање значења постане доминантно. У другом делу разматраћемо неке примере појмова које у логици које, како ћемо показати, разумемо на интензионалан начин. Најважнији од њих је појам дедукције и њиме се бави општа теорија доказа. Један од централних питања те теорије је питање у чему се састоји смисао формалног извођења. Према тој теорији, смисао извођења се састоји у томе како се закључак дедукује из хипотеза. Он се дакле састоји у самој дедукцији. Значење појма дедукције у општој теорији доказа одређујемо тако што дефинишемо услове под којима можемо рећи да два извођења имају исти смисао. Проблем налажења тих услова се назива проблемом једнакости доказа и он представља једну од централних тема те теорије. О проблему једнакости доказа, интензионалном приступу у општој теорији доказа, као и о резултатима коју су на њему засновани детаљније ћемо да говоримо у другом поглављу. Један од главних циљева овог рада је да тај приступ покушамо да применимо на проблем одређења појма алгоритма. Алгоритам је појам који је врло значајан не само за логику већ и за теоријско рачунарство. Међутим, наше разумевање алгоритама је донекле још неформално, тај појам није сасвим прецизно дефинисан. Иако о том проблему није до сада пуно писано, он је добио на популарности током последње две деценије посебно захваљујући радовима математичара Јаниса Московакиса (Yiannis Moschovakis). Московакис је о проблему одређења појма алгоритма писао у многим својим радовима. Он је аргументовао како можемо наћи одговарајућу дефиницију алгоритма само ако тај појам схватимо интензионално. У трећем поглављу ћемо рећи нешто више о тим аргументима. Такође ћемо приказати и критички испитати дефиницију алгоритма коју Московакис даје. Та дефиниција заснива се на појму рекурзора о којем ће у том поглављу бити нешто више речи. Као што је проблем једнакости доказа један од главних питања у општој теорији доказа, тако и Московакисова појмовна анализа питању једнакости алгоритама даје централно место. То питање ће и за нас бити од кључне важности и оно се може изразити на следећи начин: Када можемо рећи да су два алгоритма представљају исту процедуру израчунавања? У трећем поглављу ћемо видети како изгледа Московакисово решење тог проблема. Показаћемо, међутим, да критеријум једнакости алгоритама који он предлаже поседује значајна ограничења. У четвртом и последњем поглављу показаћемо како се појам алгоритма може анализирати унутар ламбда рачуна. Ламбда рачун је формални систем заснован на схватању појма функције као правила повезивања. Овај једнакосни рачун кога је открио Алонзо Черч (Alonzo Church) тридесетих година прошлог века значајан је пре свега као формализација појма ефективне израчунљивости. Као што су показали Тјуринг (Alan Turing) и Клини (Stephen Kleene), функције које се могу на одређен начин представити у ламбда рачуну су све и само рекурзивне функције односно све и само функције које можемо израчунати помоћу Тјурингове машине. У четвртом поглављу ћемо показати како помоћу ламбда рачуна можемо да представимо не само све израчунљиве функције већ и алгоритме којима их израчунавамо. Решење које ћемо предложити има ту предност што проблем једнакости алгоритама своди на питање једнакости одговарајућих ламбда терама. У четвртом поглављу ћемо разматрати више различитих критеријума једнакости за алгоритме. У оквиру тих разматрања дефинисаћемо и неке нове једнакости између ламбда терама.

The extensional approach to meaning is based on the assumption that the meaning of words and larger linguistic compounds consists entirely in what they signify. On the other hand, the intensional approach is the one where meaning is not reduced in such a manner to its referential aspects, the semantical content is also seen as important. Although seemingly naive, the extensional view of meaning is dominant in logic, while the intensional has mostly been neglected. The difference between extensional and intensional is not new in philosophy. However, it often hasn’t been defined clearly and precisely enough. One of the aims of this work is to explain what it means to give an intensional analysis of a concept in logic and mathematics. We will also show that the intensional approach may be advantageous in these disciplines when it comes to solving certain conceptual problems. One of these problems that we are particularly interested in is the problem of defining the concept of algorithm. The first chapter is introductory and provides a historical and philosophical background for the questions we aim to answer in the remaining chapters. In the first part of that introduction, we will point to some of the reasons that led to the extensional view becoming prevalent in logic. In the second part, we will consider some examples of notions in logic that are understood intensionally. The most important of these is the concept of proof which is the subject matter of general proof theory. One of the central questions in this theory is the question of the sense of a formal derivation. According to this theory, the sense of a derivation is a deduction - how we derive the conclusion from the given hypothesis. The meaning of the concept of deduction is then defined by determining the conditions under which two derivations have the same sense. The problem of determining these conditions is called the problem of proof identity and it is the central topic of general proof theory. In the second chapter, we will talk in more detail about the problem of proof identity, the intensional approach in general proof theory, and about the results that are based on it. One of the main aims of this work is to apply this approach to the problem of defining the notion of algorithm. An algorithm is a concept that is significant not just for logic but for computer science as well. Although not that many authors have written about it, it has gained some attention in the last two decades or so, especially thanks to the work of the mathematician Yiannis Moschovakis. Moschovakis has written about this problem in detail in many of his works. He has argued that to give an adequate definition of an algorithm one needs to understand this concept intensionally. We are going to say something more about these arguments in the third chapter. There we will present and evaluate Moschovakis’ definition of an algorithm and his views on algorithms in general. That definition is based on the concept of recursor that we will introduce in the same chapter. While in general proof theory the analysis of the concept of proof is based on the problem of proof identity, Moschovakis’ approach revolves around the problem of algorithm identity. That problem is one of the main topics of this work and it can be expressed in the following way. When can one say that two algorithms represent the same computational procedure? In the third chapter of this work, we are going to present Moschovakis’ solution to this problem. However, as we will show, the identity criteria proposed by Moschovakis have considerable limitations. In the fourth and final chapter we show how the concept of an algorithm can be analyzed inside the lambda calculus. The lambda calculus is a formal system that is based on the concept of function seen as a rule of correspondence. This equality calculus was discovered by Alonzo Church in the 1930s. Its significance consists primarily in the formalization of the notion of effective calculability. As shown by Turing and Kleene, functions that are representable in the lambda calculus are exactly the recursive functions, that is, the functions that can be calculated by a Turing machine. In this chapter, we will show how we can represent not only computable functions inside lambda calculus but also algorithms that we used to calculate them. According to our proposal, the problem of algorithm equality is thus reduced to the question of the equality of the appropriate terms in the lambda calculus. In the last chapter, we consider several different equality criteria. We also define some new equalities between lambda terms.