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:interpretation_quotient_under_congruence [2009/05/14 14:06]
vkuncak
sav08:interpretation_quotient_under_congruence [2015/04/21 17:30] (current)
Line 4: Line 4:
 ===== Example: quotient on pairs of natural numbers ===== ===== Example: quotient on pairs of natural numbers =====
  
-Let ${\cal N} = \{0,​1,​2,​\ldots,​ \}$.  Consider a structure with domain $N^2$, with functions +Let ${\cal N} = \{0,​1,​2,​\ldots,​ \}$.  Consider a structure with domain $N^2$, with functions ​(plus and minus): 
-\[+\begin{equation*}
     p((x_1,​y_1),​(x_2,​y_2)) = (x_1 + x_2, y_1 + y_2)     p((x_1,​y_1),​(x_2,​y_2)) = (x_1 + x_2, y_1 + y_2)
-\] +\end{equation*} 
-\[+\begin{equation*}
     m((x_1,​y_1),​(x_2,​y_2)) = (x_1 + y_2, y_1 + x_2)     m((x_1,​y_1),​(x_2,​y_2)) = (x_1 + y_2, y_1 + x_2)
-\]+\end{equation*}
 Relation $r$ defined by Relation $r$ defined by
-\[+\begin{equation*}
    r = \{((x_1,​y_1),​(x_2,​y_2)) \mid x_1 + y_2 = x_2 + y_1  \}    r = \{((x_1,​y_1),​(x_2,​y_2)) \mid x_1 + y_2 = x_2 + y_1  \}
-\] +\end{equation*} 
-is a congruence with respect to operations $p$ and $m$.  ​+is a congruence with respect to operations $p$ and $m$.  ​Indded, we can check that, for example, if $r((x_1,​y_1),​(x'​_1,​y'​_1))$ and 
 +$r((x_2,​y_2),​(x'​_2,​y'​_2))$ then 
 +\begin{equation*} 
 +     ​r(p((x_1,​y_1),​(x_2,​y_2)),​ p((x'​_1,​y'​_1),​(x'​_2,​y'​_2))) 
 +\end{equation*}
  
 Congruence is an equivalence relation. ​ What are equivalence classes for elements: Congruence is an equivalence relation. ​ What are equivalence classes for elements:
Line 28: Line 32:
  
 In the resulting structure $([N^2], I_Q)$ we define operations $p$ and $m$ such that the following holds: In the resulting structure $([N^2], I_Q)$ we define operations $p$ and $m$ such that the following holds:
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
    ​I_Q(p)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + x_2, y_1 + y_2)] \\    ​I_Q(p)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + x_2, y_1 + y_2)] \\
    ​I_Q(m)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + y_2, y_1 + x_2)]     ​I_Q(m)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + y_2, y_1 + x_2)] 
 \end{array} \end{array}
-\]+\end{equation*}
 This construction is an algebraic approach to construct from natural numbers one well-known structure. ​ Which one? ++| $({\cal Z}, + , -)$ where ${\cal Z}$ is the set of integers. ++ This construction is an algebraic approach to construct from natural numbers one well-known structure. ​ Which one? ++| $({\cal Z}, + , -)$ where ${\cal Z}$ is the set of integers. ++
  
Line 46: Line 50:
  
 For each element $x \in D$, define For each element $x \in D$, define
-\[+\begin{equation*}
     [x] = \{ y \mid (x,y) \in \alpha(eq) \}     [x] = \{ y \mid (x,y) \in \alpha(eq) \}
-\]+\end{equation*}
 Let Let
-\[+\begin{equation*}
     [D] = \{ [x] \mid x \in D \}     [D] = \{ [x] \mid x \in D \}
-\]+\end{equation*}
 The constructed model will be $I_Q = ([D],​\alpha_Q)$ where  The constructed model will be $I_Q = ([D],​\alpha_Q)$ where 
-\[+\begin{equation*}
     \alpha_Q(R) = \{ ([x_1],​\ldots,​[x_n]) \mid (x_1,​\ldots,​x_n) \in \alpha(R) \}     \alpha_Q(R) = \{ ([x_1],​\ldots,​[x_n]) \mid (x_1,​\ldots,​x_n) \in \alpha(R) \}
-\]+\end{equation*}
 In particular, when $R$ is $eq$ we have In particular, when $R$ is $eq$ we have
  
Line 65: Line 69:
  
 Functions are special case of relations: Functions are special case of relations:
-\[+\begin{equation*}
     \alpha_Q(f) = \{ ([x_1],​\ldots,​[x_n],​[x_{n+1}]) \mid (x_1,​\ldots,​x_n,​x_{n+1}) \in \alpha(f) \}     \alpha_Q(f) = \{ ([x_1],​\ldots,​[x_n],​[x_{n+1}]) \mid (x_1,​\ldots,​x_n,​x_{n+1}) \in \alpha(f) \}
-\]+\end{equation*}
  
 Interpretation of variables is analogous to interpretation of constants: Interpretation of variables is analogous to interpretation of constants:
-\[+\begin{equation*}
    ​\alpha_Q(x) = [\alpha(x)]    ​\alpha_Q(x) = [\alpha(x)]
-\]+\end{equation*}
  
 **Lemma 0:** For all $x_1,​\ldots,​x_n \in D$, **Lemma 0:** For all $x_1,​\ldots,​x_n \in D$,
-\[+\begin{equation*}
     ([x_1],​\ldots,​[x_n]) \in \alpha_Q(R) \mbox{ iff }  (x_1,​\ldots,​x_n) \in \alpha(R)     ([x_1],​\ldots,​[x_n]) \in \alpha_Q(R) \mbox{ iff }  (x_1,​\ldots,​x_n) \in \alpha(R)
-\]+\end{equation*}
  
 **Lemma 1:** For each function symbol $f$ with $ar(f)=n$, the relation $\alpha_Q(f)$ is a total function $[D]^n \to [D]$ and for all $x_1,​\ldots,​x_n \in D$, **Lemma 1:** For each function symbol $f$ with $ar(f)=n$, the relation $\alpha_Q(f)$ is a total function $[D]^n \to [D]$ and for all $x_1,​\ldots,​x_n \in D$,
-\[+\begin{equation*}
     \alpha_Q(f)([x_1],​\ldots,​[x_n]) = [\alpha(f)(x_1,​\ldots,​x_n)]     \alpha_Q(f)([x_1],​\ldots,​[x_n]) = [\alpha(f)(x_1,​\ldots,​x_n)]
-\]+\end{equation*}
  
 **Lemma 2:** For each term $t$ we have $e_T(t)(I_Q) = [e_T(t)(I)]$. **Lemma 2:** For each term $t$ we have $e_T(t)(I_Q) = [e_T(t)(I)]$.
 
sav08/interpretation_quotient_under_congruence.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice