Есептеудегі шешілмейтін мәселе: Гильберт пен Аккерманның 1928 жылғы сынағы. Универсалды жарамдылықты анықтайтын алгоритм жоқ екені дәлелденді. Тьюринг машинасы, логика.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Компьютерлік ғылымдағы шешілмейтін міндет
Impossible task in computing
Математика мен компьютерлік ғылымда ; ) – Дэвид Гилберт пен Вильгельм Акерман 1928 жылы қойған қиын мәселе. Мәселе бір мәлімдемені кіріс ретінде қарастырып, мәлімдеме әмбебап түрде дұрыс па, яғни барлық құрылымдарда дұрыс па, соған қарай "иә" немесе "жоқ" деп жауап беретін алгоритмді табуды талап етеді.
In mathematics and computer science, the ; ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "yes" or "no" according to whether the statement is universally valid, i. e., valid in every structure.
Толықтық теоремасы
Бірінші реттік логиканың толықтық теоремасы бойынша, бір мәлімдеме жалпыға бірдей жарамды егер және тек қана ол логикалық ережелер мен аксиомалар арқылы шығарыла алса. Сондықтан, Entscheidungsproblem мәселесін берілген мәлімдемені логика ережелерін қолдана отырып дәлелдеуге болатынын анықтайтын алгоритмді табу туралы сұрақ ретінде де қарастыруға болады. 1936 жылы Алонзо Черч және Алан Тьюринг тәуелсіз зерттемелер жариялап, "нақты есептелетін" интуитивті ұғымы Тьюринг машинасымен есептелетін функциялармен (немесе эквивалентті түрде, лямбда-есептеуде берілетіндермен) сипатталса, онда Entscheidungsproblem-нің жалпы шешімі болмайтынын көрсетті. Бұл болжам қазір Черч-Тьюринг тезисі деп белгілі.
By the completeness theorem of first order logic, a statement is universally valid if and only if it can be deduced using logical rules and axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable using the rules of logic. In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notion of "effectively calculable" is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus). This assumption is now known as the Church–Turing thesis.
Проблеманың тарихы
Entscheidungsproblem мәселесінің бастауы Готфрид Лейбницке дейін жетеді, ол XVII ғасырда сәтті механикалық есептеу машинасы құрастырғаннан кейін, математикалық тұжырымдардың дұрыстығын анықтау үшін символдармен жұмыс істейтін машина жасау армандады. Ол алғашқы қадамның нақты формалды тіл болуы керектігін түсінді, ал оның кейінгі еңбектерінің көп бөлігі осы мақсатқа бағытталды. 1928 жылы Дэвид Гильберт және Вильгельм Аккерман мәселені жоғарыда көрсетілгендей қойды. Өзінің "бағдарламасын" жалғастыра отырып, Гильберт 1928 жылы халықаралық конференцияда үш сұрақ қойды, олардың үшіншісі "Гильберттің Entscheidungsproblem" деп белгілі болды. 1929 жылы Мозес Шёнфинкель Пол Бернейс дайындаған шешім мәселесінің арнайы жағдайлары туралы бір мақала жариялады. 1930 жылға дейін Гильберт шешілмейтін мәселелердің бола қоймауына сенді.
The origin of the Entscheidungsproblem goes back to Gottfried Leibniz, who in the seventeenth century, after having constructed a successful mechanical calculating machine, dreamt of building a machine that could manipulate symbols in order to determine the truth values of mathematical statements. He realized that the first step would have to be a clean formal language, and much of his subsequent work was directed toward that goal. In 1928, David Hilbert and Wilhelm Ackermann posed the question in the form outlined above. In continuation of his "program", Hilbert posed three questions at an international conference in 1928, the third of which became known as "Hilbert's Entscheidungsproblem". In 1929, Moses Schönfinkel published one paper on special cases of the decision problem, that was prepared by Paul Bernays. As late as 1930, Hilbert believed that there would be no such thing as an unsolvable problem.
Жоқ жауап
Бұл сұраққа жауап беру үшін "алгоритм" ұғымын ресми түрде анықтау қажет болды. Бұл 1935 жылы Алонзо Черч өзінің λ-саны негізінде "тиімді есептеу" концепциясымен, ал келесі жылы Алан Тьюринг өзінің Тьюринг машиналары концепциясымен іске асырылды. Тьюринг бұл есептеудің эквивалентті модельдер екенін бірден мойындады. Ессектюнгс проблемасына теріс жауапты 1935–36 жылдары Алонзо Черч (Черч теоремасы) және одан кейін көп ұзамай 1936 жылы Алан Тьюринг (Тьюрингтің дәлелі) берді. Черч екі λ-сандық өрнектің тең немесе тең емес екенін анықтайтын есептелетін функцияның жоқтығын дәлелдеді. Ол Стивен Клиннің бұрынғы еңбектеріне көп сүйенді. Тьюринг Ессектюнгс проблемасын шеше алатын "алгоритм" немесе "жалпы әдіс" бар ма деген мәселені, кез келген Тьюринг машинасының тоқтауы немесе тоқтамауы туралы шешім қабылдайтын "жалпы әдіс" бар ма деген сұраққа дейін тоғыстырды (тоқтау мәселесі). Егер "алгоритм" Тьюринг машинасы түрінде бейнеленетін әдіс ретінде түсінілсе және соңғы сұраққа жауап теріс болса (жалпы алғанда), Ессектюнгс проблемасы үшін алгоритмнің болуы туралы сұрақ та теріс болуы керек (жалпы алғанда). 1936 жылғы мақаласында Тьюринг былай деді: "Әр есептеу машинасына 'ол' сәйкес формула 'Un(ол)' құрастырылады және егер 'Un(ол)' дәлелденетінін анықтаудың жалпы әдісі болса, онда 'ол' ешқашан 0-ді басып шығаратынын анықтаудың жалпы әдісі бар екенін көрсетеміз". Черч пен Тьюрингтің жұмысына Курт Гёдельдің өзінің толық еместік теоремасы бойынша бұрынғы еңбектерінің, әсіресе логиканы арифметикаға дейін тоғыстыру үшін логикалық формулаларға сандарды (Гёдель нөмірлеуі) тағайындау әдісінің үлкен әсері тиді. Ессектюнгс проблемасы Хилберттің оныншы проблемасымен байланысты, ол Диофанти теңдеулерінің шешімі бар ма, жоқ па, оны анықтау үшін алгоритмді сұрайды. Мұндай алгоритмнің жоқ екендігі, Юрий Матиясевич, Джулия Робинсон, Мартин Дэвис және Хилари Путнамның жұмысымен, 1970 жылы дәлелдеудің соңғы бөлігімен расталды, сонымен қатар Ессектюнгс проблемасына теріс жауап береді.
Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by Alonzo Church in 1935 with the concept of "effective calculability" based on his λ calculus, and by Alan Turing the next year with his concept of Turing machines. Turing immediately recognized that these are equivalent models of computation. A negative answer to the Entscheidungsproblem was then given by Alonzo Church in 1935–36 (Church's theorem) and independently shortly thereafter by Alan Turing in 1936 (Turing's proof). Church proved that there is no computable function which decides, for two given λ calculus expressions, whether they are equivalent or not. He relied heavily on earlier work by Stephen Kleene. Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the Entscheidungsproblem to the question of the existence of a 'general method' which decides whether any given Turing machine halts or not (the halting problem). If 'algorithm' is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the Entscheidungsproblem also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0". The work of both Church and Turing was heavily influenced by Kurt Gödel's earlier work on his incompleteness theorem, especially by the method of assigning numbers (a Gödel numbering) to logical formulas in order to reduce logic to arithmetic. The Entscheidungsproblem is related to Hilbert's tenth problem, which asks for an algorithm to decide whether Diophantine equations have a solution. The non existence of such an algorithm, established by the work of Yuri Matiyasevich, Julia Robinson, Martin Davis, and Hilary Putnam, with the final piece of the proof in 1970, also implies a negative answer to the Entscheidungsproblem.
Жалпылау
Дедукция теоремасын қолдана отырып, Entscheidungsproblem берілген бірінші реттік сөйлемнің, берілген шекті жиын сөйлемдерден логикалық түрде туындайтынын анықтаудің көбірек жалпылама проблемасын қамтиды, бірақ шексіз көп аксиомасы бар бірінші реттік теориялардағы дұрыстықты тікелей Entscheidungsproblem-ге келтіруге болмайды. Дегенмен, мұндай көбірек жалпылама шешу проблемалары практикалық тұрғыдан маңызды. Кейбір бірінші реттік теориялар алгоритмдік тұрғыдан шешіледі; мысалы, Пресбургер арифметикасы, нақты жабық өрістер және көптеген бағдарламалау тілдерінің статикалық типтік жүйелері. Ал, Пеано аксиомаларымен берілген қосу және көбейту операциялары бар натурал сандардың бірінші реттік теориясы алгоритм арқылы шешілмейді.
Using the deduction theorem, the Entscheidungsproblem encompasses the more general problem of deciding whether a given first order sentence is entailed by a given finite set of sentences, but validity in first order theories with infinitely many axioms cannot be directly reduced to the Entscheidungsproblem. Such more general decision problems are, however, of practical interest. Some first order theories are algorithmically decidable; examples of this include Presburger arithmetic, real closed fields, and static type systems of many programming languages. On the other hand, the first order theory of the natural numbers with addition and multiplication expressed by Peano's axioms cannot be decided with an algorithm.
Фрагменттер
Әдетте, бөлімдегі сілтемелер Пратт Хартманнан (2023). Классикалық Entscheidungsproblem бірінші реттік формула берілген кезде, оның барлық модельдерде ақиқат екенін сұрайды. Шектеулі мәселе барлық шекті модельдерде ақиқат екенін сұрайды. Трахтенброт теоремасы бұл да шешілмейтінін көрсетеді. Кез келген үшін EXPTIME-толық (5.4.1-бөлім). Кез келген үшін NEXPTIME-толық (5.4.2-бөлім). Бұл нәтижені бірінші болып Акерманн жариялаған. Кез келген және PSPACE-толық (5.4.3-бөлім). Börger және авторлар (2001) квантор префиксі, функцияның аргумент саны, предикаттың аргумент саны және теңдік/теңсіздіктің барлық мүмкін комбинациялары бар әрбір мүмкін фрагмент үшін есептеу күрделілігінің деңгейін сипаттайды.
By default, the citations in the section are from Pratt Hartmann (2023). The classical Entscheidungsproblem asks that, given a first order formula, whether it is true in all models. The finitary problem asks whether it is true in all finite models. Trakhtenbrot's theorem shows that this is also undecidable. For any , is EXPTIME complete (Section 5.4.1). For any , is NEXPTIME complete (Section 5.4.2). This implies that is decidable, a result first published by Ackermann. For any , and are PSPACE complete (Section 5.4.3). Börger et al. (2001) describes the level of computational complexity for every possible fragment with every possible combination of quantifier prefix, functional arity, predicate arity, and equality/no equality.
Шешім қабылдаудың практикалық тәртібі
Логикалық формулалардың кластары үшін практикалық шешімдерді анықтау процедуралары бағдарламалық қамтамасыздылықты тексеру және схемаларды тексеру үшін маңызды. Таза Буль логикалық формулалары көбінесе DPLL алгоритміне негізделген SAT шешу техникаларын қолдану арқылы шешіледі. Бірінші реттік теориялардың күрделі шешім мәселелері үшін сызықтық нақты немесе рационал арифметикадағы конъюнкциялар симплекс алгоритмі арқылы, ал сызықтық бүтін арифметикадағы (Пресбургер арифметикасы) формулалар Купер алгоритмі немесе Уильям Пьюгтың Омега тесті арқылы шешіледі. Жоқтаулар, конъюнкциялар және дизъюнкцияларды қамтитын формулалар қанағаттандырылатындығын тексеру қиындықтарын конъюнкцияларды шешу қиындықтарымен біріктіреді; қазіргі таңдағы олар көбінесе SMT шешу техникаларын қолдану арқылы шешіледі, бұл SAT шешуді конъюнкциялар үшін процедуралармен және тарату техникаларымен біріктіреді. Нақты жабық өрістер теориясы деп те аталатын нақты полиномдық арифметика шешімді; бұл Тарски-Сейденберг теоремасы, ол цилиндрлік алгебралық декомпозицияны пайдалану арқылы компьютерлерде іске асырылған.
Having practical decision procedures for classes of logical formulas is of considerable interest for program verification and circuit verification. Pure Boolean logical formulas are usually decided using SAT solving techniques based on the DPLL algorithm. For more general decision problems of first order theories, conjunctive formulas over linear real or rational arithmetic can be decided using the simplex algorithm, formulas in linear integer arithmetic (Presburger arithmetic) can be decided using Cooper's algorithm or William Pugh's Omega test. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT solving techniques, which combine SAT solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of real closed fields, is decidable; this is the Tarski–Seidenberg theorem, which has been implemented in computers by using the cylindrical algebraic decomposition.