Формалды тілдер: математика, логика, лингвистика және информатикадағы сөздердің құрылысы, грамматика, алфавит туралы мағлұмат. Бағдарламалау тілдеріне негіз.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Сөздердің белгілі бір ережелер бойынша құрылған тізбегі – математика және информатикадағы техникалық термин.
Sequence of words formed by specific rules
a technical term in mathematics and computer science
Логика, математика, информатика және лингвистикада формальды тіл – әріптері әліпбиден алынған және нақты ережелер жинағына сәйкес дұрыс құрылған сөздерден тұрады. Формальды тілдің әліпбиі символдардан, әріптерден немесе сөздер құрауға қолданылатын таңбалардан тұрады. Белгілі бір формальды тілге жататын сөздер кейде дұрыс құрылған сөздер немесе дұрыс құрылған формулалар деп аталады. Формальды тіл көбінесе оның құралу ережелерін қамтитын ресми грамматика, мысалы, тұрақты грамматика немесе контекстсіз грамматика арқылы анықталады. Компьютерлік ғылымда формальды тілдер, басқалармен қатар, бағдарламалау тілдерінің грамматикасын және табиғи тілдердің формалдануға ұшыраған түрлерін анықтау үшін негіз ретінде қолданылады, онда тілдің сөздері мағыналармен немесе семантикамен байланысты ұғымдарды көрсетеді. Есептеу күрделілігі теориясында шешімдерді табуға қойылатын мәселелер әдетте формальды тілдер ретінде беріледі, ал күрделілік кластары – шектеулі есептеу мүмкіндіктері бар машиналармен талдана алатын формальды тілдердің жиынтығы ретінде анықталады. Логика мен математика негіздерінде формальды тілдер аксиоматикалық жүйелердің синтаксисін бейнелеу үшін қолданылады, ал математикалық формализм – математиканың барлық бөлігін осылайша формальды тілдердің синтаксистік өңдеуіне дейін тоғытуға болатын философия. Формальды тілдер теориясы осындай тілдердің таза синтаксистік аспектілерін, яғни олардың ішкі құрылымдық ерекшеліктерін зерттейді. Формальды тілдер теориясы лингвистикадан туындады, ол табиғи тілдердің синтаксистік реттелілігін түсінудің бір жолы ретінде пайда болды.
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well formed according to a specific set of rules called a formal grammar. The alphabet of a formal language consists of symbols, letters, or tokens that concatenate into strings called words. Words that belong to a particular formal language are sometimes called well formed words or well formed formulas. A formal language is often defined by means of a formal grammar such as a regular grammar or context free grammar, which consists of its formation rules. In computer science, formal languages are used, among others, as the basis for defining the grammar of programming languages and formalized versions of subsets of natural languages, in which the words of the language represent concepts that are associated with meanings or semantics. In computational complexity theory, decision problems are typically defined as formal languages, and complexity classes are defined as the sets of the formal languages that can be parsed by machines with limited computational power. In logic and the foundations of mathematics, formal languages are used to represent the syntax of axiomatic systems, and mathematical formalism is the philosophy that all of mathematics can be reduced to the syntactic manipulation of formal languages in this way. The field of formal language theory studies primarily the purely syntactic aspects of such languages—that is, their internal structural patterns. Formal language theory sprang out of linguistics, as a way of understanding the syntactic regularities of natural languages.
Тарих
XVII ғасырда Готфрид Лейбниц пиктограммаларды қолданатын универсалды және формалды тіл – characteristica universalis-ті ойлап тапты және сипаттады. Кейін Карл Фридрих Гаусс Гаусс кодтарының мәселесін зерттеді. Готтлоб Фреге Лейбництің идеяларын жүзеге асыруға тырысты, осы мақсатта алғаш рет "Begriffsschrift" (1879) еңбегінде сипатталған және оның 2 томдық "Grundgesetze der Arithmetik" (1893/1903) еңбегінде толыққанды дамыған белгілеу жүйесін пайдаланды. Бұл «таза тілдің формалды тілін» сипаттады. ХХ ғасырдың бірінші жартысында формалды тілдерге қатысты бірнеше маңызды жетістіктер болды. Аксель Тью 1906 және 1914 жылдар аралығында сөздер мен тілге қатысты төрт мақала жариялады. Соңғысы кейіннен Эмиль Пост «Тьюе жүйелері» деп атаған, ал шешілмейтін мәселенің алғашқы мысалын ұсынды. Пост бұл мақаланы 1947 жылы «жартылай топтар үшін сөз мәселесінің рекурсивті түрде шешілмейтінін» дәлелдеу үшін негіз ретінде пайдаланды және кейіннен формалды тілдерді құрудың канондық жүйесін жасады. 1907 жылы Леонардо Торрес Квеведо Венада механикалық суреттерді (механикалық құрылғыларды) сипаттау үшін формалды тілді енгізді. Ол «Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas» («Машиналарды сипаттауды жеңілдетуге арналған белгілер мен символдар жүйесі туралы») атты еңбегін жариялады. Хайнц Земанек оны машина құралын сандық басқаруға арналған бағдарламалау тіліне балама деп бағалады. Ноам Чомский формалды және табиғи тілдердің абстрактілі бейнесін жасады, ол Чомский иерархиясы деп белгілі. 1959 жылы Джон Бэкус FORTRAN құрудағы жұмысынан кейін жоғары деңгейдегі бағдарламалау тілінің синтаксисін сипаттау үшін Backus-Naur формасын әзірледі. Питер Наур ALGOL60 есебінің хатшысы/редакторы болды, онда ол ALGOL60-тың формалды бөлігін сипаттау үшін Backus-Naur формасын қолданды.
In the 17th century, Gottfried Leibniz imagined and described the characteristica universalis, a universal and formal language which utilised pictographs. Later, Carl Friedrich Gauss investigated the problem of Gauss codes. Gottlob Frege attempted to realize Leibniz's ideas, through a notational system first outlined in Begriffsschrift (1879) and more fully developed in his 2 volume Grundgesetze der Arithmetik (1893/1903). This described a "formal language of pure language." In the first half of the 20th century, several developments were made with relevance to formal languages. Axel Thue published four papers relating to words and language between 1906 and 1914. The last of these introduced what Emil Post later termed 'Thue Systems', and gave an early example of an undecidable problem. Post would later use this paper as the basis for a 1947 proof "that the word problem for semigroups was recursively insoluble", and later devised the canonical system for the creation of formal languages. In 1907, Leonardo Torres Quevedo introduced a formal language for the description of mechanical drawings (mechanical devices), in Vienna. He published "Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas" ("On a system of notations and symbols intended to facilitate the description of machines"). Heinz Zemanek rated it as an equivalent to a programming language for the numerical control of machine tools. Noam Chomsky devised an abstract representation of formal and natural languages, known as the Chomsky hierarchy. In 1959 John Backus developed the Backus Naur form to describe the syntax of a high level programming language, following his work in the creation of FORTRAN. Peter Naur was the secretary/editor for the ALGOL60 Report in which he used Backus–Naur form to describe the Formal part of ALGOL60.
Әліпбидегі сөздер
Алфавит, формалды тілдер контекстінде, кез келген жиын болуы мүмкін; оның элементтері әріптер деп аталады. Алфавитта шексіз көп элементтер болуы мүмкін; мысалы, бірінші реттік логика көбінесе ∧, ¬, ∀ және жақшалар сияқты символдардан өзге, x0, x1, x2 сияқты шексіз көп элементтерді қамтиды, олар айнымалылар рөлін атқарады. Дегенмен, формалды тіл теориясындағы көптеген анықтамалар шектеулі элементтері бар алфавиттерді көрсетеді, және көптеген нәтижелер тек оларға ғана қатысты. Көбінесе, сөзді оның әдеттегі мағынасында немесе ASCII немесе Unicode сияқты кез келген шектеулі таңбалық кодтауды қолдану орынды. Алфавит бойынша сөз – әріптердің кез келген шекті тізбегі (яғни, жол) болуы мүмкін. Алфавит Σ бойынша барлық сөздер жиыны әдетте Σ* (Клине жұлдызын пайдаланып) деп белгіленеді. Сөздің ұзындығы – оны құрайтын әріптер саны. Кез келген алфавит үшін ұзындығы 0 болатын бір ғана сөз бар, ол бос сөз, оны көбінесе e, ε, λ немесе тіпті Λ арқылы белгілейді. Сөздерді біріктіру арқылы екі сөзді жаңа сөз құрауға болады, оның ұзындығы бастапқы сөздердің ұзындықтарының қосындысына тең. Сөзді бос сөзбен біріктірудің нәтижесі бастапқы сөз болады. Кейбір қолданыстарда, әсіресе логикада, алфавит сөздік деп те аталады, ал сөздер формулалар немесе сөйлемдер деп белгіленеді; бұл әріп/сөз метафорасын жойып, оны сөз/сөйлем метафорасымен алмастырады.
An alphabet, in the context of formal languages, can be any set; its elements are called letters. An alphabet may contain an infinite number of elements;For example, first order logic is often expressed using an alphabet that, besides symbols such as ∧, ¬, ∀ and parentheses, contains infinitely many elements x0, x1, x2, that play the role of variables. however, most definitions in formal language theory specify alphabets with a finite number of elements, and many results apply only to them. It often makes sense to use an alphabet in the usual sense of the word, or more generally any finite character encoding such as ASCII or Unicode. A word over an alphabet can be any finite sequence (i. e., string) of letters. The set of all words over an alphabet Σ is usually denoted by Σ* (using the Kleene star). The length of a word is the number of letters it is composed of. For any alphabet, there is only one word of length 0, the empty word, which is often denoted by e, ε, λ or even Λ. By concatenation one can combine two words to form a new word, whose length is the sum of the lengths of the original words. The result of concatenating a word with the empty word is the original word. In some applications, especially in logic, the alphabet is also known as the vocabulary and words are known as formulas or sentences; this breaks the letter/word metaphor and replaces it by a word/sentence metaphor.
Анықтама
Формальды тіл L, алфавит Σ үстінде, Σ* жиынының ішкі жиыны болып табылады, яғни, бұл алфавиттен құралған сөздердің жиынтығы. Кейде сөздер жиынтығы тіркестерге топтастырылады, ал "дұрыс құрылған тіркестерді" жасау үшін ережелер мен шектеулер белгіленеді. Компьютер ғылымы мен математикада, әдетте жаратылыс тілдерімен жұмыс істемейтін жағдайларда, "формальды" деген сөз жиі артық деп есептеледі. Формальды тілдер теориясы көбінесе синтаксистік ережелермен сипатталатын формальды тілдерді зерттейді, бірақ "формальды тіл" ұғымының нақты анықтамасы осылай болады: берілген алфавиттен құралған, шекті ұзындығы бар (мүмкін шексіз) жолдардың жиынтығы, одан артық немесе кем емес. Іс жүзінде, ережелермен сипатталатын көптеген тілдер бар, мысалы, реттелген тілдер немесе контекстсіз тілдер. Формальды грамматика ұғымы, синтаксистік ережелермен сипатталған "тіл" деген түсінікке жақын болуы мүмкін. Анықтаманы шартты түрде пайдалану арқылы, нақты формальды тіл оны сипаттайтын формальды грамматикамен байланыстырылып қарастырылады.
A formal language L over an alphabet Σ is a subset of Σ*, that is, a set of words over that alphabet. Sometimes the sets of words are grouped into expressions, whereas rules and constraints may be formulated for the creation of 'well formed expressions'. In computer science and mathematics, which do not usually deal with natural languages, the adjective "formal" is often omitted as redundant. While formal language theory usually concerns itself with formal languages that are described by some syntactic rules, the actual definition of the concept "formal language" is only as above: a (possibly infinite) set of finite length strings composed from a given alphabet, no more and no less. In practice, there are many languages that can be described by rules, such as regular languages or context free languages. The notion of a formal grammar may be closer to the intuitive concept of a "language", one described by syntactic rules. By an abuse of the definition, a particular formal language is often thought of as being accompanied with a formal grammar that describes it.
Бағдарламалау тілдері
Компилятордың әдетте екі ерекше компоненті болады. Лексикалық талдаушы, кейде lex сияқты құралмен жасалатын, бағдарламалау тілінің грамматикасының символдары – мысалы, идентификаторлар немесе кілт сөздер, сандық және жол мәндері, тыныш белгілер мен операторлар – анықтайды. Бұл символдардың өзі әдетте тұрақты өрнектер арқылы сипатталатын, қарапайым формальды тілмен беріледі. Ең қарапайым түсінік деңгейінде, талдаушы, кейде yacc сияқты талдау генераторымен жасалатын, бастапқы бағдарламаның синтаксистік жағынан дұрыс екенін, яғни компилятор құрылған бағдарламалау тілінің грамматикасына сәйкес келіп, дұрыс құрылғандығын анықтауға тырысады. Әрине, компиляторлар бастапқы кодты талдаудан басқа да көп жұмыс жасайды – олар оны көбінесе орындалатын форматқа аударады. Сондықтан талдаушы әдетте "иә" немесе "жоқ" деген жауаптан гөрі көп нәрсе шығарады, көбінесе абстрактілі синтаксистік ағаш түрінде. Бұл компилятордың келесі кезеңдерінде аппараттық құрылғыда тікелей орындалатын машиналық кодты немесе виртуалды машинада орындалуын қажет ететін аралық кодты қамтитын орындалатын файлды жасау үшін қолданылады.
A compiler usually has two distinct components. A lexical analyzer, sometimes generated by a tool like lex, identifies the tokens of the programming language grammar, e. g. identifiers or keywords, numeric and string literals, punctuation and operator symbols, which are themselves specified by a simpler formal language, usually by means of regular expressions. At the most basic conceptual level, a parser, sometimes generated by a parser generator like yacc, attempts to decide if the source program is syntactically valid, that is if it is well formed with respect to the programming language grammar for which the compiler was built. Of course, compilers do more than just parse the source code – they usually translate it into some executable format. Because of this, a parser usually outputs more than a yes/no answer, typically an abstract syntax tree. This is used by subsequent stages of the compiler to eventually generate an executable containing machine code that runs directly on the hardware, or some intermediate code that requires a virtual machine to execute.
Формалды теориялар, жүйелер және дәлелдемелер
Математикалық логикада формальды теория – формальды тілде білдірілген сөйлемдер жиынтығы. Формальды жүйе (сондай-ақ логикалық есептеу немесе логикалық система деп аталады) формальды тіл мен дедуктивті аппараттан (сондай-ақ дедуктивті жүйе деп аталады) тұрады. Дедуктивті аппарат трансформация ережелері жиынтығынан – олар жарамды қорытынды ережелері ретінде қарастырылуы мүмкін, немесе аксиомалар жиынтығынан, немесе екеуінен де құралуы мүмкін. Формальды жүйе бір немесе бірнеше өрнектерден басқа бір өрнекті шығару үшін қолданылады. Формальды тілді оның формулалары арқылы анықтауға болады, бірақ формальды жүйені оның теоремалары арқылы анықтауға болмайды. Екі формальды жүйе бірдей теоремаларға ие болуы мүмкін, бірақ олар маңызды дәлелдемелік жағынан ерекшеленуі мүмкін (мысалы, А формуласы Б формуласының синтаксистік салдары біреуінде болса, екіншісінде болмауы мүмкін). Формальды дәлел немесе туынды – жақсы құрылған формулалардың шекті тізбегі (оларды сөйлемдер немесе пікірлер ретінде қарастыруға болады), олардың әрқайсысы аксиома болып табылады немесе тізбектегі алдыңғы формулалардан қорытынды ережесі арқылы туындайды. Тізбектегі соңғы сөйлем – формальды жүйенің теоремасы. Формальды дәлелдемелер пайдалы, себебі олардың теоремаларын нақты пікірлер ретінде қарастыруға болады.
In mathematical logic, a formal theory is a set of sentences expressed in a formal language. A formal system (also called a logical calculus, or a logical system) consists of a formal language together with a deductive apparatus (also called a deductive system). The deductive apparatus may consist of a set of transformation rules, which may be interpreted as valid rules of inference, or a set of axioms, or have both. A formal system is used to derive one expression from one or more other expressions. Although a formal language can be identified with its formulas, a formal system cannot be likewise identified by its theorems. Two formal systems and may have all the same theorems and yet differ in some significant proof theoretic way (a formula A may be a syntactic consequence of a formula B in one but not another for instance). A formal proof or derivation is a finite sequence of well formed formulas (which may be interpreted as sentences, or propositions) each of which is an axiom or follows from the preceding formulas in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system. Formal proofs are useful because their theorems can be interpreted as true propositions.
Түсіндірмелер мен үлгілер
Ресми тілдер табиғаты жағынан толыққанды синтаксистік болып табылады, бірақ тіл элементтеріне мағына беруге мүмкіндік беретін семантикамен жабдықталуы мүмкін. Мысалы, математикалық логикада нақты бір логиканың барлық мүмкін формулалар жиыны формальды тіл болып саналады, ал интерпретация әрбір формулаға мағына тағайындайды – әдетте, шындық мәнін. Формальды тілдердің интерпретацияларын зерттеу ресми семантика деп аталады. Математикалық логикада бұл көбінесе модельдер теориясы арқылы жүзеге асырылады. Модельдер теориясында формулаларда кездесетін терминдер математикалық құрылымдардағы объектілер ретінде интерпретацияланады, ал белгілі бір құралымдық интерпретация ережелері формуланың шындық мәнін оның терминдерінің интерпретациясынан қалай шығаруға болатынын анықтайды; формуланың моделі – бұл формуланың шындыққа айналуын қамтамасыз ететін терминдердің интерпретациясы.
Formal languages are entirely syntactic in nature, but may be given semantics that give meaning to the elements of the language. For instance, in mathematical logic, the set of possible formulas of a particular logic is a formal language, and an interpretation assigns a meaning to each of the formulas—usually, a truth value. The study of interpretations of formal languages is called formal semantics. In mathematical logic, this is often done in terms of model theory. In model theory, the terms that occur in a formula are interpreted as objects within mathematical structures, and fixed compositional interpretation rules determine how the truth value of the formula can be derived from the interpretation of its terms; a model for a formula is an interpretation of terms such that the formula becomes true.