Why do you think so? It's a completely standard usage. For example, we can ask MathWorld:
> In logic, a term is a variable ['a', 'f'], constant ['1', '"hello"'], or the result of acting on variables and constants by function symbols ['1+2', 'f(a)'].
In particular, note that by this wording, if you're looking at '1+2', the "term" is not the string '"1+2"' but the result of adding '1' to '2', which is '3'.
You can talk about 'terms' in the context of how a compiler views source code. Or you can talk about 'terms' in the context of how type theory applies to some computation. They'll be called 'terms' either way; you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
Your quote points out that a term can be a variable. A variable represents a value, but it is not a value itself. The same goes for compound expressions. There are distinctions between variables, values, and expressions, and these distinctions are significant. You may have a sloppy head canon that blurs all these concepts together, but that’s not how they’re treated formally.
Terms are a syntactic concept while Values are a semantic runtime concept. The key to understanding is that Values are Terms which have been reduced (i.e. evaluated) to normal form and hence cannot be reduced further. The nuance lies in the fact that while both unreduced Terms and reduced Values can have semantic meanings, only at the Value stage is it canonical and fully computed.
In fact the "Calculus of Constructions" (CoC) derived from Typed Lambda Calculus unifies everything into a Term like so;
Term ::= variable | lambda abstraction | lambda application | dependant product | sorts (type of types)
But "term" is not a term that is restricted to computation. In normal mathematical usage, all values are always 'fully computed'. You may not personally know what they are, but that doesn't matter. These are just different names that we give to a single object.
True. But even in Mathematical Logic, a Term is a syntactical construct. You need to apply a "interpretation function" (mapping to a specific domain) to get a Value.
In Computation this is just made explicit and clear using a "eval function".
> you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
I used the compiler to illustrate the issue to people who clearly aren’t familiar with type theory. You imply that you are, but in that case, how do you justify the nonsense quoted above?
Why do you think so? It's a completely standard usage. For example, we can ask MathWorld:
> In logic, a term is a variable ['a', 'f'], constant ['1', '"hello"'], or the result of acting on variables and constants by function symbols ['1+2', 'f(a)'].
(I've added the bracketed material, which provides examples of the senses that MathWorld gives. https://mathworld.wolfram.com/Term.html )
In particular, note that by this wording, if you're looking at '1+2', the "term" is not the string '"1+2"' but the result of adding '1' to '2', which is '3'.
You can talk about 'terms' in the context of how a compiler views source code. Or you can talk about 'terms' in the context of how type theory applies to some computation. They'll be called 'terms' either way; you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.