應用到 lambda calculus

編碼的方式是找一個只有兩個物件 $1, T$ 的 category $M$ ，讓 lambda calculus 的 terms 是 $M$ -morphisms，這些技巧在 Categorical semantic 領域內相當常見。

到這裡必須檢查 lambda calculus 確實存在 point-surjective，歡迎自行嘗試。

按此編碼後可以得到 $ev \circ \phi\circ \langle p, p\rangle \xrightarrow{encode} \phi(p)(p)$ 。套到等式上

f \circ ev \circ \phi\circ \langle p, p\rangle = ev \circ \phi\circ \langle p, p\rangle

可以得到以下編碼

f(\phi(p)(p)) = \phi(p)(p)

把 $\phi(p)$ 改寫成 $q$ ，於是等式可以寫成 $q(p) = f(\phi(p)(p))$ ，而函數套用語法可以用 $\lambda$ 退化，於是得到

q = \lambda x. f(\phi(x)(x))

注意到 $q$ 的定義是非遞迴的，因此一定是可定義的。

計算即可發現確實 $q(p) = \phi(p)(p) = f(\phi(p)(p))$ 。因為所有的 $\lambda$ -term 都屬於 $T$ ，所以現在我們知道任何 lambda calculus 的函數都有不動點。