В лямбда-исчислении , ветви математической логики, связанной с формальным изучением функций, стратегия сокращения - это то, как сложное выражение сводится к простому выражению путем последовательных шагов сокращения. Это похоже на понятие стратегии оценки в информатике, но немного отличается от него .
Обзор [ править ]
Грубо говоря, стратегия сокращения - это функция, которая отображает член лямбда-исчисления с приводимыми выражениями в одно конкретное приводимое выражение, которое будет сокращено следующим. Математические логики изучали свойства этой системы на протяжении десятилетий, и внешнее сходство между описанием стратегий оценки и стратегий сокращения первоначально привело к тому, что исследователи языков программирования предположили, что они идентичны, - убеждение, которое все еще просматривается в популярных учебниках с самого начала 1980-е годы; [1] это, однако, разные концепции. [ необходима цитата ]
Однако в 1973 году Плоткин [2] показал, что правильная модель стратегии оценки требует формулировки новой аксиомы для вызовов функций, то есть совершенно нового исчисления. Он подтверждает эту идею с помощью двух различных исчислений: одно для вызова по имени, а другое для вызова по значению , каждое для чисто функциональных языков программирования . Он также показывает, что такое исчисление удовлетворяет двум естественным критериям. Во-первых, исчисление определяет функцию оценки, которая отображает закрытые термины (представления программ) на ответы (представления результатов). Эта теорема основана на обычной теореме Черча – Россера.для модифицированного исчисления. Функция оценки определяется с помощью традиционной теоремы стандартизации Карри – Фейса. Во-вторых, исчисление - это надежная система рассуждений по уравнениям по отношению к понятию Морриса об эквивалентности наблюдений. [3]
Двадцать лет спустя Крэнк и Фелляйзен показали, как масштабировать работу Плоткина на языки с императивными операторами присваивания. [4] Они определяют исчисления для языка с переменными, функциями, приложением функции и оператором присваивания, которые охватывают традиционные понятия передачи параметров и стратегии оценки широкого спектра языков программирования. Они показывают, что каждое исчисление удовлетворяет критериям Плоткина, включая традиционные теоремы Черча – Россера и Карри – Фейса соответственно. Кроме того, они вводят исчисление, которое подкрепляет понятие ссылочной ячейки в ML .
Ariola и Felleisen [5] и независимо друг от друга Maraist, Одерский и Wadler [6] завершили эту линию работы с дизайном лямбды - исчисление , что именно относится к понятию вызова по необходимости аки ленивым функциональное программирование на эквациональную систему расчета. В отличие от исчислений вызова по значению и вызова по имени Плоткина, это исчисление вызова по необходимости требует четырех аксиом для характеристики вызовов функций. Чанг и Фелляйзен [7] в конечном итоге смогли показать, как создать исчисление по необходимости с единственной, но сложной аксиомой.
См. Также [ править ]
- Вызов по значению , семантическая парадигма, которая позволяет работать как с вызовом по имени, так и с вызовом по значению.
- Абстрактная машина с динамической геометрией взаимодействия - это эффективная основанная на графах структура для любой стратегии оценки (см. Интерактивную онлайн- реализацию ).
Ссылки [ править ]
- ^ Структура и интерпретация компьютерных программ Абельсоном и Сассманом, MIT Press 1983
- ^ Вызов по имени, вызов по значению и лямбда-исчисление
- ^ "Языки программирования и лямбда-исчисление Джеймсом Моррисом, MIT 1968"
- ^ Передача параметров и лямбда-исчисление Крэнком и Фелляйзеном, Принципы языков программирования 1991
- ^ Лямбда-исчисление по требованию Ариолы и Фелляйзена, Журнал функционального программирования, 1997 г.
- ^ Лямбда-исчисление по требованию Мараиста Одерски и Вадлера, Журнал функционального программирования, 1999 г.
- ^ Лямбда-исчисление по требованию, пересмотренное Чангом и Фелляйзеном, Европейский симпозиум по программированию, 2012 г.
