Программирование вычислимых функций - Programming Computable Functions

В Информатика, Программирование вычислимых функций ' (PCF) это напечатанный функциональный язык представлен Гордон Плоткин в 1977 г. на основании ранее неопубликованных материалов автора Дана Скотт.^{[примечание 1]} Его можно рассматривать как расширенную версию типизированное лямбда-исчисление или упрощенная версия современных типизированных функциональных языков, таких как ML или же Haskell.

А полностью абстрактный модель для ПКФ была впервые дана Milner (1977). Однако, поскольку модель Милнера была по существу основана на синтаксисе PCF, она считалась менее чем удовлетворительной (Ong, 1995). Первые две полностью абстрактные модели, не использующие синтаксис, были сформулированы в 1990-х годах. Эти модели основаны на семантика игры (Hyland and Ong, 2000; Abramsky, Jagadeesan, and Malacaria, 2000) и Крипке логические отношения (О'Хирн и Рике, 1995). Какое-то время считалось, что ни одна из этих моделей не была полностью удовлетворительной, поскольку они не были эффективно презентабельны. Тем не мение, Ральф Лоадер продемонстрировали, что не может существовать эффективно представимой полностью абстрактной модели, поскольку вопрос об эквивалентности программ в конечном фрагменте PCF не разрешим.

Синтаксис

В типы ПКФ индуктивно определяются как

• нац это тип
• Для типов σ и τ, есть тип σ → τ

А контекст это список пар х: σ, куда Икс это имя переменной и σ - это тип, поэтому имя переменной не дублируется. Затем определяют типизацию суждений терминов в контексте обычным способом для следующих синтаксических конструкций:

• Переменные (если х: σ является частью контекста Γ, тогда Γ ⊢ Икс : σ)
• Заявление (срока вида σ → τ к сроку типа σ)
• λ-абстракция
• В Y комбинатор с фиксированной точкой (составляя термины типа σ вне терминов типа σ → σ)
• Преемник (succ) и предшественник (пред) операции на нац и постоянная 0
• Условный если с правилом набора текста:

${\displaystyle {\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {if}}(t,s_{0},s_{1})\;:\sigma }}}$

(нацs здесь будет интерпретироваться как логическое значение с условием, что ноль обозначает истину, а любое другое число обозначает ложность)

Семантика

Денотационная семантика

Относительно простой семантикой для языка является Модель Скотта. В этой модели

• Типы интерпретируются как определенные домены.
  • ${\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}$ (натуральные числа с присоединенным нижним элементом, с плоским порядком)
  • ${\displaystyle [\![\sigma \to \tau \,]\!]}$ интерпретируется как область Скотт-непрерывный функции от ${\displaystyle [\![\sigma ]\!]\,}$ к ${\displaystyle [\![\tau ]\!]\,}$, с точечным порядком.
• Контекст ${\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}}$ интерпретируется как продукт ${\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}$
• Термины в контексте ${\displaystyle \Gamma \;\vdash \;x\;:\;\sigma }$ интерпретируются как непрерывные функции ${\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}$
  • Переменные термины интерпретируются как прогнозы
  • Лямбда-абстракция и приложение интерпретируются с помощью декартово закрыто структура категории областей и непрерывных функций
  • Y интерпретируется как наименьшая фиксированная точка аргумента

Эта модель не является полностью абстрактной для ПКФ; но это полностью абстрактно для языка, полученного добавлением параллельно или оператор в PCF (стр. 293 в ссылке Hyland and Ong 2000 ниже).

Примечания

1. «PCF - это язык программирования для вычислимых функций, основанный на LCF, логике вычислимых функций Скотта» (Плоткин 1977 ). Программирование вычислимых функций используется (Митчелл 1996 ). Его также называют Программирование с помощью вычислимых функций или же Язык программирования для вычислимых функций.

Рекомендации

• Скотт, Дана С. (1969). "Теоретико-типовая альтернатива CUCH, ISWIM, OWHY" (PDF). Неопубликованная рукопись. Появился как Скотт, Дана С. (1993). «Теоретико-типовая альтернатива CUCH, ISWIM, OWHY». Теоретическая информатика. 121: 411–440. Дои:10.1016 / 0304-3975 (93) 90095-б.
• Плоткин, Гордон Д. (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.
• Митчелл, Джон С. (1996). «Язык ПКФ». Основы языков программирования.
• Абрамский, С., Джагадисан, Р., и Малагария, П. (2000). «Полная абстракция для ПКФ». Информация и вычисления. 163 (2): 409–470. Дои:10.1006 / инк.2000.2930.
• Hyland, J. M. E. & Ong, C.-H. Л. (2000). «О полной абстракции для ПКФ». Информация и вычисления. 163 (2): 285–408. Дои:10.1006 / инк.2000.2917.
• О'Хирн, П. В. и Рике, Дж. Г. (1995). "Логические отношения Крипке и ПКФ". Информация и вычисления. 120 (1): 107–116. Дои:10.1006 / inco.1995.1103.
• Загрузчик, Р. (2001). «Финитарный ПКФ не разрешим». Теоретическая информатика. 266 (1–2): 341–364. Дои:10.1016 / S0304-3975 (00) 00194-8.
• Онг, Ч.-Х. Л. (1995). «Соответствие операционной и денотационной семантики: проблема полной абстракции для PCF». По Абрамскому, С .; Gabbay, D .; Майбау, Т. С. Э. (ред.). Справочник по логике в компьютерных науках. Издательство Оксфордского университета. С. 269–356. Архивировано из оригинал на 2006-01-07. Получено 2006-01-19.

внешняя ссылка

• Введение в RealPCF
• Лексер и парсер для PCF, написанные на SML