A term consists of: zero or more immediate subterms; for each subterm's place, a list of zero or more binding variables; and a nonempty list of non-term constituents, such as strings or numbers, which we call "operator parameters" or "op-parms" for reasons to be indicated below. For example, the term
Normally one can infer the relevant term structure from the definitions provided for operators, or when the notation is standard or familiar. When we want to show the form of a term explicitly for some reason, we employ a uniform notation we have adopted for that purpose. For example, the form of
all{}(A; x.0x)
which shows that the first subterm is
The general form for this way of showing term structure is:
<opid>{<parms>}(<bterms>)
where
nat natural_number{4:n} 4 token{abc:t} "abc" variable{x:v} x variable{a:v}(x) a(x) (second-order variable instance)variable{a:v}(x; y) a(x;y) (second-order variable instance)add(a; b) a+b lambda(x.b) x.b all(A; x.B) x:A. B let(a; x.b) let x = a in b sym(A; x,y.B) Sym x,y:A. B decide(e; x.a; y.b) InjCase(e; x. a; y. b) wellfounded{i:l}(A; x,y.B) WellFnd{i}(A;x,y.B)
Any combination of term components forms a term. Note that there are several kinds of op-parm values, indicated after the colon in the above forms: [nat]:n [token]:t [string]:s [var]:v [level]:l.
See
About: