В аналитической философии и информатике ссылочная прозрачность и ссылочная непрозрачность являются свойствами лингвистических конструкций [1] и расширением языков . Лингвистическая конструкция называется ссылочно прозрачной, если для любого построенного на ее основе выражения замена подвыражения другим, обозначающим то же значение [2] , не приводит к изменению значения выражения. [3] [4] В противном случае его называют ссылочно непрозрачным . Каждое выражение, построенное на основе ссылочно непрозрачной лингвистической конструкции, что-то сообщает о подвыражении, тогда как каждое выражение, построенное на основе ссылочно прозрачной лингвистической конструкции, сообщает что-то не о подвыражении, а это означает, что подвыражения «прозрачны» для выражения, действуя просто как «ссылки». к чему-то другому. [5] Например, лингвистическая конструкция «_ был мудрым» референциально прозрачна (например, « Сократ был мудр» эквивалентно «Основатель западной философии был мудр» ), но «_ сказал _» референциально непрозрачна (например, Ксенофонт сказал «Сократ был мудрым» не эквивалентно словам Ксенофонта: «Основатель западной философии был мудрым» ).
Ссылочная прозрачность зависит от значений, связанных с выражениями, то есть от семантики языка. Таким образом, как декларативные языки , так и императивные языки могут быть ссылочно прозрачными или ссылочно непрозрачными в зависимости от заданной им семантики.
Важность ссылочной прозрачности заключается в том, что она позволяет программисту и компилятору рассуждать о поведении программы как о переписывающей системе . Это может помочь доказать правильность , упростить алгоритм , помочь изменить код, не нарушая его, или оптимизировать код посредством мемоизации , исключения общих подвыражений , ленивого вычисления или распараллеливания .
Эта концепция возникла в книге Альфреда Норта Уайтхеда и Бертрана Рассела « Principia Mathematica» (1910–1913): [5]
Пропозиция как средство истины или ложности представляет собой частное событие, в то время как пропозиция, рассматриваемая фактически, представляет собой класс подобных явлений. Именно пропозиция, рассматриваемая фактически, встречается в таких высказываниях, как « А верит в р » и « р относится к А ».
Конечно, можно делать утверждения относительно конкретного факта: «Сократ — грек». Мы можем сказать, сколько сантиметров она имеет длину; мы можем сказать, что оно черное; и так далее. Но это не те утверждения, которые склонен делать философ или логик.
Когда утверждение возникает, оно делается посредством конкретного факта, который является примером утверждаемого предложения. Но этот конкретный факт, так сказать, «прозрачен»; о нем ничего не говорится, но посредством него говорится о чем-то другом. Именно это «прозрачное» качество принадлежит предложениям, когда они встречаются в функциях истинности. Это относится к p , когда p утверждается, но не тогда, когда мы говорим, что « p истинно».
Он был принят в аналитической философии в книге Уилларда Ван Ормана Куайна «Слово и объект» (1960): [3]
Когда термин в единственном числе используется в предложении исключительно для указания его объекта и это предложение истинно в отношении объекта, тогда предложение, несомненно, останется истинным, когда будет заменен любой другой термин в единственном числе, обозначающий тот же объект. Здесь мы имеем критерий того, что можно назвать чисто референтной позицией : позиция должна быть подчинена субститутивности идентичности .
[…]
Ссылочная прозрачность имеет дело с конструкциями (§ 11); способы содержания, точнее, единичных терминов или предложений в единичных терминах или предложениях. Я называю способ вложения φ референциально прозрачным, если всякий раз, когда появление единственного термина t является чисто референциальным в термине или предложении ψ ( t ) , оно чисто референциально и в содержащем термине или предложении φ ( ψ ( t )) .
Этот термин появился в его современном использовании в информатике при обсуждении переменных в языках программирования в оригинальном наборе конспектов лекций Кристофера Стрейчи «Фундаментальные концепции языков программирования» (1967): [4]
Одним из наиболее полезных свойств выражений является то, что Куайн [4] назвал ссылочной прозрачностью . По сути это означает, что если мы хотим найти значение выражения, которое содержит подвыражение, единственное, что нам нужно знать о подвыражении, — это его значение. Любые другие особенности подвыражения, такие как его внутренняя структура, количество и природа его компонентов, порядок их вычисления или цвет чернил, которыми они написаны, не имеют отношения к значению основного выражения. выражение.
Есть три фундаментальных свойства, касающихся заменяемости в формальных языках: ссылочная прозрачность, определенность и развертываемость. [6]
Обозначим синтаксическую эквивалентность через ≡ и семантическую эквивалентность через =.
Позиция определяется последовательностью натуральных чисел . Пустая последовательность обозначается ε, а конструктор последовательности — «.».
Пример. — Позиция 2.1 в выражении (+ (* e 1 e 1 ) (* e 2 e 2 )) — это место, занимаемое первым появлением e 2 .
Выражение e с выражением e' , вставленным в позицию p , обозначается e [ e' / p ] и определяется как
Пример. — Если e ≡ (+ (* e 1 e 1 ) (* e 2 e 2 )) то e [ e 3 /2.1] ≡ (+ (* e 1 e 1 ) (* e 3 e 2 )) .
Позиция p является чисто ссылочной в выражении e и определяется формулой
Другими словами, позиция является чисто референтной в выражении тогда и только тогда, когда она подлежит замене равными. ε является чисто ссылочным во всех выражениях.
Оператор Ω ссылочно прозрачен в том месте, где i определяется формулой
В противном случае Ω является ссылочно непрозрачным в месте i .
Оператор ссылочно прозрачен , если он ссылочно прозрачен во всех местах. В противном случае он ссылочно непрозрачен .
Формальный язык ссылочно прозрачен , поскольку все его операторы ссылочно прозрачны. В противном случае он ссылочно непрозрачен .
Пример. — Оператор «_ живет в _» ссылочно прозрачен:
Действительно, вторая позиция в утверждении является чисто референциальной, поскольку замена Лондона столицей Соединенного Королевства не меняет ценности утверждения. Первая позиция также является чисто референтной по той же причине подстановки.
Пример. — Операторы «_ содержит _» и кавычки ссылочно непрозрачны:
Действительно, первая позиция в заявлении не является чисто референтной, поскольку замена Лондона на столицу Соединенного Королевства меняет ценность заявления и цитаты. Таким образом, в первой позиции операторы «_ содержит _» и кавычки разрушают связь между выражением и значением, которое оно обозначает.
Пример. — Оператор «_ относится к _» ссылочно прозрачен, несмотря на ссылочную непрозрачность оператора кавычки:
Действительно, первая позиция в утверждении является чисто референциальной, хотя ее нет в цитате, поскольку замена Лондона на столицу Соединенного Королевства не меняет значения утверждения. Таким образом, в первой позиции оператор «_ относится к _» восстанавливает связь между выражением и значением, которое оно обозначает. Вторая позиция также является чисто референтной по той же причине подстановки.
Формальный язык определен , когда все вхождения переменной в его области действия обозначают одно и то же значение.
Пример. — Математика определенна:
Действительно, два вхождения x обозначают одно и то же значение.
Формальный язык разворачивается , поскольку все выражения β-сводимы .
Пример. — Лямбда-исчисление разворачивается:
Действительно, ((λ x . x + 1) 3) = ( x + 1)[3/ x ] .
Ссылочная прозрачность, определенность и раскрываемость независимы. Определенность подразумевает развертываемость только для детерминированных языков. Недетерминированные языки не могут одновременно обладать определенностью и развертываемостью.