Конспект установочных лекций по комплексному курсу Информатика, Теория информации



         

Связывание (свободных) идентификаторов: абстракция функций - часть 2


конечно, полностью равнозначно (3) f(y) = у * (у + 1) для всех у

 N.

Это может быть выражено через явное задание квантора всеобщности:

, (4)

nat х: f(x) = х * (х + 1).

Тем самым описание функции делается независимым от выбора конкретного идентификатора х пли у, правда, ценой введения идентификатора f для описываемой функции.

В ЯП используется более последовательная нотация вида fet f= (nat x) nat: х * (х + 1), которая объединяет в себе и задание области (1), и определяющее функцию равенство (4). Кроме того, благодаря этому делается ясным, что идентификатор х используется исключительно в качестве держателя мес­та для свободно выбираемого фактического аргумента. При таком способе записи можно полностью проигнорировать введение обозначения f для функции благодаря использованию (в ЯП) записи (nat х) nat: х * (х + 1) как нотационного представления соответствующего отображения. При этом х в функциональном выражении называют уже не свободным,

а связанным, так как х синтаксически (через nat х) выделяется' как держатель места (формальный параметр). Поэтому х в подстановке теперь уже нс может заменяться на заданное выражение Е. В частности, связанные идентификаторы могут систематически заменяться на любые другие идентификаторы без изменения интерпретации (значения) функционального выражения, пока не возникает конфликта .со свободным вхождением встречающихся обозначений в рассматриваемое выражение. Это переименование связанных обозначений называется

-конверсией.

Пусть Е - выражение типа s. Запись

(s1x1,…, snxn) s: Е

называется абстракцией функции, причем x1,…, xn называются формальными параметрами.

Последовательность символов (s1x1,…, snxn)s называется заголовком абстракции функции; она, в частности, задает тип абстракции функции. Тем самым специфицируется, что указанная выше абстракция функции представляет собой функцию вида

М1 * ... *

Мn
М,

причем Мi обозначают носители типа si,. Выражение Е называется телом (англ. body) абстракции функции.

Для каждой заданной конкретизации

 вышеприведенная абстракция функции определяет функцию




Содержание  Назад  Вперед