如何在lambda微積分中正確減去TRUE和TRUE？

Question

我想了解lambda微積分。但是，我有點卡住這個表達式：TRUE和TRUE。我無法弄清楚如何才能得到

((\T F -> T) (\T F -> T)) 

到

(\F T F -> T) 

，不

(\F -> (\T F -> T)) 

\是λ-簽名

Answer 1

(\F T F -> T) 

和

(\F -> (\T F -> T)) 

是一樣的。

https://en.wikipedia.org/wiki/Lambda_calculus_definition#Notation：

• 最外括號被丟棄：的M N代替(M N)
• [...]
• 一個抽象的主體延伸直到右儘可能：λx. M N裝置λx. (M N)和不是(λx. M) N
• 一系列的抽象是合同的：λx. λy. λz. N是abb reviated如λxyz. N

特別地，

(\F -> (\T F -> T)) 

可以寫成

(\F -> \T F -> T) 

，因爲我們可以刪除多餘的括號和外拉姆達的主體最右延伸儘可能，然後可以寫入

(\F -> \T -> \F -> T) 

或

(\F T F -> T) 

由最後一個規則（收縮）。