value (element of an algebra), constant, variable, ground and non-ground terms, free algebras : there is a need for clarification

Question

I have been developing an algorithm to compute the congruence defined by a finite set of "generators" and a finite set of equations (in the sense of equational theories). The algorithm terminates if the free algebra defined by the generators and the function symbols used by the equations is finite. (Its carrier is finite.) Now the following question arises: are the "generators" values, constants, or variables ?

This simply is a question of terminology.

My method uses a data structure representing large families of ground terms and the generators are considered as constants in those terms. On the other hand, the generators are elements of the free algebra. And, finally, the generators of the free algebra are generally considered as variables in the equations. So I am faced with a problem of terminology. Note also that, in my method, nothing prevents me from using the generators in the equations. But then I consider them as constants. In a sense, in my method, I combine the equations and the generators to generate ground equations. Since the free algebra is finite, only a finite number of equations needs to be generated. However, in the end, when the free algebra is computed, it represents (a huge number of) equalities wherein the generators can be interpreted as universally quantified variables. Thus, my question: are the generators constants or variables? Should I call them constant or variable. Similarly, the equalities represented by the free algebra : are they equalities between ground or non-ground terms?

Answer 1

You should just call them a set. What you are computing is the free E-algebra generated by a set X, where E is your presentation. The presentation E consists of an algebraic signature with some function symbols and constants of various arities, along with some universally quantified equations. Given E, you can form the set of terms TX over a set X, defined inductively: if x is in X, then x is a term; and if t1,...,tn are terms and f is n-ary, then f(t1,...,tn) is a term. This includes the case n=0, in which case f is a constant, if your signture contains such a thing. Now you can form the least congruence relation == on terms containing all substitution instances of your equations. The quotient algebra TX/== consisting of the equivalence classes of terms modulo == is the free E-algebra on generators X. It has the property that any set function X -> A to the carrier of any E-algebra lifts uniquely to an E-algebra homomorphism TX/== -> A. Hope this helps!

Answer 2

This is a semi-arbitrary and very subfield-dependent distinction of terminology, without a standardised answer.

Within the subfields I know, different communities tend to draw the lines between these terms in different places. Sometimes this reflects genuine differences in how the formal systems they use treat these notions; other times it’s just a difference of terminology.

For context: my own work is computer-formalisation and proof assistants; I also have a little familiarity with some other communities in mathematical computation and theory of programming languages. In the communities I know, your generators might be called any of “variables”, “constants”, “constant symbols”, “uninterpreted constants”, just “generators”, or other terms. They wouldn’t be called “values”, as that has a slightly different technical meaning for us — but I can well imagine there may be other communities who would use “value” for this.

So generally, you should match what’s used by other people working on related topics, or in the same research community. We can’t tell you what this is without knowing more about the precise context of your work, and what research it’s connected to. But if you’re aiming to do research in the area, you should be reading enough of the subfield’s literature (and/or informal communication forums) to get familiar with its terminological conventions yourself. I don’t mean “you must read all the papers ever published on the topic” — but you must be reading at least some recent papers on related prior work, and they should (among other things) give you an answer for this question.

Answer 3

Apparently, there are no general definitions of the constant and variable notions that are universally relevant. One must give the appropriate definition in each particular situation. Sometimes a symbol that is called a variable in some context, must be represented by another object or by the same object called a constant, in another context, when one establishes a correspondance between the two. This is because the terminology is different in the first area and in the second one. In my case, I use so called ground terms to generate equations using universally quantified variables. The terminology "ground terms" must be used because I use a data structure related to congruence closure techniques where variables cannot be instantiated.