What have you found for these years?

2011-07-05

〈磔刑の聖女〉& probability monad

這兩天一直在放《Märchen》的第八首〈磔刑の聖女〉。
我很喜歡前半段的一些旋律。或是更精確地說,是 00:53 ~ 01:30
這一段吧,不知道是誰唱的。感覺很難形容,以後再慢慢想...
不限於這片的這一段,之前也有聽過不少會給我這種感覺的。

唉,然後每次聽這個就會想到金頂電池爆炸弄壞我的限定版盒子...
接著又會想到之前有幾張也想收普通版,因為覺得圖滿好看的,
而限定版比較醜。

然後昨天還前天,我才忽然想起來,之前買的 live DVD 好像還沒看完...
怎麼,好像找不到時間看?連我看到第幾片都忘記了 :/

* * *

確定的是昨天本來想打一下 GuildWars, 因為實在很累沒什麼力氣
弄別的。結果才剛準備開始打,上個廁所在想 Learn You a Haskell
for Great Good!
裡面的 Probability monad, 手癢忍不住就關掉
GuildWars 來寫一次看看。因為其實那時我也沒很想打 GuildWars...
目前要打的進度讓人有點提不起幹勁,因為很難打,都不能打 hard
mode, 不然失敗率太高了。

而 probability monad 我也想寫很久了。那乾脆就心血來潮一下吧!
尤其這幾天打 Estiah 又在想,如果我要第二抽到 Nightmare Blade,
那這樣到底放幾張可以讓勝率達到最高?與其用手算,還不如看看是否
能真的用 probability monad 幫我算出來。多實際。

結果寫是寫完了啦,成果在這 Prob.hs, 但是卻發覺要算第幾張抽到的
機率的話,光是這樣完全不夠。感覺這好像是需要「重複排列」的算法。
高中數學我完全忘光了。不過我現在還能從 P 推出 C, 可是 H 就沒有
那麼直覺了,洗澡的時候一時想不到,可能要用紙筆稍微推算一下。

但不管怎麼樣,單用 probability monad 都不足以算這些。我需要更好的
方式定義「總數」和「組合數」。可是光把 Prob.hs 寫完,就已經弄到
太晚了,我也沒什麼精神繼續寫下去。想到這裡,又想起之前用 Scala
寫的踩地雷 AI minei 也還沒寫完,我好不容易推算出所有的排列組合運算,
但只在腦海裡,來不及寫出來,也來不及寫成程式,過這麼久我看大概
忘光了吧。嘖。這要是寫出來,雖然肯定會跑很慢,但應該會很強...

然後如果把這 probability moand 寫得好用一點,說不定還能拿來輔助用。
至少至少,可以拿來算到底放幾張 Nightmare Blade 比較有勝算吧...。
雖然我用手算肯定比較快 :/

另外,排列組合和機率也幾乎可以說是我在學校裡學的數學,比較有興趣的...
或是說唯一完全沒忘光,而且自己還可以推算的。看什麼時候會想繼續做
下去吧。

* * *

在 Prob.hs 中也試了 QuickCheck 來驗證 probability monad 的 functor
laws 和 monad laws. 最讓人頭痛的是 monad 上的 composition 的
associativity, 用 QuickCheck 產生任意 function 看起來是沒什麼問題,
但是產生這麼多的 function 跑起來真的是慢到不能接受。而且不知道
為什麼,愈後面愈慢,我猜是 quickcheck 有用某種方式去調整產生的
東西,可能因為前面範圍還很大很容易產生,後面愈來愈難之類的,亂猜。
總之讓他跑完一次確定沒問題後,我就不想再跑第二次了,或是跑一半就
切掉。如果能限制他不要跑 100 次,而是 50 次的話倒是能接受。主要是
超過 50 之後才會開始變得慢到讓人難以忍受。

其實我這邊寫得很隨便,而且好像也沒查到什麼很明確的 functor laws
or monad laws, 所以就隨便選幾個我比較喜歡的寫... 反正全都要過就對了 :x
我不是很確定這些可不可以用證明的。每篇文章都說 functor/monad laws
要作者自己確認,但好像沒說過要怎麼確認才對。


胡言亂語,終。

2011-07-02

最近 (2)



今天躺在床上滾來滾去時,忽然想到,應該從另一個角度來欺騙的。
原本想的兩種都太沒有說服力了。而單純只是忽略,根本無法持久,
忽然間感覺還是會浮上然後就沮喪很久。但如果是這個欺騙角度的話,
說服力就很夠了,夠到甚至可以說並不算欺騙。雖然這樣想不免會
覺得也未免太沒有希望了吧。可是應該總比結果只在那邊滾來滾去
而一事無成要來得好..。

至少今天是想到這樣才從床上爬起來的。

一些想法關於 What Philosophy of Science Can Say for Software Engineers

What Philosophy of Science Can Say for Software Engineers

這篇滿長的,其實我沒很仔細看,有些想法但沒辦法講得很清楚,所以
大概就是隨意摘些文摘吧。邊吃晚餐時邊看的... 雖然這樣可能會消化不良。

Yang 說:

How do we know induction works? We’ve used in the past successfully.
But the act of generalizing this past success to the future is itself
induction, and thus the justification is circular.

這讓我想到之前還沒看完的 Alan Kay 的訪談。
A Conversation with Alan Kay

Kay 提到:

We looked at Java very closely in 1995 when we were starting on a
major set of implementations, just because it’s a lot of work to do a
viable language kernel. The thing we liked least about Java was the
way it was implemented. It had this old idea, which has never worked,
of having a set of paper specs, having to implement the VM (virtual
machine) to the paper specs, and then having benchmarks that try to
validate what you’ve just implemented—and that has never resulted
in a completely compatible system.

用自己來實作自己,稱作 bootstrap, 乍看之下需要多花很多功夫,又不會
有什麼好處。但事實上 Kay 說:

The technique that we had for Smalltalk was to write the VM in itself,
so there’s a Smalltalk simulator of the VM that was essentially the
only specification of the VM. You could debug and you could answer
any question about what the VM would do by submitting stuff to it,
and you made every change that you were going to make to the VM
by changing the simulator. After you had gotten everything debugged
the way you wanted, you pushed the button and it would generate,
without human hands touching it, a mathematically correct version of
C that would go on whatever platform you were trying to get onto.

Java 用 C 去實作的問題是,怎麼確保在不同平台上,所有的實作結果都是
相同的?一個語言可以有兩種方式去定義標準,一個是有個 specification,
然後所有實作要依照這個 spec 去做。怎麼解釋 spec, 誰做的是對的,就看人
解釋了。或是有個 reference implementation, 這個 implementation
怎麼說,那這個 language 的 semantic 就是怎麼樣。

前者我們仰賴人類的解釋,後者則仰賴實作這個語言的語言。以 Java 為例,
就是 C 了。(雖然我不確定 JVM 是不是 C 寫的)然後 C 又仰賴... C.
如果不是 C 呢?

而如果 Smalltalk 實作了 Smalltalk (Squeak), 那改了 Smalltalk VM 整個
Smalltalk 就變了。不管在哪裡的 Smalltalk 都變了。

理論上說來好像合理,但其實我也不是很確定這樣說到底對不對。畢竟我們
當初一定會有一個最早拿來 bootstrap 的 Smalltalk, 到底有沒有算仰賴他?
self-referential 往往會帶來令人困惑的結果..。Gödel's incompleteness
theorems 到現在也還是搞不太懂。

* * *

Yang 說:

Falsification improves over inductivism by embracing the theory-
dependence of observation. Falsificationists don’t care where you
get your theory from, as long as you then attempt to falsify it,
and also accept the fact that there is no way to determine if a
theory is actually true in light of evidence. This latter point is
worth emphasizing: whereas induction attempts to make a
non-deductive step from a few cases to a universal, falsification
can make a deductive step from a negative case to a negative
universal. To use a favorite example, it is logically true that if
there is a white raven, then not all ravens are black. Furthermore,
a theory is better if it is more falsifiable: it suggests a specific set
of tests.

我很喜歡這種說法。有點忘記是在哪裡看到了[0],有人說 test 是程式正確性的
upper bound, 而 proof 則是 lower bound. 解釋起來像是,test 告訴我們
在這些例子中,我們的程式運作是符合預期的。但其實我們真正要的程式的
意義(語意),並沒有那麼多。我們只是窮舉所有可能而已。雖然現實上
其實也沒辦法真的窮舉。另一方面,proof 則是假設這些程式絕對是正確的,
但其實我們要的很可能更多,包括那些沒辦法被證明的!例如 halting problem?

前一陣子,在 twitter 看到有人說這個說法是錯的,但他沒解釋。很想問
為什麼他覺得是錯的... 但也很擔心碰到 test 狂之類的。

很多年前,在 ptt CSSE 上看到「可證偽性」,那時不太明白是什麼意思。
這邊解釋得很清楚。一個愈好的理論,就應該是愈容易可被證明他是錯的。
最簡單的證明就是舉反例就好了。其實這比較像是 test...

也就是說,上述的 inductivism 像是 proof, 而 falsificationism 像是 test.

「可證偽性」應該也是拿來挑戰偽科學很好用的工具之一..。

[0] 我找到了: What To Know Before Debating Type Systems
難怪會說這個說法很有名,這篇本身應該是很有名沒錯..。


這篇應該細讀的,非常有趣。不過這種東西讀多了,就會覺得人類
其實是多麼地不理智,大多理智的思考都是違反直覺的? XD

Yang 說:

Suppose that our crashing program has two bugs (here we use “bug”
in the sense of “source code defect”). Is it true that the first bug
causes the crash? Well, if we removed that bug, the program would
continue to crash. Thus, under the counterfactual theory of causation,
the first bug doesn’t cause the crash. Neither does the second bug,
for that matter. We have a case of causal overdetermination.
(Lewis claims the true cause of the bug is the disjunction of the
two bugs. Perhaps not too surprising for a computer scientist, but
this sounds genuinely weird when applied to every-day life.)

So true. :)

All texts are licensed under CC Attribution 3.0