1\chapter{Syntax} 2{ 3 \newcommand{\term} {\mbox{\it term}} 4 \newcommand{\IMP} {\mbox{\tt ==>}} 5 \newcommand{\ALL} {\mbox{\tt !}} 6 \newcommand{\EXISTS} {\mbox{\tt ?}} 7 \newcommand{\CHOOSE} {\mbox{\tt @}} 8 \newcommand{\EXISTSONE} {\mbox{\tt ?!}} 9 \newcommand{\LET} {\mbox{\tt let}} 10 \newcommand{\und} {\mbox{\tt and}} 11 \newcommand{\IN} {\mbox{\tt in}} 12 \newcommand{\CONS} {\mbox{\tt CONS}} 13 \newcommand{\INSERT} {\mbox{\tt INSERT}} 14 \newcommand{\SUC} {\mbox{\tt SUC}} 15 \newcommand{\vstr} {\mbox{\it vstr}} 16 \newcommand{\numeral} {\mbox{\it numeral}} 17 \newcommand{\charseq} {\mbox{\it charseq}} 18 19The HOL logic is a classical higher-order predicate calculus. Its 20syntax enjoys two main differences from the syntax of standard first 21order logic.\footnote{We assume the reader is familiar with first 22 order logic.} First, there is no distinction in HOL between terms 23and formulas: HOL has only terms. Second, each term has a type: types 24are used in order to build well-formed terms. There are two ways to 25construct types and terms in HOL: by use of a parser, or by use of the 26programmer's interface. In this chapter, we will focus on the concrete 27syntax accepted by the parsers. 28 29 30\section{Types} 31 32A HOL type can be a variable, a constant, or a compound type, which is 33a constant of arity $n$ applied to a list of $n$ types. 34\[ 35\begin{array}{rclr} 36 \type & ::= & \mbox{\bf '}\ident & \mbox{(type variable)} \\ 37 & | & \verb+bool+ & \mbox{(type of truth values)} \\ 38 & | & \verb+ind+ & \mbox{(type of individuals)} \\ 39 & | & \type\ \verb+->+\ \type & \mbox{(function arrow)} \\ 40 & | & \type\ \ident\ \type\ & \mbox{(binary compound type)}\\ 41 & | & \ident & \mbox{(nullary type constant)} \\ 42 & | & \type\; \ident & \mbox{(unary compound type)} \\ 43 & | & (\type_1,\ldots,\type_n) \ident & \mbox{(compound type)} 44\end{array} 45\] 46Type constants are also known as type operators. They must be 47alphanumeric. Type variables are alphanumerics written with a leading 48prime ('). In \HOL{}, the type constants {\tt bool}, {\tt fun}, and 49{\tt ind} are primitive. The introduction of new type constants is 50described in Section~\ref{type-defs}. {\tt bool} is the two element type 51of truth values. The binary operator {\tt fun} is used to denote 52function types; it can be written with an infix arrow. The nullary 53type constant {\tt ind} denotes an infinite set of individuals; it is 54used for a few highly technical developments in the system and can be 55ignored by beginners. Thus 56\begin{verbatim} 57 'a -> 'b 58 (bool -> 'a) -> ind 59\end{verbatim} 60are both well-formed types. The function arrow is ``right associative'', 61which means that ambiguous uses of the arrow in types are resolved by 62adding parentheses in a right-to-left sweep: thus the type expression 63\begin{verbatim} 64 ind -> ind -> ind -> ind 65\end{verbatim} 66is identical to 67\begin{verbatim} 68 ind -> (ind -> (ind -> ind)). 69\end{verbatim} 70The product (\verb+#+) and sum (\verb!+!) are other infix type 71operators, also right associative; however, they are not loaded by 72default in \HOL{}. How to load in useful logical context is described 73in Section~\ref{theoryfns}. 74 75\section{Terms} 76 77Ultimately, a HOL term can only be a variable, a constant, an 78application, or a lambda term. 79\[ 80\begin{array}{rclr} 81 \term & ::= & \ident & \mbox{(variable or constant)} \\ 82 & | & \term\ \term & \mbox{(combination)} \\ 83 & | & \bs\ident.\ \term & 84 \mbox{(lambda abstraction)} 85\end{array} 86\] 87In the system, the usual logical operators have already been defined, 88including truth (\verb+T+), falsity (\verb+F+), negation (\verb+~+), 89equality (\verb+=+), conjunction (\verb+/\+), disjunction (\verb+\/+), 90implication (\verb+==>+), universal (\verb+!+) and existential 91(\verb+?+) quantification, and an indefinite description operator 92(\verb+@+). As well, the basis includes conditional, lambda, and `let' 93expressions. Thus the set of terms available is, in general, an 94extension of the following grammar: 95\[ 96\begin{array}{rclr} 97 \mbox{\it term} & ::= & \term : \type & \mbox{(type constraint)} \\ 98 & | & \term\ \term & \mbox{(application)} \\ 99 & | & \verb+~+ \term & \mbox{(negation)} \\ 100 & | & \term\ =\ \term & \mbox{(equality)} \\ 101 & | & \term\ \IMP\ \term & \mbox{(implication)} \\ 102 & | & \term\ \verb+\/+\ \term & \mbox{(disjunction)} \\ 103 & | & \term\ \verb+/\+\ \term & \mbox{(conjunction)} \\ 104 & | & \texttt{if}\ \term\ \texttt{then}\ \term\ \texttt{else}\ \term & 105 \mbox{(conditional)} \\ 106 & | & \bs\ident_1\ldots\ident_n.\ \term & \mbox{(lambda abstraction)} \\ 107 & | & \ALL \ident_1\ldots\ident_n.\ \term & \mbox{(forall)} \\ 108 & | & \EXISTS \ident_1\ldots\ident_n.\ \term & \mbox{(exists)} \\ 109 & | & \CHOOSE \ident_1\ldots\ident_n.\ \term & \mbox{(choose)} \\ 110 & | & \EXISTSONE \ident_1\ldots\ident_n.\ \term &\mbox{(exists-unique)} \\ 111 & | & \LET\; \ident = \term & \\ 112 & & [\und\ \ident = \term]^{*}\ \IN\ \term & \mbox{(let expression)} \\ 113 & | & \verb+T+ & \mbox{(truth)} \\ 114 & | & \verb+F+ & \mbox{(falsity)} \\ 115 & | & \ident & \mbox{(constant or variable)} \\ 116 & | & \verb+(+ \term \verb+)+ & \mbox{(parenthesized term)} 117\end{array} 118\] 119 120Some examples may be found in Table \ref{syntaxExamples}. Term 121application can be iterated. Application is left associative so that 122$\term\ \term\ \term \ldots \term$ is equivalent in the eyes of the 123parser to $(\ldots((\term\ \term)\ \term) \ldots)\ \term$. 124 125The lexical structure for term identifiers is much like that for 126ML: identifiers can be alphanumeric or symbolic. Variables must be 127alphanumeric. A symbolic identifier is any concatenation of the characters 128in the following list: 129\begin{verbatim} 130 #?+*/\=<>&%@!,:;_|~- 131\end{verbatim} 132with the exception of the keywords \verb+\+, \verb+;+, \verb+=>+, 133\verb+|+, and \verb+:+ (colon). Any alphanumeric can be a constant except the 134keywords \verb+let+, \verb+in+, \verb+and+, and \verb+of+. 135 136 \begin{table}[h] 137\begin{center} 138 \begin{tabular}{|r|l|} \hline 139 \verb+x = T+ & {\it x is equal to true.} \\ 140 \verb+!x. Person x ==> Mortal x+ & {\it All persons are mortal.} \\ 141 \verb+!x y z. (x ==> y) /\ (y ==> z) ==> x ==> z+ & {\it Implication is 142 transitive.} \\ 143 \verb+!x. P x ==> Q x+ & {\it P is a subset of Q} \\ 144 \verb+S = \f g x. f x (g x)+ & {\it Definition of a famous combinator.} \\ \hline 145 \end{tabular} 146 \caption{Concrete Syntax Examples}\label{syntaxExamples} 147\end{center} 148 \end{table} 149 150 151%%% Local Variables: 152%%% mode: latex 153%%% TeX-master: "description" 154%%% End: 155