Հայաստանի ատենախոսությունների բաց մատչելիության պահոց = Open Access Repository of the Armenian Electronic Theses and Dissertations (Armenian ETD-OA) = Репозиторий диссертаций Армении открытого доступа

Ֆունկցիոնալ ծրագրերի տիպային կոռեկտության մասին

Առաքելյան, Արա Հայկի (2011) Ֆունկցիոնալ ծրագրերի տիպային կոռեկտության մասին. PhD thesis, ԵՊՀ.

[img]
Preview
PDF (Abstract)
Available under License Creative Commons Attribution.

Download (217Kb) | Preview

    Abstract

    Աշխատանքը նվիրված է ֆունկցիոնալ ծրագրավորման խնդիրներին: Հետազոտության առարկան հանդիսանում են առանց տիպերի λ-թերմերը և դրանք օգտագործող ֆունկցիոնալ ծրագրերը, իսկ դիտարկվող հիմնական խնդիրը՝ այդ թերմերի և ֆունկցիոնալ ծրագրերի տիպային կոռեկտության խնդիրը: Տիպերը ծրագրավորման լեզուներում օգտագործվում են տարբեր նպատակներով, որոնցից են ծրագրում առկա տիպերի անհամաձայնության սխալների ավելի վաղ հայտնաբերումը (մինչև ծրագրի աշխատանքը), որոշակի օպտիմիզացիաների կատարումը և այլն: Այս աշխատանքի հիմնական խնդիրը կապված է ֆունկցիոնալ ծրագրավորման լեզուներում վերը նշված նպատակներից առաջինի իրագործման հետ. ստուգելով ծրագրի տիպային կոռեկտությունը մինչև նրա աշխատանքը՝ խուսափել ծրագրի աշխատանքի ընթացքում ի հայտ եկող տիպերի անհամաձայնության սխալներից: Մի շարք ծրագրավորման լեզուներում ծրագրավորողը բացահայտ կերպով չի նշում ինֆորմացիա տիպերի մասին: Այդպիսի ֆունկցիոնալ ծրագրավորման լեզուներից են հետևյալ լեզուները՝ Lisp, SML, OCaml, F# և այլն: Այդ դեպքում անհրաժեշտություն է առաջանում ստեղծել տիպերի արտածման համակարգեր, որոնք օգտագործվում են ծրագրերի տիպայնացման ժամանակ՝ փորձելով վերականգնել տիպերի մասին ծրագրավորողի կողմից չնշված ինֆորմացիան: Տիպայնացման ալգորիթմների կիրառելիության համար կարևոր պայման է հանդիսանում այն, որ այդ ալգորիթմները պետք է ապահովեն իրենց կողմից տիպայնացվող ցանկացած ծրագրի տիպային կոռեկտությունը: Այսինքն, եթե այդ ալգորիթմը տիպայնացնում է տվյալ ծրագիրը, ապա դա նշանակում է, որ այդ ծրագրի համար ինտերպրետատորի աշխատանքի ընթացքում չեն հանդիպելու տիպերի անհամաձայնության սխալներ: Սովորաբար օգտագործվում են ֆունկցիոնալ ծրագրերի ինտերպրետացիայի այնպիսի ալգորիթմներ, որոնք հիմնված են տեղադրումների և ռեդուկցիաների վրա: Այսպիսով, տիպայնացման ալգորիթմները «պարտավոր են մերժել» այն բոլոր ծրագրերը, որոնց ինտերպրետացիայի ընթացքում հանդիպելու են տիպերի անհամաձայնության սխալներ: Диссертационная работа посвящена проблемам функционального программирования. Объектами исследования являются бестиповые λ-термы и функциональные программы использующие такие термы, а основной проблемой является задача о типовой корректности этих термов и программ. В языках программирования типы используются в разных целях: для обнаружения ошибок несоответсвия типов в программе до начала её работы, для выполнения некоторых оптимизаций и т.д. Основная задача данной работы связана с первой из вышеупомянутых целей для функциональных программ: избегать ошибок несоответствия типов во время выполнения программы путём проверки её типовой корректности до начала работы программы. В некоторых языках программирования не даётся информация о типах явным образом. Примерами таких функциональных языков являются Lisp, SML, OCaml, F# и т.д. В этих случаях появляется необходимость создания систем вывода типов и алгоритмов типизации, которые пытаются восстанавить недостающую информацию о типах программ. Для алгоритмов типизации важно, чтобы они гарантировали типовую корректность типизируемых ими программ. То есть, если некоторый алгоритм типизации типизирует программу, то во время функционирования интерпретатора, в случае данной программы, ошибкa несоответсвия типов не должнa возникнуть. В основном используются алгоритмы интерпретации основанные на подстановках и редукциях. Из вышесказанного следует, что алгоритмы типизации должны “отвергать” все такие программы, во время интерпретации которых происходит ошибка несоответствия типов. С другой стороны, кроме программ содержащих ошибку типа, алгоритмы типизации могут “отвергать” ещё и такие программы, во время интерпретации которых ошибка несоответствия типов не происходит. The thesis is dedicated to the problems of functional programming. The main objects of the research are the untyped λ-terms and functional programs that use such terms and the main problem of the research is the problem of type correctness of that terms and functional programs. Types are used in programming languages for different purposes, such as detecting type errors earlier (before execution of the program), doing some optimizations etc. The main problem of the thesis is concerning to the first one of the objectives mentioned above: avoid type errors occurring during the program execution by checking its type correctness before the program execution. In some programming languages there is no explicit type information provided by the programmer. Such functional programming languages are Lisp, SML, OCaml, F# etc. In that case it is required to create type inference systems and typification algorithms, which are used for the typification of the programs and try to recover type information missed by the programmer. For the usage of the typification algorithms it is important to guarantee type correctness of the programs typified by them, i.e. if that typification algorithm typifies given program, than during the work of interpretation algorithm (generally interpretation algorithms based on the substitutions and reductions are considered) for that program no type error must occur. Hereby typification algorithms must reject all the programs, during interpretation of which type error will occur. On the other hand, except the programs containing type errors, typificiation algorithms can reject also some other programs, during interpretation of which type error will not occur. Hence, for the typification algorithms it is also important to reject as few programs as possible, which don’t contain type errors indeed. The following question is appeared: is it possible to construct such algorithm of typification, which rejects all the programs during the interpretation of which type error will occur and accepts all the programs during the interpretation of which type error will not occur? By summarizing we can conclude, that the problems concerning to the type correctness of the functional programs are actual.

    Item Type: Thesis (PhD)
    Additional Information: О типовой корректности функциональных программ. On type correctness of functional programs.
    Uncontrolled Keywords: Аракелян Ара Гайкович, Arakelyan Ara H.
    Subjects: Mathematics and Cybernetics
    Divisions: UNSPECIFIED
    Depositing User: NLA Circ. Dpt.
    Date Deposited: 15 Mar 2017 16:28
    Last Modified: 15 Mar 2017 16:28
    URI: http://etd.asj-oa.am/id/eprint/4286

    Actions (login required)

    View Item