Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
О гипотезах Ходжа, Тэйта и Мамфорда–Тэйта для расслоенных произведений семейств регулярных поверхностей с геометрическим родом 1
Get PDFThe Hodge, Tate and Mumford-Tate conjectures are proved for the fibre product of two non-isotrivial 1-parameter families of regular surfaces with geometric genus 1 under some conditions on degenerated fibres, the ranks of the N\'eron - Severi groups of generic geometric fibres and representations of Hodge groups in transcendental parts of rational cohomology.Let be a projective non-isotrivial family (possibly with degeneracies) over a smooth projective curve . Assume that the discriminant loci are disjoint, for any smooth fibre , and the following conditions hold: for any point and the Picard-Lefschetz transformation , associated with a smooth part of the morphism and with a loop around the point , we have ; the variety , the curve and the structure morphisms are defined over a finitely generated subfield .If for generic geometric fibres \, and \, at least one of the following conditions holds: is an odd prime number, ; the ring is an imaginary quadratic field, is a totally real field or \,\, b_2(X_{1s})- rank NS(X_{1s})\,>\, b_2(X_{2s})- rank NS(X_{2s}) ; ; ,then for the fibre product the Hodge conjecture is true, for any smooth projective -variety with the condition the Tate conjecture on algebraic cycles and the Mumford-Tate conjecture for cohomology of even degree are true.Доказаны гипотезы Ходжа, Тэйта и Мамфорда-Тэйта для расслоенного произведения двух неизотривиальных 1-параметрических семейств регулярных поверхностей с геометрическим родом 1 при некоторых условиях на вырожденные слои, ранги групп Нерона-Севери общих геометрических слоёв семейств и представления групп Ходжа в трансцендентных частях рациональных когомологий.Пусть проективное неизотривиальное семейство поверхностей (возможно, с вырождениями) над гладкой проективной кривой . Предположим, что дискриминантные локусы не пересекаются, для любого гладкого слоя , причём выполнены следующие условия: для любой точки и преобразования Пикара--Лефшеца , ассоциированного с гладкой частью морфизма и с обходом вокруг точки , имеем неравенство ; многообразия , кривая и структурные морфизмы определены над некоторым конечнопорожденным подполем .Если для общих геометрических слоев \, и \, выполнено хотя бы одно из следующих условий: является нечетным числом, ; кольцо - мнимое квадратичное поле, -- вполне вещественное поле или \, b_2(X_{1s})- rank NS(X_{1s})\,>\, b_2(X_{2s})- rank NS(X_{2s}); ; , то для расслоенного произведения верна гипотеза Ходжа, для любого гладкого проективного -многообразия с условием верны гипотеза Тэйта об алгебраических циклах и гипотеза Мамфорда-Тэйта для когомологий чётной степени.Более того, пространство порождается классами дивизоров.
О переносе ряда понятий статистической радиофизики в теорию одномерных точечных отображений
Get PDFIn the article, the possibility of using a bispectrum under the investigation of regular and chaotic behaviour of one-dimensional point mappings is discussed. The effectiveness of the transfer of this concept to nonlinear dynamics was demonstrated by an example of the Feigenbaum mapping. Also in the work, the application of the Kullback-Leibler entropy in the theory of point mappings is considered. It has been shown that this information-like value is able to describe the behaviour of statistical ensembles of one-dimensional mappings. In the framework of this theory some general properties of its behaviour were found out. Constructivity of the Kullback-Leibler entropy in the theory of point mappings was shown by means of its direct calculation for the ”saw tooth” mapping with linear initial probability density. Moreover, for this mapping the denumerable set of initial probability densities hitting into its stationary probability density after a finite number of steps was pointed out. В статье обсуждается возможность использования биспектра при исследовании регулярного и хаотического поведения одномерных точечных отображений. Эффективность трансфера этого понятия в нелинейную динамику продемонстрирована на примере отображения Фейгенбаума. Также в работе рассмотрено применение энтропии Кульбака–Лейблера в теории точечных отображений. Показано, что эта величина информационного характера пригодна для описания поведения статистических ансамблей одномерных отображений. В рамках этой теории выявлены некоторые общие свойства её поведения. Конструктивизм энтропии Кульбака–Лейблера в теории точечных отображений показан также прямым её вычислением для отображения «зуб пилы» с линейным начальным распределением вероятностей. Кроме того, для этого отображения указано счётное множество начальных распределений вероятностей, попадающих в его стационарное распределение вероятностей за конечное число шагов.
Применение нейронных сетей для распознавания конструктивных элементов рельсов на магнитных и вихретоковых дефектограммах
Get PDFTo ensure traffic safety of railway transport, non-destructive test of rails is regularly carried out by using various approaches and methods, including magnetic and eddy current flaw detection methods. An automatic analysis of large data sets (defectgrams) that come from the corresponding equipment is an actual problem. The analysis means a process of determining the presence of defective sections along with identifying structural elements of railway tracks on defectograms. This article is devoted to the problem of recognition of rail structural element images in magnetic and eddy current defectograms. Three classes of rail track structural elements are considered: 1) a bolted joint with straight or beveled connection of rails, 2) a butt weld of rails, and 3) an aluminothermic weld of rails. Images that cannot be assigned to these three classes are conditionally considered as defects and are placed in a separate fourth class. For image recognition of structural elements in defectograms a neural network is applied. The neural network is implemented by using the open library TensorFlow. To this purpose each selected (picked out) area of a defectogram is converted into a graphic image in a grayscale with size of 20 x 39 pixels.Для обеспечения безопасности движения на железнодорожном транспорте регулярно проводится неразрушающий контроль рельсов с применением различных подходов и методов, включая методы магнитной и вихретоковой дефектоскопии. Актуальной задачей является автоматический анализ больших массивов данных (дефектограмм), которые поступают от соответствующего оборудования. Под анализом понимается процесс определения по дефектограммам наличия дефектных участков наряду с выявлением конструктивных элементов рельсового пути. Данная статья посвящена задаче распознавания образов конструктивных элементов железнодорожных рельсов по дефектограммам многоканальных магнитных и вихретоковых дефектоскопов. Рассматриваются три класса конструктивных элементов рельсового пути: 1) болтовой стык с прямым или скошенным соединением рельсов, 2) электроконтактная сварка рельсов и 3) алюмотермитная сварка рельсов. Образы, которые не могут быть отнесены к этим трем классам, условно считаются дефектами и выносятся в отдельный четвертый класс. Для распознавания образов конструктивных элементов на дефектограммах применяется нейронная сеть, реализованная в рамках открытой библиотеки TensorFlow. С этой целью каждая выделенная для анализа область дефектограммы преобразуется в графический образ в градации серого цвета размером 20 на 39 пикселей
О некоторых подходах к решению задачи «Useful Proof-of-work for blockchains»
Get PDFoai:oai.mais.elpub.ru:article/732The blockchain technology is based on the ”Proof-of-work” principles. The essence of this principle is that some event (for example the bill-to-bill money transaction) becomes significant after the confirmation by a certain computer work. So, a demand arose for such computational problems to work on, and we will spend on it about the whole blockchain system computing capacity. Now the main kind of such a problem is a hash-puzzle – the problem to find a bit string with a hash that satisfies some conditions. The important hash-puzzle weakness is the lack of the useful application outside of the blockchain technology. In this work, we offer some approaches to ”Useful Proof-of-work for blockchains” problem, namely, consider some practical variants of the NP-complete problems that could be solved with the help of SAT or LLL-solvers as the Proof-of-Work computational problems. The use of the FPTproblems requires special study. The offered approach allows to provide the following characteristics of the proof-of-work computational problems: usefulness, problems complexity management (through the dimension change, choosing problems of certain kind, the indication of necessary solution precision), mass character. Herewith we admit that not every solved problem can be useful but we consider the opportunity to solve some practical problems with the help of the blockchain technology. Among other things it is also possible to compare the virtual crypto-currency value (through the energy costs spent) and the effective result of the practical problems solution. The most complicated points of the described approach are the realization of the events-problems (providing the computer work for these events) relations and the realization of the problems complexity analysis system. This issue should be viewed as the study program because of many technical details that must be worked out further.Технология блокчейн основана на принципе доказательства работой «Proof-ofwork». Суть данного принципа состоит в том, что некоторое событие (например, перевод денежных средств с одного счета на другой) становится значимым только после того, как оно подтверждено определенным объемом вычислительной работы. Соответственно возникает потребность в вычислительных задачах, над которыми такую работу можно производить, причем на решение этих задач будет тратиться практически вся вычислительная мощность блокчейн-сети. На сегодня в качестве таких задач получили распространение «хэш-головоломки» – задачи поиска битовой строки с хэшем, удовлетворяющим определенным условиям. Существенным недостатком хэш-головоломок является отсутствие у них какого-либо полезного применения за пределами технологии блокчейн. В работе описываются подходы к решению задачи «Useful Proof-of-work for blockchains», а именно предлагается рассматривать в качестве вычислительных задач для доказательства работой возникающие на практике индивидуальные представители NP-полных задач, которые могут решаться, например, SAT- или LLL-решателями. Отдельной проработки требует вопрос об использовании FPT-задач. Предлагаемый подход позволяет обеспечить следующие свойства вычислительных задач для доказательства работой: полезность, управляемость сложностью задач (через изменение размерности, выбор задач определенного вида, указание точности необходимого решения), массовость. При этом допускается, что не каждая решенная задача может оказаться полезной, однако предоставляется возможность решать с помощью технологии блокчейн задачи, возникающие на практике. Кроме прочего, таким образом становится возможным сопоставить стоимость виртуальной криптовалюты через затраты электроэнергии при ее генерации с практическим результатом от решения вычислительных задач. Наиболее трудными вопросами в контексте рассматриваемого подхода являются реализация связи событий и задач, обеспечивающих эти события вычислительной работой, и реализация системы анализа сложности задач. Статью следует воспринимать как программу исследований, поскольку многие технические детали требуют отдельной проработки
О методах верификации и разработки программ развития сельскохозяйственных территорий
Get PDFNowadays, the methods of program-targeted management for the development of various socio-economic systems of complex structure, such as agricultural areas, have become universal. Therefore, the current tasks at hand are the verification of already created development programs and the development of "proper" programs for the development of such systems, by analogy with the verification and development of proper computer programs through developed disciplines in theoretical programming. In this paper, in order to solve the problem of verification of development programs for agricultural territories, a structural scheme of the program is first constructed, through which the axiomatic theory is created, using Hoare’s algorithmic logic system. The main problem in the construction of the axiomatic theory is the development of the axioms of the theory reflecting the preconditions and effects of the implementation of meaningful actions indicated in the text of the development program. The verification of the development program corresponds to the probability of some Hoare triplet, according to the initial and target conditions of the program. For the task of elaboration of the right development programs, the mechanism for constructing a domain model using the PDDL family description languages is described. The description of a specific model is purely declarative in nature and consists of descriptions of predicates and actions of the chosen subject area. In this paper, it is shown how on the described model with the help of intelligent planners, including temporal planners such as OPTIC, solutions to the targets of development programs can be automatically built. Based on expert knowledge and activity standards, a model of an agricultural territory is constructed, a brief description of which is given in the work. The conducted experiments showed the effectiveness of the proposed approach for the development of proper development programs. В настоящее время повсеместными стали методы программно-целевого управления развитием различных социально-экономических систем сложной структуры, например, таких как территории сельскохозяйственного назначения. Поэтому актуальными задачами являются верификация уже созданных программ развития и разработка «правильных» программ развития таких систем, по аналогии с верификацией и разработкой правильных компьютерных программ – развитыми дисциплинами в теоретическом программировании. В данной работе для решения задачи верификации программ развития сельскохозяйственных территорий сначала строится структурная схема программы, по которой создается аксиоматическая теория, использующая аппарат алгоритмических логик Хоара. Основной проблемой при построении аксиоматической теории является разработка аксиом теории, отражающих предусловия и эффекты выполнения содержательных действий, указанных в тексте программы развития. Верификация программы развития соответствует проверке доказуемости некоторой тройки Хоара, соответствующей начальным и целевым условиям программы. Для задачи разработки правильных программ развития описывается механизм построения модели предметной области с использованием языков описания моделей семейства PDDL. Описание конкретной модели имеет чисто декларативный характер и представляет собой набор описаний предикатов и действий выбранной предметной области. Показывается, как на описанной модели с помощью интеллектуальных планировщиков, включая темпоральные планировщики типа OPTIC, автоматически строить решения целевых задач программ развития. На основе экспертных знаний и отраслевых стандартов построена модель сельскохозяйственной территории, краткое описание которой приводится в работе. Проведенные эксперименты показали эффективность предлагаемого подхода к разработке правильных программ развития
Полипрограммы и бисимуляция полипрограмм
No full textA polyprogram is a generalization of a program which admits multiple definitions of a single function. Such objects arise in different transformation systems, such as the Burstall-Darlington framework or equality saturation. In this paper, we introduce the notion of a polyprogram in a non-strict first-order functional language. We define denotational semantics for polyprograms and describe some possible transformations of polyprograms, namely we present several main transformations in two different styles: in the style of the Burstall-Darlington framework and in the style of equality saturation. Transformations in the style of equality saturation are performed on polyprograms in decomposed form, where the difference between functions and expressions is blurred, and so is the difference between substitution and unfolding. Decomposed polyprograms are well suited for implementation and reasoning, although they are not very human-readable. We also introduce the notion of polyprogram bisimulation which enables a powerful transformation called merging by bisimulation, corresponding to proving equivalence of functions by induction or coinduction. Polyprogram bisimulation is a concept inspired by bisimulation of labelled transition systems, but yet it is quite different, because polyprogram bisimulation treats every definition as self-sufficient, that is a function is considered to be defined by any of its definitions, whereas in an LTS the behaviour of a state is defined by all transitions from this state. We present an algorithm for enumerating polyprogram bisimulations of a certain form. The algorithm consists of two phases: enumerating prebisimulations and converting them to proper bisimulations. This separation is required because polyprogram bisimulations take into account the possibility of parameter permutation. We prove correctness of this algorithm and formulate a certain weak form of its completeness. The article is published in the author’s wording.Полипрограмма — это обобщение программы, допускающее множественность определений одной и той же функции. Подобные объекты возникают в различных системах преобразования программ, таких как система Бёрстолла–Дарлингтона и насыщение равенствами. В данной работе мы вводим понятие полипрограммы на нестрогом функциональном языке первого порядка. Мы определяем денотационную семантику полипрограмм и описываем некоторые преобразования полипрограмм в двух разных стилях: в стиле системы Бёрстолла–Дарлингтона и в стиле насыщения равенствами. Преобразования в стиле насыщения равенствами осуществляются над полипрограммами в расчленённой форме, в которой стирается грань между функциями и выражениями и между подстановкой и раскрытием вызова функции. Расчленённые полипрограммы хорошо подходят для реализации и проведения рассуждений, но трудны для человеческого восприятия. Мы также вводим понятие бисимуляции полипрограмм, на котором основано преобразование — слияние по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Бисимуляция полипрограмм — понятие, вдохновлённое понятием бисимуляции размеченных систем переходов, но несколько от него отличающееся, поскольку бисимуляция полипрограмм рассматривает каждое определение как самодостаточное, т.е. функция полипрограммы задаётся любым своим определением, в то время как в размеченной системе переходов поведение системы в состоянии определяется всей совокупностью переходов, которые можно осуществить из этого состояния. Мы предлагаем алгоритм перечисления бисимуляций некоторого определённого вида. Алгоритм состоит из двух фаз: перечисление пребисимуляций и преобразование их в бисимуляции. Такое разделение требуется из-за того, что бисимуляции полипрограмм учитывают возможность перестановки параметров функций. Мы доказываем корректность данного алгоритма, а также формулируем некоторую слабую форму его полноты. Статья публикуется в авторской редакции
Инвариантные характеристики вынужденных колебаний балки с продольным сжатием
Get PDFOscillations of an elastic beam with longitudinal compression are considered. The beam consists of two steel strips connected on free ends and fixed on opposite ones. Compression is achieved by a strained string. Excitation of oscillations is performed by exposure of alternating magnetic field on a magnet placed on the loose end. The law of motion with a change in the frequency of the harmonic action is registered. As a result of the full-scale experiment a large set of data is obtained. This set contains ordered periodic oscillations as well as disordered oscillations specific to dynamical systems with chaotic behaviour. To study the invariant numerical characteristics of the attractor of the corresponding dynamical system, a correlation integral and a correlation dimensionality as well as β-statentropy are calculated. A large numerical experiment showed that the calculation of β-statentropy is preferable to the calculation of the correlation index. Based on the developed algorithms the dependence of β- statentropy on the frequency of the external action is constructed. The constructed dependence can serve as an effective tool for measuring the adequacy of the mathematical model of forced oscillations of buckling beam driven oscillations. Рассматриваются колебания упругой балки с продольным сжатием. Такая балка может быть реализована из двух упругих стальных полос, соединённых на свободных концах. Сжатие в балке происходит за счет натянутой нити. Возбуждение колебаний осуществляется воздействием переменного магнитного поля на магнит, установленный на конце балки. Регистрировался закон движения при изменении частоты гармонического воздействия. В результате натурного эксперимента был получен большой массив данных, представляющих собой как упорядоченные периодические колебания, так и неупорядоченные колебания, характерные для динамических систем с хаотическим поведением. Для изучения инвариантных числовых характеристик аттрактора соответствующей динамической системы вычислялись корреляционный интеграл и корреляционная размерность, а также β-статэнтропия. Объемный численный эксперимент показал, что вычисление β-статэнтропии предпочтительнее расчёта корреляционного показателя. На основе разработанных алгоритмов построена зависимость β-статэнтропии от частоты внешнего воздействия. Эта зависимость может служить эффективным инструментом для оценки адекватности математической модели вынужденных колебаний балки с потерей устойчивости
О корректности моделирования модульных вычислительных систем реального времени с помощью сетей временных автоматов
Get PDFIn this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possible model runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements.Рассматривается задача проверки допустимости конфигураций модульных вычислительных систем реального времени (МВС РВ). Конфигурация считается допустимой, если все работы успевают выполниться на МВС РВ в рамках своих директивных интервалов. Предложена обобщенная модель функционирования МВС РВ и метод построения на её основе модели для конкретной конфигурации. Модель представляет собой сеть временных автоматов с остановкой таймеров. По вычислению сети автоматов предлагается строить временную диаграмму (ВД) функционирования МВС РВ, необходимую для проверки допустимости. В работе обосновывается корректность предложенного подхода. Из спецификаций на МВС РВ был выделен ряд требований, применимых к моделям МВС РВ и их компонентов на выбранном уровне абстракции. Модели считаются корректными, если удовлетворяют этим требованиям. Доказано, что если все модели компонентов системы удовлетворяют соответствующим требованиям, то модель МВС РВ, построенная согласно предложенному подходу, удовлетворяет требованиям к модели системы в целом (то есть корректна), а также является детерминированной. Под детерминированностью понимается однозначность построения ВД сети автоматов, соответствующей заданной конфигурации. Это позволяет использовать для проверки допустимости конфигурации любое вычисление соответствующей сети автоматов, что крайне важно для эффективности предложенного подхода, так как число возможных вычислений сети автоматов растет экспоненциально с числом работ в системе. Выполнение требований корректности к моделям компонентов системы может быть проверено автоматически с использованием верификатора и подхода автоматов-наблюдателей. Все разработанные нами модели компонентов системы удовлетворяют соответствующим требованиям, что было доказано с помощью верификатора UPPAAL. Если пользовательские модели компонентов системы удовлетворяют требованиям корректности, то они могут быть включены в модель МВС РВ, которая при этом останется корректной и детерминированной
Об алгоритме расщепления носителя для индуцированных кодов
Get PDFIn the paper, the analysis of the stability of the McEliece-type cryptosystem on induced codes for key attacks is examined. In particular, a model is considered when the automorphism group is trivial for the base code C, on the basis of which the induced code Flq ⊗ C is constructed. In this case, as shown by N. Sendrier in 2000, there exists such a mapping, called a complete discriminant, by means of which a secret permutation that is part of the secret key of a McEliece-type cryptosystem can be effectively found. The automorphism group of the code Flq ⊗ C is nontrivial, therefore there is no complete discriminant for this code. This suggests a potentially high resistance of the McEliece-type cryptosystem on the code Flq ⊗ C. The algorithm for splitting the support for the code Flq ⊗ C is constructed and the efficiency of this algorithm is compared with the existing attack on the key of the McElice type cryptosystem based on the code Flq ⊗ C.В 2000 г. Н. Сендриер показал, что если для линейного [n, k, d]-кода C(⊆ Fnq ) длины n и размерности k с кодовым расстоянием d группа автоморфизмов PAut(C) этого кода тривиальна, то может быть построен детерминированный алгоритм расщепления носителя, позволяющий для кода D, перестановочно-эквивалентного коду C, найти такую перестановку σ, что σ(C) = D. Этот алгоритм, в частности, может быть применен для осуществления атаки на ключ кодовой криптосистемы типа Мак-Элиса на коде C. Целью настоящей работы является построение и анализ алгоритма расщепления носителя для кода Flq ⊗ C, индуцированного кодом C, l ∈ N. Так как группа автоморфизмов PAut(Flq ⊗ C) нетривиальна даже в случае, когда группа автоморфизмов базового кода C тривиальна, то это позволяет предположить потенциально высокую стойкость криптосистемы типа Мак-Элиса на коде Flq ⊗C к атаке на основе расщепления носителя. В работе строится алгоритм расщепления носителя для кода Flq ⊗ C и сравнивается эффективность этого алгоритма с имеющейся атакой на ключ криптосистемы типа Мак-Элиса на основе кода Flq ⊗ C
Верификация программ со взаимной рекурсией на языке Пифагор
Get PDFIn the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and has only data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in the mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. An example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function.В работе рассматривается верификация программ со взаимной рекурсией для языка функционально-потокового параллельного программирования Пифагор. В языке используется модель представления программы в виде графа потока данных (информационного графа), в котором нет дополнительных управляющих связей, а присутствуют только информационные зависимости. Это позволяет упростить процесс верификации, так как не требует анализа возникающих в традиционных архитектурах дополнительных ресурсных конфликтов. Доказательство корректности программы опирается на удаление взаимных рекурсий посредством преобразования программы. Универсальным способом удаления взаимной рекурсии произвольного количества функций является построение универсальной рекурсивной функции, которая выполняет работу всех исходных функций и принимает, кроме аргумента выполняемой функции, натуральное число, являющееся номером выполняемой функции. В ряде случаев, когда присутствует косвенная рекурсия, можно использовать более простой способ преобразования — объединение кода функций, при котором происходит объединение тел вызывающих друг друга функций. Для преобразования произвольной рекурсии в прямую предлагается построение графа всех связанных функций и последующая трансформация данного графа путём удаления функций, не связанных с рассматриваемой, объединения косвенно рекурсивных функций и построения универсальной рекурсивной функции. Доказывается, что изменение функции на языке Пифагор при объединении кода и построении универсальной рекурсивной функции не влияет на корректность исходной программы. Приводится пример доказательства частичной корректности программы на языке Пифагор, осуществляющей синтаксический разбор простого арифметического выражения. После построения графа всех связанных функций рассматриваются два способа доказательства: с использованием объединения кода функций и с построением универсальной рекурсивной функции