• English only

# Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:standard-model_semantics_of_hol [2008/05/28 02:24]
vkuncak
sav08:standard-model_semantics_of_hol [2015/04/21 17:30] (current)
Line 16: Line 16:

We require that $\alpha$ map constant $=_{t \Rightarrow t \Rightarrow o}$ into (curried) equality relation on the set $D_t$. ​ That is, it is a function that, given $x$, returns a characteristic function $sing_x$ of the singleton set $\{x\}$, given by We require that $\alpha$ map constant $=_{t \Rightarrow t \Rightarrow o}$ into (curried) equality relation on the set $D_t$. ​ That is, it is a function that, given $x$, returns a characteristic function $sing_x$ of the singleton set $\{x\}$, given by
-$\begin{array}{l}+\begin{equation*}\begin{array}{l} ​sing_x(y) = true, \mbox{ if } y=x \\ ​sing_x(y) = true, \mbox{ if } y=x \\ ​sing_x(y) = false, \mbox{ if } y \neq x \\ ​sing_x(y) = false, \mbox{ if } y \neq x \\ -\end{array}$+\end{array}\end{equation*}
On the other hand, we require $\alpha(\iota_{(i \Rightarrow o) \Rightarrow o})$ to be some choice function, which has the property that $\alpha(\iota)(sing_x) = x$.  Note that $\iota$ is defined for other functions as well, but we do not specify how it should behave on such functions. On the other hand, we require $\alpha(\iota_{(i \Rightarrow o) \Rightarrow o})$ to be some choice function, which has the property that $\alpha(\iota)(sing_x) = x$.  Note that $\iota$ is defined for other functions as well, but we do not specify how it should behave on such functions.

Line 25: Line 25:

Whereas $\alpha$ maps values of equalities and the choice function, an //​assignment//​ $\varphi$ maps values of variables, mapping each variable of type $t$ into element of $D_t$.  ​ Whereas $\alpha$ maps values of equalities and the choice function, an //​assignment//​ $\varphi$ maps values of variables, mapping each variable of type $t$ into element of $D_t$.  ​
+

===== General Model ===== ===== General Model =====

We call an interpretation $((D_t)_t, \alpha)$ a //general model// if there exists a meaning function $e$ mapping each term of type $t$ to element of $D_t$ such that for all interpretations $\varphi$ the following holds: We call an interpretation $((D_t)_t, \alpha)$ a //general model// if there exists a meaning function $e$ mapping each term of type $t$ to element of $D_t$ such that for all interpretations $\varphi$ the following holds:
-$\begin{array}{l}+\begin{equation*}\begin{array}{l} e(\varphi)(x) = \varphi(x) \\ e(\varphi)(x) = \varphi(x) \\ e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ Line 35: Line 36: e(\varphi)(\lambda x_t. B) = f \mbox{ where } f(v) = e(\varphi[x:​=v])(B) \mbox{ for all } v \in D_t e(\varphi)(\lambda x_t. B) = f \mbox{ where } f(v) = e(\varphi[x:​=v])(B) \mbox{ for all } v \in D_t \end{array} \end{array} -$ +\end{equation*}
-If such interpretation function $e$ exists, then it is unique. ​ The reason it may not exist is only if $D_t$ for some $t$ does not have sufficiently many elements ​to define all functions.  But for standard model this is certainly true, and the meaning ​of terms is the expected one.+If such interpretation function $e$ exists, then it is unique. ​ The reason it may not exist is only if $D_t$ for some $t$ does not have sufficiently many elements ​so that $e(\varphi)(F) \in D_t$.  But for standard model this is not a concern, and in such case the meaning is what we would expect, with lambda terms denoting total functions and quantification denoting quantification over all functions.

===== Standard Model ===== ===== Standard Model =====

sav08/standard-model_semantics_of_hol.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice