Язык CCP (Calculus of Computable Predicates) - язык исчисления вычислимых предикатов, определяющий множество вычислимых формул исчисления предикатов. К языку предъявляются два требования: полноты и простоты. Язык CCP должен предоставлять достаточно полный набор конструкций, чтобы запрограммировать любой алгоритм, представимый на некотором чистом функциональном языке. Язык должен быть максимально простым, чтобы облегчить исследование свойств программ.
Программа на языке CCP состоит из набора определений предикатов. Определение предиката A º K сопоставляет вычислимую формулу K определяемому предикату A. Вычислимая формула K представляется в виде параллельного оператора, оператора суперпозиции или условного оператора. Всякий оператор определяет композицию двух предикатов. Вхождение предиката в составе оператора называется вызовом предиката. Вызов предиката имеет следующее представление:
j(d1, d2, …, dn: e1, e2, …, em) , (4.1)
где n ³ 0, m > 0, j - имя предиката или переменной предикатного типа (см. разд. 4.2); d1, d2, …, dn - имена переменных, называемых аргументами вызова; e1, e2, …, em - имена переменных, различающихся между собой и отличных от d1, d2, …, dn. Переменные e1, e2, …, em называются результатами вызова. Вычисление предиката по значениям аргументов определяет значения результатов. Для предиката (4.1) будем также использовать компактное обозначение j(d: e), где d и e обозначают наборы имен d1, d2, …, dn и e1, e2, …, em соответственно.
В случае, когда требуется вычислить логическое значение предиката j (т. е. набор e пуст), будем использовать в качестве результата дополнительный параметр b логического типа и записывать предикат в виде j(d: b). Предикат j(d: e) в случае пустого набора d (т. е. без аргументов при n = 0) соответствует константе. Выражений [12] и констант нет в языке CCP.
Определение нового предиката есть конструкция вида
A(x:y) º K(x:y) . (4.2)
Здесь A обозначает имя определяемого предиката; x и y - наборы переменных, причем все переменные различны; K(x:y) обозначает параллельный оператор, оператор суперпозиции или условный оператор. Переменные набора x называются аргументами предиката, а набора y - результатами предиката. Определение предиката может быть рекурсивным (см. разд. 4.11).
Произвольный предикат языка CCP либо имеет определение вида (4.2), либо является базисным вычислимым предикатом, используемым для константы и элементарной операции. Каждый тип данных однозначно определяется некоторым набором базисных предикатов. Совокупность всех базисных предикатов определяет систему типов данных.