1.2.2. Функції

Аналіз алгебри даних показує, що в мові SIPL можна вирізнити два види функцій: 1) n-арні функції на базових типах даних, та 2) функції над станами змінних. Другий вид функцій будемо називати номінативними функціями. Назва пояснюється тим, що вони задані на наборах іменованих даних (латинське nomen – ім’я).

Визначимо тепер наступні класи функцій, які будуть задіяні при визначенні семантики мови SIPL:

1. n-арні операції над базовими типами:

• FNA=Intⁿ  Int – n-арні арифметичні функції (операції),

• FNB=Boolⁿ  Bool – n-арні бульові функції (операції),

• FNAB=Intⁿ  Bool – n-арні функції (операції) порівняння.

2. Функції над станами змінних

• FA=State  Int – номінативні арифметичні функції,

• FB=State  Bool – номінативні предикати,

• FS=State  State – біномінативні функції –перетворювачі (трансформатори) станів.

Для операцій мови SIPL зазвичай n=2, а для бульової операції заперечення n=1.

1.2.3. Композиції

Композиції формалізують методи побудови програм. Аналіз мови SIPL дає підстави говорити про те, що будуть вживатися композиції різних типів, а саме:

• композиції, які пов’язані з номінативними функціями та предикатами,

• композиції, пов’язані з біномінативними функціями.

Перший клас композицій використовується для побудови семантики арифметичних виразів та умов, другий – операторів.

Цей клас композицій складається з композицій суперпозиції в n-арні функції, які задані на різних основах (класах функцій):

• суперпозиція номінативних арифметичних функцій в n-арну арифметичну функцію має тип Sⁿ: FNAFAⁿFA,

• суперпозиція номінативних арифметичних функцій в n-арну фунцію порівняння має тип Sⁿ: FNABFAⁿFB,

• суперпозиція номінативних предикатів в n-арну бульову фунцію має тип Sⁿ: FNBFBⁿFB.

Зауваження: суперпозиції різного типу позначаємо одним знаком.

Суперпозиція задається формулою (тут f – n-арна функція, g₁,…,g_n – номінативні функції відповідного типу):

(Sⁿ(f, g₁,…,g_n ))(st)=f(g₁(st),…,g_n(st)).

Другий клас композицій складається з наступних композицій.

• Присвоєння AS^x: FA  FS (x – параметр).

Присвоєння задається формулою:

AS^x (fa)(st)=st [x fa(st)]

• Послідовне виконання  : FS²FS

Послідовне виконання задається формулою:

(fs₁fs₂)(st)=fs₂(fs₁(st))

• Умовний оператор (розгалуження): IF:FBFS²FS. Задається формулою:

• Цикл (ітерація з передумовою): WH:FBFSFS. Задається рекурентно (індуктивно) наступним чином:

WH(fb,fs)(st)=st_n, де

st₀=st, st₁=fs(st₀), st₂=fs(st₁),…, st_n=fs(st_n-1), причому

fb(st₀)=true, fb(st₁)=true,…, fb(st_n-1)=true, fb(st_n)=false.

Важливо відзначити, що для циклу наведена послідовність визначається однозначно. Позначимо число n (кількість ітерацій циклу) як NumItWH((fb, fs), st). Однозначність визначення n дозволяє розглядати NumItWH((fb, fs), st) як тернарне відображення, яке залежить від fb, fs, st. Якщо цикл не завершується, то NumItWH((fb, fs), st) вважається невизначеним. Це відображення буде використовуватись в індуктивних доведеннях властивостей циклу.