[PRL] polyadic, unordered binders

[Dave Herman]

Imagine a language with a polyadic binding construct where you could 
permute the bindings without changing its meaning. Say, a parallel-let form:

     (let/par ((x1 e1) ... (xn en)) e)

Then it seems the alpha-equivalence relation would hold up to permuting 
bindings:

     pi * (x_i ...) = (x_j ...)                   (z_j ...) fresh
                        forall j . e_j == e'_j
                e[z_j/x_j, ...] == e'[z_j/y_j, ...]
     ------------------------------------------------------------
     (let/par ((x_i e_i) ...) e) == (let/par ((y_j e'_j) ...) e')

This should be read as existentially positing a permutation `pi' of the 
bindings on the left-hand side to unify with the bindings of the 
right-hand side. It's simple enough to specify, although it's a royal 
pain to implement efficiently, i.e. to avoid comparing n! permutations 
of bindings.

This seems natural but I've never seen it before, since polyadic binders 
are usually order-sensitive. Does anyone know of a precedent for this 
kind of thing?

Thanks,
Dave