Теория языков программирования

Теория языков программирования (англ. programming language theory, PLT) — раздел информатики, посвящённый вопросам проектирования, анализа, определения характеристик и классификации языков программирования и изучением их индивидуальных особенностей^[1]. Тесно связана с другими ветвями информатики, результаты теории используются в математике, в программной инженерии и лингвистике.

История

В некотором смысле история теории языка программирования предшествует даже развитию самих языков программирования. В частности, λ-исчисление, разработанное Алонзо Чёрчем и Стивеном Клини в 1930-х годах, фактически является первым языком программирования, даже при том, что оно было предназначено больше для теоретических вопросов вычислимости, нежели является средством для программистов; многие современные функциональные языки программирования являются вариантами λ-исчисления. Дальнейшая история теории тесно переплетена с историей языков программирования, при этом в рамках теоретических исследований создавались новые парадигмы, конструкции и методы, а результаты внедрения их в практические языки программирования обеспечивали обратную связь для развития теории.

Первым языком программирования, который был изобретён для применения в действующей электронно-вычислительной машине, считается Планкалкюль Конрада Цузе, однако не получил известности у современников (изучен лишь в 1970-е годы и реализован в 1990-е годы). Первым же широко известным и успешным языком программирования стал Фортран (1954—1957), разработанный командой исследователей IBM во главе с Джоном Бэкусом. Успех Фортрана привёл к формированию комитета учёных, которые пытались разработать «универсальный» компьютерный язык; результатом их усилия был Алгол-58. Параллельно Джон Маккарти из MIT разработал язык программирования Лисп (основанный на λ-исчислении), который является первым успешным языком с академически проработанной теоретической основой. К 1950-м годам относятся разработка иерархии Хомского, оказавшая непосредственное влияние теорию языков программирования.

В 1964 году Питер Лэндин^[англ.] впервые реализовал вариант λ-исчисления, которое могло быть использовано для моделирования языков программирования (SECD-машина и J-оператор, по существу являющийся разновидностью продолжения). В 1966 году Лэндин разработал абстрактный язык программирования ISWIM.

В 1966 году Коррадо Бёмом и Джузеппе Якопини (итал. Giuseppe Jackopini) доказана теорема, согласно которой алгоритм может быть преобразован к виду, использующему только три структуры управления — последовательной, ветвление и цикл, впоследствии этот результат стал теоретическим фундаментом структурного программирования. В созданном Оле-Йоханом Далем и Кристеном Нюгором в 1967 году языке Симула был разработан, как полагают, первый пример языка объектно-ориентированного программирования и введено понятие сопрограммы. Важной вехой в развитии направления стал курс лекций Fundamental Concepts in Programming Languages^[англ.] Кристофера Стрейчи (англ. Christopher Strachey), выпущенный в 1967 году, где, кроме систематизации знаний по теории языков программирования, глубоко исследовано понятие полиморфизма. Значительный вклад в становление понятия о типах в языках программирования связывают с работой 1969 года Роджера Хиндли^[англ.], результаты которой вылились обобщённый в алгоритм вывода типов.

В 1969 году Тони Хоар разработал логику Хоара — первый пример аксиоматической семантики для языков программирования, обеспечивающей формальную верификацию программного кода. В 1970 году Даной Скоттом разработана денотационная семантика.

В 1972 году создана парадигма логического программирования и язык Пролог, в котором программа состоит непосредственно из набора хорновских дизъюнктов. Другой областью интересов теоретиков языков программирования начала 1970-х годов стало внедрение абстрактных типов данных на уровне конструкций языка, первым таким языком считается Клу (1974, Барбара Лисков).

Важной вехой на пути становления парадигмы функционального программирование стала разработка независимо Жираром (фр. Jean-Yves Girard; 1971) и Рейнольдсом (англ. John C. Reynolds; 1974) системы F — типизированного λ-исчисления второго порядка, обеспечивающего возможность конструирования термов, зависящих от типов. Также заметный вклад в развитие функционального программирования в середине 1970-х годов внесён разработчиками языка программирования Scheme — диалекта Лисп, включившего лексическую область видимости, объединённое пространство имён и элементы из модели акторов, в том числе продолжения. Подъём широкого интереса к функциональному программированию связан с тьюринговской лекцией создателя Фортрана Бэкуса 1977 года, в которой он критически проанализировав состояние популярных на тот момент языков программирования пришёл к функциональной парадигме.

В 1980 году Уильям Ховард (англ. William Alvin Howard), ссылаясь на труды логика Хаскелла Карри 1950-х годов, выявил структурное соответствие между компьютерными программами и математическими доказательствами, ставшее известным как изоморфизм Карри — Ховарда и ставшего теоретической основой класса языков автоматического доказательства.

В первую половину 1980-х годов значительное внимание уделено исследованиям по воплощению параллелизма в языках программирования и разработкам вариантов исчисления процессов: созданы исчисление взаимодействующих систем (Милнер, 1980), язык взаимодействующих последовательных процессов (Хоар, 1985), окончательно сформировалась модель акторов Хьюитта (англ. Carl Hewitt).

Выпуск языка Миранда в 1985 году подогрел академический интерес к ленивым чистым функциональным языкам программирования, в результате был создан комитет для определения открытого стандарта такого языка, в итоге в 1990 году вышел стандарт версии 1.0 языка Haskell.

В 1986 году в рамках работ по созданию языка Eiffel создана парадигма контрактного программирования (Бертран Мейер, 1986).

Разделы науки и смежные области

Теория изучает аспекты языков программирования, насколько это возможно, как совокупности, используя тот или иной конкретный язык как пример, но при этом задействуя средства достаточно высокого уровня общности, для возможности применения результатов к некоторому классу языков. Часто в теоретических разработках создаётся некоторый специализированный, «академический» язык программирования, не пригодный в силу тех или иных причин для практической реализации, но демонстрирующий те или иные теоретические результаты, которые впоследствии применяются к используемым в отрасли языкам. Для теоретических исследований используется инструментарий оснований математики и математической логики, включая теорию множеств, теорию моделей, теорию вычислимости, а также таких абстрактных разделов, как теория категорий, универсальная алгебра, теория графов, и существенно зависит от результатов прикладных направлений, в том числе теории сложности вычислений, теории кодирования.

Формальная семантика

Формальная семантика — такое формальное описание языков программирования, которое позволяет математически интерпретировать «смысл» компьютерной программы, написанной на этом языке. Существует три общих подхода, чтобы описать семантику языка программирования: денотационная семантика, операционная семантика и аксиоматическая семантика.

Теория типов

Теория типов — исследование систем типов; является «послушным синтаксическим методом для доказательства недостатков поведения определённой программы путём классификации фраз по уровню значений, которые они вычисляют»^[2]. Много языков программирования отличаются характеристиками их систем типов.

Анализ программы и преобразование

Анализ программы^[англ.] — общая проблема исследования программы и определения основных характеристик (таких как отсутствие ошибок в программе).

Преобразование программы^[англ.] — процесс преобразования программы из одной формы (языка) в другую форму.

Сравнительный анализ языка программирования

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

Обобщённое и метапрограммирование

Обобщённое программирование — парадигма программирования, заключающаяся в таком описании данных и алгоритмов, которое можно применять к различным типам данных, не меняя само это описание.

Метапрограммирование — генерация программ высшего порядка, которые, когда выполняются, создают программы (возможно на другом языке или в подмножестве первоначального языка) в результате своей работы.

Предметно-ориентированные языки

Предметно-ориентированные языки — языки, которые созданы для эффективного решения задач в конкретной предметной области.

Конструкция компилятора

Теория компилятора — это теория написания компиляторов (или в более общем плане трансляторов); программы, которые переводят программу, написанную на одном языке, в другую форму.

Действия компилятора традиционно разбиты на:

лексический анализ
синтаксический анализ (сканирование и парсинг)
семантический анализ (определение того, что программа должна сделать)
оптимизация (улучшает производительность программы, как указано некоторой метрикой; обычно это скорость выполнения)
генерация кода (генерация и вывод эквивалентной программы на некотором выходном языке; часто это система команд процессора).

Среда выполнения

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

См. также

Примечания

↑ Ракитов А. И. Науковедческие исследования. — Directmedia, 2014. — С. 121. — 255 с. — ISBN 5248006538. Архивировано 20 декабря 2016 года.
↑ Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA.

Литература

https://web.archive.org/web/20170125145344/http://foswiki.cs.uu.nl/foswiki/Techno/ProgrammingLanguageTheoryTextsOnline
Abadi, Martín and Cardelli, Luca. A Theory of Objects. Springer-Verlag.
Michael J. C. Gordon. Programming Language Theory and Its Implementation. Prentice Hall.
Gunter, Carl and Mitchell, John C. (eds.). Theoretical Aspects of Object Oriented Programming Languages: Types, Semantics, and Language Design. MIT Press.
Harper, Robert. Practical Foundations for Programming Languages. Draft version.
Knuth, Donald E. (2003). Selected Papers on Computer Languages. Stanford, California: Center for the Study of Language and Information.
Mitchell, John C.. Foundations for Programming Languages.
Mitchell, John C.. Introduction to Programming Language Theory.
O’Hearn, Peter. W. and Tennent, Robert. D. (1997). Algol-like Languages. Progress in Theoretical Computer Science. Birkhauser, Boston.
Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.
Pierce, Benjamin C. Advanced Topics in Types and Programming Languages.
Pierce, Benjamin C. et al. (2010). Software Foundations.

Ссылки

Computer Languages History (англ.)
Lambda the Ultimate, a community weblog for professional discussion and repository of documents on programming language theory.
Great Works in Programming Languages. Collected by Benjamin C. Pierce (University of Pennsylvania).
Classic Papers in Programming Languages and Logic. Collected by Karl Crary (Carnegie Mellon University).
Programming Language Research. Directory by Mark Leone.
Programming Language Theory Texts Online. At Utrecht University.
λ-Calculus: Then & Now by Dana S. Scott for the ACM Turing Centenary Celebration
Grand Challenges in Programming Languages. Panel session at POPL 2009.

[1] Ракитов А. И. Науковедческие исследования. — Directmedia, 2014. — С. 121. — 255 с. — ISBN 5248006538. Архивировано 20 декабря 2016 года.

[2] Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA.

[1]

[2]