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:homework10 [2008/04/30 16:56]
vkuncak
sav08:homework10 [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Let ${\cal F}$ be the set of all first-order formulas (viewed as syntax trees) and let $r$ be the implication relation on formulas: Let ${\cal F}$ be the set of all first-order formulas (viewed as syntax trees) and let $r$ be the implication relation on formulas:
-\[+\begin{equation*}
    r = \{ (F_1,F_2) \mid \models F_1 \rightarrow F_2 \}    r = \{ (F_1,F_2) \mid \models F_1 \rightarrow F_2 \}
-\]+\end{equation*}
 Check whether $r$ is reflexive, antisymmetric,​ and transitive relation. Check whether $r$ is reflexive, antisymmetric,​ and transitive relation.
  
Line 12: Line 12:
  
 Let $(A,​\sqsubseteq)$ be a [[:partial order]] such that every set $S \subseteq A$ has the greatest lower bound. ​ Prove that then every set $S \subseteq A$ has the least upper bound. Let $(A,​\sqsubseteq)$ be a [[:partial order]] such that every set $S \subseteq A$ has the greatest lower bound. ​ Prove that then every set $S \subseteq A$ has the least upper bound.
 +
 ===== Problem 3 ===== ===== Problem 3 =====
  
Line 17: Line 18:
  
 Let function $f : A \to A$ be given by Let function $f : A \to A$ be given by
-\[+\begin{equation*}
     f(x) = \left\{\begin{array}{l}     f(x) = \left\{\begin{array}{l}
 \frac{1}{2} + \frac{1}{4}x,​ \mbox{ if } x \in [0,​\frac{2}{3}) \\ \frac{1}{2} + \frac{1}{4}x,​ \mbox{ if } x \in [0,​\frac{2}{3}) \\
Line 23: Line 24:
 \frac{3}{5} + \frac{1}{5}x,​ \mbox{ if } x \in [\frac{2}{3},​1] \frac{3}{5} + \frac{1}{5}x,​ \mbox{ if } x \in [\frac{2}{3},​1]
 \end{array}\right. \end{array}\right.
-\]+\end{equation*}
 (It may help you to try to draw $f$.) (It may help you to try to draw $f$.)
  
Line 36: Line 37:
 === Part c) === === Part c) ===
  
-Define $iter(x) = \sqcup \{ f^n(x) \mid n \in \{0,​1,​2,​\ldots \}\}$. ​ (This is in fact equal to $\lim_{n\to\infty} f^n(x)$.)+Define $iter(x) = \sqcup \{ f^n(x) \mid n \in \{0,​1,​2,​\ldots \}\}$. ​ (This is in fact equal to $\lim_{n\to\infty} f^n(x)$ ​when $f$ is a monotonic bounded function.)
  
 Compute $iter(0)$ (prove that the computed value is correct by definition of $iter$, that is, that the value is indeed $\sqcup$ of the set of values). ​ Is $iter(0)$ a fixpoint of $f$?  Is $iter(iter(0))$ a fixpoint of $f$? Is $f$ an $\omega$-continuous function? Compute $iter(0)$ (prove that the computed value is correct by definition of $iter$, that is, that the value is indeed $\sqcup$ of the set of values). ​ Is $iter(0)$ a fixpoint of $f$?  Is $iter(iter(0))$ a fixpoint of $f$? Is $f$ an $\omega$-continuous function?
 
sav08/homework10.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice