Comment soustraire TRUE et TRUE dans lambda calcul correctement?

Question

J'essaie de comprendre le calcul lambda. Cependant, je suis un peu coincé sur cette expression: VRAI et VRAI. Je ne peux pas comprendre comment vous pouvez obtenir de

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

à

(\F T F -> T) 

, non

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

\ lambda est la signature

Answer 1

(\F T F -> T) 

et

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

sont la même chose.

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

• entre parenthèses Ultrapériphériques sont abandonnées: M N au lieu de (M N)
• [...]
• Le corps d'une abstraction s'étend jusqu'à droite possible: λx. M N signifie λx. (M N) et (λx. M) N
• Une séquence d'abstractions est contractée: λx. λy. λz. N est abb reviated comme λxyz. N

En particulier,

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

peut être écrit

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

parce que nous pouvons laisser tomber entre parenthèses redondantes et le corps du lambda externe se prolonge jusqu'à droite possible , qui peut ensuite être écrit

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

ou

(\F T F -> T) 

par la dernière règle (contraction).