logoalt Hacker News

thaumasiotes • today at 12:22 AM • 0 replies • view on HN

> This is not correct.

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.