Типы конституент

ID Название Описание
X# Базисное множество Базовое (невыводимое) понятие, интерпретация которого задается разработчиком
C# Константное множество Вспомогательное понятие, имеющие общеизвестную интерпретацию в рассматриваемой предметной области
S# Родовая структура Базисное (невыводимое) структурированное понятие, интерпретация которого задается разработчиком и ограничивается аксиомами
H# Ступень Сокращение множества-ступени. Не является понятием. Использовалось для анализа типизаций термов до появления анализаторов, вычисляющих типизацию автоматически.
A# Аксиома Логическое выражение, задающее некоторое усмотренное в предметной области ограничение на базовые и выводимые понятия. В корректной КМ аксиомы истинны для всех значений локальных переменных.
D# Терм Выводимое понятие, задаваемое теоретико-множественным выражением
F# Терм-функция Статически типизированное параметризованное теоретико-множественное выражением. Используется для сокращения выражений выводимых понятий, имеющих схожий способ вывода и используемые понятия.
T# Теорема Логическое выражение, выводимое в проектируемой системе понятий

Под объявлением терм-функции понимается выражение вида

F# = [α1∈ТМВ1, α2∈ТМВ2, ... ,αk∈ТМВk] ТМВ(α1, ... , αk), где

F# - имя терм функции

α1, ... , αk - параметры терм-функции. Имена переменных-параметров терм-функции не должны совпадать с внутренними переменными выражения ТМВ(α1, ... , αk) и именами конституент РС-формы.

ТМВ1, ... , ТМВk - области определения параметров терм-функции, заданные ступенями, принадлежащими шкале ступеней над базисными и константными множествами РС-формы.

 

ТМВ(α1, ... , αk) - "тело" терм-функции - теоретико-множественное типизированное выражение, зависящее от параметров терм-функции и конституент типов базисное множество, константное множество, родовая структура, ступень, терм.

Под использованием терм-функции понимается выражение вида

F#[A1, A2, ... , Ak], где

F# - имя объявленной ранее терм-функции

A1, A2, ... , Ak - имена конституент или локальных переменных, для которых биективно переносимо (корректно типизировано) выражение А1>∈ТМВ1 & А2∈ТМВ2 & ... & Аk∈ТМВk.