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