Manual/Logic/syntax.tex

27 The \HOL{} syntax contains syntactic categories of types and terms whose
34 terms of a fixed set of sets $\cal U$, which will be called the {\em
388 and semantics of terms to be given below, where there is a dependency
440 \label{terms}
442 The terms of the \HOL{} logic are expressions that denote elements of the sets
444 is used to range over arbitrary terms, possibly decorated
447 There are four kinds of terms in the \HOL{} logic. These can be
476 Informally, a $\lambda$-term\index{lambda terms, in HOL logic@lambda terms, in \HOL{} logic}\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!abstract form of} $\lambda x.\ t$ denotes
486 traditionally used to range over terms of type $\sigma$. A
488 terms is:
498 type structure $\Omega$, the formal definition of terms is relative to
505 The set {\sf Terms}$_{\Sigma_{\Omega}}$ of terms over
554 A term is called polymorphic\index{polymorphic terms, in HOL logic@polymorphic terms, in \HOL{} logic} if it contains a type
571 \label{terms-in-context}
607 terms are said to be $\alpha$-equivalent if they differ only in the
608 names of their bound variables.} In the semantics of terms to be given
609 below we will restrict attention to such terms. Then the meaning of an
618 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of terms} context of the term $t$.
620 \subsection{Semantics of terms}
621 \label{semantics of terms}
624 structure $\Omega$ (see Section~\ref{terms}). A {\em model\/} $M$ of
641 The meaning of \HOL{} terms in such a model will now be described. The
642 semantics interprets closed terms involving no type variables as
768 $\den{t_{\tau}}(X\!s)()\in\den{\alpha\!s.\tau}(X\!s)$. So for closed terms
778 The semantics of terms appears somewhat complicated because of the
782 of several terms denoting logical constants is given.
787 Since terms may involve both type variables and
789 on terms which have to be considered---substitution of types for type
790 variables and substitution of terms for variables.
792 \subsubsection*{Substituting types for type variables in terms}
841 \subsubsection*{Substituting terms for variables in terms}
847 $\sigma_j$. If one has terms-in-context $\alpha\!s,\!x\!s'.t_{j}$ for
850 $\alpha\!s,\!x\!s'.t''$ by substituting the terms
882 Up to now the syntax of types and terms  has been  very general.   To
888 terms\index{type variables, in HOL logic@type variables, in \HOL{} logic!abstract form of}\index{terms, in HOL logic@terms, in \HOL{} logic!as logical formulas} of  type \ty{bool}.   In addition, various
993 Terms of type \ty{bool} are  called {\it formulas\/}\index{formulas as terms, in HOL logic@formulas as terms, in \HOL{} logic}.