# Lambda calculus with unordered application

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?

• Have you looked at Explicit subsitutions? Feb 23 at 16:40
• Generally, explicit substitutions have rules for moving one substitution past another (though it is non-trivial), is that what you have in mind? Of course, you can't get away from having lambda, only substitutions isn't enough.
– cody
Feb 25 at 4:33
• @cody Why aren't substitutions enough? (Genuine question.)
– SEC
Feb 25 at 13:51
• Well, for instance, how would you translate $(\lambda x.x\ x)(\lambda x.x\ x)$, and have it reduce infinitely?
– cody
Feb 25 at 21:07
• Sounds like named parameters. Several languages have those. Mar 5 at 1:31