2,619
次編輯
「Program=Proof筆記-第1章」修訂間的差異
跳至導覽
跳至搜尋
→抽象化描述
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） （→抽象化描述） |
||
| 行 184： | 行 184： | ||
** F的不動點 <math>fix(F) = \bigcap \{x \in \mathcal{P}(\mathcal{U})|F(X) \subseteq X\}</math> | ** F的不動點 <math>fix(F) = \bigcap \{x \in \mathcal{P}(\mathcal{U})|F(X) \subseteq X\}</math> | ||
* 在隱微的Kleene fixpoint theorem 假設，可以顯現出 | * 在隱微的Kleene fixpoint theorem 假設，可以顯現出 | ||
<math>fix(F)=\bigcup_{n \in \ | <math>fix(F)=\bigcup_{n \in \N} F^n (\emptyset)</math> | ||
*假設我們有<code>type 'a leaf = Leaf 'a | Node (a, 'a leaf ,'a leaf)</code> | *假設我們有<code>type 'a leaf = Leaf 'a | Node (a, 'a leaf ,'a leaf)</code> | ||
*<math>F^0(\emptyset) = \emptyset</math> | *<math>F^0(\emptyset) = \emptyset</math> | ||
*<math>F^1(\emptyset) = \{Leaf(n)|n \in \ | *<math>F^1(\emptyset) = \{Leaf(n)|n \in \N\}</math>（高度<=1） | ||
*<math>F^2(\emptyset) = \{Leaf(n)|n \in \ | *<math>F^2(\emptyset) = \{Leaf(n)|n \in \N\} \cup \{Node(n,t_1, t_2)|n \in \mathbf N \and t_1, t_2 \in F^1(\emptyset)\}</math>（高度<=2） | ||
這個定理這樣推演下去，任何tree都是有固定的高度。 | 這個定理這樣推演下去，任何tree都是有固定的高度。 | ||