相關：
第一數學歸納法 vs 第二數學歸納法 vs 良序定理
第二數學歸納法：硬币問題和堆垛遊戲
第一數學歸納法：施塔特中心的地闆磚
良序原理：算術基本定理的證明
在這篇博文中我會依次複習一下狀态機的定義、不變性原理、部分正确性和可終結性這四個和狀态機相關的知識，并舉出一些有意思的例子輔以說明，最後解決一個關于穩定婚姻的有趣問題。
0. 什麼是狀态機
狀态機是對“step-by-step“過程的一種抽象模型。
由于計算機程式本身就是一種确定的”step-by-step“過程，是以狀态機在計算機科學領域用的很普遍。其中最重要的一個用途就是證明在程式運作的過程中某一些屬性能夠确定被保持，這些屬性也被稱為”不變量“。在實際生活中有很多”不變量“，例如飛機自動飛行的過程中要保證高度值不能低于1KM，或者核電站在運作的過程中内芯溫度不能高于1K攝氏度等等。
1. 狀态機的狀态與轉換
從集合論的角度來看，狀态機就是将一個二維關系映射到一個集合上——這個集合的元素叫做”狀态“，他們之間的關系稱為”轉換“，p轉換為q寫為p -> q。一個狀态機的所有可能轉換被稱為轉換圖，每一個狀态機都有一個設計的”起始狀态“。
下面舉一個簡單的例子，有一個從0到99的累加器，當累加器的狀态達到99後再進行累加就會發生溢出：
将這個累加器用公式表示就是：
如果一個狀态機的狀态是有限的，我們就稱其為有限狀态機，例如上面這個例子。相反，如果狀态有無窮多個，我們就稱其為無限狀态機，如果上面這個累加器不設定溢出的話就會變成一個無線狀态機。在實際使用時，轉太極的狀态轉換可能會有一些輸入輸出，轉換時對不同的狀态也會有不同的花費或者幾率，這篇博文中不考慮這些因素。
2. 不變性原理
如果一個狀态能夠在狀态機的某次執行中出現，我們就稱之為”可到達的“。如果P是一個狀态機的不變量，那麼無論何時P(n)成立，當狀态n -> r後，P(r)也成立。特别地，如果對于一個狀态機的起始狀态P(n)成立，那麼對于任何可到達的狀态r，P(r)都成立。
可以看出，不變性原理就是适用于狀态機的歸納法 ——如果某個謂語在一開始成立，那麼就推出在接下來的所有步驟中它均成立。
下面舉一個例子，在《虎膽龍威3》這部電影中，恐怖分子在一個噴泉旁放置了炸彈，并提供了一個5加侖的桶和一個3加侖的桶，如果拆彈人員能夠利用這兩個桶準确的得到4加侖的水并放在一旁的秤上，炸彈就不會爆炸。
這個問題看起來也不難，一個國小生也能馬上想出來，例如這樣一個解法：将3加侖桶裝滿，全部倒入5加侖桶中，然後再将3加侖裝滿，倒入5加侖桶中直到5加侖桶滿，然後倒掉5加侖桶裡的水。這時3加侖桶裡有1加侖水，将這1加侖的水倒入剛剛清空的5加侖桶中，然後裝滿3加侖桶并全部倒入5加侖桶中，這時5加侖桶中的水就是4加侖了。
那麼，對于任何兩個容積的水桶這個問題都是有解的嗎？如果我們将5加侖的水桶換成9加侖的水桶，還能拆除炸彈嗎？顯然是不行的，因為我們每次的操作都隻能是3的整數倍，是以結果也一定是3的整數倍，也就不可能得到4這個結果了。下面我們利用不變性原理來證明這一點：
首先我們建立一個狀态機，它的狀态表示為(b, l)，其中b代表big jug，l代表little jug，是以0 <= b <= 9, 0 <= l <= 3且b、l均為整數。該狀态機的起始狀态為(0, 0)，對于關系的轉換，有以下6種可能：
- 裝滿小水桶：(b, l) -> (b, 3)
- 裝滿大水桶：(b, l) -> (9, l)
- 清空小水桶：(b, l) -> (b, 0)
- 清空大水桶：(b, l) -> (0, l)
- 将小水桶裡的水倒入大水桶中。(1) 如果b + l <= 9，(b, l) -> (b+l, 0). (2)否則，(b, l) -> (9, l - (9-b))
- 将大水桶裡的水倒入小水桶中。(1) 如果b + l <= 3, (b, l) -> (0, b+l). (2)否則，(b, l) -> (b - (3-l), 3)
注意到這個狀态機和我們之前那個計數器狀态機不同，它每一次的狀态轉換的選擇不止一個，像這樣的狀态機就稱為”非确定性的“（nondeterministic），計數器狀态機則稱為”确定性的“（deterministic）。
設P((b, l))為“b，l均為3的整數倍”，下面我們證明它是對狀态機所有狀态都成立的不變量：
首先證明如果P(q)成立，q -> r，那麼P(r)也成立：
- “裝滿操作”，得到(9, l)或者(b, 3)，由于9, 3, l, b都是3的整數倍，命題成立
- “清空操作”，得到(0, l)或者(b, 0)，由于0, l, b都是3的整數倍，命題成立
- 将小水桶裡的水倒入大水桶中。(1) 如果b + l <= 9，(b, l) -> (b+l, 0) 由于b+l, 0都是3的整數倍，命題成立 (2)否則，(b, l) -> (9, l - (9-b)) 由于9, l - (9-b)都是3的整數倍，命題成立。
- 将大水桶裡的水倒入小水桶中。(1) 如果b + l <= 3, (b, l) -> (0, b+l) 由于0, b+l都是3的整數倍，命題成立 (2)否則，(b, l) -> (b - (3-l), 3) 由于b - (3-l), 3都是3的整數倍，命題成立。
綜上，P是該狀态機的一個不變量。又因P(0, 0)也成立，而(0, 0)是該狀态機的起始狀态，由不變性原理，P對于該狀态機所有可到達的狀态都成立。因為4不是3的整數，是以我們不可能得到一個裝有4加侖水的桶。證畢。
3. 狀态機的部分正确性和可終結性
我們可以從兩個方面判定程式（狀态機）是否可用：部分正确性（partial correctness）和可終結性（termination）。部分正确性并不是指程式結果是部分正确的，而是因為程式在計算“部分關系”（partial relation）的時候可能不會終止，是以這個正确性是“部分的”，或者這麼說，如果程式最終停止，得出的結論一定是正确的。可終結性則是指程式理論上是會最終停止的。
通常情況下，部分正确性可以用不變性原理證明，而可終結性可以用良序原理證明。下面我們用一個常見的快速求幂算法來解釋這兩個性質，對于求a^b的值，算法如下：
首先建立起這個狀态機：其的狀态為(x, y, z)，是以其起始狀态為(a, 1, b)，狀态轉換為：(1) 如果z != 0 && z為偶數，(x, y, z) -> (x^2, y, z/2) (2) 如果z != 0 && z為奇數，(x, y, z) -> (x^2, xy, z/2)。
接着證明該狀态機的不變量P((x, y, z))：z為自然數且y*(x^z) = a^b。設P((x, y, z))成立；則在第一種轉換下，z為自然數，y*((x2)(z/2)) = ab。在第二種轉換下，z為自然數，y*x*((x2)^(z/2))（z除2後舍去了餘數1）= a^b。得證，又因為起始狀态P((a, 1, b))依然成立，由不變性原理我們便證明了該程式/狀态機的部分正确性。
在證明該程式的可終結性之前，先介紹一下“派生變量”（Derived Variables）這個概念：
我們在證明程式是可終止的時候通常會使用程式中的一個非負數值，如果它在程式每一步的運作中都是嚴格遞減的，由良序原理，它不可能無限遞減，最終會達到那個最小值，也就是程式終止。如果更普遍的了解，我們将一套設計好的操作f作用于狀态p，稱之為f(p)，如果f(p)是嚴格遞減的，即(p -> q) implies f(q) < f(p)，且對于所有可到達狀态，f(p)構成一個良序集合，那麼就可以得到該程式/狀态機是可終止的（f類似于實體學裡面的勢能函數）。
另外，這種方法也常常用于算法的分析，即對于一個算法生成一個派生變量，在算法運作的過程中觀察這個變量的變化。
對于上面例子中的算法，我們可以令派生變量f((x, y, z)) = z，我們已經證明了z是自然數（即良序集合），且當z不為0時z/2 < z即f((x, y, z)) > f((x', y', z'))，是以可以得出該程式是可終止的。
綜上，我們證明了該算法具有可終止性和部分正确性。
4. 穩定婚姻問題
假設你是一位媒人，現在男人和女人的數量一樣，每一個男人按照他的标準在心中給所有的女人排一個名單次序，女人也一樣，這個配偶名單不一定是對稱的，也就是說，如果小明最希望小紅稱為他的妻子，小紅可能最希望小剛成為她的丈夫。這裡不考慮同志的問題，你的任務就是找到一種比對的方法，讓每個人都找到自己的配偶，并且所有的婚姻都是穩定的 ，即不存在兩個不是配偶的人互相喜歡勝過各自的配偶。舉一個不穩定婚姻的例子：
如果我們将Brad和Jennifer配對，Billy Bob和Angelina配對，那麼Brad喜歡Angelina勝過自己的配偶Jennifer(1 < 2)，而Angelina也喜歡Brad勝過自己的配偶Billy Bob，這就形成了一個不穩定的婚姻：Brad和Angelina可能會在晚上一起悄悄的做數學作業！與此相反，如果我們将如果我們将Brad和Angelina配對，Billy Bob和Jennifer配對，雖然Billy Bob和Jennifer可能會有些不高興，但是婚姻将會是穩定的——即使Jennifer去勾引Brad，Brad還是會深愛着Angelina的；）Billy Bob也無法讓Angelina對自己感興趣。
上面是一個4個人的例子，如果給你2n個人和他們的理想配偶名單（對所有異性的好感度），你還能設計出一個配對方法嗎？
事實上，無論是對少個人，隻要不存在同性婚姻，都會有一種穩定婚姻的配對方法——而且這種方法非常簡單和易懂：
- 首先每一個男人去向他名單上最靠前的女士示愛，示愛後他即成為該名女士的候選者。
- 随後每一個女人從她所有的候選者裡選出她最喜歡的男士對他說“我們可能結婚，請不要将我從你的名單劃掉”，并對其他的男人說“我對你不感興趣，回家做數學作業去吧！”。
- 示愛被拒絕的男人他的名單中将拒絕她的女士劃掉。
- 當每一個女人都有且僅有一個候選人時，配對完成。否則跳轉到第一步。
我們需要證明這個算法具有以下性質：
- 該算法最終會結束。（可終結性）
- 結束時每一個人都會結婚。
- 結婚後婚姻是穩定的。（這兩條是部分正确性）
為了便于分析，我們将這個過程建立為一個狀态機——每次的狀态為每個男人和該輪次他會去示愛的女士，即他名單的首位女士。
1.該算法最終會結束：
設派生變量f(x) = 每個男人名單上留下的女士數量之和，一開始f(x) = n^2。每次循環時f(x)都會減少——因為這意味着至少有一名女士被兩個男士示愛了，是以循環才不會終止，被拒絕的男士也會将她從名單上劃去。又因為不會有女士新增到男士的名單上，是以f(x)在該狀态機轉換過程中是單調遞減的。又因為f(x) >= n（終止時情況），是以f(x)的取值在一個良序集合中，得到該狀态機是可終止的。
2.1結束時每一個人都會結婚：
可以觀察到，對于一名女士而言，如果她這一輪次将Frank留了下來，Frank就不會将她從他的名單上劃去，第二天Frank依然會來找她示愛。如果第二天該名女士遇到了她更喜歡的男人，她才會趕走Frank，是以說，女士的候選者隻會“越來越好”。這好像是一個不變量：設P(w, m)為男士w将m從他的名單中劃去，那麼m一定有了更好的候選人。由于P(w, m)對于一開始也成立，由不變性原理P對所有的狀态都成立。
反證法，如果結束的時候有一個男士Bob沒法結婚，即他的名單上所有的女性都拒絕了他（他的名單為空了），那麼由于P對所有狀态成立，所有的女性都有一個比Bob更好的候選人，由于男人和女人的數量是一樣的，是以這是不成立的，是以結束時每一個人都會結婚。
2.2結婚後婚姻是穩定的：
我們可以證明比對完成後不存在可能有暧昧關系的兩個人。假設比對完成後Jen和Brad兩個人不是配偶，那麼根據Brad的名單會有以下兩種情況：
Case 1: Brad名單上已經沒有Jen了，即他向Jen示愛過并被拒絕了。由上面的不變量P，Jen一定有一個比Brad更加喜歡候選人并和他結了婚，是以Jen不會被Brad吸引，即他們不會有暧昧關系。
Case 2: Jen還在Brad的名單上，由于Brad是按照好感順序去示愛的，如果最後Jen還在他的名單上，Jen又沒有和他結婚，那麼Brad一定和一個他更有好感的女人結了婚，是以Brad不會在意Jen的“勾引”，也就不會和她有暧昧關系。
由于Brad和Jen的選擇是随機的，是以比對後任何人之間不會産生暧昧關系，即婚姻一定是穩定的。
這個方法對男人有利還是女人有利？
你可能覺得女人具有選擇權——她們每天都能選擇一個更好的配偶，男人隻能被拒絕——隻能選擇越來越差的配偶，但實際上在該算法中女人是很弱勢的一方！我們前面隻證明了婚姻比對方法得出來的比對的正确性，事實上，穩定的比對方法可能不止一種，例如，如果我們還是利用婚姻比對算法，将比對時的男女屬性換一下就可能得到不同的結果（還是穩定的）。
稱一個人對于另一個人是“可行配偶”如果在某一個的穩定比對中他們可以成為夫妻。下面證明上面算法的狀态機具有一個不變量Q：對于女人w和男人m，如果w被m從名單中劃掉了，那麼w對于m不可能是“可行配偶”。
反證法，假設某個時候Alice要被Bob從名單中劃去因為Alice選擇了另一位叫Frank的男性，如果Alice和Bob成為了配偶，那麼Frank也就隻能劃掉Alice選擇更“差”的一位女性，而Alice也就隻能跟着不那麼喜歡的Bob，是以Frank和Alice之間就可能發生暧昧關系，是以Alice和Bob不可能是可行配偶。
稱在一個人所有的”可行配偶“中Ta最喜歡的那一個為”最理想配偶“，最不理想的那一個為”最不理想配偶“。下面證明如果使用上面的婚姻比對算法，男人們總會娶到”最理想老婆“，而女人們總會娶到”最不理想老公“。
證明：如果Bob利用上面的算法和Alice結了婚，那麼之前在名單中Alice之上的女性都被Bob劃掉了，由不變性Q，被劃掉的女性都不是”可行配偶“，而Alice又是劃掉操作後最排行最高的女性，是以Alice是Bob的”最理想配偶“。另一方面，如果Alice對她的丈夫好感度低于對Bob的，那麼Bob一定取了一位不是”最理想配偶“的人，這樣Alice和Bob就可能發展暧昧關系，是以Bob一定是Alice的”最不理想配偶，證畢。
婚姻比對算法的實際應用：
- 在50年代的時候，美國啟動了一項名為國家公民比對（National Resident Matching Program，NRMP）的計劃，該計劃主要是為了解決從學校畢業的學醫學生和醫院之間的比對關系——盡量使學生和醫院都滿意，在該計劃中就大量使用到了婚姻比對算法，即醫院和學生分别充當男人和女人。其發明人Shapley獲得了2012年的諾貝爾經濟學獎。
- 大量的交友網站使用到了該算法（當然男人不會向女人去示愛，都是計算機完成的）。
- 《Mathematics for Computer Science 》的作者之一Tom Leighton創立了網際網路接口公司Akamai, 他們将婚姻比對算法用到了伺服器和使用者的資源調配之中（CDN）。其中網絡請求（客戶）作為女人，網站伺服器作為男人；網絡請求對伺服器的“好感度”取決于延遲和丢包率，網站伺服器對于網絡請求的“好感度” 取決于連接配接帶寬和主機代管商的成本。
參考：
- Mathematics for Computer Science