The long-standing problem of adequate formalization of local names in mathematical formulas and semantics of references in object-oriented languages taken on their own without objects, is discussed. Reasons why the existing approaches cannot be considered suitable solutions, are explained. An introduction is given to the relatively recent works on the theories of names and references of the group lead by Andrew Pitts. The concept of referential transparency, in which contextual equivalence is used instead of the usual equality of values, is analyzed. It is the main property, which these theories are based upon: such modified referential transparency is preserved when a purely functional language is extended with names and references as data. An outline of a constructive denotational semantics of the extended functional language is given. It is argued that the modified referential transparency, along with many other valuable properties, can be also preserved for mutable objects that change to a limited extent. This leads to a model of computation between functional and object-oriented ones, allowing for a deterministic parallel implementation.
Consider the long-standing problem of adequate formalization of local names, bound variables in
formal languages and references in object-oriented languages. In mathematics and programming, over
the years, a certain style of working with names and references has been established, and it may seem
that there is no problem here. However, in Section 2 we show that this is not the case: the methods of
working with formulas with quantifiers presented in textbooks on mathematical logics (for example,
[
A group of mathematicians led by Andrew Pitts has been developing the missing theories of names
for almost thirty years [
In Section 6, we rectify this and show that if in the definition of referential transparency, the usual equality of values is replaced by contextual equivalence (a.k.a. observational equivalence, Leibniz equivalence), then such modified referential transparency holds for a functional language with names or references. This observation is the cornerstone, which the theories developed by A. Pitts' group are based upon. The properties that are preserved and that are violated in the extended functional language are analyzed in Section 7.
In Section 8, we give an idea and outline of a constructive denotational semantics of the extended functional language. We hope that after reading this section, the feeling of mystery will disappear.
In Section 9, we list the steps that can (and should) be performed further from a functional language with names and references to objects with states—first immutable and then with restricted mutation – so that referential transparency based on contextual equivalence is preserved.
We also point out the practical significance of these works in the field of parallel programming: maintaining the contextual equivalence of the results of computation in any order means determinacy. In cases where a parallel program has the determinacy of both final and intermediate results of computation, it is much easier to debug, it is predictable and reliable. (Such strong form of determinacy is referred to as internal.)
Our contributions are as follows. We point out the problem of adequate formalization of names and references as data and argue that the works by Andrew Pitts’ group have almost closed the problem for functional languages and opened the way to complete semantics of object-oriented languages, which has yet to be developed. We demonstrate that contextual equivalence, together with the modified referential transparency, is the cornerstone of the theories of languages with names or references as data. We present an outline of a constructive denotational semantics of the extended functional language. We discuss steps from A. Pitts’ theories to a restricted object-oriented language that retain some of the nice properties of a functional one.
In programming languages, the concept of a name appears in two seemingly different guises: identifiers of variables in program code and references to objects (Note that references and pointers arose in programming and made sense before the concept of an object was fully established in objectoriented languages).
Identifiers and references “live” in different times: variable identifiers – in static time from the moment when a program is written until it is converted by a compiler into executable code; references – in run time when a program is executed and does not change, while data are created and manipulated. These times overlap when it comes to metaprograms, programs that analyze and transform programs, where interpreters and compilers are the most known among such ones. In metaprograms, variables of ground programs are usually represented by references to some objects that store the necessary information. The question arises: Is this mapping of variables into references a purely programmatic trick or does it make some sense?
What about names in mathematics? Using the language of mathematics in everyday scientific activity, we differently perceive variables, letters as elements of a text on paper with which we work, on the one hand (“static time”), and data domains, from which variable takes values in some ideal mathematical “run time”, on the other hand. They overlap in metamathematics, in logics, when the language of mathematics becomes an object of study, description, analysis and transformation. And in programming—in computer algebra systems, where a computer rather than a person manipulates formulas, “code” in mathematical languages.
Let us look at the part of the mathematical world where variables in formulas become an object of definition and manipulation.
Mathematical language is based on the fundamental concept of free and bound variables. For example, in the formula ∀ ∃ ( , , ) the variables and y are bound by the quantifiers ∀ and ∃, respectively, and is a free variable, a parameter of the entire formula. It seems simple, but let us open the classic textbook [13, p. 48] and see, for example, a definition of such an obscure (auxiliary!) notion:
If is a well-formed formula and is a term, then t us said to be free for in if and only if no free occurrences of in lie within the scope of any quantifier ∀ , where is a variable in .
This phrase just means that the term t can be directly substituted for x in the formula A. Another common way to overcome the same problem is to provide a renaming requirement in the definition of substitution:
When substituting a term t into a formula A, variables under quantifiers in formula A are renamed, if necessary, so that there is no conflict with the free variables in t.
For example, when substituting ( ) for y in ∀x P(x, y) one needs to replace with, say, : ∀ ( , ( )).
In addition, extra phrases such as “up to renaming variables”, “up to -equivalence”, “fresh variable" are often found in reasoning, theorems and proofs about formal languages, which clutter up the code in proof assistants such as Coq and Agda.
Where do these problems come from? Our intuitive understanding of quantifiers doesn't seem to contain such “tricks”. Looking at a variable bound by a quantifier, we perceive it differently than a free one – not just as a letter. We imagine that the bound variable in the above example is a completely different entity than the letter of the free variable in it:
The letter of a bound variable under the quantifier along with its occurrences in the scope of the quantifier, represents a certain entity that differs from the letters of all variables and all values in this formular and elsewhere in the mathematical world.
Intuitively thinking this way, we don't feel any need for renamings when substituting a term with such entities under quantifiers into anything.
Thus, the notion of a term free for a given variable, as well as the requirement for renaming when substituting, are just artifacts of a certain way of formalization of mathematics in common mathematical textbooks and have nothing to do with the essence of the idea of quantifiers and bound variables.
Of course, this is not news. Let us recall the formalization of quantifiers given by N. Bourbaki [
According to N. Bourbaki, quantifiers ∀ and ∃ with variables are not primary notions, but rather a
readable representation of formulas in the basic language of mathematics introduced in Chapter 1 of
Volume 1 of Treatise [
In Treatise, the quantifiers ∀ and ∃ are defined through the terms of the form τxP(x) (with the informal meaning “such that P( ) is true”), which in turn expand into a construct without the letter . Let us show Bourbaki’s method of excluding variable letters, as if it were applied directly to the quantifiers, without going down to the level of -terms.
Encoding quantifiers in the style of N. Bourbaki, we replace the occurrences of bound variables with signs □ and draw lines to the corresponding quantifiers ∀ and ∃, depicting a link between them. Free variables remain letters. For example, ∀ ∃ ( , , ( , )) is encoded as ∀ ∃ (□, □, (□, )_).
What is instructive about this approach? Undoubtedly, N. Bourbaki sought to make the basic level of the language of mathematics as simple as possible. However, they made its representation not linear, but graphical: the code in the base language is not a linear sequence of symbols but a graph, which in itself is far from a trivial concept. Such decisions are not accidental.
N. Bourbaki transferred the complexity here from another place. From where? From the substitution operation. Now the substitution of any term for any bound variable is defined without conditions like “a term is free for a variable” and other measures against the capture of free variables by external quantifiers.
Moreover, such representation reflects our intuition, mentioned above, that a variable bound by a quantifier is a completely different entity than a free variable: each bound variable is different from all other variables in the world because it is linked to the unique occurrence of a quantifier into a mathematical text. We can hypothesize that this was the decisive argument why N. Bourbaki transferred the complexity of the presentation of formulas to this level.
Back to programming. How do we encode Bourbaki’s graph representation in an object-oriented language? The simplest solution is to keep the reference to the object representing the quantifier in the representation of each variable occurrence. This is how it is usually done in compilers after the name resolution stage: each occurrence of an identifier contains the reference to its declaration.
Such a solution based on a graph representation cannot be programmed in a purely functional language, bearing in mind that an adequate implementation should have the same computational complexity of transitions from a vertex to a vertex along an edge as in object-oriented languages, O(1), as intuitively expected. The fundamental flaw of functional languages is that they do not provide means to efficiently represent general graphs, but only trees. The natural representation of a graph in functional languages is the list of vertices and arcs. Accessing such lists is more complex than O(1). Moreover, this solution is complicated by the fact that it is necessary to assign unique identifiers to vertices and, perhaps, edges. There are no simpler solutions (except for the implementations of specialized libraries by lower level means).
In mathematics, the notion of a graph is defined in this way as well. Apologists of purely functional languages love them just for this—for their close correspondence to classical mathematics with set theory as a basis. On the other hand, object-oriented languages fall out of this mathematical picture. They provide effective means for adequately representing a variety of data structures, including graphs. This indicates unresolved problems in the foundations of mathematical semantics of programming languages.
Returning to the graph representation of N. Bourbaki’s basic language, we see an interesting picture. It is based on the non-trivial notion of a graph, which is considered intuitive. Then, in set theory, it turns out that its concepts are not enough to adequately describe its own language (Note that the completeness/incompleteness of theories has nothing to do with this issue. In reasoning about the incompleteness, it is allowed to use arbitrary complex encoding of one theory in another; only the possibility of mapping is important. On the other hand, by the “adequacy” we mean the preservation of computational complexity).
These questions come up in programming when we perform analysis, program verification, and equivalent transformations preserving semantics. To do this, the semantics must be well defined, so that it is convenient and efficient to implement in proof assistants. Simply contemplating Bourbaki’s representation with the words “it’s intuitively clear that it works” is not enough. 4. Works on nominal methods
30 years ago, mathematician Andrew Pitts not only saw these problems of names and references
(he was not the only one; see, for example, [
In 2019, Andrew Pitts and Murdoch Gabbay received the ACM Alonzo Church Award for their
ground-breaking work introducing the theory of nominal representations [
To see the sources of problems and appreciate achievements, consider a purely functional language
extended by a generator of new names or references. We use the later terms as synonyms, since
references are names of objects, the authors of nominal methods have applied them to formulas and
program code with local names and use this word, while the theory is well applicable to references to
objects that interest us more. In language FreshML [
The notion of an object consists of 2 parts: the notion of a reference and the notion of the state of an object, where references can be talked about separately from states, but not vice versa. In addition, to deal with changing states, the concept of computational time is necessary. But while we are considering references alone, the concept of time is not required. In the language under consideration, where there are no objects with changing states, all the results of function calls do not depend on the order of computation, and time plays no role. Now we will deal only with the semantics of names and references as such.
Every evaluation of the operator generates an atomic datum, the only property of which is to be equal to itself (reflexivity of equality) and to be unequal to everything else, that is, to all values in the data domain and all data generated by other calls to the operators. Thus, although time does not matter to us, it is necessary to distinguish between individual evaluation actions.
Let us look at examples. Below we use the ≔ sign in the following two roles: in our functional language, in the statement to introduce a local name with a single evaluation of the right-hand side and to define functions; in the metalanguage of our reasoning as “equal by definition”.
For the rest, we use generally accepted mathematical notation, hoping that they will be understood without lengthy explanation.
Example. The following expressions in a functional language with the operator evaluate to True: , ≔ , ≔ ,
We see that re-evaluating the operator produces unequal references and copying preserves equality.
Another example. The following function produces a pair of unequal elements, because every time ( ) is evaluated, the first element of the pair will be a new reference unequal to any other value in the world:
( ) ∶= 〈 , 〉. ∀ ( ) ≠ ( ).
The above examples point to the first (and main) problem of a functional language with the operator: referential transparency is broken.
Referential transparency is a property of a term (expression, subexpression) in a given language that replacing any occurrence of a term with its value, evaluated only once, is an equivalent transformation. For a referentially transparent language, the following properties hold for all terms and functions that can be defined in the language:
= , = ⟹ ( ) = ( ).
Referential transparency is so deeply rooted in the language of mathematics, mathematical logics that it seems difficult to approach the construction of a theory of a language, in which it is absent, without falling into the operational semantics with the notion of computational time. In particular, the denotation semantics of purely functional languages, which maps code of function definitions into functions of set theory, relies heavily on referential transparency.
Nevertheless, as the work of A. Pitts’ group has shown, such a theory is possible, interesting, and productive. Its success is based on the following observation:
The values obtained by multiple evaluation of a term in a functional language with the operator possess contextual equivalence (observational equivalence, Leibniz equivalence).
Two values x and y of some type D are contextually equivalent (denoting x ≈ y) if they are indistinguishable by any predicate c, that is, a function of type D → Bool, defined in language L: x ≈ y ≔ (∀ ∈ ) ( ) = ( ).
operator has the following property.
and more than that
≈ , = ⟹ ( ) ≈ ( ) ≈ ⟹ ( ) ≈ ( ).
What we have obtained is a modified referential transparency, where equality of values is replaced with contextual equivalence.
Note that contextual equivalence cannot be checked within a language, there is no such computable relation as ≈, unlike the usual equality of values =. Contextual equivalence is a notion of the theory, the mathematical metalanguage.
A functional language with a reference generator retains many of the good properties of purely functional languages, when equality = is replaced by equivalence ≈. Of course, when formulating equivalent transformations, it is necessary to keep track of which of these relations plays a role.
For example, the common subexpression (subterm) elimination is no longer an equivalent transformation in the general case (here the ⟹ sign means “equivalently converts to”, rather than “implies” as above): … … … ⟹ ≔ … … …
Nevertheless, such transformations can be used by imposing restrictions on the corresponding piece of code so that it does not go beyond the purely functional subset or go “not very much”. Two examples of such restriction:
In case the language is statically typed: The type of term does not use the reference type. 2. During evaluation of , no new reference is generated (e.g., if there are no operators in the code of function used in ) or new references do not fall into the value of (which can sometimes be determined by static analysis of data dependencies).
Violation of the equivalence of the common subexpression elimination indicates that the classical construction of denotation semantics for functional languages, which assigns each language term its denotate, no longer works. According to the traditional denotational semantics, copies of the denotate of a term can be used as the result of evaluating all the occurrences of the term, which is not our case.
Nevertheless, the following properties are preserved in a functional language with references,
albeit in a modified form:
There exists the notion of a denotate of a term, which, although not a ready-made value, can
be used instead of re-evaluating each copy of the term with a complexity not exceeding that of
copying the denotate. This follows from the work of A. Pitts’ group on set-theoretic models of
nominal sets and the so-called -calculus [
Let us show the essence of the idea by presenting an outline of a semantics of an extended
functional language with references. The semantics is denotational in the sense that it assigns to each
function definition and to each closed term a certain entity, which can be used instead of evaluating a
function call. On the other hand, it is not a value, copies of which can be used instead of a term, as in
the traditional denotational semantics. The construction is a little trickier. Below we follow our
presentation at a conference [
Consider a pure functional language of your choice – be it statically typed (as Haskell) or untyped (as Lisp). A first-order language (without lambda expressions) is sufficient for our purposes, although there are no problems with a higher-order language either. Any of the usual operational semantics of the language is suitable.
Now extend the data domain with references that are atomic in the sense that each one has no other property than being equal to itself and unequal to other data, along with the operator that generates a new reference each time it is called. The values passed as arguments and returned by functions are like the usual ones, but may contain references inside, e.g., a list of references is a first-class value.
The usual set-theoretic denotational semantics, where each term is assigned a single denotation
that can be used in place of all occurrences of the term, does not work, because the result of a function
call containing new references, e.g., that of term in the simplest case, cannot serve as such a
denotation. Moreover, the data domain with references is not a set in the sense of classical set theory. Of
course, non-standard set-theoretical models are possible, and they were indeed developed by A. Pitts’
group [
Let the denotation of a closed term not be the result of its evaluation , as usual, but a term of the following form, obtained from by considering as variables all new references 1, … , produced during the evaluation of and prepending the list of new references to : Here is a special symbol (like in lambda expressions). Results of each evaluation action of the term are obtained from this denotation by evaluating the following lambda expression: ν 1 … . . ( 1 … . ) … which means this: substitute new references for all variables 1, … , in .
Let the denotation of a function be a set of terms of the following form (rather than a set of argument-value pairs, as usual):
1 … . ↦ 1 … . .
Such function denotation determines the result of evaluating a function call ( ) as follows. Find the element of the denotation with such left-hand side and such references 1, … , occurring in that = ( 1 … . ) 1 … . Then return the result by evaluating the following lambda expression ( 1 … . )(( 1 … . ) … ) 1 … .
We see that this semantics satisfies the usual requirements for denotational ones: every term and function in a program has a denotation, although denotations are constructive terms rather than elements of the set-theoretic world. Therefore, it is referred to as constructive denotational semantics.
One can look at the function denotations from an operational point of view as they grow during computation. The denotations are gradually collected at each function call ( ) by constructing an element of the denotation of from the argument-value pair, where 1 … are all references found in the argument , 1 … are the references generated during evaluation of the function call. It can be proved that the ordinary evaluation and the evaluation using these denotations give contextually equivalent results. This operational view shows the idea of tabulation or memoization that can be implemented for such languages.
Andrew Pitts, Ion Stark, Murdoch Gabbay and other authors [
The next step that has yet to be done is to build a complete theory of objects in object-oriented
languages using a suitable theory of references. Existing theories are incomplete, as they leave
questions of the exact semantics of references to naïve or semi-formal reasoning. As far as the authors of
this article are aware, there has been no significant progress in the field of semantics object-oriented
languages for decades, but this should happen after the ACM Award [
Along this path, a theoretically interesting and practically important question is the construction of computational models intermediate between functional languages with a reference generator and general object-oriented languages. They can be created either by extending functional languages while retaining the selected properties, or by restricting object-oriented languages so that the necessary properties are fulfilled, or by a combining both.
Our main task here is to move along this scale as far as possible while maintaining the modified referential transparency based on contextual equivalence as a fundamental property, from which other useful properties follow, albeit in a modified form. In particular, it is more reasonable to define the determinacy of parallel computation through the broader notion of contextual equivalence, rather than through the equality relation built into programming languages, since the indistinguishability of the results obtained in different orders of computation, rather than their equality, matters from a practical point of view.
Currently, the following stages of loosening restrictions and adding notions are observed:
As a starting point, take a purely functional language with a reference generator, but without
the concept of a stateful object. This level is discussed above.
Add the notion of an immutable object. At first glance, there is little practical benefit from
this, except that the reference equality is more efficient, it is checked much faster than comparing
the content of objects (of course, provided that it corresponds to the meaning of the task).
However, there is both a theoretical and a practical purpose of equality by reference: it can be defined for
all data, including those that previously have no reasonable computable equality. For example, the
functional values generated by lambda expressions, closures, are of this type. Some languages
(e.g., Haskell) forbid comparing closures based on the idea that the equality of functions is
algorithmically undecidable. However, closures are trivially equivalent if they are copies of the result
of the same evaluation of a lambda expression – similar to how equal references go back to the
same evaluation action of the operator . Such equality can always be defined for all data. Its
only flaw is the lack of referential transparency. The special role of such equality is not accidental:
it is initial in the sense of category theory, that is, the strongest relation entailing any other
equivalence relation.
Next, we allow mutation of the states of objects, but only those that are invisible from the
point of view of the “observer” (from program code in this language), that is, the side effects are
such that any order of computation produces contextually equivalent results. An open problem: Is
it theoretically possible to characterize object classes defined in an object-oriented language that
retain contextual equivalence for all (sub)expressions in the language? The general answers to
these and similar questions seem to be negative, since here we are faced with algorithmic
undecidability. But, as is usually the case both in mathematics and in programming practice, it is often
possible (and necessary) to identify and study interesting special cases for which something
meaningful can be said.
Such a rich special case are objects that can be described as changing monotonically on some
(semi)lattice [
The present authors are working on such model of computation, intermediate between functional
and object-oriented ones, and a Java-like language that satisfies the above properties, with the
practical goal of implementing a deterministic parallel programming system that will free the programmer
from the torment of debugging non-deterministic parallel programs on a fairly wide class of problems
[
The authors are very grateful to the participants of the seminars at which this material was presented and thoroughly discussed: Igor Adamovich, Arkady Klimov, Yuri Klimov, Alexander Konovalov, Antonina Nepeivoda, Sergei Romanenko. Special thanks to Sergei Meshveliani who made valuable comments at the conference presentations. 11. Conclusion
We have considered the long-standing problem of adequate formalization of local names in formal languages in both mathematics and programming languages, as well as the problem of formalization of the semantics of references in object-oriented languages. Considering the history of the issue, motivations and solutions, we came to the conclusion that these are one and the same problem, and the seeming difference is that these concepts refer to different kinds, times, periods of activity, which have well-established names in programming: we deal with names in formal texts in static time, when a mathematical text or program is written and processed, e.g., by a compiler; and manipulation of data with references happens “in dynamics”, during run time of a program on a computer and when mathematical statements are evaluated in some ideal mathematical world. These periods intersect when a mathematical text becomes an object of manipulation on a computer, in computer algebra systems, in logics and metamathematics, and programs undergo deep analysis and transformation in metacomputation. An adequate theory of names and references is wanted.
Over the past decades, Andrew Pitts' group has made significant progress in the construction of
such theories [
It was demonstrated that the success of building these theories and the expectation of their fruitful development up to mutable objects are based on the modified referential transparency, in which the contextual equivalence is used instead of the usual equality of values. In particular, the notion of determinacy of parallel computation essentially requires contextual equivalence of results in different orders of computation, rather than equality of values. Based on such weakened referential transparency, we are able to extend purely functional languages with references, and then even with mutable objects subject to certain restrictions, while retaining many of the valuable properties of functional programs.
In the last section we presented our view of the possible stages of extending purely functional
languages to object-oriented ones, first with references without objects, as in the works of A. Pitts’
group, and then with mutable objects under certain restrictions that ensure the preservation of the
modified reference transparency and the properties resulting from it. Some results have been already
obtained; others remain open problems for future work. What is most valuable in this development is
the emergence of a model of computation and programming languages between functional and
objectoriented ones (which the present authors work on [
SIGPLAN Notices 38:9 (2003) 263–274. https://doi.org/10.1145/944705.944729. [21] I. D. B. Stark, Categorical Models for Local Names, Lisp and Symbolic Computation 9:1 (1996) 77–107. https://doi.org/10.1007/BF01806033.