Naslov (srp)

Интензионалност и појам алгоритма : докторска дисертација

Autor

Maksimović, Katarina, 1991-

Doprinosi

Petrić, Zoran, 1963-
Lazović, Živan, 1958-
Adžić, Miloš, 1982-

Opis (srp)

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

Opis (srp)

Филозофија - Филозофија математике, логика / Philosophy - Philosophy of mathematics, logic Datum odbrane: 30.01.2023.

Opis (eng)

The extensional approach to meaning is based on the assumption that the meaning of words andlarger linguistic compounds consists entirely in what they signify. On the other hand, theintensional approach is the one where meaning is not reduced in such a manner to its referentialaspects, the semantical content is also seen as important. Although seemingly naive, theextensional view of meaning is dominant in logic, while the intensional has mostly beenneglected. 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 workis 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 whenit comes to solving certain conceptual problems. One of these problems that we are particularlyinterested in is the problem of defining the concept of algorithm.The first chapter is introductory and provides a historical and philosophical background for thequestions we aim to answer in the remaining chapters. In the first part of that introduction, wewill point to some of the reasons that led to the extensional view becoming prevalent in logic. Inthe second part, we will consider some examples of notions in logic that are understoodintensionally. The most important of these is the concept of proof which is the subject matter ofgeneral proof theory. One of the central questions in this theory is the question of the sense of aformal derivation. According to this theory, the sense of a derivation is a deduction - how wederive the conclusion from the given hypothesis. The meaning of the concept of deduction is thendefined by determining the conditions under which two derivations have the same sense. Theproblem of determining these conditions is called the problem of proof identity and it is thecentral topic of general proof theory. In the second chapter, we will talk in more detail about theproblem of proof identity, the intensional approach in general proof theory, and about the resultsthat are based on it.One of the main aims of this work is to apply this approach to the problem of defining the notionof algorithm. An algorithm is a concept that is significant not just for logic but for computerscience as well. Although not that many authors have written about it, it has gained someattention in the last two decades or so, especially thanks to the work of the mathematicianYiannis 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 thisconcept intensionally. We are going to say something more about these arguments in the thirdchapter. There we will present and evaluate Moschovakis’ definition of an algorithm and hisviews on algorithms in general. That definition is based on the concept of recursor that we willintroduce in the same chapter. While in general proof theory the analysis of the concept of proofis based on the problem of proof identity, Moschovakis’ approach revolves around the problemof algorithm identity. That problem is one of the main topics of this work and it can be expressedin the following way. When can one say that two algorithms represent the same computationalprocedure? In the third chapter of this work, we are going to present Moschovakis’ solution tothis problem. However, as we will show, the identity criteria proposed by Moschovakis haveconsiderable limitations.In the fourth and final chapter we show how the concept of an algorithm can be analyzed insidethe lambda calculus. The lambda calculus is a formal system that is based on the concept offunction seen as a rule of correspondence. This equality calculus was discovered by AlonzoChurch in the 1930s. Its significance consists primarily in the formalization of the notion ofeffective calculability. As shown by Turing and Kleene, functions that are representable in thelambda calculus are exactly the recursive functions, that is, the functions that can be calculatedby a Turing machine. In this chapter, we will show how we can represent not only computablefunctions inside lambda calculus but also algorithms that we used to calculate them. Accordingto our proposal, the problem of algorithm equality is thus reduced to the question of the equalityof the appropriate terms in the lambda calculus. In the last chapter, we consider several differentequality criteria. We also define some new equalities between lambda terms.

Jezik

srpski

Datum

2022

Licenca

Ovo delo je licencirano pod uslovima licence
Creative Commons CC BY-NC-ND 3.0 AT - Creative Commons Autorstvo - Nekomercijalno - Bez prerada 3.0 Austria License.

http://creativecommons.org/licenses/by-nc-nd/3.0/at/legalcode

Predmet

OSNO - Opšta sistematizacija naučnih oblasti, Simbolička logika. Matematička logika

algorithm, algorithm identity, intensionality, intension identity, lambda calculus, general proof theory, proof identity, recursor

OSNO - Opšta sistematizacija naučnih oblasti, Simbolička logika. Matematička logika

алгоритам, једнакост алгоритама, интензионалност, једнакост интензија, ламбда рачун, општа теорија доказа, једнакост доказа, рекурзор