状态机：如何构建稳定的婚姻( 三 ) _状态

< z即f((x, y, z)) > f((x', y', z'))，所以可以得出该程序是可终止的。
综上，我们证明了该算法具有可终止性和部分正确性。
4. 稳定婚姻问题
假设你是一位媒人，现在男人和女人的数量一样，每一个男人按照他的标准在心中给所有的女人排一个名单次序，女人也一样，这个配偶名单不一定是对称的，也就是说，如果小明最希望小红称为他的妻子，小红可能最希望小刚成为她的丈夫。这里不考虑同性恋的问题，你的任务就是找到一种匹配的方法，让每个人都找到自己的配偶，并且所有的婚姻都是稳定的，即不存在两个不是配偶的人互相喜欢胜过各自的配偶。举一个不稳定婚姻的例子：

文章插图
如果我们将Brad和配对，Billy Bob和配对，那么Brad喜欢胜过自己的配偶(1 < 2)，而也喜欢Brad胜过自己的配偶Billy Bob，这就形成了一个不稳定的婚姻：Brad和可能会在晚上一起悄悄的做数学作业！与此相反，如果我们将如果我们将Brad和配对，Billy Bob和配对，虽然Billy Bob和可能会有些不高兴，但是婚姻将会是稳定的——即使去勾引Brad，Brad还是会深爱着的；）Billy Bob也无法让对自己感兴趣。
上面是一个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更好的候选人，由于男人和女人的数量是一样的，所以这是不成立的，因此结束时每一个人都会结婚。