Все выпуски

В данной работе представлен новый подход к интерпретации логических формул для синтеза алгоритмов и программ. Предложенный метод сочетает в себе черты реализации Клини и интерпретации Гёделя «диалектика», но не опирается на них непосредственно. Рассматривается простой вариант позитивного языка логики предикатов без функций, с конъюнкцией, дизъюнкцией, импликацией и кванторами всеобщности и существования. Описана новая реализационная семантика формул и секвенций, в которой рассматривается не просто реализация формулы, а реализация с дополнительной поддержкой. Реализация примерно соответствует реализации Клини. Поддержка предоставляет дополнительные данные в пользу того, что реализация корректна. Поддержка должна подтвердить, что реализация работает корректно для формулы в любых корректных условиях применения. Представлен язык доказательств, для которого доказана теорема о корректности, показывающая, что любая выводимая секвенция имеет реализацию и поддержку, подтверждающую, что эта реализация работает правильно для этой формулы в любых корректных условиях при подходящем интерпретаторе используемых программ.

This paper presents a novel approach to interpreting logical formulas for synthesizing algorithms and programs. The proposed method combines features of Kleene realizability and Gödel's “dialectica” interpretation but does not rely on them directly. A simple version of positive predicate logic without functions is considered, including conjunction, disjunction, implication, and universal and existential quantifiers. A new realizability semantics for formulas and sequents is described, which considers not just a realization of a formula, but a realization with additional support. The realization roughly corresponds to Kleene realizability. The support provides additional data in favor of the correctness of the realization. The support must confirm that the realization works correctly for the formula under any valid conditions of application. A proof language is presented for which a correctness theorem is proved showing that any derivable sequent has a realization and support confirming that this realization works correctly for this formula under any valid conditions with a suitable interpreter for the programs used.

Под термином «размыкание предиката» понимается сведение задачи поиска и изучения свойств множества истинности заданного предиката к задаче поиска и изучения свойств неподвижных точек некоторого отображения. Размыкание предиката дает дополнительные возможность анализа его множества истинности, а также позволяет строить элементы этого множества с теми или иными свойствами. Известны примеры размыкания нетривиальных предикатов, таких как предикат «быть стабильным (слабо инвариантным) множеством», предикат «быть неупреждающим селектором», предикат «быть седловой точкой», предикат «быть равновесием Нэша». В упомянутых случаях вопрос об априорной оценке возможности размыкания того или иного интересующего нас предиката и о построении соответствующего размыкающего отображения оставался за рамками рассмотрения: размыкающие отображения предоставлялись как готовые объекты. В предлагаемой заметке мы постараемся отчасти закрыть этот пробел: приводятся формальное определение операции размыкания предиката, способы построения и исчисления размыкающих отображений и их основные свойства. Описываемый подход примен\'им во всех упомянутых выше положительных примерах. В качестве иллюстрации проведено следующее этому способу построение размыкающего отображения для предиката «быть нэшевским равновесием».

The term “predicate unlocking” is understood as the reduction of the problem of finding and studying the set of truth of a predicate to the problem of finding and studying the set of fix points of a map. Predicate unlocking provides opportunities for additional investigation of the truth set and also allows one to build the elements of this set with particular properties. There are examples of nontrivial predicate unlocking such as: the predicate “be a stable (weakly invariant) set”, the predicate “be a nonanticipatory selector”, the predicate “be a saddle point”, and the predicate “be a Nash equilibrium”. In these cases, the question of the a priori evaluation of the possibility of unlocking this or other predicate of interest and the question of constructing a corresponding unlocking map remained beyond consideration: the unlocking mappings were provided as ready-made objects. In this note we try to partly close this gap: we provide a formal definition of the predicate unlocking operation, methods for constructing and calculating of the unlocking mappings and their basic properties. As an illustration, the “routine” construction of unlocking mapping for the predicate “be a Nash equilibrium” is carried out. The described approach is far from universality, but, at least, it can be applied to all aforementioned positive examples.

Работа посвящена связи параллельных и последовательных вычислений. С одной стороны, рассматривается класс словарных предикатов, основанных на последовательных вычислениях, ограниченных по памяти константами и имеющих полиномиальную временную сложность. С другой стороны, рассматривается класс словарных предикатов, вычислимых на параллельных альтернирующих машинах за логарифмическое время. Доказано совпадение соответствующих классов. Предложено направление использования полученных результатов для взаимного преобразования и сочетания вычислений на молекулярных биоподобных последовательных машинах и параллельных вычислениях на векторно-матричных компьютерах. Предполагаемые области применения: обработка изображений в реальном масштабе времени для задач управления, анализ больших текстов и других больших данных.

The work is devoted to the connection between parallel and sequential computing. On the one hand, we consider a class of word predicates based on sequential calculations, limited in memory by constants and having polynomial time complexity. On the other hand, we consider a class of word predicates that are computable on parallel alternating machines in logarithmic time. The coincidence of the corresponding classes is proven. The direction of using the obtained results for mutual transformation and combination of calculations on molecular biosimilar sequential machines and parallel calculations on vector-matrix computers is proposed. Intended applications: real-time image processing for control tasks, analysis of large texts and other big data.

Рассматривается проблема эффективной вычислимости разрешимых моделей классификации конечных объектов. Исследуется конструктивизация условий симультанности (предельно короткого цикла) принятия решения в классификации. Симультанность ("однотактность") достигается параллельным сравнением компонент неизвестной реализации с информативными элементами всех эталонов в обучающей выборке. Конструктивизация условий симультанности предусматривает: выделение информативных элементов (идентификационных меток) в информативных зонах классифицируемых множеств; параллельное покомпонентное сравнение неизвестной реализации конечного объекта с информативными элементами всех эталонов из обучающей выборки. Полученные результаты симультанной схемы принятия решений в классификации интерпретируются в нейронных сетях, в обобщенной модели распознавания, в задачах идентификации.

Consideration is given to the problem of efficient computability of solvablemodels of finite objects classification. We investigate the constructivization of simultaneity (extremely short cycle) conditions of decision adoption in the classification. Simultaneity is achieved by parallel comparing of the components of the unknown implementation with informative elements of all etalons in the training sample. Constructivization of simultaneity conditions includes: a selection of informative elements (identification labels) in the informative areas of classified sets; the parallel component-wise comparison of the unknown realization of a finite object with informative elements of etalons from the training set. The obtained results of simultaneous decision trees in classification is interpreted in neural networks, in a generalized model of recognition, in problems of identification.

В работе разрабатывается метод, именуемый «размыкание предиката», сводящий задачу поиска множества истинности предиката к задаче поиска множества неподвижных точек некоторого (вообще говоря, многозначного) отображения. Предлагаемая техника дает дополнительные возможности анализа задач и построения решений путем систематического привлечения результатов теории неподвижных точек. Даны формальное определение операции размыкания предиката, способы построения и исчисления размыкающих отображений и их основные свойства. В случае когда область определения предиката частично упорядочена, указаны способы построения размыкающих функций, обладающих свойством сужаемости. Это позволило получить представления интересующих элементов решения в виде итерационных пределов. Предлагаемый подход в силу абстрактности имеет широкую сферу применения. Вместе с тем эффективность полученного решения зависит от специфики рассматриваемой задачи и выбранного варианта реализации метода. В качестве иллюстрации в работе рассмотрена процедура построения размыкающего отображения для предиката «быть неупреждающим селектором». На основе этого отображения получено выражение для наибольшего неупреждающего селектора заданной мультифункции.

We consider an approach to constructing a non-anticipating selection of a multivalued mapping; such a problem arises in control theory under conditions of uncertainty. The approach is called “unlocking of predicate” and consists in the reduction of finding the truth set of a predicate to searching fixed points of some mappings. Unlocking of predicate gives an extra opportunity to analyze the truth set and to build its elements with desired properties. In this article, we outline how to build “unlocking mappings” for some general types of predicates: we give a formal definition of the predicate unlocking operation, the rules for the construction and calculation of “unlocking mappings” and their basic properties. As an illustration, we routinely construct two unlocking mappings for the predicate “be non-anticipating mapping” and then on this base we provide the expression for the greatest non-anticipating selection of a given multifunction.

Исследуются методы представления отношений предикатами Радемахера, предлагается метод коллективного голосования для распознавания отношений.

We investigate the methods of presenting relationships by using Rademacher’s predicates and offer a method of collective voting to recognize relationships.