Его логическая и операционная семантика

Нас интересуют языки программирования, допускающие построение логической семантики. Во-первых, следует исключить из рассмотрения языки для реактивных систем, определяющих взаимодействующие параллельные процессы. Адекватной моделью для таких систем является алгебра процессов Р. Милнера [8] или Т. Хоара [9]. Проблематично построение логической семантики для императивных языков. Логическая семантика может быть построена для чистых языков функционального программирования. Каждой конструкции языка функционального программирования может быть сопоставлена эквивалентная формула на языке исчисления предикатов.

Множество вычислимых формул исчисления предикатов будем рассматривать в качестве общего базиса для всех языков, допускающих построение логической семантики. Вычислимые формулы будем записывать на языке исчисления вычислимых предикатов. Исчисление определяет набор базисных вычислимых предикатов, три базисных оператора (оператор суперпозиции, параллельный оператор и условный оператор) и механизм рекурсивного определения предикатов. Данный язык исчисления определен в форме языка программирования CCP (Calculus of Computable Predicates). Язык CCP определяет минимальный полный базис, достаточный, чтобы запрограммировать любой алгоритм, реализуемый в классе языков с логической семантикой. Язык неудобен для программирования и не предназначен для этого. Простота языка облегчает изучение математических свойств программ.

Язык CCP определяется в качестве минимального ядра для чистых языков функционального программирования. Система типов данных представлена в виде математической модели. Определяется логическая и операционная семантика языка. Доказывается теорема согласованности логической и операционной семантики.