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.


Blogger yen34/30/2008 12:23 am 說:


Blogger yen34/30/2008 12:27 am 說:

btw Greedy Theorem和Greedy Algorithm有關係嗎?

Blogger Josh Ko4/30/2008 12:44 am 說:

剛好近幾篇都是非普遍級而已 XD。

Greedy Theorem 導出的演算法傳統上有時候會被視為 dynamic programming algorithms。實際與傳統的 greedy algorithms 重疊的程度我還不太清楚。(看 scm 老師有沒有興趣講解一下 XD。)

Blogger yen34/30/2008 1:18 am 說:


Anonymous scm5/01/2008 8:10 am 說:

Comment 的篇幅好像只能大概說明一下耶.. :)

確實 greedy theorem 和 greedy algorithm 有關係。大致上我們先試著把問題描述成:「先用一個 fold 產生所有可能解,然後取最好的一個。」(yen3 還記得 fold 吧?)如果這個 fold 滿足某些性質,就可以把它轉成一個 greedy algorithm. 不過這只是某個類型的 greedy algorithm 而已。後來還有人做其他的推廣。

如果沒法滿足那麼強的條件,可能就變成 dynamic programming algorithm. 另外有個叫做 "thinning theorem" 的東西,跟這個比較有關。


<< 回到主頁