Программирование вычислимых функций
В информатике представленный Программирование Вычислимых Функций (PCF) — это типизированный функциональный язык, Гордоном Плоткиным в 1977 году. [1] основано на ранее неопубликованном материале Даны Скотт . [примечание 1] Его можно рассматривать как расширенную версию типизированного лямбда-исчисления или упрощенную версию современных типизированных функциональных языков, таких как ML или Haskell .
модель Полностью абстрактная PCF была впервые предложена Робином Милнером . [2] Однако, поскольку модель Милнера по существу была основана на синтаксисе PCF, она была сочтена менее чем удовлетворительной. [3] Первые две полностью абстрактные модели, не использующие синтаксис, были сформулированы в 1990-х годах. Эти модели основаны на игровой семантике. [4] [5] и логические отношения Крипке . [6] Какое-то время считалось, что ни одна из этих моделей не является полностью удовлетворительной, поскольку они не обладают эффектным презентабельным видом. Однако Ральф Лоудер продемонстрировал, что эффективно представимая полностью абстрактная модель не может существовать, поскольку вопрос эквивалентности программ в конечном фрагменте PCF неразрешим. [7]
Синтаксис
[ редактировать ]Типы как ПКФ индуктивно определяются
- нат - это тип
- Для типов σ и τ существует тип σ → τ
Контекст — это список пар x : σ , где x — имя переменной, а σ — тип, так что ни одно имя переменной не дублируется. Затем обычным способом определяются суждения о типизации терминов в контексте для следующих синтаксических конструкций:
- Переменные (если x : σ является частью контекста Γ , то Γ ⊢ x : σ )
- Применение (термина типа σ → τ к терму типа σ )
- λ-абстракция
- Комбинатор неподвижной точки Y (создание термов типа σ из термов типа σ → σ )
- Операции преемника ( succ ) и предшественника ( pred ) над nat и константой 0.
- Условное if с правилом типизации:
- ( nat s здесь будет интерпретироваться как логические значения с таким соглашением, как ноль, обозначающий истину, и любое другое число, обозначающее ложь)
Семантика
[ редактировать ]Денотационная семантика
[ редактировать ]Относительно простой семантикой языка является модель Скотта . В этой модели
- Типы интерпретируются как определенные домены .
- (натуральные числа с присоединенным нижним элементом, с плоским порядком)
- интерпретируется как область определения непрерывных по Скотту функций из к , с поточечным упорядочением.
- Контекст интерпретируется как произведение
- Термины в контексте интерпретируются как непрерывные функции
- Переменные термины интерпретируются как прогнозы.
- Абстракция и применение лямбда интерпретируются с использованием декартовой замкнутой структуры категории областей и непрерывных функций.
- Y интерпретируется путем взятия наименее фиксированной точки аргумента
![{\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _ {\bot }}](https://wikimedia.org/api/rest_v1/media/math/render/svg/172645ff005d9c6b718219bfe5916ccfb9d63a68)
![{\displaystyle [\![\sigma \to \tau \,]\!]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f9216cddd2bbf07883a0a6d7259a98c7127a90d)
![{\displaystyle [\![\sigma ]\!]\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a3d0b607b4da282559d62257f064d874d4778c1f)
![{\displaystyle [\![\tau ]\!]\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fa3d8b955ce6db8d09b4b1605e705ecb8b4d7d16)
![{\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6e22396cfb4399fd87de4bf7388afd3409997e09)
![{\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a7ade925a4ceea33e5b118ee2c54a171c2cf15a4)
Эта модель не является полностью абстрактной для PCF; но он полностью абстрактен для языка, полученного добавлением параллельного оператора или к PCF. [4] : 293
Примечания
[ редактировать ]- ^ «PCF — это язык программирования для вычислимых функций, основанный на LCF, логике вычислимых функций Скотта». [1] Программирование вычислимых функций используется ( Mitchell 1996 ). Его также называют программированием с помощью вычислимых функций или языком программирования для вычислимых функций .
Ссылки
[ редактировать ]- ^ Перейти обратно: а б Плоткин, Гордон Д. (1977). «LCF рассматривается как язык программирования» (PDF) . Теоретическая информатика . 5 (3): 223–255. дои : 10.1016/0304-3975(77)90044-5 .
- ^ Милнер, Робин (1977). «Полностью абстрактные модели типизированных λ-исчислений» (PDF) . Теоретическая информатика . 4 : 1–22. дои : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
- ^ Онг, К.-ХЛ (1995). «Соответствие между операционной и денотационной семантикой: проблема полной абстракции для PCF» . В Абрамский С.; Габбай, Д.; Майбау, TSE (ред.). Справочник по логике в информатике . Издательство Оксфордского университета. стр. 269–356. Архивировано из оригинала 7 января 2006 г. Проверено 19 января 2006 г.
- ^ Перейти обратно: а б Хайланд, JME и Онг, C.-HL (2000). «О полной абстракции для PCF» . Информация и вычисления . 163 (2): 285–408. дои : 10.1006/inco.2000.2917 .
- ^ Абрамский С., Джагадисан Р. и Малакария П. (2000). «Полная абстракция для PCF» . Информация и вычисления . 163 (2): 409–470. дои : 10.1006/inco.2000.2930 .
{{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка ) - ^ О'Хирн, П.В. и Рике, Дж.Г. (1995). «Логические отношения Крипке и ПКФ» . Информация и вычисления . 120 (1): 107–116. дои : 10.1006/inco.1995.1103 .
- ^ Лоадер, Р. (2001). «Финитарные ПКФ неразрешимы» . Теоретическая информатика . 266 (1–2): 341–364. дои : 10.1016/S0304-3975(00)00194-8 .
- Скотт, Дана С. (1969). «Теоретико-типовая альтернатива CUCH, ISWIM, OWHY» (PDF) . Неопубликованная рукопись . Появился как Скотт, Дана С. (1993). «Теоретико-типовая альтернатива CUCH, ISWIM, OWHY» . Теоретическая информатика . 121 : 411–440. дои : 10.1016/0304-3975(93)90095-б .
- Митчелл, Джон К. (1996). «Язык ПКФ» . Основы языков программирования . ISBN 9780262133210 .