Remix.run Logo
▲ thaumasiotes 4 hours ago

> 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.

▲rramadass 13 minutes ago | parent [-]

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)

For reference see Brandl's work that i list here - https://news.ycombinator.com/item?id=50028902