Manual/Logic/syntax.tex

135 \put(.5,1.5){\makebox(0,0)[b]{\footnotesize function types}}
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
270 for each type constant $(\nu,n)$ an $n$-ary function
284 single set, but is rather a set-valued function, ${\cal
317 $\alpha\!s.\sigma$ over $\Omega$, define a function
327 projection function, which sends $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$
330 \item If $\sigma$ is a function type\index{function types, in HOL logic@function types, in \HOL{} logic!formal semantics of}
344 the function
358 interpreted by full function sets.
370 is the function sending $X\in{\cal U}$ to $(X\fun\two)\fun X\in{\cal U}$.
373 U}^{2}\longrightarrow{\cal U}$ is the function sending $(X,Y)\in{\cal
462 \put(.5,1.5){\makebox(0,0)[b]{\footnotesize function applications}}
463 \put(.5,0){\makebox(0,0)[b]{\footnotesize (function $t$, argument $t'$)}}
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
477 a function $v\mapsto t[v/x]$, where $t[v/x]$ denotes the result of
478 substituting $v$ for $x$ in $t$. An application\index{function application, in HOL logic@function application, in \HOL{} logic!abstract form of} $t\ t'$ denotes the result of applying the
479 function denoted by $t$ to the value denoted by $t'$. This will be
547 Function application\index{function application, in HOL logic@function application, in \HOL{} logic!associativity of} is assumed to associate
634 $M(\con{c},\sigma)$ is a (dependently typed) function
647 U}^{n}}Y(X\!s)$, where the function $Y:{\cal U}^{n}\longrightarrow{\cal
650 function which, when applied to any meanings chosen for the type
653 variables but no type variables, then it is interpreted as a function
657 of the term; thus the meaning of the term is a function which, when
726 Suppose $t$ is a function application\index{combinations, in HOL logic@combinations, in \HOL{} logic!formal semantics of} term $(t_{1}\
727 t_{2})$\index{function application, in HOL logic@function application, in \HOL{} logic!formal semantics of} where $t_{1}$ is of type
730 $\den{\alpha\!s.\tau'\fun\tau}(X\!s)$, is a function from the set
736 \item Suppose $t$ is the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!formal semantics of}
739 $\den{\alpha\!s.\tau}(X\!s)$ is the function set
742 this set which is the function sending
750 dependently typed function
926 $\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denotes a choice function
933 standard implication\index{implication, in HOL logic@implication, in \HOL{} logic!formal semantics of} function, sending $b,b'\in\two$ to
944 X\fun\two$ is the function assigning to each $X\in{\cal U}$ the
945 equality\index{equality, in HOL logic@equality, in \HOL{} logic!formal semantics of} test function, sending $x,x'\in X$ to
956 U}}.(X\fun\two)\fun X$ is the function assigning to each $X\in{\cal
957 U}$ the choice\index{choice operator, in HOL logic@choice operator, in \HOL{} logic!formal semantics of} function sending $f\in(X\fun\two)$ to
968 universe $\cal U$ given in Section~\ref{introduction}. The function