Terms occur on the object level; specifically as components of declarations, most notably as types and definitions of constants. They represent syntax trees with binding, e.g. first-order terms and formulas, types, lambda expressions etc.
Terms are defined recursively:
- Symbol references are terms (OMID)
- Variable references are terms (OMV)
- Applications of a term to a list of arguments (terms) are terms (OMA)
- Binding applications of a term - binding (optionally typed) variables - to a list of arguments are terms (OMBIND)
The precise abstract syntax is explained in more detail here.
In the MMT language, terms are given by using symbol/variable names and the notations of the symbols in the current context (previous declarations in the containing module). Binders extend the current context for their arguments by the variables they bind.
a + (b ⋅ c)would be an application (OMA) of a symbol
+(OMS) to a symbol
a(OMS) and (an application (OMA) of a symbol
⋅(OMS) to a symbol
b(OMS) and a symbol
c(OMS)). We can write this as:
+,⋅,a,b,chave to be in context, of course.
λx:t. x+awould be a binding application (OMBIND) binding a variable
tto (an application of …). We can write this as:
λextends the inner context of the argument by the variable
x, guaranteeing that
x+ais a well-formed term.