Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Изменяется ли поведение программы при перестановке выражений и их значений?
Референтная прозрачность в теории языков программирования
Whether a program behaves differently if expressions and their values are interchanged
referential transparency in programming language theory
В аналитической философии и информатике референтная прозрачность и референтная непрозрачность – это свойства лингвистических конструкций и, как следствие, языков. Лингвистическая конструкция называется референтной прозрачной, если для любого выражения, построенного на её основе, замена подвыражения другим, обозначающим то же значение, не изменяет значение всего выражения. В противном случае конструкция называется референтной непрозрачной. Каждое выражение, построенное с использованием референтной непрозрачной конструкции, содержит утверждение о конкретном подвыражении, в то время как каждое выражение, построенное с использованием референтной прозрачной конструкции, содержит утверждение не о подвыражении, а о его значении, то есть подвыражения "прозрачны" для выражения и выступают лишь как "ссылки" на что-то другое. Например, лингвистическая конструкция "был мудрым" является референтной прозрачной (например, "Сократ был мудрым" эквивалентно "Основатель западной философии был мудрым"), а конструкция "сказал" – референтной непрозрачной (например, "Ксенофонт сказал: 'Сократ был мудрым'" не эквивалентно "Ксенофонт сказал: 'Основатель западной философии был мудрым'"). Референтная прозрачность зависит от значений, связанных с выражениями, то есть от семантики языка. Следовательно, как декларативные, так и императивные языки могут быть референтными прозрачными или непрозрачными, в зависимости от заданной им семантики. Важность референтной прозрачности заключается в том, что она позволяет программисту и компилятору рассуждать о поведении программы как о системе преобразований. Это может помочь в доказательстве корректности, упрощении алгоритма, облегчении модификации кода без его нарушения или оптимизации кода с помощью мемоизации, исключения общих подвыражений, ленивых вычислений или параллелизации.
In analytic philosophy and computer science, referential transparency and referential opacity are properties of linguistic constructions, and by extension of languages. A linguistic construction is called referentially transparent when for any expression built from it, replacing a subexpression with another one that denotes the same value does not change the value of the expression. Otherwise, it is called referentially opaque. Each expression built from a referentially opaque linguistic construction states something about a subexpression, whereas each expression built from a referentially transparent linguistic construction states something not about a subexpression, meaning that the subexpressions are ‘transparent’ to the expression, acting merely as ‘references’ to something else. For example, the linguistic construction ‘ was wise’ is referentially transparent (e. g., Socrates was wise is equivalent to The founder of Western philosophy was wise) but ‘ said ’ is referentially opaque (e. g., Xenophon said ‘Socrates was wise’ is not equivalent to Xenophon said ‘The founder of Western philosophy was wise’). Referential transparency depends on the values associated to expressions, that is on the semantics of the language. So, both declarative languages and imperative languages can be referentially transparent or referentially opaque, according to the semantics they are given. The importance of referential transparency is that it allows the programmer and the compiler to reason about program behavior as a rewrite system. This can help in proving correctness, simplifying an algorithm, assisting in modifying code without breaking it, or optimizing code by means of memoization, common subexpression elimination, lazy evaluation, or parallelization.
Определенность
Формальный язык считается определенным, если все вхождения переменной в пределах ее области видимости обозначают одно и то же значение. Пример. — Математическое выражение определено: 3x² + 2x + 17. Действительно, два вхождения x обозначают одно и то же значение.
A formal language is definite is defined by all the occurrences of a variable within its scope denote the same value. Example. — Mathematics is definite:
3x^(2) + 2x + 17. Indeed, the two occurrences of x denote the same value.
Нескладимость
Формальный язык называется разворачиваемым, если все его выражения β-редуцируемы. Пример. — Лямбда-исчисление разворачиваемо: ((λx. x + 1) 3). Действительно, 1 = ((λx. x + 1) 3) = (x + 1)[x := 3].
A formal language is unfoldable is defined by all expressions are β reducible. Example. — The lambda calculus is unfoldable:
((λx. x + 1) 3). Indeed, 1=((λx. x + 1) 3) = (x + 1)[3/x].
Отношения между свойствами
Референтная прозрачность, определённость и развёртываемость независимы. Определённость подразумевает развёртываемость только для детерминированных языков. Недетерминированные языки не могут обладать определённостью и развёртываемостью одновременно.
Referential transparency, definiteness, and unfoldability are independent. Definiteness implies unfoldability only for deterministic languages. Non deterministic languages cannot have definiteness and unfoldability at the same time.