Do we always apply our input to the left most term in a lamda expression?

For instance, take the expressions:

$λP λQ. ∀x P(x)→Q(x)$ which we can rewrite as $[λP λQ[ ∀x P(x)→Q(x)]]$

$λP. λQ. ∀x P(x)→Q(x)$ which we can rewrite as $[λP [λQ[ ∀x P(x)→Q(x)]]]$

If we apply an input to each expression, would the input in both expressions replace P? But if that's the case, wouldn't that make the two expressions equivalent?

  • $\begingroup$ I don't see a difference between the two terms besides the dot, which has no meaning. $\endgroup$ – Couchy311 Nov 21 '18 at 7:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.