Ссылочная прозрачность
В философии и информатике аналитической референциальная прозрачность и референциальная непрозрачность являются свойствами лингвистических конструкций. [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 ] и определяется как
- е [ е′ /ε] ≡ е′
- и [ е ' / я . p ] ≡ <Ω e 1 … e i [ e′ / p ] … e n > if e ≡ <Ω e 1 … e i … e n > else не определено, для всех операторов Ω и выражений e 1 , …, e n .
Пример. — Если е ≡ (+ (∗ е 1 е 1 ) (∗ е 2 е 2 )) то е [ е 3 /2.1] ≡ (+ (∗ е 1 е 1 ) (∗ е 3 е 2 )) .
Позиция p является чисто ссылочной в выражении e и определяется выражением
- e 1 = e 2 подразумевает e [ e 1 / p ] = e [ e 2 / p ] для всех выражений e 1 , e 2 .
Другими словами, позиция является чисто референциальной в выражении тогда и только тогда, когда она подлежит замене равными. ε является чисто ссылочным во всех выражениях.
Оператор Ω в ссылочно прозрачен том месте, где i определяется формулой
- p является чисто ссылочным в ei , подразумевает i . p является чисто референциальным в e ≡ <Ω e 1 … e i … e n > для всех позиций p и выражений e 1 , …, e n .
В противном случае Ω является ссылочно непрозрачным в месте i .
Оператор ссылочно прозрачен , если он ссылочно прозрачен во всех местах. В противном случае он ссылочно непрозрачен .
Формальный язык ссылочно прозрачен , поскольку все его операторы ссылочно прозрачны. В противном случае он ссылочно непрозрачен .
Пример. — Оператор «_ живет в _» ссылочно прозрачен:
- Она живет в Лондоне.
Действительно, вторая позиция в утверждении является чисто референтной, поскольку замена Соединенного Королевства столицей Лондона не меняет ценности утверждения. Первая позиция также является чисто референтной по той же причине подстановки.
Пример. — Операторы «_ содержит _» и кавычки ссылочно непрозрачны:
- Слово «Лондон» состоит из шести букв.
Действительно, первая позиция в заявлении не является чисто референтной, поскольку замена столицу Соединенного Королевства на Лондона меняет ценность заявления и цитаты. Таким образом, в первой позиции операторы «_ содержит _» и кавычки разрушают связь между выражением и значением, которое оно обозначает.
Пример. — Оператор «_ относится к _» ссылочно прозрачен, несмотря на ссылочную непрозрачность оператора кавычки:
- «Лондон» относится к крупнейшему городу Соединенного Королевства.
Действительно, первая позиция в утверждении является чисто референциальной, хотя ее нет в цитате, поскольку замена столицу Соединенного Королевства на Лондона не меняет значения утверждения. Таким образом, в первой позиции оператор «_ относится к _» восстанавливает связь между выражением и значением, которое оно обозначает. Вторая позиция также является чисто референтной по той же причине подстановки.
Определенность [ править ]
Формальный язык определен , когда все вхождения переменной в его области действия обозначают одно и то же значение.
Пример. — Математика определенна:
- 33x 2 + 2 х + 17 .
Действительно, два вхождения x обозначают одно и то же значение.
Раскладываемость [ править ]
Формальный язык разворачивается , поскольку все выражения β-сводимы .
Пример. — Лямбда-исчисление разворачивается:
- ((λ x . x + 1) 3) .
Действительно, ((λ x . x + 1) 3) = ( x + 1)[3/ x ] .
Отношения между свойствами [ править ]
Ссылочная прозрачность, определенность и раскрываемость независимы.Определенность подразумевает развертываемость только для детерминированных языков.Недетерминированные языки не могут одновременно обладать определенностью и развертываемостью.
См. также [ править ]
Ссылки [ править ]
- ^ Лингвистическая конструкция (также называемая режимом вложения, контекстом или оператором) — это выражение с дырами.
- ^ Здесь значение — это обозначение (также называемое значением, объектом или референтом) выражения, а не результат процесса оценки.
- ↑ Перейти обратно: Перейти обратно: а б Куайн, Уиллард Ван Орман (1960). Слово и объект (1-е изд.). Кембридж, Массачусетс: MIT Press. п. 144. ИСБН 978-0-262-17001-7 .
- ↑ Перейти обратно: Перейти обратно: а б Стрейчи, Кристофер (1967). Фундаментальные концепции языков программирования (Технический отчет). Конспекты лекций для Международной летней школы компьютерного программирования в Копенгагене. Также: Стрейчи, Кристофер (2000). «Основные понятия языков программирования» . Вычисления высшего порядка и символьные вычисления . 13 (1–2): 11–49. дои : 10.1023/А:1010000313106 . S2CID 14124601 .
- ↑ Перейти обратно: Перейти обратно: а б Уайтхед, Альфред Норт ; Рассел, Бертран (1927). Принципы математики . Том. 1 (2-е изд.). Кембридж: Издательство Кембриджского университета. п. 665. ИСБН 978-0-521-06791-1 .
- ^ Сёндергаард, Харальд; Сестофт, Питер (1990). «Ссылочная прозрачность, определенность и раскрываемость» (PDF) . Акта Информатика . 27 (6): 505–517. дои : 10.1007/bf00277387 .