Добрый день всем!
Форвардирую объявление о семинаре по компьютерной алгебре на факультете ВМиК
МГУ, на котором выступит И.Г.Ключников с докладом:
"Выявление и доказательство свойств функциональных программ методами
суперкомпиляции".
На этом семинаре будет сделано 2 доклада. Доклад Ильи второй. На него выделено
45 мин. - второй учебный час пары.
Андрей
----- Original Message -----
From: Victor Edneral
To: Victor Edneral
Sent: 13 Oct 2010 14:31
Subject: Seminar on Computer Algebra on 20.10.2010
Dear Colleagues,
The meeting of the Computer Algebra seminar will take place on Wednesday,
October 20, at 16.20 in room 582 of VMK building of Moscow State University.
Regards,
Victor Edneral
---------------------------------------------------------------------------
Повестка дня:
1. Доклад: "Дифференциальные идеалы".
Д.Трушин (Mеханико-математический факультет МГУ).
Работа посвящена решению следующих трех проблем: нахождение критерия
конечности дифференциальных стандартных базисов, описание квазиспектра алгебры
разделенных степеней и построение алгебраической теории конструируемых
дифференциальных полей.
2. Доклад: "Выявление и доказательство свойств функциональных программ методами
суперкомпиляции".
И.Г.Ключников (ИПМ им.М.В.Келдыша РАН).
На основе существующих алгоритмов суперкомпиляции для функциональных языков
первого порядка был разработан новый алгоритм суперкомпиляции для
функционального языка высшего порядка, ориентированный на трансформационный
анализ. Суть трансформационного подхода к анализу программ можно сформулировать
следующим образом: вместо того, чтобы анализировать исходную программу, вначале
преобразуем эту программу в эквивалентную ей, но легче поддающуюся анализу.
Разработанный алгоритм реализован в экспериментальном суперкомпиляторе
HOSC, являющимся первым суперкомпилятором для языка Haskell, для которого
формально доказаны теоремы корректности и завершаемости.
Суперкомпилятор HOSC способен распознавать эквивалентность большого класса
выражений на основе синтаксического сравнения остаточных программ в полностью
автоматическом режиме, а также выявлять среди распознанных эквивалентных
выражений улучшающие леммы.
Предложен новый метод многоуровневой суперкомпиляции, основанный на
применении улучшающих лемм. Многоуровневый суперкомпилятор способен выполнять
более глубокие содержательные преобразования программ, а также улучшать
асимптотику программ.
Результаты могут использоваться в других системах преобразования программ,
доказательства теорем, компьютерной алгебре, где проводятся манипуляции с
лямбда-термами и надо решать такие задачи как обобщение термов, завершаемость
процесса преобразований и т.п.
----------------------------------------------------------------------------
Agenda:
1. Report: "Differential ideals".
D. Trushin (Faculty of Mechanics and Mathematics of MSU).
Our purpose is to solve the following three problems: finding a criterion
for a differential ideal to have a finite differential standard basis,
describing the quasi-spectrum of a ring of divided powers, and constructing an
algebraic theory of constructible differential fields.
2. Report: "Inferring and proving properties of functional programs by means of
supercompilation".
I.G.Klyuchnikov (Keldysh Institute of Applied Mathematics, RAS).
A new algorithm of supercompilation for higher-order functional language
has been developed, which, unlike other algorithms, is intended to be used for
program analysis, rather than optimization, the main idea being that the
transformed program may be easier to analyze, than the original one.
This algorithm has been implemented in an experimental supercompiler HOSC,
the first supercompiler for Haskell whose correctness and termination
properties have been carefully investigated and formally proved.
HOSC is able to automatically prove the equivalence of a large class of
higher-order expressions by just comparing the corresponding residual
expressions for syntactical identity. Moreover, a slight modification of HOSC
is often capable to check if a pair of equivalent expressions forms an
improvement lemma.
A new method of multi-level supercompilation, based on the use of
improvement lemmas, is suggested. We show that a multi-level supercompiler, in
comparison to single-level ones, is able to perform deeper program
transformations, improving asymptotic complexity of programs.
The results obtained are applicable also to other areas where lambda terms
are transformed, generalized or there is a need to ensure the termination of
rewriting -- such as program transformation systems, theorem provers, computer
algebra, etc.
