Программные продукты и системы, 2014, № 3 (107)
международный научно-практический журнал
Покупка
Основная коллекция
Издательство:
НИИ Центрпрограммсистем
Наименование: Программные продукты и системы
Год издания: 2014
Кол-во страниц: 184
Дополнительно
Тематика:
ББК:
УДК:
ГРНТИ:
Скопировать запись
Фрагмент текстового слоя документа размещен для индексирующих роботов.
Для полноценной работы с документом, пожалуйста, перейдите в
ридер.
Научно-исследовательский институт
«Центрпрограммсистем»
Программные
продукты и системы
МЕЖДУНАРОДНЫЙ НАУЧНО-ПРАКТИЧЕСКИЙ ЖУРНАЛ
№ 3 (107), 2014
Главный редактор
С.В. ЕМЕЛЬЯНОВ, академик РАН
Тверь
PROGRAMMNYE PRODUKTY
I SISTEMY
(SOFTWARE & SYSTEMS)
International research and practice journal
no. 3 (107), 2014
Editor-in-Chief
S.V. EMELYANOV, Academician of the Russian Academy of Sciences
Tver
Russian Federation
Research Institute CENTERPROGRAMSYSTEM
ПРОГРАММНЫЕ ПРОДУКТЫ И СИСТЕМЫ Издатель НИИ «Центрпрограммсистем» (г. Тверь)
Международное научно-практическое Учредители: МНИИПУ (г. Москва),
приложение к международному журналу Главная редакция международного журнала
«ПРОБЛЕМЫ ТЕОРИИ И ПРАКТИКИ УПРАВЛЕНИЯ» «Проблемы теории и практики управления»
(г. Москва),
Главный редактор Закрытое акционерное общество
С.В. ЕМЕЛЬЯНОВ, академик РАН (г. Москва) «Научно-исследовательский институт
«Центрпрограммсистем» (г. Тверь)
Научный редактор номера
Н.А. СЕМЕНОВ, д.т.н., профессор, ТГТУ (г. Тверь) Журнал зарегистрирован
в Комитете Российской Федерации
Рецензенты номера: по печати 26 июня 1995 г.
Г.С. Плесневич, к.ф.-м.н., профессор МЭИ (г. Москва)
А.Н. Сотников, д.ф.-м.н., профессор МСЦ РАН (г. Москва) Регистрационное
свидетельство № 013831
С.В. Ульянов, д.ф.-м.н., профессор Международного университета
природы, общества и человека «Дубна» (г. Дубна) Подписной индекс в каталоге
А.П. Еремеев, д.т.н., профессор МЭИ (г. Москва) Агентства «Роспечать» 70799
С.Х. Шигалугов, д.ф.-м.н., доцент НИИ (г. Норильск) ISSN 0236-235X (печатн.)
Н.А. Семенов, д.т.н., профессор ТГТУ (г. Тверь) ISSN 2311-2735 (онлайн)
МЕЖДУНАРОДНАЯ РЕДАКЦИОННАЯ КОЛЛЕГИЯ
Семенов Н.А. – д.т.н., профессор Тверского государственного технического университета, заместитель главного
редактора (г. Тверь, Россия)
Решетников В.Н. – д.ф.-м.н., профессор Российского государственного технологического университета
им. К.Э. Циолковского, заместитель главного редактора (г. Москва, Россия)
Арефьев И.Б. – д.т.н., профессор Морской академии Польши (г. Щецин, Польша)
Батыршин И.З. – д.т.н., профессор Мексиканского института нефти (г. Мехико, Мексика)
Вагин В.Н. – д.т.н., профессор Московского энергетического института (технического университета)
(г. Москва, Россия)
Голенков В.В. – д.т.н., профессор Белорусского государственного университета информатики и радиоэлектроники
(г. Минск, Беларусь)
Еремеев А.П. – д.т.н., профессор Московского энергетического института (технического университета)
(г. Москва, Россия)
Котов А.С. – кандидат наук, ассистент профессора университета Уэйна (штат Мичиган) (г. Детройт, США)
Кузнецов О.П. – д.т.н., профессор Института проблем управления РАН (г. Москва, Россия)
Курейчик В.М. – д.т.н., профессор Технологического института Южного федерального университета
(г. Таганрог, Россия)
Лисецкий Ю.М. – к.т.н., генеральный директор «S&T Ukraine» (г. Киев, Украина)
Нгуен Тхань Нги – д.ф.-м.н., профессор, проректор Ханойского открытого университета (г. Ханой, Вьетнам)
Николов Р.В. – доктор наук, профессор Университета библиотековедения и информационных технологий Софии
(г. София, Болгария)
Осипов Г.С. – д.ф.-м.н., профессор, заместитель директора Института системного анализа РАН (г. Москва, Россия)
Палюх Б.В. – д.т.н., профессор Тверского государственного технического университета (г. Тверь, Россия)
Попков В.К. – д.ф.-м.н., профессор, академик МАИ (г. Новосибирск, Россия)
Рахманов A.A. – д.т.н., профессор, заместитель генерального директора Концерна «РТИ Системы» (г. Москва, Россия)
Серов В.С. – д.ф.-м.н., профессор Университета прикладных наук Оулу (г. Оулу, Финляндия)
Сотников А.Н. – д.ф.-м.н., профессор, Межведомственный суперкомпьютерный центр РАН (г. Москва, Россия)
Сулейманов Д.Ш. – академик АН Республики Татарстан, д.т.н., профессор Казанского государственного
технического университета (г. Казань, Республика Татарстан, Россия)
Тарасов В.Б. – к.т.н., Московский государственный технический университет им. Н.Э. Баумана (г. Москва, Россия)
Хорошевский В.Ф. – д.т.н., профессор Московского физико-технического института (технического университета)
(г. Москва, Россия)
Язенин А.В. – д.ф.-м.н., профессор Тверского государственного университета (г. Тверь, Россия)
АССОЦИИРОВАННЫЕ ЧЛЕНЫ РЕДАКЦИИ
Московский энергетический институт (технический университет), г. Москва, Россия
Технологический институт Южного федерального университета, г. Таганрог, Россия
Тверской государственный технический университет, г. Тверь, Россия
Научно-исследовательский институт «Центрпрограммсистем», г. Тверь, Россия
АДРЕС РЕДАКЦИИ Подписано в печать 27.08.2014 г.
Россия, 170024, г. Тверь, Отпечатано ООО ИПП «Фактор и К»
Россия, 170028, г. Тверь, ул. Лукина, д. 4, стр. 1
пр. 50 лет Октября, 3а Заказ № 148
Телефон (482-2) 39-91-49 Выпускается один раз в квартал
Год издания двадцать седьмой
Факс (482-2) 39-91-00 Формат 6084 1/8
Тираж 1000 экз.
E-mail: red@cps.tver.ru Объем 184 стр.
www.swsys.ru Цена 198 руб.
Автор статьи отвечает за подбор, оригинальность и точность приводимого фактического материала.
Авторские гонорары не выплачиваются. При перепечатке материалов ссылка на журнал обязательна.
PROGRAMMNYE PRODUKTY I SISTEMY Publisher Research Institute
(SOFTWARE & SYSTEMS) CENTERPROGRAMSYSTEM (Tver)
International research and practice supplement for International magazine The Founders: International Scientific
THEORETICAL AND PRACTICAL ISSUES OF MANAGEMENT and Research Institute
Editor-in-chief for Management Issues (Moscow),
S.V. Emelyanov, Academician of the Russian Academy of Sciences (Mosсow, Russian Federation) the Chief Editorial Board
Science editor of the issue of International Magazine Theoretical
N.A. Semenov, Dr.Sc. (Engineering), Professor, TGTU (Tver, Russian Federation) and practical issues of management
Reviewers of the issue: (Moscow),
G.S. Plesniewicz, Ph.D. (Physics and Mathematics), Professor, MPEI (Mosсow, Russian Federation) ZAO Research Institute
A.N. Sotnikov, Dr.Sc. (Physics and Mathematics), Professor, CENTERPROGRAMSYSTEM (Tver)
JSCC of the Russian Academy of Sciences (Mosсow, Russian Federation)
S.V. Ulyanov, Dr.Sc. (Physics and Mathematics), Professor, Dubna Internacional University for Nature, The magazine is on record
Socitty and Man (Dubna, Russian Federation) in Russian committee
th
A.P. Eremeev, Dr.Sc. (Engineering), Professor, MPEI (Mosсow, Russian Federation) on press 26 of June 1995
S.Kh. Shigalugov Dr.Sc. (Physics and Mathematics), Associate Professor, Registration certificate № 013831
NII (Norilsk, Russian Federation) ISSN 0236-235X (print)
N.A. Semenov, Dr.Sc. (Engineering), Professor, TGTU (Tver, Russian Federation) ISSN 2311-2735 (online)
INTERNATIONAL EDITORIAL BOARD
Semenov N.A. – Dr.Sc. (Engineering), Professor of Tver State Technical University, Deputy Editor-in-Chief
(Tver, Russian Federation)
Reshetnikov V.N. – Dr.Sc. (Physics and Mathematics), Professor of Russian State Technological University (MATI),
Deputy Editor-in-Chief (Mosсow, Russian Federation)
Arefev I.B. – Dr.Sc. (Engineering), Professor of Poland Szczecin Maritime Academy (Szczecin, Poland)
Batyrshin I.Z. – Dr.Sc. (Engineering), Professor of Mexican Institute of Petroleum (Mexico City, Mexico)
Vagin V.N. – Dr.Sc. (Engineering), Professor of Moscow Power Engineering Institute (Technical University)
(Mosсow, Russian Federation)
Golenkov V.V. – Dr.Sc. (Engineering), Professor of Belarusian State University of Informatics and Radioelectronics (BSUIR)
(Minsk, Republic of Belarus)
Eremeev A.P. – Dr.Sc. (Engineering), Professor of Moscow Power Engineering Institute (Technical University)
(Moscow, Russian Federation)
Kotov A.S. – Ph.D. (Computer Science), Assistant Professor, Wayne State University (Detroit, MI, USA)
Kuznetsov O.P. – Dr.Sc. (Engineering), Professor of the Institute of Control Sciences of the Russian Academy of Sciences
(Moscow, Russian Federation)
Kureichik V.M. – Dr.Sc. (Engineering), Professor of Taganrog Technology Institute at Southern Federal University
(Taganrog, Russian Federation)
Lisetskiy Yu.M. – Ph.D.Tech.Sc., CEO of S&T Ukraine (Kiev, Ukraine)
Nguyen Thanh Nghi – Dr.Sc. (Physics and Mathematics), Professor, Vice-Principal of Hanoi Open University (Hanoi, Vietnam)
Nikolov R.V. – Full Professor of the University of Library Studies and Information Technology (Sofia, Bulgaria)
Osipov G.S. – Dr.Sc. (Physics and Mathematics), Professor, Deputy of the Principal of Institute of Systems Analysis
of the Russian Academy of Sciences (Mosсow, Russian Federation)
Palyukh B.V. – Dr.Sc. (Engineering), Professor of Tver State Technical University (Tver, Russian Federation)
Popkov V.K. – Dr.Sc. (Physics and Mathematics), Professor, Academician of IIA (Novosibirsk, Russian Federation)
Rakhmanov A.A. – Dr.Sc. (Engineering), Professor, Deputy of the CEO of Concern RTI Systems
(Mosсow, Russian Federation)
Serov V.S. – Dr.Sc. (Physics and Mathematics), Professor of the Oulu University of Applied Sciences (Oulu, Finland)
Sotnikov A.N. – Dr.Sc. (Physics and Mathematics), Professor, Joint Supercomputer Center of the Russian Academy
of Sciences (Moscow, Russian Federation)
Suleimanov D.Sh. – Academician of TAS, Dr.Sc. (Engineering), Professor of Kazan State Technical University
(Kazan, Republic of Tatarstan, Russian Federation)
Tarassov V.B. – Ph.D. (Engineering), Bauman Moscow State Technical University (Mosсow, Russian Federation)
Khoroshevsky V.F. – Dr.Sc. (Engineering), Professor of Moscow Institute of Physics and Technology
(Moscow, Russian Federation)
Yazenin A.V. – Dr.Sc. (Physics and Mathematics), Professor of Tver State University (Tver, Russian Federation)
ASSOCIATED EDITORIAL BOARD MEMBERS
Moscow Power Engineering Institute (Technical University), Moscow, Russian Federation
Technology Institute at Southern Federal University, Taganrog, Russian Federation
Tver State Technical University, Tver, Russian Federation
Research Institute CENTERPROGRAMSYSTEM, Tver, Russian Federation
Passed for printing 27.08.2014
EDITORIAL OFFICE ADDRESS Printed in printing-office “Faktor i K”
50 let Octyabrya Ave. 3а, Lukina St. 4/1, Tver, 170028, Russian Federation
Tver, 170024, Russian Federation Prod. order № 148
Published quarterly
Phone: (482-2) 39-91-49 27th year of publication
Fax: (482-2) 39-91-00 Format 6084 1/8
E-mail: red@cps.tver.ru Circulation 1000 copies
www.swsys.ru Wordage 184 pages
Price 198 rub.
Вниманию авторов!
Международный журнал «Программные продукты и системы» публикует материалы научного и науч но-практического характера по новым информационным технологиям, результаты академических и отрасле вых исследований в области использования средств вычислительной техники. Практикуется выпуск тематиче ских номеров по искусственному интеллекту, системам автоматизированного проектирования, по технологии
разработки программных средств и системам защиты, а также специализированные выпуски, посвященные
научным исследованиям и разработкам отдельных вузов, НИИ, научных организаций.
Решением Президиума Высшей аттестационной комиссии (ВАК) Министерства образования и науки
РФ № 8/13 от 02.03.2012 международный журнал «Программные продукты и системы» внесен в Перечень ве дущих рецензируемых научных журналов и изданий, в которых должны быть опубликованы основные науч ные результаты диссертаций на соискание ученых степеней кандидата и доктора наук.
Информация об опубликованных статьях по установленной форме регулярно предоставляется в систе му Российского индекса научного цитирования (РИНЦ) и готовится для передачи в международные базы ци тирования.
Условия публикации
К рассмотрению принимаются ранее нигде не опубликованные материалы, соответствующие тематике
журнала (специализация 05.13.ХХ – Информатика, вычислительная техника и управление) и отвечающие ре дакционным требованиям.
Работа представляется в электронном виде в формате Word (шрифт Times New Roman, размер 11 пунк тов с полуторным межстрочным интервалом). При обилии сложных формул обязательно наличие статьи и в
формате PDF. Формулы должны быть набраны в редакторе формул Word (Microsoft Equation или MathType).
Объем статьи вместе с иллюстрациями – не менее 10 000 знаков. Иллюстративный материал присылается в
формате tiff или jpeg с разрешением 300 dpi. Диаграммы, схемы, графики должны быть доступными для ре дактирования. Все иллюстрации для полиграфического воспроизведения представляются в черно-белом вари анте. Цветные, тонированные, отсканированные, не подлежащие редактированию средствами Word рисунки и
экранные формы следует присылать в хорошем качестве для их дополнительного размещения на сайте журна ла в макете статьи (с доступом по ссылке). Кроме того, публикация материалов с использованием гипертекста,
графики, аудио-, видео-, программных средств и др. возможна в нашем новом электронном издании «Про граммные продукты, системы и алгоритмы», сайт www.swsys-web.ru. Заголовок должен быть информатив ным; сокращения, а также терминологию узкой тематики желательно в нем не использовать. Количество авто ров на одну статью – не более 4, количество статей одного автора в номере, включая соавторство, – не более 2.
Список литературы (оформленный в соответствии с ГОСТ Р 7.05–2008), наличие которого обязательно, дол жен включать не менее 5 пунктов.
Необходимы также аннотация (150–200 слов), ключевые слова (7–10) и индекс УДК. Название статьи,
аннотация и ключевые слова должны быть переведены на английский язык (машинный перевод недопустим),
а фамилии авторов, названия и юридические адреса организаций (если нет официального перевода), приста тейные списки литературы – транслитерированы по стандарту BGN/PCGN.
Вместе со статьей следует прислать отзыв-рекомендацию в произвольной форме, экспертное заключе ние, лицензионное соглашение, а также сведения об авторах: фамилия, имя, отчество, название и юридический
адрес организации, должность, ученые степень и звание (если есть), контактный телефон, электронный адрес,
почтовый адрес для отправки бесплатного авторского экземпляра журнала.
Порядок рецензирования
Все статьи, поступающие в редакцию (соответствующие тематике и оформленные согласно требовани ям к публикации), подлежат обязательному рецензированию в течение месяца с момента поступления.
В редакции есть устоявшийся коллектив рецензентов, среди которых члены международной редколле гии журнала, эксперты из числа крупных специалистов в области информатики и вычислительной техники ве дущих вузов страны, а также ученые и специалисты НИИ «Центрпрограммсистем» (г. Тверь).
Рецензирование проводится конфиденциально. Автору статьи предоставляется возможность ознако миться с текстом рецензии. При необходимости статья отправляется на доработку.
Рецензии обсуждаются на заседаниях рабочей группы, состоящей из членов научного совета журнала.
Заседания проводятся раз в месяц в НИИ «Центрпрограммсистем» (г. Тверь), где принимается решение о це лесообразности публикации статьи.
Статьи, одобренные редакционным советом, публикуются в течение полугода с момента одобрения,
а отправленные на доработку – с момента поступления после устранения замечаний.
Редакция международного журнала «Программные продукты и системы» в своей работе руководству ется сводом правил Кодекса этики научных публикаций, разработанным и утвержденным Комитетом по эти ке научных публикаций.
Программные продукты и системы № 3, 2014 г.
AN APPROACH TO CASE-BASED SYNTHESIS
OF FUNCTIONAL PROGRAMS
(The work is done with support from the Russian Foundation for Basic Research, grant № 14-01-00214а)
N.N. Fastovets, Postgraduate Student
(Lomonosov Moscow State University,
Leninskie Gory, Moscow, 119991, Russian Federation, nnf-cmc@cs.msu.ru)
Received 19.05.2014
Abstract. This article deals with an automatic functional programs synthesis problem. We consider the way to apply
case-based reasoning approach to program synthesis. In order to use such framework for our problem we have to consider
several subproblems: definition of a "similarity" relation over program specifications space, search of the most suitable
known program for a given specification and adaptation of a chosen program to new specification. We will consider
adaptation method only in this article and leave other subproblems for further work. We can consider the problem of
adaptation as a problem of program correction: we have to modify given (chosen in search procedure) program, so that it will
satisfy a given specification. There is a method for functional logic program correction, which have a form of conditional
term-rewriting systems. So, our idea is to translate a functional program to term-rewriting system and then apply the
correction method to it. In this article we will consider procedures of such translation and adaptation of the correction method
for our task.
Keywords: artificial intelligence, program synthesis, program correction, case based reasoning, term rewriting system.
УДК 004.4 Дата подачи статьи: 19.05.2014
ПОДХОД К СИНТЕЗУ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ,
ОСНОВАННОМУ НА ПРЕЦЕДЕНТАХ
(Работа выполнена при поддержке РФФИ, грант № 14-01-00214а)
Фастовец Н.Н., аспирант
(Московский государственный университет им. М.В. Ломоносова,
Ленинские горы, г. Москва, 119991, Россия, nnf-cmc@cs.msu.ru)
Аннотация. В данной статье рассматривается проблема автоматического синтеза функциональных программ.
Описывается способ применения рассуждений на основе прецедентов в синтезе программ. Для применения этого
подхода к задаче необходимо рассмотреть несколько подзадач: определение отношения «похожести» в пространстве
спецификаций программ, поиск наиболее подходящей к заданной спецификации известной программы и адаптация
выбранной программы к новой спецификации. Авторы рассматривают только подзадачу адаптации, оставив осталь ные подзадачи для дальнейшей работы.
Задачу адаптации можно рассматривать как коррекцию программы, то есть модификации выбранной в ходе по иска программы таким образом, чтобы она удовлетворяла заданной спецификации. Существует метод коррекции
функционально логических программ, имеющих вид системы переписывания термов с условиями. Таким образом,
идея авторов состоит в трансляции функциональной программы в систему переписывания термов и в применении к
ней известного метода коррекции. В данной статье рассматриваются процедура такой трансляции и адаптация мето да коррекции для поставленной задачи.
Ключевые слова: искусственный интеллект, синтез программ, коррекция программ, рассуждения на основе
прецедентов, переписывание термов.
Nowadays we can see significant growth of auto- in modern versions of .Net framework [2] can be con mation in wide range of human activities and process- sidered as a rough example of such change.
es [1]. This builds up a new level of software devel- There are several different methods of automatic
opment requirements: programming must be quicker, synthesis which can be classified in three approaches
as cheap as possible and provide needed level of pro- [1]: deductive synthesis, where a specification is rep duced programs quality. So, these conditions make resented via theorem over input and output variables,
software development process automation actual. and a program can be obtained from the proof of the
Such automation is partially achieved by existing theorem; inductive synthesis, where a specification is
high-level programming languages. However, in- represented as a set of input-output examples and a
creasing of abstraction level requires significant com- program can be constructed by them; transformational
plication of translation (and/or compilation) algo- synthesis, where a synthesis procedure must construct
rithms. So, we meet the problem of automatic pro- a new version, which is optimized by some measure.
gram synthesis here. It is automatic or automated con- Also, there are some little-bit unusual approaches, like
struction of executable program by formal specifica- generation of program as game strategy [3]. But most
tion that can also be executable. The main advantage of these approaches are not very useful in practice that
of automatic synthesis is a possibility to manipulate makes further research actual.
an effect (computation) instead of tool (programming At the same time, there is an interesting bio language). Using of LINQ queries to objects (enu- inspired approach to intelligent problem solving. It is
merable collections) instead of for and foreach loops case-based reasoning (CBR) [4]. Roughly speaking,
5
Программные продукты и системы № 3, 2014 г.
the main idea of CBR is using known solutions for Functional logic (FL) languages are extensions of
new tasks. In general, problem solving with CBR in- functional languages with logic programming princi cludes steps of so-called 4-Re’s cycle: Retrieving, ples [6, 7]. Computing in FL-programs is based on a
Reusing, Revising and Remaining. When CBR sys- narrowing process that is generalization of term re tem receives a new task T it performs search of most writing process. We need to describe several defini similar task T in case-memory (Retrieving step). tions here.
Then, the system can reuse information from known Conditional term rewriting systems [7, 8] are a
solution S of T and try to apply this information for computation model for rule-based languages [7].
constructing the solution S for the task T. Next, a sys- Term rewriting system defined as a pair of R and
Σ sets. Σ is a set of functional symbols f /n , …, f /n ,
tem has to check an obtained solution S and add a new 1 1 k k
where n is an arity of function f. R is a set of rules:
case (T, S) to case-memory for further solutions. This i i
approach can be very useful in such problem domains {(C}. We can split Σ on two disjointed sub i i i
which have no efficient theory, applicable for problem sets Σ=FC where F is a set of so-called defined
solving (e.g. medicine). We share an opinion [5] that functional symbols and C is a set of constructive
CBR could be useful for a program synthesis prob- symbols. A functional symbol f/n is defined if and on lem. But we have to solve several issues of case-based ly if R contains a rule of form (λ→ρ) where λ has
reasoning application: how to define “similarity” form f (t , …, t ) and t , …, t are some terms. C is a
1 n 1 n
measure for tasks (programs specification), how to complement to F in Σ. Constructive term is a term of
organize case-memory for an efficient search of the form c(t , …, t ) where c/n is a constructive symbol
1 n
most similar case and how to adapt a chosen case and t , …, t are constructive terms. We use several
(program) for a given task. Obviously, search proce- 1 n
special denotations: for t term t is a subterm of t on
dure is closely related to adaptation method, because u
the position u; t[] is a term t, where a subterm of t
we want to perform successful adaptation of a chosen u
case to a new task. Due to this, we restrict this work on the position u is replaced by ρ.
to the adaptation method only and leave studying of Let R be a program and g be a goal. We say that g
search procedure for future work. is conditionally narrows into g' if there is a position u
So, in this paper attracts attention to the method of in g, a standardized apart variant of rule r=(λ→ρ)<<
<<R, and a substitution π such that: π is the most
known case adaptation to a new task. Our cases are general unifier for g and λ, and g(C, g [] ).
u u
known programs and the tasks are formal specifica- We denote this fact as g ,,ru g Also, we use de tions – first order logic clauses which express re-
notation * to express that a s can be obtained
ts
quirements to the synthesized program behavior. In R
program synthesis we can consider adaptation proce- from by narrowing derivation with R.
dure as correction: for a new given specification S1 Functional logic programs are a powerful tool for
search procedure chooses program P2 that satisfies its solving equations. For an equation e[ x ](s[ x ]=
specification S ; if P satisfies S , then system can re- =t[ x ]), where s and t are some terms over variables
2 2 1
turn P as an answer. But we expect that P does not x , we can obtain evaluation of variables from used
2 2
satisfy S and, hence, it can be considered as incorrect unifiers in the sequence of narrowing steps (narrow 1
implementation for S , that has to be corrected. Cor- ing derivation) of the applicable program R, if R nar 1
rection here is a transformation of P to a new certain rows the equation to the constant true. Formally, the
2
program P that satisfies S . In this paper we consider ca
1 1 operational semantics O (R) of R can be defined as a
functional programs (functions) and show adaptation set of equations, which are reduced to the true
of functional-logical programs correction method for by R:
such functions. Oca R { f x, , x x |
R 11N N
Preliminaries *
f ( f x , , x x true},
11N N R
We are going to describe base concepts and prop- where c x , , x c x , , x is a
R i 11M i M
ositions of the synthesis method in this section. First i i i i
of all, we will describe the concepts of functional and set of reflexivity axioms for constructive symbols
c occurring in R, and x , …, x are distinct varia functional logic programs, terms narrowing and rela- i 1 N+1
tions between functions and term rewriting systems. bles.
Functional and functional logic programs. We In this work we are going to confront functional
consider of functional programs synthesis. These are programs with functional logic programs. For every
functional program f (x , …, x ) that computes output
programs created from constants and variables occurs, 1 N
value for specified values of the
functional calls (including recursive calls) and condi- y f x , , x
1 N
tional branching. This paradigm is close to mathemat- 00
xx, ,
arguments 1 N we can construct a functional
ical concept of functions. Semantics of functional 00
programs is mapping from input space to output val- logic program R that solve equations of form f(x , …,
f 1
ues space. x ) = y with specified values of arguments x , …,
N 1
6
Программные продукты и системы № 3, 2014 г.
x . In other words, R has to narrow left hand side of Correction of functional programs
N+1 f
such equations to a computed value of f function.
Correctness of programs. We say that a program In general, the main workflow of the proposed
is correct if it computes required output values for method contains follow steps.
given values of input parameters. 1. Translation of given function φ to the term re We say that functional program f ( x )= y satisfies writing system form. Source function y = φ(x) com a specification S=P[ x ]E[ x , y ], where P and E are putes output value y from a specified values of input
first order logic expressions with functional symbols, arguments. We can construct a term-rewriting system
if and only if for all input values x , which satisfy (TRS) that solves equation φ(x) = y for the instantiat 0 ed values of x and apply the original method for cor precondition P, the expression E[ x , f( x )] is holded. rection of such TRS. Then, thus corrections will be
We say that functional logic program R satisfies a mapped to φ, and obtained function φ' would be re specification of the intended semantics set IR, if and turned as answer of system.
ca ca
only if O (R) IR and IR O (R). Since the intend- 2. Computation of negative examples set. We
ed semantics set for R can be represented as another suspect that specification at this step is already repre functional logic program RSpec, we can say that R sat- sented as a set of examples. So, our task here is to
ca ca ca construct positive and negative examples set from
isfies RSpec if O (R) O (RSpec) and O (RSpec)
ca that.
O (R). 3. Correction of the obtained R w.r.t. sets of pos Functional logic programs correction. Correction φ
of programs using base method, described in [7], is itive and negative examples. This step consists in ap performed by iterative application of so-called unfold- plication of the base top-down unfolding-based cor ing operator. Unfolding is defined as follows. rection algorithm to the obtained program and exam Let R be the program. ples. The result of such correction is a new program
1. Suppose r , r << R are rules, such that r = Rc .
1 2 1 φ4. Translation of the obtained Rc to a functional
=( p C ) and r = ( p C ). The rule φ
1 1 1 2 2 2 2 program, which can be computed in usual way. At the
unfolding of r with relation to r is
1 2 final step we translate obtained correct term-rewriting
, ru,
2 c
U r { C | y, C y, C ,
system R , that solves equations of form φ'(x) = y, to
r 11φ
2 the function φ'(x), that satisfies given specification.
u inn }, where y is a new variable.
1 This function will be returned as answer of the sys 2. Suppose r << R. The program unfolding of r is tem.
defined as: U (r) = (R U U (r)) \ {r}.
R rR r Translation of a function to a term rewriting sys Next several definitions are required for correction tem. At this step we construct an equivalent function process description. We say, that rule r is unfoldable al-logic program for given functional program. First
with relation to R if and only if UR(r) R \ {r}. We of all, we define a values representation method.
say, that rule r is discriminable if and only if r is Since we will work with TRS, it is easier to represent
unfoldable and it occurs in narrowing derivation for at numbers via special functions. For natural numbers
p
least one e E . we use function s(x), that returns “next” value for the
The top-down correction algorithm that we use as argument: s(0) = 1, s(s(0)) = 2, … For integer values
a base for our adaptation technique is follows. Input (with negative values) we introduce function d(x) (ad data for processing are sets of positive and negative ditional to s(x)), which returns “previous” value for
examples, and a program that we want to correct. the argument: d(0) = –1, d(d(0)) = –2, … Real values
1. If program does not narrow any positive ex- could be represented via special function dv(x, y), that
ample, we finish the procedure. The program cannot represents relation of arguments x and y: dv(s(0),
be corrected (with the considering method). s(s(0)))=1/2, dv(d(d(0)), s(s(s(0))))=2/3, … With this
2. Initialize current form of program R with R. representation we can define, for example, less-or 0
3. Enter the main loop of algorithm – unfolding equal relation as follows: 0 0true; 0 s(x)
phase. While there is a rule r in R that is used for der i true; 0 d(x) false; s(x) 0 false; d(x) 0
ivation positive and negative example, we choose a true; s(x) s(y) x y; d(x) d(y) x y;
discriminable rule r in R and construct a new version
j s(x) d(y) false; d(x) s(y) true.
of program |R = U (r). k k
i+1 R Also, we will use denotation s (x) and d (x) for
4. After unfolding step a deletion phase starts. short representation of positive and negative numbers
We remove all rules from R, which are used for deri- 3
i k respectively: s (0) will be a short denotation of
vation of negative examples computation. s(s(s(0))).
5. Then, correction procedure returns obtained In addition to this numbers representation, we also
program R as a correct version.
i introduce the special function switch(w, x, y) for rep Now, we are ready to describe our adaptation of resentation of conditional branching, where w repre the functional logic program correction method to sents condition or result of condition evaluation, x and
functional programs. y represent true and false branches respectively. Defi 7
Программные продукты и системы № 3, 2014 г.
nition of switch is obvious: switch(true, x, y) x; call of the new function (x, k) and added a new rule
1
switch(false, x, y) y. Now we are ready to describe (x, k) x pow(x, k – 1) in R .
1 pow
translation procedure. Next step in the same way gives us
The first step of our correction process is transla
pow x,k switch k 0, x, k ,1 ;
tion of given functional program body to a equivalent 1
R x, k x x, k ; .
functional logic program in form of term rewriting
pow 12
system. We split the given function to a set of compo-
x, k pow x, k1
2
nents, which correspond to nodes of abstract syntactic
tree of the target function body. These components Then, new iteration of step 2 will not change Rpow
can represent variables, function calls, constants (as and we can go to step 4 and add a simple definition of
special case of functional calls for 0-arity functional the functions switch and >. So, we obtain final form
symbols) and conditional branching points. The main of program
idea of the translation procedure is to represent these
pow x,k switch k 0, x, k ,1 ;
1
components via rules in obtained TRS: left hand sides
x, k x x, k ;
of such rules have to represent these components and 12
right hand sides has to describe the process of values
x, k pow x, k1 ;
2
computation for corresponding components. Next,
R switchtrue, x, y x; .
since main elements of correction in base method are pow
narrowing rules, we are interested in more detailed
switch false, x, y y;
components splitting. For that we propose follow pro-
00 false; s x 0true;
cedure.
0s x false; s x s y x y
Assume we have a function φ( x ) = E[ x ] and ini-
tially empty program R .
φ The functional logical program obtained during
1. First of all, we put a rule φ(x , …, x ) E[x , our translation process can be analyzed using the base
…, x ] in R . 1 n 1
n φ method of correction. For that we have to split a given
2. For each rule r = () in R we perform fol- examples set to sets of positive and negative examples
low transformations: φ and then apply the described top-down correction al a. if ift then t else t , we replace r in R by gorithm.
1 2 3 φ Separation of examples. We suspect that correc r (switch(t , t , t ));
1 2 3 tion will work with specifications, which are repre b. if ' ' '' '' '
f(t ,,t , g(t ,,t ,h(t ,,t )),,t ,
1 i 1 j 1 w m sented by sets of computation examples. Such exam we introduce new function (x , …, x ), where
,)t 1 k ples can be obtained from specification in form of
n CTRS [7], while the last can be constructed from
k m is count of different variables, occurring in g- clause of some assertion language [9]. That deals with
headed subterm, replace r in R by f (t , …, t,
φ 1 i general idea of our synthesis process: source program
(p , …, p ), … t ) and add a new rule
1 k n is taken from case-memory after execution of search
xx,, g x ,,x , h x ,,x ,,x
1 k i i i i i procedure. Obviously, that sets of examples are an in 1 m n p d teresting base for similarity measure between cases:
in R .
φ when user gives a set of examples to a system, the
3. If R did not change during previous step, we
φ most similar case is the function, which closes the
finish translation procedure, else we return to the se- biggest part of these examples.
cond step. So, we need to separate these examples into posi 4. Next, we add to R definition of the function
φ tive and negative sets. We achieve this just by appli switch(w, x, y) and other non built-in functions (in cation of the program to left hand sides of examples
general, all used functions excluding s(x), d(x) and and comparing the result with corresponding right
dv(x, y)). hand sides.
In order to illustrate this translation, we can con- So, we have a set of examples E = {l = r}, where
sider following example. Assume we want to con- i i
l = ( x ) in every l . For each equation e in E we
struct term rewriting system that represents the func- i i
apply the considering program R , which narrows
tion pow (x, k) = if k > 0 then x pow(x, k – 1) else 1. φ
true or false answer. Examples, where R narrowed
After first step of translation we obtain R = {pow(x, φ
pow the true answer, we put in set of positive examples E.
k) if k > 0 then x pow(x, k – 1) else 1}. First itera- In another case, where R narrows a term s from l,
tion of step 2 with rule (a) gives us R = {pow (x, φ i i
pow we put the equation l = s in the set of negative exam k) switch (k > 0, x pow(x, k – 1), 1)}. Since R n i i
pow ples E .
has been changed, we repeat step 2. Now we will ap- For every example e we can construct (by applica ply rule (b) and obtain R = {pow(x, k)
pow tion of R) the derivation sequence
switch(k>0, (x, k), 1); (x, k) x pow(x,
1 1 ru,, ru,,
i 1 in
1 n
D (e) = e e … e true
k–1)}. We just replaced subclause pow(x, k – 1) by R 1 2 n
8
Программные продукты и системы № 3, 2014 г.
and occurring rules set OR (DR(e)) = r , r , , r . So, our future work will be directed to solving this
i i i
12 n problems and integration of these methods in case We will use this concepts later, during correction al- based program synthesis system.
gorithm, but note, that examples separation phase
gives us initial DR(e) and OR (DR(e)) for each exam- References
ple in the specification.
1. Kreitz C. Program Synthesis. Chapter III.2.5 of Automated
Application of the top-down algorithm. Proceed Deduction – A Basis for Applications. Kluwer Publ., 1998,
to the next step in main phase of program correction. pp. 105–134.
We apply the base top-down correction algorithm to 2. Magennis T. LINQ to Objects Using C# 4.0: Using and
Extending LINQ to Objects and Parallel LINQ (PLINQ). Addison the program R , that represents source function φ, and Wesley Professional Publ., 2010, 336 p.
φ
n 3. Kugler H., Segall I. Compositional synthesis of reactive
the positive and negative examples sets E and E re- systems from live sequence chart specifications. Proc. of the 15th
spectively, given by user. The first condition of the int. conf. on tools and algorithms for the construction and analysis
algorithm application is that the considering program of systems: held as part of the joint European Conferences on
has to derive at least one positive example. It was theory and practice of software (Proc. TACAS '09). ETAPS, Berlin,
checked at (unconsidered) step of most similar case Springer-Verlag Publ., Heidelberg Publ., 2009, pp. 77–91.
search and, besides that, at the examples set separa- 4. Aamondt A., Plaza E. Case-based reasoning: foundational
tion step. The initial form of the considering program issues, methodological variations, and system approaches. AI Com munications. 1994, vol. 7, no. 1, pp. 39–59.
(denoted as R ) is our program R itself. 5. Gomes P., Pereira F., Paiva P., Seco S., Carreiro P.,
0 φ Ferreira J., Bento C. Using CBR for automation of software design
First phase of the algorithm is consecutive search patterns. Proc. of the European Conf. on Base-Based Reasoning
of a discriminable rules and unfolding them with rela- (ECCBR’02). Cambridge, 2002.
tion to a current form of the program R. At each step 6. Hanus M. The integration of functions into logic pro i gramming: from theory to practice. Journ. of Logic Programming.
of this phase we check OR D e sets for each
1994, vol. 19&20, pp. 583–628.
Rk
i 7. Alpuente M., Ballis D., Correa F., Falaschi M. An integra n
example e E E and perform unfolding for a dis- ted framework for the diagnosis and correction of rule-based pro criminable rule and check intersection of them: if grams. Theoretical Computer Science archive. Elsevier Science
there are no rules that are used in derivation of a posi- Publ. Ltd. Essex, UK, 2010, vol. 411, iss. 47, pp. 4055–4101.
tive as well as a negative examples. 8. Klop J.W., de Vrijer R. Extended term rewriting systems.
Next phase is deletion: we remove all rules that Conditional and Typed Rewriting Systems. Lecture Notes in Com puter Science. 1991, vol. 516, pp. 26–50.
are used in derivation of negative examples and return 9. Comini M., Gori R., Levi G. Assertion based inductive
the obtained form of the program Rc. verification methods for logic programs. Electronic Notes in Theo Translation of TRS to function. At the previous retical Computer Science. 2001, vol. 40, pp. 52–69.
step we obtained the corrected version of the term re- Литература
writing system that represents the source function.
Now, we have to restore a function from the obtained 1. Kreitz C. Program Synthesis. Chapter III.2.5 of Automated
Deduction – A Basis for Applications. Kluwer Publ., 1998,
TRS. This procedure is similar unfolding, but we ap- pp. 105–134.
ply all applicable rules to right-hand side of the first 2. Magennis T. LINQ to Objects Using C# 4.0: Using and
rule simultaneously. Thus, the abstract program R = Extending LINQ to Objects and Parallel LINQ (PLINQ). Addison ={f(x) switch (g(x, 0), (x), (x)); (x) Wesley Professional Publ., 2010, 336 p.
1 2 1 3. Kugler H., Segall I. Compositional synthesis of reactive
s(s(x)); 2(x) d (d (x))} shall take form of the systems from live sequence chart specifications. Proc. of the 15th
function: f (x) = if g (x, 0) then s (s (x)) else d (d (x)). int. conf. on tools and algorithms for the construction and analysis
of systems: held as part of the joint European Conferences on
theory and practice of software (Proc. TACAS '09). ETAPS, Berlin,
Conclusion Springer-Verlag Publ., Heidelberg Publ., 2009, pp. 77–91.
4. Aamondt A., Plaza E. Case-based reasoning: foundational
issues, methodological variations, and system approaches. AI Com In this article we considered an adaptation of func- munications. 1994, vol. 7, no. 1, pp. 39–59.
tional logic programs correction method to the correc- 5. Gomes P., Pereira F., Paiva P., Seco S., Carreiro P.,
tion of functional programs. This method can be used Ferreira J., Bento C. Using CBR for automation of software design
patterns. Proc. of the European Conf. on Base-Based Reasoning
at reusing step of bigger program synthesis system (ECCBR’02). Cambridge, 2002.
that uses case-based reasoning approach. 6. Hanus M. The integration of functions into logic pro There are several problems that restrict applicabi- gramming: from theory to practice. Journ. of Logic Programming.
1994, vol. 19&20, pp. 583–628.
lity of the method for synthesis tasks: a specification 7. Alpuente M., Ballis D., Correa F., Falaschi M. An integra has to be given in form of examples, instead of com- ted framework for the diagnosis and correction of rule-based
pact first-order logic clause in deductive synthesis programs. Theoretical Computer Science archive. Elsevier Science
method; the system has to perform main loop several Publ. Ltd. Essex, UK, 2010, vol. 411, iss. 47, pp. 4055–4101.
8. Klop J.W., de Vrijer R. Extended term rewriting systems.
times; the correct answer is not guaranteed; and some Conditional and Typed Rewriting Systems. Lecture Notes in
others. But we hope that considering of functional Computer Science. 1991, vol. 516, pp. 26–50.
programs from term-rewriting point of view could be 9. Comini M., Gori R., Levi G. Assertion based inductive
an efficient way for solution of a synthesis problem. verification methods for logic programs. Electronic Notes in
Theoretical Computer Science. 2001, vol. 40, pp. 52–69.
9
Программные продукты и системы № 3, 2014 г.
MODULAR SOM FOR DYNAMIC OBJECT IDENTIFICATION
A.N. Averkin, Ph.D. (Physics and Mathematics), Associate Professor
(Dorodnicyn Computing Centre, RAS, Vavilova St. 40, Moscow, 119333, Russian Federation,
averkin2003@inbox.ru);
I.S. Povidalo, Postgraduate Student
(Dubna Internacional University for Nature, Socitty and Man,
Universitetskaya St. 19, Dubna, 141980, Russian Federation, ipovidalo@gmail.com)
Received 19.05.2014
Abstract. Object identification is complicated if noises are present in the source data, some of the object parameters
change according to unknown laws or the exact number of the object parameters is unknown. In such cases neural network
can be applied for dynamic object identification. There are a lot of different types of neural networks that can be used for dy namic object identification. Among different neural network architectures applicable for dynamic object identification a class
of neural networks based on self-organizing maps (SOM) can be noted. In this article, a number of neural networks based on
self-organizing maps that can be successfully used for dynamic object identification are described. Unique SOM-based mod ular neural networks, inspired by mammal's brain cortex studies, with vector quantized associative memory and recurrent
self-organizing maps as modules are presented. The structure and algorithms of learning and operation of such SOM-based
neural networks are described in details. Some experimental results and comparison with some other neural networks are giv en.
Keywords: neural networks, modular neural networks, forecasting, time series prediction, dynamic object identification,
VQTAM, RSOM.
УДК 004.9 Дата подачи статьи: 19.05.2014
ИДЕНТИФИКАЦИЯ ДИНАМИЧЕСКИХ ОБЪЕКТОВ
С ПОМОЩЬЮ МОДУЛЬНЫХ САМООРГАНИЗУЮЩИХСЯ КАРТ
Аверкин А.Н., к.ф.-м.н., доцент (Вычислительный центр им. А.А. Дородницына РАН,
ул. Вавилова, 40, г. Москва, 119333, Россия, averkin2003@inbox.ru);
Повидало И.С., аспирант (Международный университет природы, общества и человека «Дубна»,
ул. Университетская, 19, г. Дубна, 141980, Россия, ipovidalo@gmail.com)
Аннотация. Идентификация динамического объекта затруднена, если в исходных данных присутствуют шумы, неко торые параметры динамического объекта изменяются по неизвестным законам или точное число параметров объекта не из вестно. В таких случаях для решения задачи идентификации могут быть успешно применены нейронные сети. Существует
множество различных типов нейронных сетей, применимых для идентификации динамического объекта. Среди всевозмож ных нейросетевых структур, применимых для решения задачи идентификации, выделяется класс нейронных сетей, осно ванных на самоорганизующихся картах (SOM). В данной статье описан ряд нейронных сетей, основанных на самооргани зующихся картах и успешно применимых для идентификации динамических объектов. Представлены уникальные модуль ные нейронные сети на основе SOM, полученные в результате исследований коры головного мозга млекопитающих, где в
качестве модулей применены векторная квантовая память и рекуррентные самоорганизующиеся карты. Подробно описаны
структура и алгоритмы обучения и работы таких сетей, также приведены некоторые результаты экспериментов и сравнения
с другими нейросетевыми алгоритмами идентификации динамических объектов.
Ключевые слова: нейронные сети, модульные нейронные сети, прогнозирование, предсказание временных рядов,
идентификация динамических объектов, VQTAM, RSOM.
Identification theory solves problems of construct- Among different neural network architectures ap ing mathematical models of dynamic systems accord- plicable for dynamic object identification a class of
ing to the observations of their behaviour. The object neural networks based on self-organizing maps
identification step is one of the most important steps (SOM) can be noted. Neural networks of such type
while constructing mathematical models of objects or will be given special attention in this article due to
processes. The quality of the model relies on this step. their wider spread and successful application in solv Therefore, the quality of control that is based on this ing different kinds of problems of recognition [2],
model or results of a research with this model also re- identification [3], etc. A number of biomorphic neural
ly on this step. networks, architecture of which is the result of study Dynamic object identification is one of the basic ing the structure of the cerebral cortex of mammals,
problems which can be solved using many different will also be considered.
methods. For example statistic analysis or neural net-
works [1] can be used. Object identification is com- SOM-based neural networks can be used
plicated if noises are present in the source data, some for dynamic object identification
of the object parameters change according to un-
known laws or the exact number of the object parame- Problem definition. Identification of a dynamic
ters is unknown. In such cases neural network can be object that receives a vector of input parameters u(t)
applied for dynamic object identification. There are a and has a corresponding output vector y(t) can be de lot of different types of neural networks that can be scribed as finding the type of a model of this object,
that has an output ˆ and finding parameters of this
used for dynamic object identification. y()t
10