16 июня 2022 г. в МГТУ имени Н. Э. Баумана (Москва)

Пятое совместное рабочее совещание ИПС имени А.К. Айламазяна РАН и МГТУ имени Н.Э. Баумана по функциональному языку программирования Рефал

8 июня 2021 г. в МГТУ имени Н. Э. Баумана (Москва)

Четвёртое совместное рабочее совещание ИПС имени А.К. Айламазяна РАН и МГТУ имени Н.Э. Баумана по функциональному языку программирования Рефал

12 июня 2020 г. в МГТУ имени Н. Э. Баумана (Москва)

Третье совместное рабочее совещание ИПС имени А.К. Айламазяна РАН и МГТУ имени Н.Э. Баумана по функциональному языку программирования Рефал

11 июня 2019 г. в МГТУ имени Н. Э. Баумана (Москва)

Второе совместное рабочее совещание ИПС имени А.К. Айламазяна РАН и МГТУ имени Н.Э. Баумана по функциональному языку программирования Рефал

5 июня 2018 г. в МГТУ имени Н. Э. Баумана (Москва)

Совместное рабочее совещание ИПС имени А.К. Айламазяна РАН и МГТУ имени Н.Э. Баумана по функциональному языку программирования Рефал

1 марта 2018 г.

Антонина Н. Непейвода

(ИПС РАН)

Применение уравнений в словах при преобразовании программ над строковым типом.

Доклад на семинаре Института системного программирования РАН «Технологии разработки и анализа программ»

 

1. 23 ноября 2021 г.

   Антонина Н. Непейвода

   (ИПС РАН)

   Теорема Турчина в анализе контекстно-свободных языков.
   открыть аннотацию ...
   закрыть аннотацию

   Если язык L контекстно-свободен, для него выполняется известное свойство накачки Бар-Хиллела, также называемое леммой о разрастании. А именно, существует такое натуральное число N, зависящее только от L, что всякое достаточно длинное слово u языка L можно разбить на пять частей: u = x1 y1 z y2 x2 так, что слово y1 y2 не пусто, |y1 z y2|<=N и все слова вида x1 y1^i z y2^i x2 также принадлежат языку L.
   Зачастую это свойство применяется, чтобы доказать что язык L не принадлежит множеству контекстно-свободных языков. Однако формулировка леммы о разрастании такова, что она выполняется также для некоторых языков, не являющихся контекстно-свободными.
   Используя теорему Турчина, можно построить модификации этой леммы, которые позволяют делать более точный анализ свойств языка.

2. 18 ноября 2021 г.

   Сергей Д. Мешвелиани

   (ИПС РАН)

   О свойствах допустимого упорядочения на показателях мономов нескольких переменных. Конструктивный подход.
   открыть аннотацию ...
   закрыть аннотацию

   В докладе будут рассматриваться конструктивное доказательство завершаемости алгоритма NF построения нормальной формы для многочленов нескольких переменных и связанное с ним понятие допустимого упорядочения <_e на показателях мономов. В классической математике нётеровость отношения <_e выводится из леммы Диксона, и этого достаточно для обоснования завершаемости алгоритма NF. В доказательном программировании требуется более сильное свойство: свойство правильного (хорошей заданности, well-founded) отношения порядка. В докладе будет дано конструктивное доказательство этого свойства, сначала - для случая двух переменных.

3. 8 ноября 2021 г.

   Андрей П. Немытых

   (ИПС РАН)

   Полуформальное построение алгоритма Матиясевича & Кнута-Морриса-Пратта из алгоритма наивного поиска подстроки в строке.
   открыть аннотацию ...
   закрыть аннотацию

   В докладе будет показано, как можно получить программный код алгоритма Матиясевича & Кнута-Морриса-Пратта, известного как "KMP-алгоритм", из программного кода алгоритма наивного поиска подстроки в строке посредством полуформальных рассуждений, где программные коды даны в терминах некоторого функционального языка программирования. (По мотивам статьи Р.С. Бёрда, Дж. Гиббонса и Г. Джонса, 1989 г.)
   Автоматические методы оптимизации программ, основанные на подходе свертки/развертки, как правило, могут преобразовать такую программу наивного поиска в специализированный алгоритм Матиясевича & Кнута-Морриса-Пратта, когда, кроме программы, на вход оптимизатору подается конкретная искомая подстрока-образец.
   Обычно оптимизатор тестируется на двух-трех примерах таких образцов, после чего объявляется, что он "способен генерировать алгоритм Матиясевича & Кнута-Морриса-Пратта для любого фиксированного образца".
   Современное состояние указанных выше методов оптимизации не позволяет построить алгоритм Матиясевича & Кнута-Морриса-Пратта равномерно по множеству всех образцов.

4. 25 июня 2018 г.

   Сергей Д. Мешвелиани

   (ИПС РАН)

   Построение доказательных программ арифметики натуральных чисел в двоичном представлении.
   открыть аннотацию ...
   закрыть аннотацию

   Стандартная библиотека языка программирования с зависимыми типами Агды (Agda) выполняет арифметические действия над натуральными числами, вызывая встроенные функции из библиотеки Glasgow Haskell, которые обрабатывают числа, представленные в системе счисления по основанию машинное слово. Свойства этих функций считаются истинными аксиомами, то есть не доказываются средствами языка Агда. Этот недостаток может быть исправлен почти полностью.
   
   В докладе будет рассказано о реализации разработанной автором библиотеки доказательных программ Binary, которая исправляет этот недостаток и дополняет раздел Bin Стандартной библиотеки lib-0.16 языка Агда.
5. 29 ноября 2017 г.

   Антонина Н. Непейвода

   (ИПС РАН)

   Применение уравнений в словах при преобразовании программ над строковым типом.
   открыть аннотацию ...
   закрыть аннотацию

   При преобразовании программ, манипулирующих строками, часто возникает проблема поиска решений уравнений в словах. Пусть дана следующая функция F, рекурсивно реализующая некоторый предикат на множестве слов. x,y - строковые переменные, A - константа алфавита.
   
   F(xAx) = F(x);
   F( ) = True;
   F(y) = False;
   
   Пусть требуется исследовать свойства этого предиката на множестве слов вида zz, где z - параметр, пробегающий все слова в алфавите, и упростить данное определение. При попытке сопоставления параметризованного слова zz с аргументом первого правила определения функции F возникает уравнение xAx = zz, выполнимость которого при некотором z является необходимым и достаточным условием успешного сопоставления.
   
   Если стоит задача автоматической верификации некоторого свойства программы либо её оптимизации, то уравнения могут быть введены алгоритмом преобразования, перед которым стоит эта задача. Например, если алгоритм преобразования объявляет параметризованные выражения A F(x) и F(y) частными случаями выражения w F(v), получаемыми подстановками w -> A | EMPTY, v -> x | y (где EMPTY - пустое слово), и затем работает уже с выражением w F(v) как обобщением двух рассмотренных выражений, полезным окажется уточнение, что в каждом из частных случаев этого выражения выполняется уравнение Aw =wA.
   
   Суперкомпиляция - это метод преобразования программ, основанный на развёртке дерева параметризованных состояний программы и существенно использующий алгоритмы сопоставления параметризованных данных и их обобщения. В докладе будут рассмотрены некоторые возможности модельного суперкомпилятора MSCP, позволяющие ему оперировать уравнениями в словах и использовать их в данных алгоритмах.

   подробнее ...

6. 9 сентября 2013 г.

   Андрей П. Немытых

   (ИПС РАН)

   Уравнения в свободном моноиде (Лекция №2).
   открыть аннотацию ...
   закрыть аннотацию

   Я расскажу о связи систем уравнений в свободном моноиде M ранга 2 с системами (нелинейных) диафантовых уравнений и сведении вопроса разрешимости уравнения в свободном моноиде K конечного (большего единицы) ранга к разрешимости уравнения в M. Будут показаны конструкции сведения неравнства в K к формуле, содержащей только кванторы существования по неизвестным и дизъюнкции равенств в К; дизъюнкция двух равенств, в свою очередь, может быть сведена к формуле, содержащей только кванторы существования по неизвестным одного равенства в К. Также будет решено произвольное бескоэффициентное уравнение с двумя неизвестными.

   подробнее ...

7. 12 и 19 августа 2013 г.

   Андрей П. Немытых

   (ИПС РАН)

   Уравнения в свободном моноиде и язык программирования Рефал (Лекция №1).
   открыть аннотацию ...
   закрыть аннотацию

   Я попытаюсь рассказать о связи языка программирования Рефал с решением уравнений в конечнопорожденной свободной полугруппе с единицей. Вводный курс будет состоять из нескольких (более или менее регулярных) лекций. Цель курса - знакомство с некоторыми понятиями алгоритма Маканина, перечисляющего множество решений данного уравнения. В первой лекции я расскажу о двух классах уравнений в свободном моноиде конечного ранга, для которых существуют простые алгоритмы решения. Уравнения из первого класса называются квадратичными: каждая неизвестная входит в них не более двух раз. Второй класс - это уравнения с одной неизвестной.

   подробнее ...

8. 19 декабря 2012 г.

   Сергей Д. Мешвелиани

   (ИПС РАН)

   Доказуемое программирование математики на функциональном языке с зависимыми типами (часть I, введение).
   открыть аннотацию ...
   закрыть аннотацию

   Будет сделано введение в систему доказуемого программирования на зависимых типах, основанную на конструктивной теории типов (dependent types programming, intuitionistic type theory by M. Loef, языки и системы Coq, Agda). Язык программирования Agda есть расширение языка Haskell на зависимые типы. Исследуется способ построения библиотеки вычислительной алгебры с применением средства доказуемого программирования, даваемого Агдой. Будут рассмотрены различные простые примеры.

9. 3 октября 2012 г.

   Николай Н. Непейвода

   (ИПС РАН)

   Алгебры программ: новый подход (часть II).
   открыть аннотацию ...
   закрыть аннотацию

   Рассматривается алгебраический подход к программам, базирующийся на различении действий и функций, независимый от конкретных операторов алгоритмического языка и позволяющий описывать классы программ в соответствии со свойствами определяемых ими преобразований.

10. 26 сентября 2012 г.

    Николай Н. Непейвода

    (ИПС РАН)

    Алгебры программ: новый подход.
    открыть аннотацию ...
    закрыть аннотацию

    Рассматривается алгебраический подход к программам, базирующийся на различении действий и функций, независимый от конкретных операторов алгоритмического языка и позволяющий описывать классы программ в соответствии со свойствами определяемых ими преобразований.

11. 5 сентября 2012 г.

    Антонина Н. Непейвода

    (ИПС РАН)

    Об одном простом доказательстве теоремы Турчина о стековой грамматике.
    открыть аннотацию ...
    закрыть аннотацию

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