QQREADERBFDE93A8C847F704

好不容易從校內(nèi)某個(gè)ftp上下載到《2012》，木有字幕……強(qiáng)迫自己看下去，考一考自己的聽力。發(fā)現(xiàn)除了罵人的語句，其他基本上一知半解，尤其是人物在討論文學(xué)／哲學(xué)／書籍等等文化相關(guān)的話題時(shí)。看來光看美劇，不看書籍了解一下西方文化還是不行啊……

 只好乖乖去找字幕。Google和百度的第一頁都是垃圾網(wǎng)站，現(xiàn)在的SEO越來越淫蕩了……
 好不容易下了個(gè)字幕。字幕質(zhì)量不錯(cuò)，時(shí)間間隔還可以接受。不過有一個(gè)缺陷，他是單獨(dú)一個(gè)字幕，而我的DVD版《2012》是分成兩個(gè)鏡像的——也就是第二部分無法使用這個(gè)字幕了。Orz

 我用的是ＱＱ影音，試了試調(diào)整字幕的延遲，發(fā)現(xiàn)那個(gè)調(diào)整對話框超搞——有一個(gè)輸入框，但是里面的數(shù)字不是延遲／提前的時(shí)間，而是基數(shù)，每按一次左／右方向鍵就增加這個(gè)數(shù)量的時(shí)間，而這個(gè)倍數(shù)卻是設(shè)定之后就看不到的。 最終使得我下決心動手山寨一個(gè)時(shí)間軸修改器，是因?yàn)镼Q影音沒有為我保存字幕的延遲設(shè)定。

跑題太遠(yuǎn)了。打開字幕文件，是純文本，Nice，省了Google的時(shí)間了。略過文件頭，有價(jià)值的地方是一行行這樣的東東：

Dialogue: 0,1:01:56.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:58.64,1:02:00.24,en,,0000,0000,0000,,We're fine!
Dialogue: 0,1:02:04.16,1:02:07.92,en,,0000,0000,0000,,Now that you have your\nmap, where we go?
Dialogue: 0,1:02:18.00,1:02:21.16,en,,0000,0000,0000,,We need a larger aircraft.
……

其中各個(gè)段由逗號隔開，各段的意義文件里也有寫：

Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text

一目了然啦。OK，其他不管，關(guān)注Start、End即可。Start和End也不用多猜，用分號隔開的時(shí)分秒是也。接下來的工作就輕松了，直接貼代碼吧。。。

 上面的代碼是把所有字幕的開始結(jié)束時(shí)間減去第一個(gè)字幕的開始時(shí)間，也就是把時(shí)間軸提前到0啦。把原來那個(gè)文件的文件頭拷過來，第二部的字幕也拷過來，一坨新鮮熱辣的字幕就出來咯。用硬編碼的c++做這個(gè)還真是秒殺啊~。有同學(xué)問了，第二部開始到人物說話有十幾秒延遲啊，如果我不想提前到0，而是提前到例如說12秒，怎么辦捏？有個(gè)比較hack的辦法，在第一條字幕之前增加一個(gè)無用字幕，把他的時(shí)間設(shè)置得前一點(diǎn)，再在生成的字幕去掉它，嘿嘿，嘿嘿

Dialogue: 0,1:01:44.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:56.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:58.64,1:02:00.24,en,,0000,0000,0000,,We're fine!
……

前幾日google 發(fā)布了一個(gè)語言Go，那時(shí)還在宿舍修養(yǎng)中，大概瀏覽一下就丟在一邊了。
昨日下班之后，閑得蛋痛，隊(duì)試一試Go。想不到官方網(wǎng)站竟然被墻了，不由得感嘆GFW的速度效率無比偉大強(qiáng)悍……
今晚手賤，再次打開http://golang.org，不想又可以訪問了。GFW還真是充滿神秘感啊。
看了一看，估計(jì)一個(gè)晚上是看不完的了，頁面基本上是純HTML，整個(gè)網(wǎng)站下載來備著吧，說不定什么時(shí)候又上不了。
我印象中wget是可以整站下載的，搜一搜，第一篇就是……

參考自http://www.ycrc.com.cn/qinghua/18/text/chapter4/section1/1.htm

標(biāo)準(zhǔn)式的化簡步驟
　　如果一個(gè)合適公式的所有量詞均非否定的出現(xiàn)在公式的前部，而且所有的量詞的
　　約束范圍均是整個(gè)公式，則稱這樣的合適公式為前束范式。任何一個(gè)合適公式，
　　都可以等價(jià)地轉(zhuǎn)化為一個(gè)前束范式。消去前束范式中所有的存在量詞后得到的
　　合適公式，稱為S范式，這一過程稱作skolem化。S范式與它的原式不一定等價(jià)，
　　但在不可滿足性方面，二者是等價(jià)的。也就是說，如果原式是不可滿足的，
　　則其對應(yīng)的S范式也一定是不可滿足的。反之亦成立。

（1）消蘊(yùn)涵符

（2）移動否定符
如果公式中的否定符"～"不只是作用于原子公式，則要利用摩根定律對公式進(jìn)行變換，
使得否定符只作用于原子公式。

如果否定作用于量詞的話，可以用量詞轉(zhuǎn)換律將量詞提到否定的作用域之外。

（3）變量換名

（4）量詞左移
將所有的量詞移到公式的左邊，但不改變原來各量詞的排列順序。
這也是為什么在第三步要進(jìn)行變量改名的原因，否則就不能進(jìn)行這種移動。

（5）消去存在量詞（skolem化）
按照這樣的原則將公式中的存在量詞消去：設(shè)E是前束范式中的一個(gè)存在量詞，
如果在它的前面沒有出現(xiàn)全稱量詞，則所約束的變量x，全部用一個(gè)新的常量
（未在公式中出現(xiàn)過）代替；如果E前面有全稱量詞，則所約束的變量x，
全部用一個(gè)新的（未在公式出現(xiàn)過的）函數(shù)（稱為skolem函數(shù)）代替，該函數(shù)的
變量是哪些在前面的全稱量詞所約束的變量。然后將存在量詞E消去。

（6）化為合取范式
利用結(jié)合律、分配律等，可以把S范式的母式轉(zhuǎn)化為合取范式。
A(x)∨(B(x)∧C(x)) ≡ (A(x)∨B(x))∧(A(x)∨C(x))

（7）隱去全稱量詞
經(jīng)過前6步變換以后，所有的變量都是受全稱量詞約束，所以可以將全稱量詞隱去，
默認(rèn)所有的變量是受全稱量詞約束的。

（8）表示為子句集
在隱去全稱量詞以后，用"，"號代替公式中的"∧"，并用"{"和"}"括起來，就得到了
原合適公式的子句集。

（9）變量換名
對子句集中的變量再次進(jìn)行換名替換，使得不同的子句中的變量使用不同的名字。
最簡單的方法是采用加下標(biāo)的方法。注意：在有些書中并不要求對子句集中的變量
進(jìn)行換名替換，如果是這樣的話，你必須很清楚，不同子句中的變量，即便是同名的，
也可以代表不同的變量。在后邊將要介紹的歸結(jié)法中，你會發(fā)現(xiàn)，如果不進(jìn)行換名，
很容易出現(xiàn)錯(cuò)誤。因此建議大家對變量進(jìn)行換名。由于每一個(gè)子句都對應(yīng)一個(gè)不同的
合取元，變量都由全稱量詞量化，因而實(shí)質(zhì)上兩個(gè)子句的變量之間不存在任何關(guān)系，
這里的變量換名不影響公式的真值。

---------------------------------------------------
Skolem化并不影響原合適公式的永假特性
---------------------------------------------------

最近用Java做一個(gè)regex等價(jià)判斷的東東，發(fā)現(xiàn)垃圾回收真的很強(qiáng)大，資源重用輕輕易易就實(shí)現(xiàn)了。C++加上右值引用和move構(gòu)造函數(shù)能夠提高資源重用，但是可以預(yù)見要一些idiom才能用好，又帶入了新的復(fù)雜性。
.
..
...
忍不住show一下，誰能夠?qū)崿F(xiàn)一個(gè)算法，在4秒內(nèi)給出能夠區(qū)分這兩個(gè)正則表達(dá)式的字符串：
(a|b)*b(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)
(a|b)*a(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)(a|b)
要知道識別倒數(shù)第n個(gè)字符是a的正則表達(dá)式，其DFA至少有2^n個(gè)狀態(tài)（見龍書第二版英文版P164）。

Java的泛型真是玩具，在注釋那里推導(dǎo)不出類型來了……

當(dāng)時(shí)愣是沒做出來，當(dāng)時(shí)也想到要用到素?cái)?shù)模的特殊性質(zhì)來做，但是數(shù)論忘得差不多了，在那里呆坐了20分鐘就是想不起來，唉唉……
這里看起來比較小，點(diǎn)擊一下放大來看吧
 

定義：項(xiàng)由下列規(guī)則形成
    (1) 個(gè)體常量和個(gè)體變量是項(xiàng)。
    (2) 若f是n元個(gè)體函數(shù)且 t1, t2, … tn 是項(xiàng)，則 f(t1, t2, … tn) 也是項(xiàng)。
    (3) 所有項(xiàng)都只由(1) (2) 生成。
定義：原子公式
若 P(x1, x2, … xn)是n元謂詞， t1, t2, … tn是項(xiàng)，則稱 P(t1, t2, … tn)為謂詞邏輯的原子公式。
定義：合式公式
1.原子公式是wff；
2.若A是wff，則(~A)也是；
3.若A、B是wff，且在A、B中同時(shí)出現(xiàn)的個(gè)體變量同為約束或同為自由，則A∧B、A∨B、A→B、A«B也是wff；
4.若A是wff，x在A中是自由的，則"x(A)、$x(A)也是wff；
5.只有有限次使用上述四條規(guī)則形成的才是wff。

可得其文法如下：

Formula -> Formula → Formula | Formula « Formula

               | Formula ∧ Formula | Formula ∨ Formula | ~Formula

               | "Variable(Formula) | $Variable(Formula)

               | Relation

Relation -> RelationSym(TermList)

RelationSym -> Constant

TermList -> Term(,Term)*

Term -> Function

          | Variable

          | Constant

Function -> FunctionSym(TermList)

FunctionSym -> [a-b]+

Variable -> [a-b]+

Constant -> [A-Z][a-zA-Z]*

http://dev.yesky.com/140/7555640.shtml