Terms are the logical syntax. All logical statements are expressed as terms, and new term syntax is introduced with the declare directive. All operations in the system are defined on terms: all formal programs are interpreted as terms, and all logical statements in the system are defined with terms.
Terms have a single uniform syntax, defined by the following syntax:
term ::= operator { bterms } bterm ::= term | vars . term operator ::= opname [ params ] opname ::= literal | literal . opname param ::= number :n | string :s | string :t | string :v | level :l | meta-param meta-param ::= @var :n | @var:s | @var:t | @var :v | @var :l level ::= number | literal | level number | level ' | level "|" level
A simple literal is any sequence of alphabetic and numeric characters beginning with a letter. Additional literals are defined as any sequence characters from the ASCII character set enclosed in double quotes. A string is any sequence of characters enclosed in double-quotes, and a number is any sequence of digits. A var is a simple literal. The bterms and params lists use the semicolon (;) as a separator character, and the vars list uses a comma (,) as a separator character.
The operator represents the name of a term, which includes constant values defined by the parameters. The opname is name, the params are the constant values, and the bterms are the (possibly bound) subterms. If either of the bterms and params list are empty in a term, the brackets may be omitted.
Variables are a built-in term with the opname variable. There are two types of variables. First-order variables are defined with the syntax variable["v":v] (which represents the variable v). Second-order variables represent terms with substitutions (second order variables are used to define computational rewrites and inference rules). The syntax of second-order variables represents substituions with subterms. For example, the term variable["v":v]{variable["v1":v]; variable["v2":v]} is a second-order variable with two variables v1 and v2 as subterms.
The parser includes a simplifying syntax for variables: if a simple literal is prefixed with an apostrophe ('), the literal is interpreted as a variable. For example, the variable v is also represented with the syntax 'v, which is expanded by the parser into the full form variable["v":v]. Second order variables include their subterms in square brackets, so 'v['v1; 'v2] is the short form for the second-order variable in the last paragraph.
Term syntax is added to a module with the declare directive. The meaning of the term is not defined at the time of declaration; the meaning is defined with rewrites and inference rules. Terms can represent constants, like the following constants defined in Itt_int for numbers and Itt_atom for strings.
declare natural_number[@i:n] declare token[@s:t]
The declarations use meta-syntax for the parameters: the natural number includes a number parameter, and the token contains a token parameter. Once the meta-syntax has been defined, terms can be included in ML programs as quotations:
let one = << natural_number[1:n] >> let hello = << token["hello":t] >>
There is also a simplifying syntax for numbers: the parser expands numbers to the natural_number form when a term is expected.
Level-expressions are included in the parameter syntax to define type universes. For example, in the Itt_equal module, type universes are declared as:
declare univ[@i:l]
and specific instances of type universes are the base universe univ[1:l], an arbitrary universe with index i univ[i:l], and relative universes like univ[i':l] (which is the type universe containing univ[i:l]) or univ[(i | 3) : l], which is the smallest type universe containing both univ[3:l] and univ[i:l]. Level expressions can contain multiple indices: the universe univ[(i | j'):l] is the minimum type universe containing both univ[i:l] and univ[j':l].
Expressions are also defined with the term syntax. For example, the Itt_int module declares terms to represent arithmetic, including the following:
declare add{'x; 'y}
declare sub{'x; 'y}
For these terms, the opname describes the arithmetic operator, and the subterms represent numbers. The logical syntax is untyped, the following terms are valid syntax, although the second term has no meaning defined in the Itt_logic module.
let two = << add{1; 1} >>
let error = << sub{3; token["hello":s]} >>
Expressions may also include binding. The Itt_rfun module defines syntax for function abstraction and application.
declare lambda{x. 'b['x]}
declare apply{'f; 'a}
Binding variables are simple literals (so they are not quoted). The meta-syntax for lambda includes a second order variable, indictaing that the variable 'x is bound in the body 'b['x] of the function. The following function is an example of valid syntax in the Itt_rfun module:
let four = << apply{lambda{x. add{'x; 'x}}; 2} >>.
This just syntax at this point: term evaluation has not yet been defined.
Types are also declared as terms. The syntax does not differentiate between types and programs; the meaning of terms is defined by computational rewriting and inference rules. The following are some of the types defined in the Itt_logic module:
declare true
declare false
declare and{'A; 'B}
declare all{'A; x. 'B['x]}
The uniform syntax is verbose: each term contains an operator, and brackets for subterms. The verbosity can obscure the menaing implied by term expressions. The page on display forms discusses the pretty-printing mechanism for displaying terms. The parser also provides a simplified syntax for commonly occurring terms. The following tables list the simplied syntax in the left column, and the right column gives term in the uniform syntax. The simplified form is just an abbreviation; the term must still be declared. For example, the use of the term true or false requires that the term for or be declared,as in the following sequence:
declare true
declare false
declare or{'A; 'B}
let t = << true or false >>
t1 and t2 and{t1; t2} t1 & t2 and{t1; t2} t1 /\ t2 and{t1; t2} t1 or t2 or{t1; t2} t1 \/ t2 or{t1; t2} t1 => t2 implies{t1; t2} all x: t1. t2 all{t1; x. t2} exst x: t1. t2 exists{t1; x. t2}
t1 + t2 union{t1; t2} t1 * t2 prod{t1; t2} t1 -> t2 fun{t1; t2} x:t1 * t2 prod{t1; x. t2} x:t1 -> t2 fun{t1; x. t2} x, y: t1 // t2 quot{t1; x, y. t2} t1 = t2 in t3 equal{t3; t1; t2} t1 != t2 in t3 nequal{t3; t2; t1}
t1 +@ t2 add{t1; t2} t1 -@ t2 sub{t1; t2} t1 *@ t2 mul{t1; t2} t1 div t2 div{t1; t2} t1 mod t2 mod{t1; t2} t1 < t2 lt{t1; t2} t1 <= t2 le{t1; t2} t1 >= t2 ge{t1; t2} t1 > t2 gt{t1; t2}