Manual/Logic/syntax.tex

14 Church's\index{Church, A.} simple theory of types \cite{Church} and
27 The \HOL{} syntax contains syntactic categories of types and terms whose
110 \label{types}
112 The types\index{type constraint!in HOL logic@in \HOL{} logic} of the
116 range over arbitrary types.
118 There are four kinds of types in the \HOL{} logic. These can be described
121 over type variables, \textsl{c} ranges over atomic types and \textsl{op} ranges over
131 \put(.5,2.3){\makebox(0,0)[b]{\footnotesize atomic types}}
135 \put(.5,1.5){\makebox(0,0)[b]{\footnotesize function types}}
140 \put(2,3.3){\makebox(0,0)[b]{\footnotesize compound types}}
149 \noindent In more detail, the four kinds of types are as follows.
156 range over object language types.  Proofs containing type variables
163 \item {\bf Atomic types:}\index{atomic types, in HOL logic@atomic types, in \HOL{} logic} these denote fixed sets in the universe. Each
164 theory determines a particular collection of atomic types.  For
165 example, the standard atomic types \ty{bool} and \ty{ind} denote,
169 \item {\bf Compound types:}\index{compound types, in HOL logic@compound types, in \HOL{} logic!abstract form of} These have the
171 $\sigma_n$ are the argument types and $op$ is a {\it type operator\/}
182 \item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$
183 and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function
190 infix notation. It is singled out in the definition of \HOL{} types
194 Section~\ref{semantics of types}.)
199 It turns out to be convenient to identify atomic types with
200 compound types constructed with $0$-ary type operators.  For example,
204 atomic types will continue to be distinguished from compound types,
211 The term `type constant' is used to cover both atomic types and type
216 types (\ie\ $0$-ary type constants), and \textsl{op} is used to range
235 The set {\sf Types}$_{\Omega}$ of types over a structure ${\Omega}$
265 \subsection{Semantics of types}
266 \label{semantics of types}
281 polymorphic}\index{polymorphic types, in HOL logic@polymorphic types, in \HOL{} logic}\index{types, in HOL logic@types, in \HOL{} logic!polymorphic}. What is the meaning of a polymorphic type? One can
308 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of types} context of the type $\sigma$ to consist of
330 \item If $\sigma$ is a function type\index{function types, in HOL logic@function types, in \HOL{} logic!formal semantics of}
355 the semantics interprets monomorphic types over $\Omega$ as sets in
356 $\cal U$ and more generally, interprets polymorphic types\index{types, in HOL logic@types, in \HOL{} logic!polymorphic}\index{polymorphic types, in HOL logic@polymorphic types, in \HOL{} logic!formal semantics of} involving $n$ type variables as $n$-ary functions ${\cal
357 U}^{n}\longrightarrow{\cal U}$ on the universe.  Function types are
382 meanings to types in the presence of `environments' assigning sets in
383 $\cal U$ to all type variables. The use of types-in-contexts is almost
386 finite (ordered) set of type variables. At the level of types there is
395 If $\sigma$ and $\tau_1,\ldots,\tau_n$ are types over a type structure
403 The resulting type is called an {\it instance\/}\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} of $\sigma$. The
413 an instance of $\sigma$.  Then the types $\tau_1,\ldots,\tau_p$ are
418 We also need to know how the semantics of types behaves with respect
423 \noindent{\bf Lemma 2\ }{\it Given types-in-context $\beta\!s.\sigma$ and
443 denoted by types. The meta-variable $t$
482 The {\small BNF} grammar just given omits mention of types. In fact, each
497 In fact, just as the definition of types was relative to a particular
541 same name, if they have different types.
575 distinct variables whose types only contain type variables from the
582  so long as different types are attached to the
644 from the type of the term as in Section~\ref{semantics of types}). More
655 $\cal U$ are the interpretations of the types of the free variables in
667 U}^{n}\longrightarrow{\cal U}$ are determined by the types of the free
683 and $\alpha\!s.\sigma_{j}$ are types-in-context, and hence give rise
686 section~\ref{semantics of types}. The meaning of $\alpha\!s,\!x\!s.t$
717 for uniquely determined types $\tau_{1},\ldots,\tau_{p}$ (where
760 the types of those variables. (It is important to note that the list
789 on terms which have to be considered---substitution of types for type
792 \subsubsection*{Substituting types for type variables in terms}
799 types-in-context, then substituting\index{type substitution, in HOL logic@type substitution, in \HOL{} logic!formal semantics of} the types
805 In instantiating\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} the type variables $\alpha\!s$ with the types
808 occur if the variables had the same name component and their types
813 substituting the types $\tau\!s=\tau_{1},\ldots,\tau_{n}$ for the type
882 Up to now the syntax of types and terms  has been  very general.   To
897 atomic types \ty{bool} (of booleans or truth-values) and \ty{ind} (of