看到一半之處,文中提到了Church-Rosser Theorem
Church-Rosser Theorem:
如果一個expression可以用兩種不同的方法去reduce
而且他們都會得出normal forms
那麼這兩個normal forms就會是一樣的。
不過這個版本的Theorem並沒有說一定要reduce出normal form
也有可能並不存在一個normal form
thus, 並不是每個reduction sequence都會得到normal form
所以我們在原本的Theorem上面加上了strong normalisability
Strong Church-Rosser Theorem:
對一個expression
無論我們用什麼順序去reduce
我們都一定可以得出一個唯一的normal form。
而因為reduction在total function中具有Strong Church-Rosser這樣的性質
所以我們可以很自由的任意決定我們reduction sequence.
也因為total fp有這樣的性質
所以total fp也被稱為 Strong fp
相對的, partial fp就叫做 Weak fp
