Логика және компьютер ғылымы: теория мен қолданыс

Кіріспе

академиялық конференция LICS Академиялық пән Компьютерлік ғылымдағы логика логика және компьютерлік ғылым салаларының арасындағы байланысты қамтиды. Бұл тақырыпты үш негізгі салаға бөлуге болады: Теориялық негіздер және талдау Логика мамандарына көмек көрсету үшін компьютерлік технологияны пайдалану Логикалық ұғымдарды компьютерлік қолданбаларда қолдану.

Теориялық негіздер мен талдау

Логика компьютерлік ғылымда маңызды рөл атқарады. Логиканың ең маңызды салаларының кейбірі – есептеу теориясы (бұрын рекурсия теориясы деп аталатын), модальдық логика және категория теориясы. Есептеу теориясы Алонзо Черч және Алан Тьюринг сияқты логиктер мен математиктер анықтаған ұғымдарға негізделген. Черч алғаш рет өзінің лямбда-анықтамасы (lambda definability) ұғымын пайдаланып, алгоритмдік шешімі жоқ проблемалардың бар екенін көрсетті. Тьюринг «механикалық процедура» деп аталатын нәрсенің тұңғыш толыққанды талдауын жасады, ал Курт Гёдель Тьюрингтің талдауын «үлкен» деп бағалағанын айтты. Сонымен қатар, логика мен компьютерлік ғылым арасындағы теориялық байланыстың маңызды салалары:
Гёдельдің толық еместік теоремасы арифметиканы сипаттауға жеткілікті күшті кез келген логикалық жүйеде дәлелдеуге не жоққа шығаруға болмайтын мәлімдемелер болатынын дәлелдейді. Бұл бағдарламалық қамтамастың толықтығы мен дұрыстығын дәлелдеу мүмкіндігіне қатысты теориялық мәселелерге тікелей қатысты. Фрейм мәселесі – жасанды интеллект агентінің мақсаттары мен оның ортасының күйін бірінші реттік логика арқылы бейнелеген кезде шешілуі тиіс негізгі мәселе. Карри-Говард сәйкестігі – логикалық жүйелер мен бағдарламалау тілдері арасындағы байланыс. Бұл теория дәлелдер мен бағдарламалар арасында нақты сәйкестік орнатады. Атап айтқанда, қарапайым типтелген лямбда-есептеудегі терминдер интуициялық пропозициялық логиканың дәлелдеріне сәйкес екенін көрсетті. Категория теориясы – математиканы құрылымдар арасындағы қатынастарды баса назарлайтын тұрғысынан қарастырады. Ол компьютерлік ғылымның көптеген салаларымен тығыз байланысты: бағдарламалау тілдерінің типтік жүйелері, өту жүйелерінің теориясы, бағдарламалау тілдерінің модельдері және бағдарламалау тілдерінің семантикасы теориясы. Логикалық бағдарламалау – формалды логикаға негізделген бағдарламалау, деректер базасы және білімді ұсыну парадигмасы. Логикалық бағдарлама – белгілі бір проблемалық сала туралы мәлімдемелер жиынтығы. Есептеулер логикалық қорыту арқылы осы саладағы мәселелерді шешу арқылы жүзеге асырылады. Басты логикалық бағдарламалау тілдерінің отбасыларына Prolog, Answer Set Programming (ASP) және Datalog жатады.

Logic plays a fundamental role in computer science. Some of the key areas of logic that are particularly significant are computability theory (formerly called recursion theory), modal logic and category theory. The theory of computation is based on concepts defined by logicians and mathematicians such as Alonzo Church and Alan Turing. Church first showed the existence of algorithmically unsolvable problems using his notion of lambda definability. Turing gave the first compelling analysis of what can be called a mechanical procedure and Kurt Gödel asserted that he found Turing's analysis "perfect.". In addition some other major areas of theoretical overlap between logic and computer science are:
Gödel's incompleteness theorem proves that any logical system powerful enough to characterize arithmetic will contain statements that can neither be proved nor disproved within that system. This has direct application to theoretical issues relating to the feasibility of proving the completeness and correctness of software. The frame problem is a basic problem that must be overcome when using first order logic to represent the goals of an artificial intelligence agent and the state of its environment. The Curry–Howard correspondence is a relation between logical systems and programming languages. This theory established a precise correspondence between proofs and programs. In particular it showed that terms in the simply typed lambda calculus correspond to proofs of intuitionistic propositional logic. Category theory represents a view of mathematics that emphasizes the relations between structures. It is intimately tied to many aspects of computer science: type systems for programming languages, the theory of transition systems, models of programming languages and the theory of programming language semantics. Logic programming is a programming, database and knowledge representation paradigm that is based on formal logic. A logic program is a set of sentences about some problem domain. Computation is performed by applying logical reasoning to solve problems in the domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog.

Логикалық зерттеушілерге көмекші компьютерлер

Жасанды интеллект терминін алғаш қолданғандардың бірі 1956 жылы Аллен Ньюэлл, Клифф Шоу және Герберт Саймон жасаған «Логикалық теоретик» жүйесі болды. Логиктердің атқаратын жұмыстарының бірі – логикадағы бірнеше тұжырымды алып, логика заңдарына сәйкес дұрыс болуға тиіс қорытындыларды (қосымша тұжырымдарды) шығару болып табылады. Мысалы, егер «Барлық адамдар өлдір» және «Сократ – адам» деген тұжырымдар берілсе, онда «Сократ өлдір» деген қорытынды дұрыс болады. Әрине, бұл өте қарапайым мысал ғана. Шын мәніндегі логикалық жүйелерде тұжырымдар көптеген және күрделі болуы мүмкін. Осындай талдауды компьютерлердің көмегімен жүргізуге болатыны ерте түсінілді. «Логикалық теоретик» Бертран Рассел мен Альфред Норт Уайтхедтің математикалық логика саласындағы «Principia Mathematica» атты әсерлі еңбегіндегі теориялық жұмыстарын растады. Бұдан бөлек, кейінгі жүйелер логиктерге жаңа математикалық теоремалар мен дәлелдерді тексеруге және табуға көмектесті.

Компьютерлер үшін логикалық қолданбалар

Жасанды интеллект (ЖИ) саласында математикалық логиканың әрдайым күшті ықпалы болды. Саланың бастапқы кезеңдерінен-ақ логикалық қорытындыларды автоматтандыру технологиясының мәселелерді шешуге және фактілерден тұжырымдар жасауға зор мүмкіндік беретіні түсінілді. Рон Брахман бірінші реттік логиканы (FOL) барлық ЖИ білімді бейнелеу формализмдерін бағалау үшін өлшем ретінде сипаттады. Бірінші реттік логика – ақпаратты сипаттау және талдау үшін жалпы және қуатты әдіс. FOL-дің өзі компьютерлік тіл ретінде қолданылмауының себебі, ол өте кең мүмкіндіктерге ие, яғни FOL қаншалықты қуатты болса да, ешбір компьютер шеше алмайтын мәлімдемелерді оңай білдіре алады. Сондықтан, білімді бейнелеудің кез келген түрі белгілі бір дәрежеде кеңдік пен есептеу мүмкіндігі арасындағы компромисс болып табылады. Тіл неғұрлым кең болса және FOL-ге жақын болса, соғұрлым баяу жұмыс істеуі және шексіз циклге түсуі мүмкін. Мысалы, сарапшы жүйелерде қолданылатын ЕГЕР-СОН ережелері FOL-дің өте шектеулі жиынтығына жуықтайды. Логикалық операторлардың толық спектрі бар кездейсоқ формулалардан гөрі, бастапқы нүкте логиктер modus ponens деп атаған нәрсе. Нәтижесінде, ережелерге негізделген жүйелер жоғары өнімді есептеулерді қолдауға болады, әсіресе олар оңтайландыру алгоритмдері мен компиляцияны пайдаланса. Екінші жағынан, логикалық бағдарламалау, бірінші реттік логиканың Хорн клаузасының қосалқы жиынтығын монотонды емес жорамал формасымен біріктіреді, ол жоғары кеңдікке және тиімді іске асыруға ие. Атап айтқанда, логикалық бағдарламалау тілі Prolog – Тьюринг толық бағдарламалау тілі. Datalog рекурсивті қатынастармен реляциялық деректер базасы моделін кеңейтеді, ал жауап жиынтығын бағдарламалау қиын (негізінен NP қиын) іздеу мәселелеріне бағытталған логикалық бағдарламалау түрі. Логикалық теорияны зерттеудің тағы бір маңызды саласы – бағдарламалық жасақтама жасау. Білімге негізделген бағдарламалық қамтамасыз ету көмекшісі және бағдарламалаушы шәкірті сияқты ғылыми-зерттеу жобалары бағдарламалық қамтамасыз ету ерекшеліктерінің дұрыстығын растау үшін логикалық теорияны қолданды. Олар сондай-ақ түрлі платформаларда ерекшеліктерді тиімді кодқа айналдыру және іске асыру мен ерекшелік арасындағы теңдікті дәлелдеу үшін логикалық құралдарды қолданды. Бұл формалды трансформацияға бағытталған тәсіл көбінесе дәстүрлі бағдарламалық жасақтаманы әзірлеуден әлдеқайда күшті күш-жігерді қажет етеді. Алайда, тиісті формализмдер мен қайта пайдалануға болатын үлгілер бар нақты салаларда бұл тәсіл коммерциялық өнімдер үшін тиімді болып шықты. Тиісті салалар, әдетте, қару-жарақ жүйелері, қауіпсіздік жүйелері және нақты уақыт қаржылық жүйелері сияқты жүйелердің бұзылуы адам немесе қаржылық шығындар өте жоғары салалар. Мұндай саланың мысалы – өте үлкен масштабтағы интегралды (VLSI) дизайн – цифрлық құрылғылардың CPU және басқа да маңызды компоненттерінде қолданылатын микросхемаларды жобалау процесі. Чиптегі қате апатты болуы мүмкін. Бағдарламалық жасақтамадан айырмашылығы, чиптерді жаңартуға немесе түзетуге болмайды. Сондықтан, іске асыру спецификацияға сәйкес келетінін дәлелдеу үшін формалды әдістерді қолданудың коммерциялық негіздемесі бар. Логиканы компьютерлік технологияға қолданудың тағы бір маңызды саласы – фрейм тілдері мен автоматты жіктеуіштер. KL ONE сияқты фрейм тілдерін тікелей жинақ теориясымен және бірінші реттік логикамен байланыстыруға болады. Бұл классификаторлар деп аталатын теоремаларды дәлелдеушілерге берілген модельдегі жиынтықтар, кіші жиынтықтар және қатынастар арасындағы әртүрлі декларацияларды талдауға мүмкіндік береді. Осылайша модельді растауға болады және сәйкес келмейтін анықтамалар белгіленеді. Классификатор сондай-ақ жаңа ақпаратты қорытуға болады, мысалы, қолданыстағы ақпаратқа негізделген жаңа жиынтықтарды анықтау және жаңа деректерге негізделген қолданыстағы жиынтықтардың анықтамасын өзгерту. Интернет әлемінде үнемі өзгеріп отыратын өзгерістерді басқару үшін икемділік деңгейі өте жақсы. Классификатор технологиясы Web Ontology Language сияқты тілдердің үстіне құрылған, ол қолданыстағы Интернеттің үстіне логикалық семантикалық деңгейді қосуға мүмкіндік береді. Бұл қабат Семантикалық Желі деп аталады. Уақытша логика бір мезгілдегі жүйелерде ойлау үшін қолданылады.

There has always been a strong influence from mathematical logic on the field of artificial intelligence (AI). From the beginning of the field it was realized that technology to automate logical inferences could have great potential to solve problems and draw conclusions from facts. Ron Brachman has described first order logic (FOL) as the metric by which all AI knowledge representation formalisms should be evaluated. First order logic is a general and powerful method for describing and analyzing information. The reason FOL itself is simply not used as a computer language is that it is actually too expressive, in the sense that FOL can easily express statements that no computer, no matter how powerful, could ever solve. For this reason every form of knowledge representation is in some sense a trade off between expressivity and computability. The more expressive the language is, the closer it is to FOL, the more likely it is to be slower and prone to an infinite loop. For example, IF–THEN rules used in expert systems approximate to a very limited subset of FOL. Rather than arbitrary formulas with the full range of logical operators the starting point is simply what logicians refer to as modus ponens. As a result, rule based systems can support high performance computation, especially if they take advantage of optimization algorithms and compilation. On the other hand, logic programming, which combines the Horn clause subset of first order logic with a non monotonic form of negation, has both high expressive power and efficient implementations. In particular, the logic programming language Prolog is a Turing complete programming language. Datalog extends the relational database model with recursive relations, while answer set programming is a form of logic programming oriented towards difficult (primarily NP hard) search problems. Another major area of research for logical theory is software engineering. Research projects such as the Knowledge Based Software Assistant and Programmer's Apprentice programs have applied logical theory to validate the correctness of software specifications. They have also used logical tools to transform the specifications into efficient code on diverse platforms and to prove the equivalence between the implementation and the specification. This formal transformation driven approach is often far more effortful than traditional software development. However, in specific domains with appropriate formalisms and reusable templates the approach has proven viable for commercial products. The appropriate domains are usually those such as weapons systems, security systems, and real time financial systems where failure of the system has excessively high human or financial cost. An example of such a domain is Very Large Scale Integrated (VLSI) design—the process for designing the chips used for the CPUs and other critical components of digital devices. An error in a chip can be catastrophic. Unlike software, chips can't be patched or updated. As a result, there is commercial justification for using formal methods to prove that the implementation corresponds to the specification. Another important application of logic to computer technology has been in the area of frame languages and automatic classifiers. Frame languages such as KL ONE can be directly mapped to set theory and first order logic. This allows specialized theorem provers called classifiers to analyze the various declarations between sets, subsets, and relations in a given model. In this way the model can be validated and any inconsistent definitions flagged. The classifier can also infer new information, for example define new sets based on existing information and change the definition of existing sets based on new data. The level of flexibility is ideal for handling the ever changing world of the Internet. Classifier technology is built on top of languages such as the Web Ontology Language to allow a logical semantic level on top of the existing Internet. This layer is called the Semantic Web. Temporal logic is used for reasoning in concurrent systems.