All posts by hevangel

反斗車王3

不經不覺《反斗車王》已經有十年歷史,第二集白痴Mater做主角令故事超爛,以為Pixar把這系列玩死了。想不到第三集找回初心,再以賽車場比喻人生,為這系列劃上一個完滿句號。戲中時間與現實一樣,十年過去主角McQueen從第一集的新晉小子,漸漸成熟為車壇老將,勝出四次Piston Cup大賽,比師傳Doc Hudson還要多一次。可惜長江後浪推前浪,面對新世代跑車的挑戰,不論是引擎馬力,車身風阻,最高時速等,上一代的車款在比賽中顯得力不從心。與McQueen同期的車手,大部份都退休了,讓出位置給跑得更快的新人。昔日的車神面臨中年危機,在退與不退之間要作出選擇。可是他對跑道亦仍留戀,不甘心就此退下來,希望再闖高峰,保持王者地位。

下文包含劇透,不過電影玩具的車身拉花,早己經完全劇透了,所以在此我透不透也沒多大關係。

第三集與第一集的格局很相似,開場第一場比賽主角落敗(還要炒車大難不死),中段是很王道的練功加尋找自我的旅程,最後結尾的那一場比賽反敗為勝。第一集的「壞人」是出矛招的綠色鬍鬚車,這集的「壞人」則是目中無人的新晉車手Storm,戲中沒有說他們二人是師徒關係,不過二人同樣喜歡撞人,可能有點淵源。McQueen的贊助商Rusteze被賽車迷億萬富豪收購了,他出手闊卓興建高科賽車技訓練中心,決心建立一隊最頂尖的車隊。黃色跑車Cruz原來是McQueen的訓練員,亦是這齣電影的女主角。不過觀眾不用擔心Sally的正印地位,她和McQueen只限於師徒關係。仍舊與第一集一樣,中段笑聲不絕,McQueen老人家不適應高科技訓練模式,轉移陣地沙灘到特訓,然後McQueen和Cruz誤打誤撞參加了Demolition Derby(即賽車MMA混戰),特別是McQueen智勝怪獸校巴那段,阿仔笑到起身拍手。

第一集故事的轉折點是McQueen發現Doc Hudson的真正身份,而這集的轉折點是Cruz講出她想當車手的夢想,身為女生不被接納當不成車手,只好退而求其次當訓練員。電影初段一直有舖排Cruz的賽車天份,從她輕輕鬆鬆在模疑器上跑出佳績,沙灘特訓剛學慬跑沙地便能追貼McQueen,在Demolition Derby大混戰中存活下來並奪得冠軍,加上預告中的劇透,這轉變完全不意外。第一集McQueen從Sally身上學懂慢下來的道理,這一集則從老前輩身上,學懂薪火相傳的道理。當年Doc當他的師傳,找到跑道的第二個意義,現今McQueen把當年從Doc身上學到的,回饋給Cruz。結尾那場賽車的高潮,並不是McQueen反敗為勝,而是他退下來成全Cruz,給她一個當賽車手的機會。至於Cruz使出Doc的「絕招」反擊Storm,大慨已是觀眾意料之內的套路。第三集與第一集一樣,雖然McQueen沒有贏得比賽,但他贏得比獎盃更加重要的東西。

《反斗車王》一向被批評為在眾多Pixar作品中缺乏深度,今次大結局(車王都退休了,應該不會再拍續集吧)竟然有驚喜。McQueen的中年危機小朋友肯定看不明白,但陪太子睇戲的家長相信會有所共嗚。戲中的道理拍得淺白,年輕時總有無窮無盡的夢想,認為自已能有一番作為。可是隨年紀增長,不能夠永遠拼死硬闖向前衝,轉而憑經驗智取補救力量上的不足,勉強應付一眾新人的挑戰。然而花無百日紅,沙場上不許見白頭,總有一天要退下來。高峰過後退下來,如何適應轉換跑道,大慨就是所謂的中年危機。退可以退得很蕭灑,像McQueen一樣提攜後輩,退而不休贏得尊敬。亦可以不情不願留戀高位,繼續當個老海鮮指手橫腳,阻住個地球轉。但時間永遠站在新世代那邊,最後在鬥爭敗陣被迫退下來,恐怕連身為前輩的尊嚴也輸掉。

Frame Arms Girls 骨裝機娘

《骨裝機娘》是一部不折不扣的玩具廣告,賣的是壽屋的Frame Arms Girls模型系列。本家的Frame Arms是機械人模型,主打通用骨架配各種武器。Frame Arms Girl則是保留武器,把機械人的骨架改為少女。其實機械人少女(統稱機娘)的商品不少,除了壽屋外,還有Konami的武裝神姬和笨大的AGP高達少女。高達少女以高達為背景定位清楚,其他沒有動畫的機娘,只有人設,面目蒙糊,我也分不清楚誰打誰。沒有原作故事支撐的玩具角色,感覺上面目很難投入,說服讓玩家購買很脫力,大慨因此壽屋才要拍動畫谷銷量。

這部動畫是低成本製作,機娘的CG戰鬥畫面完全不合格,動作生硬打鬥設計馬虎。不知裏就先亂打一輪,然後忽然一招大絕KO對手。不過戰鬥根本不是重點,這套作品主力玩日常搞笑,女主角和機娘們大開百合。每集是獨立短篇故事,除了女主角外,就只有另一個人類角色模型宅,她的作用是介紹砌模型的小知識。在一個廣告動畫中再置入廣告,到底是什麼玩法?不過廣告倒很成功,我記得那把鬼魂上身的壽屋神剪。

要賣玩具機娘自然越出越多,最後有八隻機娘寄居於女主角家。沒有主線就沒有包伏,單完劇情可以玩得很癲,什麼異想天開的點子也可以拍出來。雖然有點白痴無聊,但勝在好好笑,這套應該算是治癒系吧。機娘玩相撲,叉電君的觀音兵傻樣,機娘玩公仔屋佈置自已間房,把機械吸塵機變為座駕,外出幫主人購物大作戰,主角發夢機娘變成真人同學。最好笑那話是忍者機娘認為正宗著和服唔可以著底底,於是潛入剪了主人條底底,保衛底底大作戰。賣萌百合番一定有浸溫泉賣肉的指定動作,不過機娘不是模型嗎,為什麼她們可以除衫浸溫泉?

沒有期望就不會失望,每週輕輕鬆鬆看一集,沒有追看故事的壓力,甚至覺得隨時砍番也不可惜,不過就是一集接一集的看到結局。多得動畫化,Frame Arms Girls比本家Frame Arms更有人氣,有點本末倒置的感覺。不知道壽屋會不會添食,索性出本家Frame Arm的動畫,如果成事就太好了。

Formal Verification – Erik Seligman, Tom Schubert

這篇不是書評,這本書亦不是一般自學程式設計的電腦書,是一本涉及非常專門的知識,只有設計晶片才會用得上的技術課本。非行內人完全看不明白,這篇只是我學習formal verification(形式化驗證)的心得和筆記,所以我亦不期望有什麼讀者。

什麼是Formal Verification?首先要講什麼是dynamic verification,設計晶片不同寫程式,寫程式有bug很簡單,除錯出patch沒有什麼大不了。晶片有bug就很大件事,因為要更正問題,就要重新tape-out多一次,去做一個全新的mask。可以想像製造晶片好印黑膠碟,先要整有一張母碟,然後才可以覆印,mask就是silicon的母碟。傳統上測式晶片設件主力用simulation(即dynamic verification),要花很多人力物力寫個testbench出來,然後模疑晶片所有的input同output。這是一個非常嚴格的工序,因為一個bug也不可以走漏。晶片出了街之後,fix一個bug的成本是幾百萬美元。寫testbench同寫普通software沒有太大分別,只不過測試硬件比測試軟件嚴格很多。Formal Verification則是用另一個方法去測試硬件,不用寫code,寫formal specification,再用數學邏輯理論,去證明硬件的設件必定等於那個specification。完全不同的思考方法,完全不同的用途。Formal Verification可以測試出simulation找不出來的bug,始終simulation並不是exhaustive,不過formal有很多限制,設計不能太大不能太深,始終formal proof係一個NP-complete problem。

多年來formal一直只是學術研究,真正的商業應用,大約五六年前才開始。早期的formal tool非常難用,常常被戲說要博士才懂用,很多designer聽見便敬而遠之。直至JasperGold的推出,formal才開始普及化,這些年來JasperGold手執牛耳,一枝獨秀差不多等同於formal的代名詞。早兩年我也嘗試過學formal,不過當年JasperGold的license太貴,我們細公司買不起,只好用了一個很差很難用的IFV,結果學師未成不了了之。去年我公司被一個大公司收購了,economy of scale讓我們有多好多tools用,今個project終於有機會用到JasperGold,同IFV相比簡直是天堂和地獄,「工欲善其善,必先利其器」,其實formal一點也不難,我花了兩星期便滿師,可以學懂簡單的formal specify,去proof我個design不會有dead lock。如果要用simulation作同樣測試,因為太多corner cases,是一件非常痛苦的差事。現在用formal去做,幾行code寫完,是一件很好玩的玩意。

我一直都有follow開formal的paper和tutorial,雖然沒有實戰經驗但formal理論大至明白,用新tool不過是學syntax,很快上手。我公司的formal expert介紹我看這本《Formal Verification》課本,這本書是三位Intel工程師編寫的,由淺入深講解很有系統地如何應用formal verification,真正的hard-core技術含量不多(技術東西可以自已看document),反而更像是過來人分享心得和經驗。這本書九成是老生常談,平時睇tutorial睇paper都學過聽過,不過餘下的一成非常有用,讓我茅塞頓開,很多看已paper不明白人家為什麼一定要這樣做的地方,經他一解釋完全明白,一理通,百理明。這本書可以說是我formal的啟蒙老師,任何一個初學formal者必定要看。市面上formal的textbook一隻手數得完,因為formal是太專門的技術,譎想想學就要交很貴學費請consultant去教,不過我認為這本書比consultant教得更好,因為作者有真正的實戰經歷,不似consultant般大多紙上談兵。

以下是我認為書中有用的formal「心法」:

  1. cover和assert是同一塊鏡子的兩面。同一個property,cover就是not左個property的assert的counter example。assert就係not左個cover既unreachable proof
  2. Formal engine係一個breath-first咁去行所有的state space。assume同assert就係cut細個state space,cut走左illegal state,如果行到去specification果個state,咪就proof度囉。
  3. 一開波不要立即寫full proof,先由cover開始玩。唔用assume,剩係寫你想睇乜output,睇下formal engine可不可以back trace你想要的input,然後再慢慢fine-tune那些assume
  4. 用cover整好晒assume,就可以上去bug hunting,專心搵assert的counter example,最後才整full proof。用之前兩個steps的assume
  5. 唔好load太多code,太多assert同cover,要divide and conquer。有些tricks可以用,如cutpoint,abstraction,free variable等等

動物朋友 Kemono Friends

一套改篇課金遊戲的動畫,還要遊戲因經營不善,早已執笠收檔,製作粗劣的CG畫面,幼齡向的弱智劇情,竟然意外爆紅。從最初數話毫無人氣,到結局篇登上17年冬番Nico的收視寶座,BD銷量超過十二萬片,破了近年動畫的銷量記錄,視為動畫研究的一個奇特現像。我很後知後覺,在網絡讀到排山倒海的評論,嘗試分析這套作品為何咸魚翻生,如何讓業界一地眼鏡碎,有的甚至將《動物朋友》比媲當年《魔法少女小圖》,將它捧上神枱,讓我不得不找來一看。

平心而論,這部作品只套一很四平八穩的治癒系,未至於某些人口中的神作,其特別在於背景設定將末世景觀萌化。在人類消失後的世界,野生動物園中的各種動物,「進化」為可愛的美少女。有一天來了個失憶的人類女孩,在各種動物朋友的幫助下,開始尋找自已是什麼物種之旅。一間只有十個員人的製作公司,在資源緊迫的情況下,觀眾對拍出來的水準也不能苛求。也許是畫面馬虎與說故事認真之間的反差,讓這套動畫在觀眾全無期望下,內裏發現有個工整的解謎故事,才引起作品的話題性,繼而把它炒熱。就好似看上去明明是大便,吃入口竟然味道不錯,人類是好奇心強的動物,有這麼特別的存在,一定要試試。

《動物朋友》頭三四話奇悶無比,不過只要能夠忍耐過去,習慣了動畫的節奏,謎題開始逐漸浮現,為何動物園變得如此荒蕪,人類全部去了那兒,黑暗怪物又從何而來,便有足夠理由吸引觀眾追看下去。每集動物少女們看似白痴低能的嬉笑胡鬧,其實在還原動物本身的特性,廣告前後加插的動物小知識,亦看出製作組的用心和誠意。人類主角包子用人類擅長思考和使用工具的能力,去幫助動物解決生活難題,讓故事益智又富有教育意義。伏線和細節處理恰當,沒有為爆而爆的超展開,主線很平穩地推進,一步步解開包子身世和樂園荒癈之謎。不少伏筆讓觀眾拍案叫絕,如擲紙飛機引開怪物,每集片尾曲後出場追著主角足蹤的浣熊,下期預告的企鵝合唱團等等。

其實觀眾的要求很簡單,有一個精彩的故事,其他方面就算做不好,都勉強可以接受。反而劇本寫不好,空有亮麗的畫面,豪華的聲優陣容,就算騙到觀眾收視不錯,最終必定被觀眾所唾棄。

Stories of Your Life and Others – Ted Chiang

看完電影《Arrival》,被故事的內容深深吸引,找來原著短篇小說《Stories of Your Life》細閱,一開之下加驚為天人,其意念比起電影版的表達更深入,電影版只拍出原著三分之一的精髓。原著收錄在Ted Chiang的短篇小說集內,恕我孤陋寡聞,初次接觸Ted Chaing的大名。此君只兼職寫科幻短篇,產量不多,但慢功出細貨,每篇均是精品。他是星雲獎和雨果獎的常客,一本小說集裏頭十二篇故事,分別有九篇提名六篇奪獎,絕對稱得上當代最有影響力的科幻作家。

Ted Chiang的科幻短篇故事性不強,不像傳統長篇科幻小說般以橋段吸引讀者追看,反而是他的故事內創新的意念,不斷衝擊著讀者的思維和慨有觀念,為讀者帶來知性上的滿足感。他的小說可以粗略分為兩類,第一類是與傳統科幻小說相近,探討未來科技帶來的可能性。他的故事有一個特色,就是主線本身並不是故事的核心,只那科幻題目哲學討論的載體。他是故事更似是一篇哲學論文,只不過以故事形式表達出來。第二類是復古科幻,故事中的世界並不遵從現實世界的物理法則,而是假若古代人對世界的錯誤理解為真,那會如何演化出一套合理的世界觀呢。讀者會讚嘆其世界心思細密的設定,發展出一套自成一角自圓其說的科學觀。在其他奇幻故事(如哈李波特,魔戒,冰與火),世界觀只是說故事的舞台,但他的故事舞台本透才是的主角,故事中的人物角色,只不過是讓舞台不至於太過空洞單調矣爾。

以下是書中我特別喜歡的故事,在此誠意推介給讀者

《Tower of Babylon》是他的成名作,若果地球就如聖經記載一樣是平,若果上帝不干涉人類起巴比倫塔,塔頂接觸天堂的底部。從一個石匠受聘花數月時間爬上通天塔去開鑿天堂之門,看那會是一個個世界

《Understand》是電影《Lucy》的硬科幻完全進化版,能使用腦袋百份百能力的超人,而若果同時有兩個這樣的人,一個外向想把世界改造成完美,一個內向想探求世界萬物的真理,兩雄相遇的結局會如何呢。

《Story of Your Life》相信不用多介紹了,《Arrival》的原著,從時間並非單向的物理悖論開始,一個語言學家從外星人學習外星文字後,從而打開了雙向時間之門,「記得」未來將會發生的事情。

《Hell is the Absence of God》是對聖經約伯記中苦難題的更深入探討,在一個神與天使經常向人顯現並行神蹟的世界,一切發生在人身上的好事和壞事都沒有解釋,那人如何保持對無常的神的信心呢?此故事同時榮獲星雲獎和雨果獎

《Liking What You See: A Documentary》如果有中文譯名,我會把它譯作《你的樣子如何,你的日子也必如何》。外貌歧視算不算歧視?如果未來科技可以改寫人腦神經,讓人只能客觀地分辨外貌,沒有愛美惡醜的主觀感覺,會如何呢?這故事是一套偽記錄片,記錄支持外貌平等的壓力團體,要求立法強制所有人都不辨美醜的一場社會運動。故事從多個不同支持和反對的角度,全面檢視美醜申延出的政治哲學,自由vs平權,社運vs美容業,分辨美醜有用vs沒有用,美醜是客觀vs主觀等等的議題。整本書我最喜觀這個故事,不過作者竟然以故事還未如理想,自動提出放棄星雲獎的提名。

《The Merchant and the Alchemist’s Gate》是另一個同時奪取星雲獎和雨果獎的故事,在中世紀回教文明黃金年代的巴格達,有一道能夠時光倒流二十年的時空門,在歷史不能改變的大前提下,說出一個戲中戲中戲的感人故事。即使歷史不能夠改變,回到過去還是有價值,可以讓看清楚當年錯過了的另一面,從而學懂纖悔,學懂寬恕,學慬放下。

《Exhalation》是我最喜歡的第二類故事,作者用一個以氣壓運作的宇宙,以活塞和槓桿發動的機械宇宙人,來作比喻我們宇宙中熵的消逝。

《The Lifecycle of Software Objects》探討AI的人權和社會關係,教養一個AI好比教養一個孩子,一個橫跨十多年的故事,不過結尾有點不了了之。故事中提出很多有趣的觀點,當我們研發出一個真正懂得學習懂得思考的AI時,將會如故事中一樣,改寫我們的法律和人倫關係。其中一個有趣的提案,雖然AI不是人,沒有人權的保障,但通過成立一個公司,為AI取得法人地位,AI自已當CEO自已當董事,AI可以擁有財產可以簽合約,基本上就擁有與人類等同的社會地位。

我寫這篇書評時,看了紐約客和他的訪問。原來Ted Chiang的正職都是以文字搵食,編寫電腦軟件的使用者手冊。很難想像同一個人,一邊寫味如嚼蠟的使用者手冊,另一邊寫獲獎無數的科幻小說。