Программирование вычислимых функций
-
Основы PCF
- PCF — это функциональный язык программирования, введенный Гордоном Плоткиным в 1977 году.
- Он является расширением типизированного лямбда-исчисления и упрощением современных функциональных языков, таких как ML и Haskell.
-
Модели и семантика
- Первая полностью абстрактная модель PCF была предложена Робином Милнером, но оказалась неудовлетворительной.
- В 1990-х годах были сформулированы две модели, основанные на игровой семантике и логических отношениях Крипке.
- Ральф Лоудер доказал, что полностью абстрактной модели для PCF не существует, так как вопрос эквивалентности программ неразрешим.
-
Синтаксис и типы
- Типы PCF определяются индуктивно, включая типы натуральных чисел и функции.
- Контекст представляет собой список пар имя переменной: тип, где имя переменной не повторяется.
- Определены типизация суждений и основные операции, включая лямбда-абстракцию и комбинатор с фиксированной точкой.
-
Семантика
- Модель Скотта является простой семантикой для PCF, где натуральные числа интерпретируются как область непрерывных функций.
- Контекст интерпретируется как продукт множеств типов переменных, а переменные и лямбда-абстракции — как прогнозы.
- Лямбда-абстракция и применение интерпретируются через декартову замкнутую структуру категорий областей и непрерывных функций.
-
Применение и рекомендации
- PCF используется для программирования вычислимых функций и называется также RealPCF.
- Существует лексический и синтаксический анализатор PCF, написанный на SML.