13. Функц яп. Декларативность прогтамм. Лямбда-исчислениею

Декларативный язык программирования (От лат. Declaratio – объявление) - язык программирования высокого уровня, построенный: - на описании данных; - на описании искомого результата. Декларативные языки подразделяются на функциональные и логические языки.

Функциональный язык программирования - язык программирования, позволяющий задавать программу в виде совокупности определений функций. В функциональных языках программирования:

- функции обмениваются между собой данными без использования промежуточных переменных и присваиваний;

- переменные, однажды получив значение, никогда его не изменят;

- циклы заменяются аппаратом рекурсивных функций.

Чистое λ-исчисление

Это простейший из семейства прототипных языков программирования, чистое λ-исчисление, термы которого, называемые также объектами (обами), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличия каких-либо констант не предполагается.

Обогатим модальное исчисление предикатов новым оператором над логическими переменными — лямбда-оператором (или, короче, λ-оператором).

Читатель, несомненно, знаком с таким способом задания множеств, как в нижеследующих примерах:

{ х | х является преподавателем университета},{ х | — 1 < x < 1, х—действительное число},

При таком определении конкретного множества нет двусмысленности; нужно только явно указать ту переменную, на которой основано определение множества. Можно поискать замену неформального определения формально логическим. Это приводит к обозначениям λ-исчисления, в котором множество описывается следующим образом:

λх (логическая формула, содержащая переменную х).

Например, рассмотрим русскую фразу "Кто-то посылает что-то Мари" и ее перевод на язык логики предикатов Посылка(х, Мари_4, у).

Выражение (называемое λ-выражением или λ-абстракцией) λy[Посылка (Жак, Мари, у)] определяет характеристическую функцию множества объектов, посылаемых Жаком.

Мари, тогда как выражение λх[Посылка (х, Мари, Книга)] определяет характеристическую функцию множества индивидов, посылающих указанную книгу Мари.

Точно так же выражение λх,у[Посылка (х, Мари_4, у)] определяет характеристическую функцию множества пap (отправитель, посылаемый объект), для которых Мари является, получателем.

Если F—формула, то λxF указывает описанное с помощью F множество, на элементах которого (являющихся конкретизациями для х) F истинна. Выражения (2) и (3) можно интерпретировать и как унарные предикаты с аргументами у и х соответственно. Оператор λ, как и кванторы общности и существования, служит для связывания вхождений переменной.

n-арное λ-выражение λx1, ... , xnF состоит из логической формулы F, называемой телом, выражения, и множества n переменных x1, ..., xn формулы F, являющихся формальными параметрами выражения.

Следующий за λ список, параметров служит для того чтобы отличить формальные параметры от других аргументов (или концептов) формулы F.

Телом λ-выражения является формула логики предикатов. Как только будут заданы значения n формальных параметров, λ-выражение станет n-арным предикатом, принимающим значения "истинно" или "ложно" в зависимости от того, какие индивидуальные значения (конкретизации) присвоены формальным параметрам.