如何在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) 

由最后一个规则（收缩）。