Half of the Hylomorphism Theorem
The Hylomorphism Theorem states that a hylomorphism is the least fixed point of a certain equation. Its proof is divided into two parts: one proving that a hylomorphism is a fixed point, and the other proving that a hylomorphism is a lower bound of all fixed points. The second part is what we need in the proof of the Greedy Theorem, and that was what I was working on (and finished) tonight. Since the proof consists of only "ordinary" arrows and composition, the entire process was quite a pleasure, even when one need to explicitly specify associativity of relation composition and various kinds of monotonicity. I haven't pushed it into the repository since the symbol for converse was changed (among others?) and I need to resolve some conflicts.
--
It is very likely that the Greedy Theorem will be proven soon.
Labels: 雜記
你以後改行用英文寫blog了嗎，如果是我得早早習慣
btw Greedy Theorem和Greedy Algorithm有關係嗎?
剛好近幾篇都是非普遍級而已 XD。
Greedy Theorem 導出的演算法傳統上有時候會被視為 dynamic programming algorithms。實際與傳統的 greedy algorithms 重疊的程度我還不太清楚。（看 scm 老師有沒有興趣講解一下 XD。）
喔喔，期待中~
Comment 的篇幅好像只能大概說明一下耶.. :)
確實 greedy theorem 和 greedy algorithm 有關係。大致上我們先試著把問題描述成：「先用一個 fold 產生所有可能解，然後取最好的一個。」(yen3 還記得 fold 吧？)如果這個 fold 滿足某些性質，就可以把它轉成一個 greedy algorithm. 不過這只是某個類型的 greedy algorithm 而已。後來還有人做其他的推廣。
如果沒法滿足那麼強的條件，可能就變成 dynamic programming algorithm. 另外有個叫做 "thinning theorem" 的東西，跟這個比較有關。
<< 回到主頁