Методи формальної семантики

В реальних МП, в кращому випадку лише синтаксис задається строго формально, а семантика задається лише інтуїтивно, Тому з кожною мовою реального програмування спражена важлива проблема – формалізація її семантики. Задання семантики в кожному випадку спряжене з подоланням серйозних труднощів. Як бачили, навіть для такої “ювелірної” мови як λ-нотація було спряжене з подоланням принципової проблематики. Дійсно, так операція Ap,задана на впорядкованій парі (a,f), де a та f мають різний тип, семантика зпряжена з розв’язком проблеми самопримінення – примінення функції f до самої себе. В реальних МП ця проблема суттєво ускладнюється. Навіть в λ-численні ця проблема стояла відкритою більше 50-ти років. Теорія Скотта створила фундамент для розв’язку проблеми формалізації λ-нотації. В основі цієї формалізації лежить інтегрована структура програмування. Дійсно, задати формально семантику λ-нотації = задати семантику терму Ap(a,f) та терму lx.t(x). Що стосується терму Ap(a,f), то він інтерпритується в семантичних структурах. Конкретніше, він інтерпритується як функція (а це поняття семантичне), що задана на парі (a,f), один з компонентів якої є знову функція (семантичне поняття) та об’єкт a (яке знову ж є теоретико-множинним елементом, а не символом – а це семантика). Звідси випливає, що інтерпритація a задається в термінах лише семантичних понять.

Розглянемо тепер другий терм - lx.t(x).. Перш за все, відзначимо, що використовуючи співвідношення Шенфінкеля, що зіставляє кожній функції f(x,y) нову функцію j(y)=f_x(y), що параметризована x-ом, ми зводимо інтерпритацію подібних термів до інтерпритації унарних функцій. Але ж, як бачимо, на відміну від семантики Ap(a,f), ми приречені поряд з суто семантичними поняттями використовувати синтаксичні поняття (типові вирази t(x) з вільно змінною x). В зв’язку з цим семантика вказаних виразів (тобто функція, що йому відповідає) задається шляхом стандартної інтерпритації терму t(x) на елементах з області значень змінної x, яка пробігає її. Таким чином, на відміну від аплікації, λ-абстракція інтерпретується шляхом від синтаксису до семантики. Таким чином, формалізація семантики λ-нотації є дійсно змішаною.