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