Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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