- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

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 ===== |