# beta reduction: order of substitution

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?

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