2,619
次編輯
「Program=Proof筆記-第1章」修訂間的差異
→1.3遞迴型別
Tankianting（討論 | 貢獻） （建立內容為「{{Nav|程式語言、邏輯學|Program=Proof筆記}} == Ch1 有型別的函數式程設 == ===1.1介紹=== <pre>(* 我是註解 *) print_endline "string" (*…」的新頁面） |
Tankianting（討論 | 貢獻） |
||
| 行 192： | 行 192： | ||
with | with | ||
| Not_found -> ...</pre> | | Not_found -> ...</pre> | ||
====抽象化描述==== | |||
因為排版 | |||
* U表示程式語言可操作的物件（項目）的集合 | |||
* P(U)表示U的冪集(powerset; U的子集合的集合) | |||
* F是recursive definition，F型別是P(U)->P(U) | |||
**tree 的型別是F的最小不動點，滿足 F(X) = X 。 | |||
**因為F是monotone單調的，所以X ⊆Y -> F(X) ⊆ F(Y) | |||
** F的不動點 <math>fix(F) = \bigcap \{x \in \mathcal{P}(\mathcal{U})|F(X) \subseteq X\}</math> | |||
* 在隱微的Kleene fixpoint theorem 假設，可以顯現出 | |||
<math>fix(F)=\bigcup_{n \in \mathbf N} F^n (\emptyset)</math> | |||
*假設我們有<code>type 'a leaf = Leaf 'a | Node (a, 'a leaf ,'a leaf)</code> | |||
*<math>F^0(\emptyset) = \emptyset</math> | |||
*<math>F^1(\emptyset) = \{Leaf(n)|n \in \mathbf N\}</math>（高度<=1） | |||
*<math>F^2(\emptyset) = \{Leaf(n)|n \in \mathbf 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的集合是F的不動點，一般來說有多個不動點。 | |||
推論：<math>\forall X, s.t. F(X)\subseteq X \rightarrow fix(F)\subseteq X</math><math></math> | |||
[[分類:資訊]] | [[分類:資訊]] | ||
[[分類:邏輯學]] | [[分類:邏輯學]] | ||