В информатике , программирование вычислимых функций (PCF) является набранным функциональным языком введен Гордоном Плоткиным в 1977 году, на основе предыдущего неопубликованного материала по Дане Скотт . [примечание 1] Его можно рассматривать как расширенную версию типизированного лямбда-исчисления или упрощенную версию современных типизированных функциональных языков, таких как ML или Haskell .
Полностью абстрактной модели для ФКВ впервые был дан Милнер (1977). Однако, поскольку модель Милнера была по существу основана на синтаксисе PCF, она считалась менее чем удовлетворительной (Ong, 1995). Первые две полностью абстрактные модели, не использующие синтаксис, были сформулированы в 1990-х годах. Эти модели основаны на семантике игр (Hyland, Ong, 2000; Abramsky, Jagadeesan, and Malacaria, 2000) и логических отношениях Крипке (O'Hearn and Riecke, 1995). Какое-то время считалось, что ни одна из этих моделей не была полностью удовлетворительной, поскольку они не были эффективно презентабельны. Однако Ральф Лоадер продемонстрировали, что не может существовать эффективно представимой полностью абстрактной модели, поскольку вопрос об эквивалентности программ в конечном фрагменте PCF не разрешим.
Синтаксис
Эти типы из PCF индуктивно определяется как
- нат это тип
- Для типов σ и τ существует тип σ → τ
Контекст представляет собой список пар х: сг , где х представляет собой имя переменной и σ представляет собой тип, например , что имя переменной не дублируется. Затем определяют типизацию суждений терминов в контексте обычным способом для следующих синтаксических конструкций:
- Переменные (если x: σ является частью контекста Γ , то Γ ⊢ x : σ )
- Применение (терма типа σ → τ к члену типа σ )
- λ-абстракция
- Y фиксированная точка комбинатор ( что делает условия типа сг из условий типа сг → сг )
- Операции преемника ( succ ) и предшественника ( pred ) над nat и константой 0
- Условное if с правилом ввода:
- ( nat s будет интерпретироваться здесь как логическое с условием, например, что ноль обозначает истину, а любое другое число обозначает ложность)
Семантика
Денотационная семантика
Относительно простой семантикой для языка является модель Скотта . В этой модели
- Типы интерпретируются как определенные домены .
- (натуральные числа с присоединенным нижним элементом, с плоским порядком)
- интерпретируется как область определения непрерывных по Скотту функций из к , с точечным порядком.
- Контекст интерпретируется как продукт
- Термины в контексте интерпретируются как непрерывные функции
- Переменные термины интерпретируются как прогнозы
- Лямбда-абстракция и приложение интерпретируются с использованием декартовой замкнутой структуры категории доменов и непрерывных функций.
- Y интерпретируется путем взятия наименьшей фиксированной точки аргумента
Эта модель не является полностью абстрактной для ПКФ; но он полностью абстрактен для языка, полученного добавлением к PCF параллельного оператора or (стр. 293 в ссылке Hyland and Ong 2000 ниже).
Заметки
- ^ «PCF - это язык программирования для вычислимых функций, основанный на LCF, логике вычислимых функций Скотта» ( Плоткин 1977 ). Программирование вычислимых функций используется ( Mitchell 1996 ). Это также называется программированием с помощью вычислимых функций или языком программирования для вычислимых функций .
Рекомендации
- Скотт, Дана С. (1969). «Теоретико-типовая альтернатива CUCH, ISWIM, OWHY» (PDF) . Неопубликованная рукопись . CS1 maint: обескураженный параметр ( ссылка ) Появился как Скотт, Дана С. (1993). «Теоретико-типовая альтернатива CUCH, ISWIM, OWHY». Теоретическая информатика . 121 : 411–440. DOI : 10.1016 / 0304-3975 (93) 90095-b . CS1 maint: обескураженный параметр ( ссылка )
- Плоткин, Гордон Д. (1977). «LCF рассматривается как язык программирования» (PDF) . Теоретическая информатика . 5 (3): 223–255. DOI : 10.1016 / 0304-3975 (77) 90044-5 . CS1 maint: обескураженный параметр ( ссылка )
- Милнер, Робин (1977). «Полностью абстрактные модели типизированных λ-исчислений» (PDF) . Теоретическая информатика . 4 : 1–22. DOI : 10.1016 / 0304-3975 (77) 90053-6 . CS1 maint: обескураженный параметр ( ссылка )
- Митчелл, Джон С. (1996). «Язык ПКФ». Основы языков программирования . CS1 maint: обескураженный параметр ( ссылка )
- Абрамский, С., Джагадисан, Р., и Малякария, П. (2000). «Полная абстракция для ПКФ» . Информация и вычисления . 163 (2): 409–470. DOI : 10.1006 / inco.2000.2930 .CS1 maint: несколько имен: список авторов ( ссылка )
- Хайленд, JME & Ong, C.-HL (2000). «О полной абстракции для ПКФ» . Информация и вычисления . 163 (2): 285–408. DOI : 10.1006 / inco.2000.2917 .
- О'Хирн, П. У. и Рике, Дж. Г. (1995). «Логические отношения Крипке и ПКФ» . Информация и вычисления . 120 (1): 107–116. DOI : 10.1006 / inco.1995.1103 .
- Загрузчик, Р. (2001). «Finitary PCF не разрешима». Теоретическая информатика . 266 (1–2): 341–364. DOI : 10.1016 / S0304-3975 (00) 00194-8 .
- Онг, К.-Х.Л. (1995). «Соответствие операционной и денотационной семантики: проблема полной абстракции для PCF» . По Абрамскому, С .; Gabbay, D .; Майбау, TSE (ред.). Справочник по логике в компьютерных науках . Издательство Оксфордского университета. С. 269–356. Архивировано из оригинала на 2006-01-07 . Проверено 19 января 2006 .
Внешние ссылки
- Введение в RealPCF
- Лексер и парсер для PCF, написанные на SML