Talk:Term algebra

Herbrand Universe

I can't tell the difference between a term algebra, and a Herbrand universe. Can someone clarify? linas (talk) 15:51, 9 April 2008 (UTC)

Err, maybe I've got it .. a Herbrand universe cannot contain any free variables, by definition. A term algebra does not even raise the issue of free variables, and so one can define a term algebra to consist of a set of constants, variables, and other terms. linas (talk) 15:57, 9 April 2008 (UTC)

I don't think they are the same, Herbrand Universe is defined for first order languages, so it's just an example (or special case) or term algebra, not the general definition, assuming Mathworld is correct. Tijfo098 (talk) 05:06, 18 April 2011 (UTC)

Unfortunately "Herbrand Universe" is used almost exclusively in comp sci texts, which are seldom the epitome of mathematical clarity. I can't find a clear definition for it. Tijfo098 (talk) 07:16, 18 April 2011 (UTC)

Herbrand structures and term algebras are topics from very different fields (Logik, Algebra). IMO, mixing them in one article can only go wrong and it already is. -- Cobalt pen (talk) 07:18, 9 December 2015 (UTC)

Where do the terms come from?

I am confused by this: "a term algebra is an algebraic structure which is freely generated from a signature", "free magmas are isomorphic to term algebras generated from a signature consisting of one binary operation". If the signature just contains the symbols which form the operation (and an arity function) then the free group on the signature {m, arity(m)=2} consisting of one binary operation is the group {e,m,m^-1}. Where do the 'terms' come from? And are term algebras elements of a variety of algebras? 131.111.28.82 (talk) 15:51, 18 December 2008 (UTC)

I am confused by your question:

• The definition of free groups has nothing to do with the choice of signatures. The free group with no generators has a single element, every other free group has infinitely many elements. There are no free groups with three elements.
• The free magma with n generators is always different from the free group with n generators. In fact, free magmas never have identity elements. (In the case of the free magma with 0 elements that's because it has no elements at all.)
• Every term algebra over a signature is an algebra of that signature and therefore a member of the variety of all algebras of that signature. But it is not a member of any proper subvariety, because no identity ever holds in a term variety.
• Term algebras over different signatures can a priori never be in the same variety.

A term is something like $m(x,m(m(x,y),z))$ (a term with three variables) in your example signature. The term algebra with 0 generators (term algebra over the empty set) consists of those terms which have no variables (in your example there are no such terms because there are no constants in the signature). Or more generally the term algebra over the set {1,2,3} contains e.g. elements $m(1,m(m(1,2),3))$, $m(1,m(m(1,3),2))$, $m(2,m(m(2,1),3))$, which are all different. --Hans Adler (talk) 23:43, 18 December 2008 (UTC)

Axioms

I am confused. A term algebra is a "freely generated algebraic structure", and there is an algebraic structure that respects an axiom. Axioms are not mentioned in the article. The question is, may a term algebra be generated from an algebraic theory and respect its axioms? If "yes", we should include some example like a free monoid. If "no", we should replace "freely generated algebraic structure" with "freely generated universal algebra". --Beroal (talk) 09:36, 7 December 2010 (UTC)

You're right, a term algebra does not include any axioms or it would not be "absolutely free". Tijfo098 (talk) 07:19, 18 April 2011 (UTC)

Decidability

In which section in the book by Ferrante is it proved? I can only find statements about special cases (two successors etc.) --Chricho ∀ (talk) 16:43, 31 October 2012 (UTC)

FWIW info was added with this edit. I don't have immediate access to the book. I wonder however it hasn't been confused with another result, of Ferrante, Rackoff (and a few others) namely that real addition is NONELEMENTARY [1] [2]. Tijfo098 (talk) 20:17, 31 October 2012 (UTC)

I was able to source that [3] "The theory of one unary function is not elementary recursive". I'm guessing that is what is meant in the wiki article by "Term algebras can be shown decidable using quantifier elimination". Tijfo098 (talk) 20:38, 31 October 2012 (UTC)

The book is about complexity issues, the main topic are lower bounds like the theorem you mentioned (which is only mentioned, but not proven). But I do not see a prove for the NONELEMENTARY claim. The book proves that the decision problem for a term algebra with one successor (aka $(\mathbb {N} ,+1)$) is not in NSPACE(n) and for two successors there exists $c\in \mathbb {Q} ,c>1$ such that the decision problem is not in NTIME($c^{n}$). That is far from NONELEMENTARY. In fact the decision problem for Presburger arithmetic can be solved in triple exponential time, thus for sufficiently simple free term algebras (one successor) it is ELEMENTARY. Maybe the general problem “given a finite signature and a formula, decide whether it holds in the term algebra generated by this signature” is NONELEMENTARY? But I do not see a proof in the source.

Regarding decidability: I have read that the quantifier elimination proof has been done by Mal'cev.[4] Here is a proof: [5] Mal'cev seems to prove decidability in a more general setting, I will read that. Decidability also obviously follows from the decidability of structures representable by tree automata. --Chricho ∀ (talk) 15:49, 2 November 2012 (UTC)

(edit conflict) Well, possibly dumb question: if it's such a direct consequence of Rabin's tree theorem (1969), why is Mal'cev proof (1971) so complicated? Tijfo098 (talk) 16:50, 2 November 2012 (UTC)

Surely Rabin's tree theorem implies that "the monadic second-order theory of any term algebra in a finite monadic signature is decidable" [6] But it this what the wiki article means by "Term algebras can be shown decidable using quantifier elimination"? Tijfo098 (talk) 17:13, 2 November 2012 (UTC)

It looks like wiki-claimed decidability result (referring to a first-order theory) is also proved in Hodges A Shorter Model Theory. [7]. Google won't let me see all relevant pages, so I'll have to go to the library. Tijfo098 (talk) 17:31, 2 November 2012 (UTC)

Mal'cev’s proof is more general, he has a wider notion of “free algebra” and also talks about “locally free algebras”, but I do not know the details.

Regarding complexity: [8] tells us that it is NONELEMENTARY if there is a function with arity ≥2. If there are only successor functions the decision problem is ELEMENTARY and in fact 2EXPSPACE, see [9]. --Chricho ∀ (talk) 17:36, 2 November 2012 (UTC)

The NONELEMENTARY result was apparently first proved in: K. J. Compton and C. W. Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. Annals of Pure and Applied Logic, 48:1–79, 1990. So it seems improbable that the book of Ferrante and Rackoff from from 1979 contained the complexity result. Tijfo098 (talk) 02:01, 3 November 2012 (UTC)

Actully Compton and Henson say on p. 52 that "Our next example gives another family of useful theories which are not elementary recursive. Lower bounds for these theories were first given by Rackoff [56] (see Ferrante and Rackoff [24])" and the "next example" is "The theory of any pairing function"; [24] is the 1979 book of Ferrante and Rackoff. [56] is C. Rackoff, The computational complexity of some logical theories, Doctoral Thesis, Massachusetts Institute of Technology, Cambridge, MA (1975). Since you can use paring functions to build all term algebras, it seems the result for term algebras follows from that. Tijfo098 (talk) 02:26, 3 November 2012 (UTC)

How do you translate pairing functions to term algebras? --Chricho ∀ (talk) 16:05, 8 November 2012 (UTC)

Well, you can build all of SO logic with just a pairing function, equality and unary/monadic relations. From Shapiro Foundations without Foundationalism, p. 63: "Another alternative would be to include only monadic predicate variables. In such languages, surrogate n-place relation (and function) variables can be introduced if there is a notation for a fixed pairing function, a one-to-one binary function from the domain to itself. If u and v are terms, let <u, v> denote the corresponding 'pair', the value of the pairing function at arguments u and v. The formula X²xy could be replaced by X¹<x, y>. This option would simplify the exposition in places, but it brings the cost of an arbitrary posit, the pairing function. It might be added that a pairing function amounts to a principle of infinity, since there is no such function on finite domains." (By X² he means a predicate with arity 2.) So I'm assuming that any logic over term algebras (which are part of the normal def of SO) can be built with just a pairing function. There is nothing explicit about term algebras in Compton and Henson, but Sturm and Weispfenning (which you found) attribute the NONELEMNETARY result to that 1990 paper of C&H. I don't see anything else in C&H [10] which could imply it. Tijfo098 (talk) 12:01, 9 November 2012 (UTC)

I’m not sure, whether this works, however: You would have to reduce pairing functions to term algebras to prove the NONELEMENTARY result for term algebras (not vice versa, since it is a lower bound). --Chricho ∀ (talk) 17:44, 9 November 2012 (UTC)

Yeah, it's not that simple; it involves an inseparability result, I think. See sect 4 in C&H for the general idea. There's no Wikipedia article on that that I can find... Tijfo098 (talk) 18:16, 9 November 2012 (UTC)

I think it's probably good to base further work on the article on Sturm and Weispfenning but give proper credit to Ferrante Rackhof and not pretend that this problem was left open decades after. I do not see the subtlety of the argument aluded above given the general definition of pairing function. (For having only unary symbols it's indeed simpler; one should clarify whether signature is part of the input or one considers a paremeterized family of decision problems.) For reference, here is a scan of the relevant page defining pairing function; it's just an injection, and a binary function symbol is always an injection: http://lara.epfl.ch/~kuncak/PairingFunction.png (use only for the purpose of clarifying this issue, please, the publication of the revised thesis is by Springer and possibly obtainable on request from the MIT library). Vkuncak (talk) 08:59, 9 September 2022 (UTC)