Manual/Logic/syntax.tex

2 % Incorporates material from both of chapters 9 and 10 of the old
7 \chapter{Syntax and Semantics}\label{logic}
12 This chapter describes the syntax and set-theoretic semantics of the
14 Church's\index{Church, A.} simple theory of types \cite{Church} and
17 various mathematical notations and conventions.  The object language
24 \cite{sml}), \ML\ is the object language under consideration---and
27 The \HOL{} syntax contains syntactic categories of types and terms whose
28 elements are intended to denote respectively certain sets and elements
30 the description of the \HOL{} syntax, and in the next chapter the \HOL\
36 semantics of \HOL{} logic} and which is assumed to have the following
42 \item[Sub] If $X\in{\cal U}$ and $\emptyset\not=Y\subseteq X$, then
45 \item[Prod] If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\times
47 consisting of ordered pairs $(x,y)$ with $x\in X$ and $y\in Y$, with
59 non-empty by {\bf Inhab} and $\ch(X)\in X$ witnesses this.
65 from a set $X$ to a set $Y$ is a subset of $P(X\times Y)$; and it is a
66 non-empty set when $Y$ is non-empty. So {\bf Sub}, {\bf Prod} and {\bf
70 \item[Fun] If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\fun Y\in{\cal U}$.
84 Similarly, because of {\bf Sub} and {\bf Infty}, $\cal U$ contains
121 over type variables, \textsl{c} ranges over atomic types and \textsl{op} ranges over
155 theory, type variables are part of the meta-language and are used to
165 example, the standard atomic types \ty{bool} and \ty{ind} denote,
166 respectively, the distinguished two-element set $\two$ and the
171 $\sigma_n$ are the argument types and $op$ is a {\it type operator\/}
183 and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function
184 type with {\it domain\/} $\sigma_1$ and {\it codomain} $\sigma_2$. It
187 $\sigma_1\fun\sigma_2$ is written without the arrow and
205 and $()c$ will still be written as $c$.
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
224 {\sf TyNames} and {\sf TyVars} are assumed disjoint.
228 name of the constant and $n$ is its arity.  Thus $\Omega\subseteq{\sf
232 \ie\ whenever $(\nu, n_1)\in\Omega$ and
244 \item If $(\nu,n)\in\Omega$ and $\sigma_i\in{\sf Types}_{\Omega}$ for
248 \item If $\sigma_1\in{\sf Types}_{\Omega}$ and $\sigma_2\in{\sf
298 type (over some given type structure) and all the type variables
307 comes with a fixed total order and define the {\em
326 $i=1,\ldots,n$ and then $\den{\alpha\!s.\sigma}_{M}$ is the $i$\/th
350 and $\den{\sigma}_{M}$ can be identified with the element
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
363 Suppose that $\Omega$ contains a type constant $(\textsl{b},0)$ and that
388 and semantics of terms to be given below, where there is a dependency
389 both on type variables and on individual variables, the approach used
392 \subsection{Instances and substitution}
393 \label{instances-and-substitution}
395 If $\sigma$ and $\tau_1,\ldots,\tau_n$ are types over a type structure
411 $\beta_1,\ldots,\beta_p$ and that
414 uniquely determined by $\sigma$ and $\sigma'$.}
423 \noindent{\bf Lemma 2\ }{\it Given types-in-context $\beta\!s.\sigma$ and
427 type-in-context and its meaning in any model $M$ is related to that of
449 which $x$ ranges over variables and $c$ ranges over constants.
502 and $\sigma\in{\sf Types}_{\Omega}$. A {\em signature} over $\Omega$
510 \item {\bf Constants:} If $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ and
514 constants\/}\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of} and are written $\con{c}_{\sigma'}$.
516 \item {\bf Variables:}  If  $x\in{\sf  Names}$  and  $\sigma\in{\sf
526 Terms}_{\Sigma_{\Omega}}$ and $t'_{\sigma'}\in{\sf
532 \in{\sf Terms}_{\Sigma_{\Omega}}$  and $t_{\sigma_2}\in{\sf
539 Note that it is possible for constants and variables\index{variables, in HOL logic@variables, in \HOL{} logic!with same names} to have the
579 some comment. Since a variable is specified by both a name and a
593 \item $\alpha\!s$ contains any type variable that occurs in $x\!s$ and $t$.
602 not appear in $t$.  Note that the combination of the second and third
603 conditions implies that a variable cannot have both free and bound
611 it having no variable both free and bound. (The semantics will equate
638 with a set in $\cal U$ and then $M(c,\sigma)$ can be
656 the term and the set $Y\in{\cal U}$ is the interpretation of the type
660 term involving $n$ type variables and $m$ free variables: it is
668 variables and the type of the term (in a type context derived from the
677 \item $x\!s=x_{1},\ldots,x_{m}$ and each $x_{j}$ has type $\sigma_{j}$
683 and $\alpha\!s.\sigma_{j}$ are types-in-context, and hence give rise
684 to functions $\den{\alpha\!s.\tau}_{M}$ and
709 $j=1,\ldots,m$, so $\tau=\sigma_{j}$ and then
714 $(\con{c},\sigma)\in\Sigma_{\Omega}$ and $\sigma'$ is an instance of
715 $\sigma$.  Then by Lemma~1 of \ref{instances-and-substitution},
723 \ref{instances-and-substitution} (since $\tau$ is $\sigma'$).
728 $\tau'\fun\tau$ and $t_{2}$ is of type $\tau'$. Then
737 term $\lambda x.t_{2}$where $x$ is of type $\tau_{1}$ and $t_{2}$ of
738 type $\tau_{2}$. Thus $\tau=\tau_{1}\fun\tau_{2}$ and
746 variable $x$ does not occur in $x\!s$ and thus
759 distinct from the bound variables of $t_{\tau}$) and the $\sigma_{j}$ are
766 If $t_{\tau}$ is a closed term, then $m=0$ and for each $X\!s\in{\cal
773 where $\alpha\!s$ is the list of type variables occurring in $t_{\tau}$ and
775 $t_{\tau}$, then $n=0$ and $\den{t_{\tau}}$ can be identified with the
779 possible dependency of a term upon both type variables and ordinary
787 Since terms may involve both type variables and
790 variables and substitution of terms for variables.
797 and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
808 occur if the variables had the same name component and their types
836 Lemma~2 in \ref{instances-and-substitution} is needed to see that both
846 and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
864 $t$ as follows. For all $X\!s\in{\cal U}^{n}$ and all
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
899 instead of  \ty{bool} and $\iota$ instead of \ty{ind}.)
901 A model $M$ of $\Omega$ is {\em standard\/} if $M(\bool)$ and $M(\ind)$ are
902 respectively the distinguished sets $\two$ and $\inds$ in the universe
905 It will be assumed from now on that type structures and their models
925 the set denoted by $\sigma$, and
936                            0 & \mbox{if $b=1$ and $b'=0$} \\
973 It will be assumed from now on that signatures and their models are
981 (`false')\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of}, $\imp$ (`implies'), $\wedge$ (`and'), $\vee$
983 exists'), $=$ (`equals'), $\iota$ (`the'), and $\hilbert$ (`a'). This
986 necessary to work with the full set of logical constants, and the
989 book~\cite{Andrews} and the references it contains.
1017 supported by the \HOL{} system. The first two are infixes and the
1018 third is a binder (see \DESCRIPTION's sections on parsing and