MetaPRL Terms

Introduction

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
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 list uses the semicolon (;) as a separator character, and the vars and params lists use a comma (,) as a separator character. :s in parameters and meta-parameters can be omitted.

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

Variables are a built-in term that are handled specially by the system. There are two types of variables. First-order variables represent the variable of the object theory. Second-order, or meta-level variables represent terms with substitutions (second order variables are used to define computational rewrites and inference rules). The syntax of second-order variables represents substitutions with 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 represented with the syntax 'v Second order variables include their subterms in square brackets, so 'v['v1; 'v2] is the second-order variable v with two arguments: v1 and v2.

Examples

Constants

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 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 = << number[1:n] >>
let hello = << token["hello":t] >>

There is also a simplifying syntax for numbers: the parser expands numbers to the 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

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_theory 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, indicating 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 true, false and and opnames have to be quoted here so that the parser would not confuse them with OCaml keywords.

Simplified Syntax

The uniform syntax is verbose: each term contains an operator, and brackets for subterms. The verbosity can obscure the meaning 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 operators for simplified syntax in the priority order (starting from the lowest order to the highest order). 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" >>

Logical connectives

 t1 => t2  implies{t1; t2}
 t1 <=> t2  iff{t1; t2}
 t1 or t2  or{t1; t2}
 t1 and t2
 t1 & t2
 and{t1; t2}
 all x:t1. t2
 exst x:t1. t2
 forany t1. t2
 thereis t1. t2
 all x. t
 exst x. t
 all x In t1. t2
 exst x In t1. t2 
 all{t1; x. t2}
 exists{t1; x. t2}
 all{t1; self. t2}
 exists{t1; self. t2}
 sall{x. t}
 sexists{x. t}
 dall{t1; x. t2}
 dexists{t1; x. t2}


 
_____
 For  
 CZF
 the-
ories

Relations

 t Type
 t1 = t2 in t
 t1
<> t2 in t
 t1
in t
 t1
= t2  
 t1 <> t2
 t1
subtype t2 
 t1
subset t2 
 t
in t1 subset t2 
 t1 ~ t2
 type{T}
 equal{t; t1; t2}
 nequal{t; t1; t2}
 equal{t; t1; t1} or member{t1; t} (*)
 equal{t1; t2}
 nequal{t1; t2}
 subtype{t1; t2)
 subset{t1; t2)
 member{t; t1; t2)
 sqeq{t1; t2}
 t1 <= t2
 t1 < t2
 t1 >= t2
 t1 > t2
 t1
=@ t2
 t1 <>@ t2
 t1
<=@ t2
 t1 <@ t2
 t1 >=@ t2
 t1 >@ t2
 le{t1; t2}
 lt{t1; t2}
 ge{t1; t2}
 gt{t1; t2}
 beq_int{t1; t2}
 bneq_int{t1; t2}
 le_bool{t1; t2}
 lt_bool{t1; t2}
 ge_bool{t1; t2}
 lt_bool{t1; t2}

(*) The "t1 in t" form is overloaded — if only one of the two operators is declared, then the declared operator is used, anf if both are declared, the equal form is used.

Mathematical operators

 t1 :: t2  cons{t1; t2}
 (t1, t2)  pair{t1; t2}

Type operators

 t1 -> t2
 x:t1 -> t2
 fun{t1; t2}
 fun{t1; x.t2}
 t1 * t2
 x:t1 * t2
 prod{t1; t2}
 prod{t1; x. t2}
 t1 + t2  union{t1; t2}
 quot x, y: t1 // t2
 t1 isect t2
 x: t1 isect t2
 Isect x: t1. t2
 t1 union t2
 Union x: t1. t2
 quot{t1; x, y. t2}
 bisect{t1; t2}
 bisect{t1; x. t2}
 isect{t1; x. t2}
 bunion{t1; t2}
 tunion{t1; x. t2}

Arithmetic operations

 t1 +@ t2
 t1 -@ t2
 add{t1; t2}
 sub{t1; t2}
 - t  minus{t
 t1 *@ t2
 t1 /@ t2
 t1 %@ t2
 t1 ^@ t2
 mul{t1; t2}
 div{t1; t2}
 rem{t1; t2}
 power{t1; t2}

Algebraic operations

 t1 op[t] t2  
 t1 ^op t2  
   where op is *,+,/,-,^,  
     or >,<,=,<>,<=,>=
 t^"op" t1 t2
 'self
^"op" t1 t2

 

Low priority operators

 if t1 then t2 else t3
 
let x = t1 in t2
 t2
where x = t1
 
open t1 in t2
 ifthenelse{t1; t2; t3}
 let{t1;x.t2}
 let{t1;x.t2}
 let{t1;self.t2}

Other operators

 t1  t2  apply{t1; t2}
 t1^x
 t1^x:=t2
 field["x":t]{t1}
 rxrd["x":t]{t2;t1

Parenthesis 

 {x : t1  |  t2}  set{t1; x.t2}
 {x : A; ... ; z : C}

 {x : A; ... ; z : C; P }
record[x:t]{A; self. . . .
 
record[z:t]{C}...}
{self:{x : A; ... ; z : C} | P}
 {x = a; ... ; z = c} rcrd[x:t]{a; . . . .
  rcrd[z:t]{c}...}