Lambda Expression simplification

Question

Is \xy.xy the same as \x.x?

I have to simplify an expression as much as possible and I don’t understand if these are equivalent

Answer 1

This question makes more sense when you think more generally about what you're doing by adding the parameter y and immediately applying it.

An equivalent question: given the function Eta = λf . λy . f y, is it true for all f that Eta f == f?

The answer depends ultimately on your definition of equality. If your definition of two functions f, g being "equal" is that, for all input expressions x, f x == g x, of course Eta f == f! The only operation to be done with a function is to apply it, so in a model of equality that only considers fully-applied values, a function that simply plumbs an argument along to its input is equal to the identity. The property that Eta f == f in some system is aptly named 'eta-equivalence', and some systems choose not to include it (notably, those that allow for syntactic manipulations).

Assuming eta-equivalence, yes, that is a legal simplification.