Ссылочная прозрачность - Referential transparency

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

В математике все приложения функций ссылочно прозрачны по определению того, что составляет математическую функцию . Однако это не всегда так в программировании, где термины процедура и метод используются во избежание вводящих в заблуждение коннотаций. В функциональном программировании рассматриваются только ссылочно прозрачные функции. Некоторые языки программирования предоставляют средства, гарантирующие ссылочную прозрачность. Некоторые языки функционального программирования обеспечивают ссылочную прозрачность для всех функций.

Важность ссылочной прозрачности заключается в том, что она позволяет программисту и компилятору рассуждать о поведении программы как о системе перезаписи . Это может помочь в проверке правильности , упрощении алгоритма , помощи в изменении кода без его нарушения или оптимизации кода с помощью мемоизации , исключения общих подвыражений , ленивого вычисления или распараллеливания .

История

Эта концепция, по-видимому, возникла в « Математических принципах» Альфреда Норта Уайтхеда и Бертрана Рассела (1910–13). Она была принята в аналитической философии по Куайну . В § 30 книги « Слово и объект» (1960) Куайн дает следующее определение:

Способ включения φ является ссылочно прозрачным, если всякий раз, когда вхождение сингулярного термина t является чисто ссылочным в термине или предложении ψ (t), оно является чисто ссылочным также и в содержащем термине или предложении φ (ψ (t)).

Этот термин появился в его современном использовании в информатике, при обсуждении переменных в языках программирования , в основополагающем наборе лекций Кристофера Стрейчи « Фундаментальные концепции языков программирования» (1967). В примечаниях к лекциям в библиографии есть ссылки на « Слово и объект» Куайна .

Примеры и контрпримеры

Если все функции, участвующие в выражении, являются чистыми функциями , тогда выражение будет ссылочно прозрачным.

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

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

Арифметические операции ссылочно прозрачны: например, 5 * 5могут быть заменены 25на. Фактически, все функции в математическом смысле прозрачны по ссылкам: sin(x)прозрачны, так как всегда будут давать одинаковый результат для каждой конкретной функции x.

Переназначения непрозрачны. Например, выражение Cx = x + 1 изменяет значение, присвоенное переменной x. Предполагая, что xизначально имеет значение 10, две последовательные оценки выражения дают соответственно 11и 12. Ясно, что замена x = x + 1на любой 11или 12дает программу с другим смыслом, и поэтому выражение не является прозрачным по ссылкам. Однако вызов такой функции, как является прозрачным, поскольку он не будет неявно изменять ввод и, следовательно, не имеет таких побочных эффектов . int plusone(int x) { return x + 1; } x

today()не является прозрачным, так как если вы оцените его и замените его значением (скажем, "Jan 1, 2001"), вы не получите того же результата, что и, если запустите его завтра. Это потому, что это зависит от состояния (даты).

В языках без побочных эффектов, таких как Haskell , мы можем заменить равными равными: т.е. если, x == yто f(x) == f(y). Это свойство также называют неотличимыми идентичностями . Такие свойства не обязательно должны соблюдаться для языков с побочными эффектами. Даже в этом случае важно ограничить такие утверждения так называемым оценочным равенством, то есть равенством терминов, проверенных системой, не включая определяемую пользователем эквивалентность для типов. Например, если B f(A x)тип Aи переопределил понятие равенства, например, сделав все члены равными, тогда можно иметь x == yи все же найти f(x) != f(y). Это связано с тем, что такие системы, как Haskell , не проверяют, что функции, определенные для типов с определяемыми пользователем отношениями эквивалентности, четко определены в отношении этой эквивалентности. Таким образом, ссылочная прозрачность ограничивается типами без отношений эквивалентности. Расширение ссылочной прозрачности на определяемые пользователем отношения эквивалентности может быть выполнено, например, с типом идентичности Мартина-Лофа, но требует системы с зависимым типом, такой как Agda , Coq или Idris .

В отличие от императивного программирования

Если подстановка выражения на его значение действительна только в определенный момент выполнения программы, то выражение не является ссылочно прозрачным. Определение и порядок этих точек последовательности являются теоретической основой императивного программирования и частью семантики императивного языка программирования.

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

Одним из преимуществ написания кода в ссылочно прозрачном стиле является то, что при наличии интеллектуального компилятора статический анализ кода становится проще, и автоматически становятся возможными более эффективные преобразования, улучшающие код . Например, при программировании на C будет снижение производительности за включение вызова дорогостоящей функции внутри цикла, даже если вызов функции может быть перемещен за пределы цикла без изменения результатов программы. Программист был бы вынужден выполнять перемещение кода вызова вручную , возможно, за счет читабельности исходного кода. Однако, если компилятор может определить, что вызов функции является ссылочно прозрачным, он может выполнить это преобразование автоматически.

Основным недостатком языков, обеспечивающих ссылочную прозрачность, является то, что они делают выражение операций, которое естественным образом соответствует императивному стилю программирования с последовательностью шагов, более неудобным и менее кратким. Такие языки часто включают механизмы, облегчающие эти задачи, сохраняя при этом чисто функциональные качества языка, такие как грамматики и монады с определенными предложениями .

Другой пример

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

int g = 0;

int rt(int x) {
  return x + 1;
}

int ro(int x) {
  g++;
  return x + g;
}

Функция rtссылочно прозрачна, что означает, что если x == ythen rt(x) == rt(y). Так , например, rt(6) = 7. Однако мы не можем сказать ничего подобного, roпотому что он использует глобальную переменную, которую он изменяет.

Ссылочная непрозрачность roзатрудняет рассуждение о программах. Например, предположим, что мы хотим обсудить следующее утверждение:

int i = ro(x) + ro(y) * (ro(x) - ro(x));

У кого-то может возникнуть соблазн упростить это утверждение до следующего:

int i = ro(x) + ro(y) * 0;
int i = ro(x) + 0;
int i = ro(x);

Однако это не сработает, roпотому что каждое вхождение ro(x)оценивает свое значение. Помните, что возвращаемое значение roосновано на глобальном значении, которое не передается и которое изменяется при каждом вызове ro. Это означает, что математические тождества, такие как x - x = 0, больше не выполняются.

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

Однако можно использовать более сложный анализ, чтобы упростить утверждение:

int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (x + tmp + 3 - (x + tmp + 4)); g = g + 4;
int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (x + tmp + 3 - x - tmp - 4)); g = g + 4;
int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (-1); g = g + 4;
int tmp = g; int i = x + tmp + 1 - y - tmp - 2; g = g + 4;
int i = x - y - 1; g = g + 4;

Это требует дополнительных шагов и степени понимания кода, невозможного для оптимизации компилятора.

Следовательно, ссылочная прозрачность позволяет нам рассуждать о нашем коде, который приведет к более надежным программам, возможности обнаружения ошибок, которые мы не могли надеяться найти путем тестирования, и возможности увидеть возможности для оптимизации .

Смотрите также

Рекомендации

Внешние ссылки