Что такое ссылочная прозрачность?

Термин «ссылочная прозрачность» происходит от аналитической философии, отрасли философии, которая анализирует конструкции естественного языка, утверждения и аргументы, основанные на методах логики и математики. Другими словами, это самый близкий предмет вне информатики к тому, что мы называем семантикой языка программирования. Философ Уиллард Куайн был ответственным за создание концепции ссылочной прозрачности, но она также подразумевалась в подходы Бертрана Рассела и Альфреда Уайтхеда.

По своей сути «ссылочная прозрачность» - очень простая и ясная идея. Термин «референт» используется в аналитической философии для обозначения того, к чему относится выражение. Это примерно то же самое, что мы подразумеваем под «значением» или «обозначением» в семантике языка программирования. Используя пример Эндрю Биркетта (сообщение в блоге), термин «столица Шотландии» относится к городу Эдинбург. Это простой пример «референта».

Контекст в предложении является «ссылочно прозрачным», если замена термина в этом контексте другим термином, относящимся к той же сущности, не меняет значения. Например

Парламент Шотландии собирается в столице Шотландии.

означает то же, что и

Парламент Шотландии встречается в Эдинбурге.

Таким образом, контекст «Парламент Шотландии встречается в ...» является ссылочно прозрачным контекстом. Мы можем заменить «столица Шотландии» на «Эдинбург», не меняя смысла. Другими словами, контекст заботится только о том, к чему относится термин, и ни о чем другом. В этом смысле контекст «референциально прозрачен».

С другой стороны, в предложении

Эдинбург является столицей Шотландии с 1999 года.

мы не можем сделать такую ​​замену. Если бы мы это сделали, мы бы получили «Эдинбург был Эдинбургом с 1999 года», что было бы чокнутым высказыванием, и оно не передает того же значения, что и исходное предложение. Таким образом, может показаться, что контекст «Эдинбург был ... с 1999 года» референциально непрозрачен (противоположен референциально прозрачному). Очевидно, его волнует нечто большее, чем то, к чему относится этот термин. Что это?

Такие вещи, как «столица Шотландии», называются определенными терминами, и долгое время они не вызывали головной боли у логиков и философов. Рассел и Куайн разобрали их, заявив, что они на самом деле не являются «ссылочными», т.е. ошибочно думать, что приведенные выше примеры используются для ссылки на сущности. Правильный способ понять, что «Эдинбург был столицей Шотландии с 1999 года» - это сказать:

Столица Шотландии существует с 1999 года, и эта столица - Эдинбург.

Это предложение нельзя превратить в сумасшедшее. Задача решена! Идея Куайна заключалась в том, чтобы сказать, что естественный язык запутан или, по крайней мере, сложен, потому что он сделан для удобства практического использования, но философы и логики должны внести ясность, понимая их правильным образом. Ссылочная прозрачность - это инструмент, который можно использовать для такой ясности смысла.

Какое все это имеет отношение к программированию? Вообще-то не очень. Как мы уже говорили, ссылочная прозрачность - это инструмент, который нужно использовать для понимания языка, то есть для присвоения значения. Кристофер Стрейчи, основавший область семантики языков программирования, использовал ее в своем исследовании смысла. Его основополагающая статья "Основные понятия языков программирования "доступно в Интернете. Это красивая газета, и каждый может ее прочитать и понять. Так что, пожалуйста, сделай это. Вы будете очень просветленными. Он вводит термин «ссылочная прозрачность» в этом абзаце:

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

Использование слова «по существу» предполагает, что Стрейчи перефразирует его, чтобы объяснить простым языком. Функциональные программисты, кажется, понимают этот абзац по-своему. Есть еще 9 случаев «ссылочной прозрачности» в статье, но они, похоже, не заботятся ни о каких других. Фактически, вся статья Стрейчи посвящена объяснению значения императивных языков программирования. Но сегодня функциональные программисты заявляют, что императивные языки программирования не ссылочно прозрачны. Стрейчи будет превращаться в могилу.

Мы можем спасти ситуацию. Мы сказали, что естественный язык «запутан или, по крайней мере, сложен», потому что он сделан для удобства практического использования. Языки программирования такие же. Они «беспорядочные или, по крайней мере, сложные», потому что сделаны удобными для практического использования. Это не значит, что им нужно нас сбивать с толку. Их просто нужно правильно понимать, используя метаязык, который является референциально прозрачным, чтобы у нас была ясность смысла. В статье, которую я процитировал, Стрейчи делает именно это. Он объясняет значение императивных языков программирования, разбивая их на элементарные концепции, нигде не теряя ясности. Важной частью его анализа является указание на то, что выражения в языках программирования имеют два типа «значений», называемых l-значения и r-значения. До статьи Стрейчи этого не понимали, и царила неразбериха. Сегодня в определении C он упоминается регулярно, и каждый программист на C понимает разницу. (Трудно сказать, понимают ли это одинаково хорошо программисты на других языках.)

И Куайн, и Стрейчи интересовались значением языковых конструкций, которые включают некоторую форму зависимости от контекста. Например, наш пример «Эдинбург был столицей Шотландии с 1999 года» означает тот факт, что «столица Шотландии» зависит от времени, в которое он считается. Такая контекстная зависимость реальна как для естественных языков, так и для языков программирования. Даже в функциональном программировании свободные и связанные переменные должны интерпретироваться с учетом контекста, в котором они появляются. Любая зависимость от контекста тем или иным образом блокирует ссылочную прозрачность. Если вы попытаетесь понять значение терминов безотносительно к контексту, от которого они зависят, вы снова попадете в путаницу. Куайн интересовался значением модальной логики. Он считал, что модальная логика референциально непрозрачна, и ее следует очистить, переведя ее в ссылочно прозрачная структура (например, рассматривая необходимость как доказуемость). Он в значительной степени проиграл эту дискуссию. Логики и философы в одинаковой мере сочли возможную мировую семантику Крипке совершенно адекватной. Аналогичная ситуация царит и с императивным программированием. Зависимость от состояния, объясненная Стрейчи, и зависимость от хранилища, объясненная Рейнольдсом (аналогично возможной мировой семантике Крипке), совершенно адекватны. Функциональным программистам мало что известно об этих исследованиях. Их идеи относительно ссылочной прозрачности следует воспринимать с большой долей скептицизма.

[Дополнительное примечание: приведенные выше примеры показывают, что простая фраза, такая как «столица Шотландии», имеет несколько уровней значения. С одной стороны, мы можем говорить о столице в настоящее время. На другом уровне мы могли бы говорить обо всех возможных капиталах, которые Шотландия могла иметь с течением времени. В обычной практике мы можем довольно легко «увеличить» конкретный контекст и «уменьшить», чтобы охватить все контексты. Эффективность естественного языка использует нашу способность делать это. Во многом такие же эффективны и императивные языки программирования. Мы можем использовать переменную x в правой части присваивания (r-value), чтобы говорить о ее значении в определенном состоянии. Или мы можем говорить о его l-значении, которое охватывает все состояния. Такие вещи редко сбивают с толку. Однако они могут или не могут быть в состоянии точно объяснить все слои значения, присущие языковым конструкциям. Все такие смысловые слои не обязательно «очевидны», и изучение их должным образом является делом науки. Однако невнятность обычных людей в объяснении таких многослойных значений не означает, что они их не понимают.]

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

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

Вот пример ссылочной прозрачной функции:

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

С помощью ссылочной прозрачной функции с учетом ввода и функции вы можете заменить ее значением вместо вызова функции. Поэтому вместо вызова plusOne с параметром 5 мы могли бы просто заменить его на 6.

Другой хороший пример - математика в целом. В математике при наличии функции и входного значения оно всегда будет отображаться в одно и то же выходное значение. f (x) = x + 1. Следовательно, математические функции референциально прозрачны.

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

Ссылочная прозрачность всегда используется в функциональных языках, таких как Haskell.

--

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

//global G
int G = 10;

int plusG(int x)
{//G can be modified externally returning different values.
  return x + G;
}

Другой пример - функция-член объектно-ориентированного языка программирования. Функции-члены обычно работают со своими переменными-членами и поэтому непрозрачны по ссылкам. Хотя функции-члены, конечно, могут быть ссылочно прозрачными.

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

Ссылочно прозрачная функция - это функция, которая зависит только от ее ввода.

[Это постскриптум к моему ответу от 25 марта с целью приблизить обсуждение к проблемам функционального / императивного программирования.]

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

• В то время как философы / логики используют такие термины, как «ссылка», «обозначение», «десигнат» и «bedeutung» (немецкий термин Фреге), функциональные программисты используют термин «значение». (Это не полностью их дело. Я заметил, что Лэндин, Стрейчи и их потомки также использовали термин «ценность», чтобы говорить о ссылке / обозначении. большая разница при наивном использовании.)

• Функциональные программисты, кажется, верят, что эти «ценности» существуют внутри языка программирования, а не за его пределами. В этом они отличаются как от философов, так и от семантиков языков программирования.

• Похоже, они верят, что эти «ценности» должны быть получены путем оценки.

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

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

Это полностью расходится с тем, что говорят философы / логики. Они говорят, что контекст является ссылочным или ссылочно прозрачным, если выражение в этом контексте может быть заменено другим выражением, которое ссылается на то же самое (коррелирующее выражение). Кто эти философы / логики? В их число входят Фреге, Рассел, Уайтхед, Карнап, Куайн, Церковь и многие другие. Каждый из них - высокая фигура. Объединенная интеллектуальная сила этих логиков, мягко говоря, ошеломляет. Все они единодушны в том, что референты / обозначения существуют вне формального языка, а выражения внутри языка могут говорить только о них. Итак, все, что можно сделать в языке, - это заменить одно выражение другим выражением, относящимся к той же сущности. Сами референты / обозначения не существуют в языке. Почему функциональные программисты отклоняются от этой устоявшейся традиции?

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

Landin:

(a) каждое выражение имеет вложенную структуру подвыражения, (b) каждое подвыражение обозначает что-то (обычно число, значение истинности или числовую функцию), (c) то, что обозначает выражение, т. е. его " value ", зависит только от значений его подвыражений, а не от других их свойств. [Добавлен акцент]

Стой:

Единственное, что имеет значение в выражении, - это его значение, и любое подвыражение может быть заменено любым другим равным по значению [выделено мной]. Более того, значение выражения в определенных пределах остается неизменным, когда бы оно ни происходило ".

Bird and Wadler:

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

Итак, в ретроспективе попытки Ландина и Стрейчи упростить терминологию путем замены «ссылки» / «обозначения» на «значение» могли быть неразумными. Как только кто-то слышит о «ценности», возникает соблазн подумать о процессе оценки, который к ней ведет. Столь же заманчиво думать о том, что производит оценка, как о «ценности», хотя может быть совершенно ясно, что это не обозначение. Это то, что, как я понимаю, произошло с концепцией «ссылочной прозрачности» в глазах функциональных программистов. Но «ценность», о которой говорили ранние семантики, не является результатом оценки или вывода функции или чего-то подобного. Это обозначение термина.

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

• Стрейчи интерпретировал переменные в императивных языках программирования как L-значения, как упоминалось в моем ответе от 25 марта, который представляет собой сложный концептуальный объект, не имеющий прямого представления в синтаксисе языка программирования.
• Он также интерпретировал команды на таких языках, как функции преобразования состояния в состояние, еще один экземпляр сложного математического объекта, который не является «значением» в синтаксисе.
• Даже побочный вызов функции в C имеет четко определенное «значение» как преобразователь состояний, который отображает состояния в пары состояний и значений (так называемая «монада» в терминологии функциональных программистов).

Нежелание функциональных программистов называть такие языки «ссылочно прозрачными» просто означает, что они неохотно признают такие сложные математические / концептуальные объекты как «значения». С другой стороны, они, кажется, вполне готовы называть преобразователь состояния «значением», если он помещен в их собственный любимый синтаксис и приправлен таким модным словом, как «монада». Я должен сказать, что они совершенно непоследовательны, даже если мы допустим, что их идея «ссылочной прозрачности» имеет некоторую последовательность.

Немного истории может пролить свет на то, как возникла эта путаница. Период с 1962 по 1967 год был для Кристофера Стрейчи очень напряженным. В период с 1962 по 1965 год он подрабатывал научным сотрудником у Мориса Уилкса, чтобы разработать и внедрить язык программирования, который стал известен как CPL. Это был императивный язык программирования, но он также должен был обладать мощными возможностями функционального языка программирования. Ландин, который был сотрудником Стрэчи в его консалтинговой компании, оказал огромное влияние на взгляды Стрэчи на языки программирования. В знаменательной статье 1965 года "Следующие 700 языков программирования" Лэндин беззастенчиво продвигает функциональные языки программирования (называя их обозначающими < / em> languages) и описывает императивные языки программирования как их «антитезу». В последующем обсуждении мы обнаруживаем, что Стрэчи вызывает сомнения в сильной позиции Ландина.