beta reduction: order of substitution

67 Views Asked by At

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?