Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:standard-model_semantics_of_hol [2008/05/28 02:19] vkuncak |
sav08:standard-model_semantics_of_hol [2008/05/28 02:24] vkuncak |
||
|---|---|---|---|
| Line 30: | Line 30: | ||
| 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} | ||
| \] | \] | ||