76 lines
4.1 KiB
HTML
76 lines
4.1 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
|
||
<HTML>
|
||
<HEAD>
|
||
<meta name="GENERATOR" content="Microsoft® HTML Help Workshop 4.1">
|
||
<meta http-equiv="Content-Type" content="text/html; charset=ANSI"/>
|
||
<link rel="stylesheet" type="text/css" href="css/style.css"/>
|
||
|
||
<Title>Типы конституент</Title>
|
||
</HEAD>
|
||
<BODY>
|
||
<h1>Типы конституент</h1>
|
||
<table>
|
||
<thead>
|
||
<tr>
|
||
<td style="width:50px;">ID</td>
|
||
<td style="width:150px">Название</td>
|
||
<td style="width:auto">Описание</td>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr>
|
||
<td>X#</td>
|
||
<td>Базисное множество</td>
|
||
<td>Базовое (невыводимое) понятие, интерпретация которого задается разработчиком </td>
|
||
</tr>
|
||
<tr>
|
||
<td>C#</td>
|
||
<td>Константное множество</td>
|
||
<td>Вспомогательное понятие, имеющие общеизвестную интерпретацию в рассматриваемой предметной области</td>
|
||
</tr>
|
||
<tr>
|
||
<td>S#</td>
|
||
<td>Родовая структура</td>
|
||
<td>Базисное (невыводимое) структурированное понятие, интерпретация которого задается разработчиком и ограничивается аксиомами</td>
|
||
</tr>
|
||
<tr>
|
||
<td>H#</td>
|
||
<td>Ступень</td>
|
||
<td>Сокращение множества-ступени. Не является понятием. Использовалось для анализа типизаций термов до появления анализаторов, вычисляющих типизацию автоматически.</td>
|
||
</tr>
|
||
<tr>
|
||
<td>A#</td>
|
||
<td>Аксиома</td>
|
||
<td>Логическое выражение, задающее некоторое усмотренное в предметной области ограничение на базовые и выводимые понятия. В корректной КМ аксиомы истинны для всех значений локальных переменных.</td>
|
||
</tr>
|
||
<tr>
|
||
<td>D#</td>
|
||
<td>Терм</td>
|
||
<td>Выводимое понятие, задаваемое теоретико-множественным выражением</td>
|
||
</tr>
|
||
<tr>
|
||
<td>F#</td>
|
||
<td>Терм-функция</td>
|
||
<td>Статически типизированное параметризованное теоретико-множественное выражением. Используется для сокращения выражений выводимых понятий, имеющих схожий способ вывода и используемые понятия.</td>
|
||
</tr>
|
||
<tr>
|
||
<td>T#</td>
|
||
<td>Теорема</td>
|
||
<td>Логическое выражение, выводимое в проектируемой системе понятий</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p>Под <b>объявлением терм-функции</b> понимается выражение вида</p>
|
||
<p>F# = [α<sub>1</sub>∈ТМВ<sub>1</sub>, α<sub>2</sub>∈ТМВ<sub>2</sub>, ... ,α<sub>k</sub>∈ТМВ<sub>k</sub>] ТМВ(α<sub>1</sub>, ... , α<sub>k</sub>), где</p>
|
||
<p>F# - имя терм функции</p>
|
||
<p>α<sub>1</sub>, ... , α<sub>k</sub> - параметры терм-функции. Имена переменных-параметров терм-функции не должны совпадать с внутренними переменными выражения ТМВ(α<sub>1</sub>, ... , α<sub>k</sub>) и именами конституент РС-формы.</p>
|
||
<p>ТМВ<sub>1</sub>, ... , ТМВ<sub>k</sub> - области определения параметров терм-функции, заданные ступенями, принадлежащими шкале ступеней над базисными и константными множествами РС-формы.</p>
|
||
<p> </p>
|
||
<p>ТМВ(α<sub>1</sub>, ... , α<sub>k</sub>) - "тело" терм-функции - теоретико-множественное типизированное выражение, зависящее от параметров терм-функции и конституент типов базисное множество, константное множество, родовая структура, ступень, терм.</p>
|
||
<p>Под <b>использованием терм-функции</b> понимается выражение вида</p>
|
||
<p>F#[A<sub>1</sub>, A<sub>2</sub>, ... , A<sub>k</sub>], где</p>
|
||
<p>F# - имя объявленной ранее терм-функции</p>
|
||
<p>A<sub>1</sub>, A<sub>2</sub>, ... , A<sub>k</sub> - имена конституент или локальных переменных, для которых биективно переносимо (корректно типизировано) выражение А<sub>1</sub>>∈ТМВ<sub>1</sub> & А<sub>2</sub>∈ТМВ<sub>2</sub> & ... & А<sub>k</sub>∈ТМВ<sub>k</sub>.</p>
|
||
</BODY>
|
||
</HTML>
|