In lambda calculus, $\lambda xy.\phi$ isn't in general equivalent to $\lambda yx.\phi$. However, it seems possible to imagine a calculus which replaces application with something like specification, where order of specification is unimportant (at least when the substitutions target different variables):
$$\mathit{Term} ::= \mathit{Var} \mid [\mathit{Var} := \mathit{Term}] \mid \mathit{Term}\, \mathit{Term}$$
In this kind of calculus, we could represent $((\lambda fx.f(f x))g)y \equiv g(g y)$ as $(f(fx))[f := g][x := y]$, or equivalently as $(f(fx))[x := y][f := g]$ (with opposite orders of "applications").
The basic idea, I guess, is to make substitutions first-class in a way they aren't in typical definitions of lambda calculus. In a way it is reminiscent of unificaition. Perhaps a fully general specification would augment standard lambda calculus with substitutions, rather than attempting to replace abstractions wholesale? And perhaps we would want to add some syntactic devices for marking the scope of a substitution.
But in general, the idea or hope is to have a calculus in which order of application is less rigid than typical in standard lambda calculus. Are there such systems? And what would be a natural way to implement something like this in, say, a functional language like Haskell?
