Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:standard-model_semantics_of_hol [2008/05/28 02:19] vkuncak |
sav08:standard-model_semantics_of_hol [2008/05/28 02:26] vkuncak |
||
|---|---|---|---|
| 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 ===== | ||
| Line 30: | Line 31: | ||
| 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{array}{l} | ||
| - | e(\phi)(x) = \phi(x) \\ | + | e(\varphi)(x) = \varphi(x) \\ |
| - | e(\phi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ | + | e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ |
| - | e(\phi)(F_1 F_2) = (e(\phi)(F_1))(e(\phi)(F_2)) \mbox{ (evaluate both arguments, perform function application) }\\ | + | e(\varphi)(F_1 F_2) = (e(\varphi)(F_1))(e(\varphi)(F_2)) \mbox{ (evaluate both arguments, perform function application) }\\ |
| - | e(\phi)(\lambda x_t. B) = f \mbox{ where } f(v) = e(\phi[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} | ||
| \] | \] | ||
| - | 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 ===== | ||