Введение в теорию программирования. Функциональный подход


Вступительная лекция - часть 5


Основным понятием для SECD-машины является понятие состояния.

Уже в 70-е годы группой ученых института INRIA (Франция), ведущую роль в работе которой сыграл Пьер Кюрьен (P.-L. Curien), была создана еще одна абстрактная машина, основанная на смене состояний и получившая название категориальной абстрактной машины (КАМ). Теория категорий в форме категориальной комбинаторной логики, которая является теоретическим фундаментом для КАМ, по сути, представляет собой вариант ламбда-исчисления. С помощью КАМ был реализован еще один современный диалект ML, получивший название CaML (по имени машины).

В ходе исследования абстрактных машин возникает проблема оптимизации стратегии вычислений.

В качестве основной формализации для настоящего курса используется комбинаторная логика Х. Карри, которая позволяет моделировать вычисления в среде абстрактных машин, в значительной мере схожих с виртуальной машиной Microsoft .NET.

Исследования различных стратегий передачи параметров при обращении к функциям языков программирования (в частности, вызова функций по имени и по значению) были проведены Г. Плоткиным (G.D. Plotkin) на основе развития формализации SECD-машины П. Лендина. Полученные результаты легли в основу стратегии моделирования вычислений в ранних версиях языка функционального программирования ML.

В 70-х годах К. Уодсворт (Christopher P. Wadsworth) предложил механизм редукции графов для моделирования так называемых "ленивых" (т.е. выполняемых исключительно по мере необходимости) вычислений с помощью фундаментальной формальной теории-исчисления ламбда-конверсий.

Несколько позже Д. Тернером был представлен аналогичный механизм для "ленивых" вычислений в более приближенной к практике программирования формальной системе, а именно, в терминах выражений комбинаторной логики.

Затем, в 80-х годах, группе ученых во главе с П. Кюрьеном удалось усовершенствовать формализацию SECD-машины П. Лендина, и была создана категориальная абстрактная машина, оптимизация кода которой изучается в данном курсе.




Начало  Назад  Вперед



Книжный магазин