Lab for Automated Reasoning and Analysis LARA

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