Формальді тілде өрнектің типін автоматты анықтау

Кіріспе

Формалды тілдегі өрнектің типін автоматты түрде анықтау

Типтік шешім шығару, кейде типтік реконструкция деп те аталады, формалды тілдегі өрнектің типін автоматты түрде анықтау процесін білдіреді. Мұндай тілдерге бағдарламалау тілдері мен математикалық типтік жүйелер ғана емес, сонымен қатар компьютерлік ғылым мен лингвистиканың кейбір салаларындағы табиғи тілдер де жатады.

Техникалық емес түсіндірме

Типтерді ең жалпы түсінік бойынша, сол типтегі объектіге қолданылатын мүмкін әрекеттерді ұсынатын және шектейтін белгілі бір мақсатқа байланыстыруға болады. Тілдегі көптеген зат есімдер осындай мақсаттарды көрсетеді. Мысалы, "қосақ" сөзі "бау" сөзінен өзгеше мақсатты білдіреді. Бір нәрсені стол деп атау, оны отын деп атаудан мүлдем басқаша белгілеуді білдіреді, бірақ олар материалдық тұрғыдан бірдей болуы мүмкін. Олардың материалдық қасиеттері заттарды кейбір мақсаттарда пайдалануға мүмкіндік берсе де, олар нақты белгілеулерге жатады. Бұл әсіресе абстрактілі салаларда, атап айтқанда математика мен компьютер ғылымында маңызды, онда материал ақырында тек биттер немесе формулалар болып табылады. Қажетсіз, бірақ материалдық тұрғыдан мүмкін болатын қолданыстарды жою үшін типтер түсінігі әртүрлі нұсқаларда анықталады және қолданылады. Математикада Расселдің парадоксы типтік теорияның алғашқы нұсқаларын тудырды. Бағдарламалау тілдерінде, ең көп кездесетін мысалдар – "тип қатесі", мысалы, компьютерге сандар емес мәндерді қосуды бұйыру. Материалдық тұрғыдан мүмкін болса да, нәтиже мағынасыз болып қана қоймай, бүкіл процеске зиян келтіруі мүмкін. Типтеу кезінде өрнек типке қарама-қарсы қойылады. Мысалы, , , және – натурал сандар үшін типпен бірге жеке тұрған шарттар. Дәстүрлі түрде, өрнектен кейін қос нүкте және оның типі келеді, мысалы, . Бұл мәннің типі екенін білдіреді. Осы формат жаңа атауларды жариялау үшін де қолданылады, мысалы, , жаңа кейіпкерді сахнаға енгізу үшін "детектив Декер" деген сөздерді қолдану сияқты. Оқиғадан айырмашылығы, онда белгілеулер біртіндеп ашылады, формальді тілдердегі объектілер көбінесе бастапқыда-ақ олардың типімен анықталуы керек. Сонымен қатар, егер өрнектер түсініксіз болса, мақсатты қолданысты нақтылау үшін типтер қажет болуы мүмкін. Мысалы, өрнек рационал немесе нақты сан ретінде де, тіпті қарапайым мәтін ретінде де қарастырылуы мүмкін. Соның салдарынан, бағдарламалар немесе дәлелдемелер типтермен соншалықты ауыртпалы болуы мүмкін, оларды контекстен анықтау қажет болады. Бұл типтелмеген өрнектің қолданылуын (анықталмаған атауларды қоса алғанда) жинау арқылы мүмкін болады. Мысалы, егер әлі анықталмаған n атауы өрнегінде қолданылса, онда n кем дегенде сан деп қорытуға болады. Өрнектен және оның контекстінен типті анықтау процесі типтік қорыту деп аталады. Жалпы, тек объектілер ғана емес, іс-әрекеттердің де типтері болады және олар тек оларды қолдану арқылы ғана енгізілуі мүмкін. Мысалы, "Жұлдызды жол" оқиғасында белгісіз іс-әрекет "телепорттау" болуы мүмкін, ол оқиғаның ағыны үшін орындалады және формальді түрде енгізілмейді. Дегенмен, оның типін (көлік) оқиғаның дамуынан анықтауға болады. Сонымен қатар, объектілер мен іс-әрекеттер де олардың бөліктерінен құрастырылуы мүмкін. Мұндай жағдайда типтік қорыту ғана емес, сонымен қатар пайдалырақ болуы мүмкін, өйткені ол құрастырылған сахнадағы барлық нәрсенің толық сипаттамасын жинауға мүмкіндік береді, сонымен бірге қарама-қайшылықты немесе қаламаған қолданыстарды анықтауға да мүмкіндік береді.

Types in a most general view can be associated to a designated use suggesting and restricting the activities possible for an object of that type. Many nouns in language specify such uses. For instance, the word leash indicates a different use than the word line. Calling something a table indicates another designation than calling it firewood, though it might be materially the same thing. While their material properties make things usable for some purposes, they are also subject of particular designations. This is especially the case in abstract fields, namely mathematics and computer science, where the material is finally only bits or formulas. To exclude unwanted, but materially possible uses, the concept of types is defined and applied in many variations. In mathematics, Russell's paradox sparked early versions of type theory. In programming languages, typical examples are "type errors", e. g. ordering a computer to sum values that are not numbers. While materially possible, the result would no longer be meaningful and perhaps disastrous for the overall process. In a typing, an expression is opposed to a type. For example, , , and are all separate terms with the type for natural numbers. Traditionally, the expression is followed by a colon and its type, such as This means that the value is of type This form is also used to declare new names, e. g. , much like introducing a new character to a scene by the words "detective Decker". Contrary to a story, where the designations slowly unfold, the objects in formal languages often have to be defined with their type from very beginning. Additionally, if the expressions are ambiguous, types may be needed to make the intended use explicit. For instance, the expression might have a type but could also be read as a rational or real number or even as a plain text. As a consequence, programs or proofs can become so encumbered with types, that it is desirable to deduce them from the context. This can be possible by collecting the uses of untyped expression (including undefined names). If, for instance, a yet undefined name n is used in an expression , one could conclude, that n is at least a number. The process of deducing the type from an expression and its context is type inference. In general not only objects, but also activities have types and may be introduced simply by their use. For a Star Trek story, such an unknown activity could be "beaming", which for sake of the story's flow is just executed and never formally introduced. Nevertheless, one can deduce its type (transport) following what happens. Additionally, both objects and activities can be constructed from their parts. In such a setting, type inference cannot only become more complex, but also more helpful, as it allows to collect a complete description of everything in a composed scene, while still being able to detect conflicting or unintended uses.

Техникалық сипаттама

Типтік тұжырымдау – өрнектің түрін компиляция кезінде толық немесе ішінара автоматты түрде анықтау мүмкіндігі. Компилятор көбінесе типтік белгілер берілмеген жағдайда да, айнымалының түрін немесе функцияның типтік сипаттамасын анықтай алады. Көп жағдайда, типтік тұжырымдау жүйесі жеткілікті деңгейде сенімді болса немесе бағдарлама немесе тіл жеткілікті қарапайым болса, бағдарламадан типтік белгілерді толығымен жоюға болады. Өрнектің түрін анықтау үшін қажетті ақпаратты алу үшін компилятор бұл ақпаратты оның кіші өрнектеріне берілген типтік белгілердің жиынтығы және одан кейінгі қысқарту арқылы немесе әртүрлі атомдық мәндердің түрін жасырын түсіну арқылы жинайды (мысалы, true: Bool; 42: Integer; 3.14159: Real; және т.б.). Өрнектердің түпкілікті түрлендіруге алынған, жасырын типтелген атомдық мәндерге дейін тоғысуын тану арқылы, типтік тұжырымдау тілінің компиляторы типтік белгілерсіз толыққанды бағдарламаны құрастыра алады. Жоғары деңгейдегі бағдарламалаудың және полиморфизмнің күрделі формаларында компилятордың барлық жағдайларда анықтауы мүмкін емес, сондықтан кейде түсініктілікті арттыру үшін типтік белгілер қажет болады. Мысалы, полиморфты рекурсияда типтік тұжырымдаудың шешілмейтіні белгілі. Сонымен қатар, кодты оңтайландыру үшін нақтырақ (жылдамырақ/кішкентайрақ) типті қолдануға компиляторды мәжбүрлеу арқылы эксплицитті типтік белгілерді пайдалануға болады. Типтік тұжырымдаудың кейбір әдістері шектеулерді қанағаттандыруға немесе теориялар бойынша қанағаттандыруға негізделген.

Хиндли-Милнер типті қорытынды алгоритмі

Алғаш рет типтік тұжырымдауды орындау үшін қолданылған алгоритм қазіргі кезде бейресми түрде Хиндли-Милнер алгоритмі деп аталады, бірақ бұл алгоритмді дұрысырақ Дамас пен Милнерге жатқызу керек. Ол сондай-ақ дәстүрлі түрде типтік қайта құру деп те аталады. Хиндлидің жұмысынан тәуелсіз, эквивалентті алгоритм, W алгоритмі ұсынылған. 1982 жылы Луис Дамас Типтік тұжырымдау алгоритмдері табиғи тілдер үшін кейбір грамматикалық индукция және шектеулерге негізделген грамматикалық жүйелерде де қолданылады.